Data Constructors in Higher Order Positions

[nikivazou]

Writing (see full example in https://liquidhaskell.goto.ucsd.edu/index.html#?demo=permalink%2F1758872050_934.hs)

{-@ foldCons :: xs:List a -> { foldr Cons Nil xs = xs } @-}

Crashes with

  crash: SMTLIB2 respSat = Error "line 3 column 27651: unknown constant MapFusion.ConsInt declared: (declare-fun MapFusion.Cons (Int (MapFusion.List Int)) (MapFusion.List Int)) "

The reason is that at SMT level (after defunctionalization) foldr expects an "integer" argument and is given the higher order Cons that is not defunctionalized.

Possible solutions:

1. Enable the {-@ LIQUID "--no-adt" @-} flag that treats data constructors simply as functions (and Cons will get defunctionalized).
2. Replace Cons in the spec with a function cons that is defined to be equal to Cons.
3. At serialization replace Cons with a defunctionalized equivalent (I believe such exist already?).
4. At serialization eta expand?

From the above 1. and 2. just work, while 3 and 4 would require edits in LH.

@AlecsFerra @clayrat @pacastega

[nikivazou]

Even if we make no edits, we should create a better error message!

[AlecsFerra]

Are there any drawbacks to having 1 enabled by default? Does Z3 have any special handling of datatypes? If so, I think 1 is not a good solution, otherwise we just enable the flag by default.

Otherwise, I think 3 is the best choice, if I understood it correctly since it’s 2 but done automatically.

[nikivazou]

Yes, there are drawbacks on 1. If you encode data constructors just as functions, you loose injectivity (D x = D y => x = y). In the original test you do not seem to need injectivity...

BTW, there might be a 5th option, where we can coerce Cons as integer in the SMT encoding...