Type mismatch in smt2

Question

The below smt2 code gives an error related to type.

( declare-datatypes ( ( List 1 ) )
  ( ( par ( T ) ( ( cons ( hd T ) ( tl ( List T ) ) )
 ( nil )
 ) )
 ) )

 (declare-sort Ty 0) 
(define-fun-rec func ((x (List Ty) ) (y (List Ty)))     (List Ty)
        (match  x   ( ((cons xt xts) ( cons xt (func xts y)) )
                      ( nil nil )
                    )
        )
)

ERROR:

(error "Both branches of the ITE must be a subtype of a common type.
then branch: ((lambda ((xt Ty) (xts (List Ty))) (cons xt (func xts y))) (hd x) (tl x))
its type   : (List Ty)
else branch: nil
its type   : (List T)
")

Why doesn't it figure out using the return type and is there any way to do that ?

One way is to have manually put it as (nil (as nil (List Ty)) ) which solves the error But I don't want to specify the return types at every nil in the program. Is there any other way ? or any option that I need to mention enable ?

Answer 1

This is by design. SMTLib's type system isn't designed to do any sort of inference, to make it easy for solvers to unambiguously load specifications. See section 3.6 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf which discusses well-sortedness requirements. So CVC4 rightfully rejects your program.

But you are correct that this is rather annoying in practice. The typical solution is to simply define the required constant at the type you are interested in once and for all:

(define-fun nilTy () (List Ty) (as nil (List Ty)))

Since all programs can only refer to a finite number of sorts, this is always possible. (And in practice, there's rarely ever more than a few different sorts lying around like this anyhow; so it isn't a big burden. This is sometimes referred to as "monomorphisation.")

Once you make the above definition, then you simply use it instead of nil in the appropriate context:

(define-fun-rec func ((x (List Ty) ) (y (List Ty)))     (List Ty)
        (match  x   ( ((cons xt xts) ( cons xt (func xts y)) )
                      ( nil nilTy)
                    )
        )
)

You'll find that CVC4 will have no trouble accepting this since it now exactly knows which sort nilTy should be used at.

Remember that SMTLib is generally not meant to be hand-written, but rather machine-generated. So the clunkiness of the above usually doesn't apply as frontend tools can implement much fancier type systems and spit out the required SMTLib under the hood. Hope that helps!