Turning --totality and --counter-examples on throws "cannot satisfy" for partial function

[mrkgnao]

From the Liquid Haskell tutorial:

{-@ type True  = {v:Bool | v    } @-}
{-@ type False = {v:Bool | not v} @-}

{-@ ex0 :: False @-}
ex0 = False

{-@ ex1 :: Bool -> True @-}
ex1 :: Bool -> Bool
ex1 True = True

Running liquid -- --short-names --totality --counter-examples on this gives a "cannot satisfy" error. The error does not occur without the --counter-examples flag (I get UNSAFE, as expected).

A verbose error log can be found here.

[ranjitjhala]

Thanks for posting this!

@mrkgnao Are you using the LH develop from github?

On the plus side, with that version, I can't get the given failure.

On the minus side, I don't get the counterexample either.

@gridaphobe, do you know what may be going on?

On Sat, Jun 10, 2017 at 1:49 AM, Soham Chowdhury notifications@github.com wrote:

From the Liquid Haskell tutorial:

{-@ type True = {v:Bool | v } @-} {-@ type False = {v:Bool | not v} @-}

{-@ ex0 :: False @-} ex0 = False {-@ ex1 :: Bool -> True @-} ex1 :: Bool -> Bool ex1 True = True

Running liquid -- --short-names --totality --counter-examples on this gives a "cannot satisfy" error. The error does not occur without the --counter-examples flag (I get UNSAFE, as expected).

A verbose error log can be found here http://lpaste.net/7305633963408621568.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1043, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOCIZdvni8FC04YTUmkNMaVnr2DmPks5sCliYgaJpZM4N2Diu .

[gridaphobe]

Haven't had a chance to look into it yet, but my first guess would be that we can't produce a model because the failed subtyping query will be one of these

Addr# <: {v:Addr# | FALSE}

things, and we don't know how to synthesize an Addr#.

It probably wouldn't be too hard to add some special logic to handle the totality errors, the Addr# is the error string, so the only interesting thing is what might be in the context.

But at the very least, we need to provide a better error message :(

[nikivazou]

@gridaphobe I think I broke counter examples generation when porting to GHC-8. Did you look at it?

[mrkgnao]

@ranjitjhala yes, I cloned LH from master on this repo.

On Mon, Jun 12, 2017, 00:08 Niki Vazou notifications@github.com wrote:

@gridaphobe https://github.com/gridaphobe I think I broke counter examples generation when porting to GHC-8. Did you look at it?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1043#issuecomment-307648089, or mute the thread https://github.com/notifications/unsubscribe-auth/ANhd7pyhDtK72N9W9Ij5VomAkxAmclxqks5sDDQzgaJpZM4N2Diu .

[ranjitjhala]

Thanks! As it happens master is somewhat older, try develop (but yes looks like the recent move to GHC 8 has perhaps broken the counterexamples?)

On Sun, Jun 11, 2017 at 1:36 PM, Soham Chowdhury notifications@github.com wrote:

@ranjitjhala yes, I cloned LH from master on this repo.

On Mon, Jun 12, 2017, 00:08 Niki Vazou notifications@github.com wrote:

@gridaphobe https://github.com/gridaphobe I think I broke counter examples generation when porting to GHC-8. Did you look at it?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/ 1043#issuecomment-307648089, or mute the thread https://github.com/notifications/unsubscribe-auth/ ANhd7pyhDtK72N9W9Ij5VomAkxAmclxqks5sDDQzgaJpZM4N2Diu .

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1043#issuecomment-307655080, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOBZ7zLoze5SOV28T16jpQ1C4ARlhks5sDE-3gaJpZM4N2Diu .

[gridaphobe]

@gridaphobe I think I broke counter examples generation when porting to GHC-8. Did you look at it?

Ah, no, that's probably the issue then.