crash SMTLIB2 on ADTs using dollar sign

[mystaroll]

Not sure how important is this to you, however, this:

proof1 ::  Proof
proof1 = Just 1 === (Just $ 1)
        ***QED

and this:

{-@ reflect foo @-}
{-@ foo :: Maybe {v:Int | v == 2 }  @-}
foo :: Maybe Int
foo = Just $ 1+1

Crash with crash: SMTLIB2 respSat = Error "line 381 column 11158: Wrong number of arguments (0) passed to function (declare-fun GHC.Maybe.Just (Int) (GHC.Maybe.Maybe Int))" Whereas, this goes well:

proof2 ::  Proof
proof2 = ((==) True False) === ((==) True $ False)
        ***QED

Currently, I avoid the $ on ADTs (even though formally proving existing code requires slightly extra manual work)

[nikivazou]

Does the crash go away if you redefine and reflect the $ or is it already reflected?

[ranjitjhala]

@nikivazou I think the trouble is that because Just is reflected in the SMT logic as a data constructor, it must always appear "fully saturated" i.e. with all arguments supplied, but the term Just $ 1 is creating some refinement term where Just is not fully saturated, which Z3 does not like.

The proper fix would be to

1. Have decent support for lambdas and
2. Saturate the terms e.g. convert plain Just to (\x -> Just x)

but I think thats highly non-trivial.

Somewhat related -- we should look into SMTLIB's native support for lambda-terms; I believe CVC has good support for them, maybe Z3 too?

[mystaroll]

Redefining $ doesn't solve the issue. I noticed that in some cases the issue doesn't happen, so I investigated a little bit more and this seems to reproduce it (demo not working | working):

{-@ LIQUID "--reflection"    @-}

{-@ reflect foo @-}
{-@ foo :: Maybe {v:Int | v == 2 }  @-}
foo :: Maybe Int
foo = Just $ (1+1)

{-@ reflect bar @-}
bar :: a -> Maybe Int
bar _ = Just (1+1)

Namely:

1. Without --reflection it works.
2. With --reflection but without the function bar it works.
3. With --reflection, bar needs to have at least 1 parameter to make it crash.

[facundominguez]

With the latest LH I get this error

<no location info>: error:
    Uh oh.
    Test.hs:6:13 Cannot lift Haskell function `foo` to logic
                 Cannot transform lambda abstraction to Logic:  \ (ds_d21p :: GHC.Types.Int) -> GHC.Maybe.Just ds_d21p

which is more informative than the one reported.

I would expect that LH can transform Just $ (1+1) into Just (1+1) before reflecting.