search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.19k stars 137 forks source link

Add proper support for NewTypes / "Crash SMTLIB2: Sorts are incompatible" #1490

Closed googleson78 closed 4 years ago

googleson78 commented 5 years ago

I managed to get a relatively small repro example for something that seems to be related to #1467. My liquid is from 406dd8bc198fad9a2ff87025689b6035e60fd9be.

Notably if I remove the B newtype and use Bool directly in A it works fine!

Here's the example:

module A where

import Foreign.Storable (Storable, poke, pokeByteOff)

data A = A B

newtype B = B Bool

instance Storable A where
  poke ptr (A (B b)) = do
    (\hsc_ptr -> pokeByteOff hsc_ptr 16) ptr b
tauren :: /tmp/liquid » cat A.hs                                                                                                                                                                                                                                            
module A where

import Foreign.Storable (Storable, poke, pokeByteOff)

data A = A B

newtype B = B Bool

instance Storable A where
  poke ptr (A (B b)) = do
    (\hsc_ptr -> pokeByteOff hsc_ptr 16) ptr b
tauren :: /tmp/liquid » liquid A.hs
LiquidHaskell Version 0.8.6.0, Git revision 406dd8bc198fad9a2ff87025689b6035e60fd9be [develop@406dd8bc198fad9a2ff87025689b6035e60fd9be (Fri May 10 09:09:19 2019 -0700)]
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: A.hs

**** [Checking: A.hs] **********************************************************

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

Working  83% [=======================================================..........]

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 382 column 1196: Sorts Bool and Int are incompatible"
googleson78 commented 5 years ago

Update:

Removing the data A and leaving only the newtype B also reproduces it! Replacing Bool with Int makes it work fine.

tauren :: ~/liquid-repro » cat B.hs
module B where

import Foreign.Storable (Storable, poke, pokeByteOff)

newtype B = B Bool

instance Storable B where
  poke ptr (B b) = pokeByteOff ptr 16 b

tauren :: ~/liquid-repro » liquid B.hs
LiquidHaskell Version 0.8.6.0, Git revision 406dd8bc198fad9a2ff87025689b6035e60fd9be [develop@406dd8bc198fad9a2ff87025689b6035e60fd9be (Fri May 10 09:09:19 2019 -0700)]
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: B.hs

**** [Checking: B.hs] **********************************************************

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

Working  75% [=================================================................]

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 353 column 1773: Sorts Bool and Int are incompatible"
ranjitjhala commented 5 years ago

Thank you very much for this! I will look into it and fix in a couple of days!

On Tue, May 14, 2019 at 12:00 AM Georgi Lyubenov notifications@github.com wrote:

Update:

Removing the data A and leaving only the newtype B also reproduces it! Replacing Bool with Int makes it work fine.

tauren :: ~/liquid-repro » cat B.hs

module B where

import Foreign.Storable (Storable, poke, pokeByteOff)

newtype B = B Bool

instance Storable B where

poke ptr (B b) = pokeByteOff ptr 16 b

tauren :: ~/liquid-repro » liquid B.hs

LiquidHaskell Version 0.8.6.0, Git revision 406dd8bc198fad9a2ff87025689b6035e60fd9be [develop@406dd8bc198fad9a2ff87025689b6035e60fd9be (Fri May 10 09:09:19 2019 -0700)]

Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: B.hs

[Checking: B.hs] **

DONE: A-Normalization ****

** DONE: Extracted Core using GHC *****

** DONE: Transformed Core *****

Working 75% [=================================================................]

** DONE: annotate *****

** RESULT: ERROR ***

:1:1-1:1: Error

crash: SMTLIB2 respSat = Error "line 353 column 1773: Sorts Bool and Int are incompatible"

— 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/1490?email_source=notifications&email_token=AAMS4OATSHIKXKXW7SC645TPVJPRHA5CNFSM4HMW2BTKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVKOZIA#issuecomment-492104864, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OGJ3VDKX5V3WYJN5YDPVJPRHANCNFSM4HMW2BTA .

ranjitjhala commented 5 years ago

Btw, the simplest workaround is to replace “new type” with “data” — as the former doesn’t exist at the “core” level which causes LH problems.

Regardless, will fix ASAP!

On Tue, May 14, 2019 at 6:17 AM Ranjit Jhala jhala@cs.ucsd.edu wrote:

Thank you very much for this! I will look into it and fix in a couple of days!

On Tue, May 14, 2019 at 12:00 AM Georgi Lyubenov notifications@github.com wrote:

Update:

Removing the data A and leaving only the newtype B also reproduces it! Replacing Bool with Int makes it work fine.

tauren :: ~/liquid-repro » cat B.hs

module B where

import Foreign.Storable (Storable, poke, pokeByteOff)

newtype B = B Bool

instance Storable B where

poke ptr (B b) = pokeByteOff ptr 16 b

tauren :: ~/liquid-repro » liquid B.hs

LiquidHaskell Version 0.8.6.0, Git revision 406dd8bc198fad9a2ff87025689b6035e60fd9be [develop@406dd8bc198fad9a2ff87025689b6035e60fd9be (Fri May 10 09:09:19 2019 -0700)]

Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: B.hs

[Checking: B.hs] **

DONE: A-Normalization ****

** DONE: Extracted Core using GHC *****

** DONE: Transformed Core *****

Working 75% [=================================================................]

** DONE: annotate *****

** RESULT: ERROR ***

:1:1-1:1: Error

crash: SMTLIB2 respSat = Error "line 353 column 1773: Sorts Bool and Int are incompatible"

— 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/1490?email_source=notifications&email_token=AAMS4OATSHIKXKXW7SC645TPVJPRHA5CNFSM4HMW2BTKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVKOZIA#issuecomment-492104864, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OGJ3VDKX5V3WYJN5YDPVJPRHANCNFSM4HMW2BTA .

ranjitjhala commented 5 years ago

Even smaller minimal example (as a record for me...)

newtype B = B Bool

{-@ fb :: Bool -> Nat @-}
fb :: Bool -> Int
fb b  = 1

{-@ foo :: B -> Nat @-}
foo :: B -> Int
foo (B b) = fb b
ranjitjhala commented 5 years ago

It looks like you can work around this right now, by adding the line:

{-@ newtype B = B Bool @-}

LH will not crash then, but will complain about the call to pokeByteOff ... which you can address by adding an instance signature for the poke method as described in tests/classes/pos/Inst00.hs.

e.g. a signature like:

{-@ pokeB :: {p:_ | PValid p 16} -> _ -> IO () @-}
pokeB ptr (B b) = pokeByteOff ptr 16 b

Of course LH will still complain because there are missing methods in that class-instance ... but you can then fill them in appropriately.

[Lets keep this open because though the current situation has a work around, it needs to be fixed!]

einargs commented 5 years ago

I've come across something that I think is related:

{-@ LIQUID "--exact-data-cons" @-}

module Repro2 () where

-- If you convert `newtype Embed` to `data Embed` the error goes away.
{-@ newtype Embed a = Embed a @-}
newtype Embed a = Embed a

{-@ autosize LTT @-}
{-@ data LTT = Pi { piTyA :: Embed LTT, piTyB :: LTT }
             | Universe
             | Var @-}
data LTT = Pi (Embed LTT) LTT
         | Universe
         | Var

{-@ measure isLttDev @-}
isLttDev :: LTT -> Bool
isLttDev (Pi (Embed t1) t2) = isLttDev t2 || isLttDev t1
isLttDev Universe = True
isLttDev Var = False

Running this with liquid built from the current develop HEAD (commit rev f4fe82cd03fbe906379c8ebeac5ec3efae0b4cd8) will produce the error:

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 31 column 101: unknown sort 'Repro2.LTT'"

(I can't easily make the conversion from newtype to data because Embed is in a library.)

ranjitjhala commented 5 years ago

Hi Einar,

thanks for pointing that out! The newtype is what is causing the problem; @nikivazou we should have an error message for this -- e.g.

"unknown newtype Embed"

If you just comment out that line, then LH works fine on this...

einargs commented 5 years ago

@ranjitjhala if you mean that commenting out {-@ newtype Embed a = Embed a @-} fixes the problem, then that doesn't exactly work for me--see the examples below, of which four is the most interesting--somehow running liquid first with the newtype annotation, then without, and finally with --diff causes it to emit "SAFE".

All of the "Commands" scripts below are executed using sh in this repository under this branch after running nix-shell. If desired, I can create something that doesn't rely on nix.

The only difference between the Repro2-has-newtype.hs and Repro2-no-newtype.hs files mentioned in the scripts below is whether {-@ newtype @-} is commented out:

-- Repro2-has-newtype.hs
{-@ newtype Embed a = Embed a @-}
-- Repro2-no-newtype.hs
-- {-@ newtype Embed a = Embed a @-}

1. Commands:

# rep1.sh
echo "rm -rf src/.liquid"
rm -rf src/.liquid

echo "without newtype"
rm ./src/Repro2.hs
cp ./Repro2-no-newtype.hs ./src/Repro2.hs
cat ./src/Repro2.hs

echo "stack exec liquid -- src/Repro2.hs"
stack exec liquid -- src/Repro2.hs

Error:

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 31 column 101: unknown sort 'Repro2.LTT'"

2. Commands:

# rep2.sh
echo "rm -rf src/.liquid"
rm -rf src/.liquid

echo "use newtype"
rm ./src/Repro2.hs
cp ./Repro2-has-newtype.hs ./src/Repro2.hs
cat ./src/Repro2.hs

echo "stack exec liquid -- src/Repro2.hs"
stack exec liquid -- src/Repro2.hs

Error:

 $CENSORED/dep-lang/src/Repro2.hs:19:46-56: Error: Uh oh.

 19 | isLttDev (Pi (Embed t1) t2) = isLttDev t2 || isLttDev t1
                                                   ^^^^^^^^^^^

     addC: malformed constraint:
forall a . a
 <:
{VV : Repro2.LTT | autolen VV < autolen ds_d1YE
                   && autolen VV >= 0}

4. Commands:

# rep4.sh
echo "rm -rf src/.liquid"
rm -rf src/.liquid

echo "use newtype"
rm ./src/Repro2.hs
cp ./Repro2-has-newtype.hs ./src/Repro2.hs
cat ./src/Repro2.hs

echo "stack exec liquid -- src/Repro2.hs"
stack exec liquid -- src/Repro2.hs

echo "remove newtype"
rm ./src/Repro2.hs
cp ./Repro2-no-newtype.hs ./src/Repro2.hs
cat ./src/Repro2.hs

echo "stack exec liquid -- src/Repro2.hs"
stack exec liquid -- src/Repro2.hs

echo "stack exec liquid -- src/Repro2.hs --diff"
stack exec liquid -- src/Repro2.hs --diff

Error: first I get a weirdly formatted trace and a SAFE message:

**** RESULT: SAFE **************************************************************
ranjitjhala commented 5 years ago

Dear @einargs,

(sorry for the delay, am traveling!)

hmm you are right. This example shows an odd-to-me limitation in the SMTLIB's encoding of data types -- which I am attaching below because right now github is being difficult with logging me in.

Anyways, the solution is to

  1. Use --no-adt to disable using the native SMT encoding;

This will let LH run to completion, but unfortunately our newtype support for measures is limited and so you get a bunch of termination related errors, because LH is somehow unable to use the measures on newtype, so:

  1. Use data instead of newtype

and then LH should say SAFE.

Can you let me know if this works for you?

Either way, thanks for pointing this bug out -- and please leave it open, because I should really fix BOTH of the above problems (the SMT encoding AND the measure instantiation.)

@nikivazou can you look at the second one? Here is a minimal failing test, there are many termination errors, but if you replace newtype with data then LH says "SAFE".

{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--no-adt" @-}

module Repro2 () where

newtype Embed a = Embed a

{-@ autosize LTT @-}
{-@ data LTT = Pi { piTyA :: Embed LTT, piTyB :: LTT }
             | Universe
             | Var @-}
data LTT = Pi (Embed LTT) LTT
         | Universe
         | Var

{-@ measure isLttDev @-}
isLttDev :: LTT -> Bool
isLttDev (Pi (Embed t1) t2) = isLttDev t2 || isLttDev t1
isLttDev Universe = True
isLttDev Var = False

On Fri, Aug 2, 2019 at 7:33 AM Einar Strandberg notifications@github.com wrote:

@ranjitjhala https://github.com/ranjitjhala if you mean that commenting out {-@ newtype Embed a = Embed a @-} fixes the problem, then that doesn't exactly work for me--see the examples below, of which four is the most interesting--somehow running liquid first with the newtype annotation, then without, and finally with --diff causes it to emit "SAFE".

All of the "Commands" scripts below are executed using sh in this repository under this branch https://github.com/einargs/dep-lang/tree/liquid-issue-reproduction after running nix-shell. If desired, I can create something that doesn't rely on nix.

The only difference between the Repro2-has-newtype.hs and Repro2-no-newtype.hs files mentioned in the scripts below is whether {-@ newtype @-} is commented out:

-- Repro2-has-newtype.hs {-@ newtype Embed a = Embed a @-}-- disabled:-- {-@ newtype Embed a = Embed a @-}

1.

Commands:

rep1.sh

echo "rm -rf src/.liquid" rm -rf src/.liquid

echo "without newtype" rm ./src/Repro2.hs cp ./Repro2-no-newtype.hs ./src/Repro2.hs cat ./src/Repro2.hs

echo "stack exec liquid -- src/Repro2.hs" stack exec liquid -- src/Repro2.hs

Error:

:1:1-1:1: Error crash: SMTLIB2 respSat = Error "line 31 column 101: unknown sort 'Repro2.LTT'"

1.

Commands:

rep2.shecho "rm -rf src/.liquid"

rm -rf src/.liquid echo "use newtype" rm ./src/Repro2.hs cp ./Repro2-has-newtype.hs ./src/Repro2.hs cat ./src/Repro2.hs echo "stack exec liquid -- src/Repro2.hs" stack exec liquid -- src/Repro2.hs

Error:

$CENSORED/dep-lang/src/Repro2.hs:19:46-56: Error: Uh oh.

19 | isLttDev (Pi (Embed t1) t2) = isLttDev t2 || isLttDev t1 ^^^^^^^^^^^

 addC: malformed constraint:

forall a . a <: {VV : Repro2.LTT | autolen VV < autolen ds_d1YE && autolen VV >= 0}

1.

Commands:

rep4.shecho "rm -rf src/.liquid"

rm -rf src/.liquid echo "use newtype" rm ./src/Repro2.hs cp ./Repro2-has-newtype.hs ./src/Repro2.hs cat ./src/Repro2.hs echo "stack exec liquid -- src/Repro2.hs" stack exec liquid -- src/Repro2.hs echo "remove newtype" rm ./src/Repro2.hs cp ./Repro2-no-newtype.hs ./src/Repro2.hs cat ./src/Repro2.hs echo "stack exec liquid -- src/Repro2.hs" stack exec liquid -- src/Repro2.hs echo "stack exec liquid -- src/Repro2.hs --diff" stack exec liquid -- src/Repro2.hs --diff

Error: first I get a weirdly formatted trace and a SAFE message:

RESULT: SAFE **

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1490?email_source=notifications&email_token=AAMS4OBJ34A36AG5R2ISJNDQCOIUXA5CNFSM4HMW2BTKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD3MLPFA#issuecomment-517519252, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OFXCDFYYVHXFDHI2UTQCOIUXANCNFSM4HMW2BTA .

ranjitjhala commented 5 years ago

Here's the SMT2 issue:

;; this is fine
(declare-datatypes (T0) ((Embed (Embed (sel0 T0)))))

;; this is also fine
(declare-datatypes () ((LTT Var (Pi (selx LTT) (sely LTT)))))

;; but this one fails with "unknown sort 'LTT_b'"
(declare-datatypes () ((LTT_b Var_b (Pi_b (selx_b (Embed LTT_b)) (sely_b
LTT_b)))))

On Mon, Aug 5, 2019 at 9:33 PM Ranjit Jhala jhala@cs.ucsd.edu wrote:

Dear @einargs,

(sorry for the delay, am traveling!)

hmm you are right. This example shows an odd-to-me limitation in the SMTLIB's encoding of data types -- which I am attaching below because right now github is being difficult with logging me in.

Anyways, the solution is to

  1. Use --no-adt to disable using the native SMT encoding;

This will let LH run to completion, but unfortunately our newtype support for measures is limited and so you get a bunch of termination related errors, because LH is somehow unable to use the measures on newtype, so:

  1. Use data instead of newtype

and then LH should say SAFE.

Can you let me know if this works for you?

Either way, thanks for pointing this bug out -- and please leave it open, because I should really fix BOTH of the above problems (the SMT encoding AND the measure instantiation.)

@nikivazou can you look at the second one? Here is a minimal failing test, there are many termination errors, but if you replace newtype with data then LH says "SAFE".

{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--no-adt" @-}

module Repro2 () where

newtype Embed a = Embed a

{-@ autosize LTT @-}
{-@ data LTT = Pi { piTyA :: Embed LTT, piTyB :: LTT }
             | Universe
             | Var @-}
data LTT = Pi (Embed LTT) LTT
         | Universe
         | Var

{-@ measure isLttDev @-}
isLttDev :: LTT -> Bool
isLttDev (Pi (Embed t1) t2) = isLttDev t2 || isLttDev t1
isLttDev Universe = True
isLttDev Var = False

On Fri, Aug 2, 2019 at 7:33 AM Einar Strandberg notifications@github.com wrote:

@ranjitjhala https://github.com/ranjitjhala if you mean that commenting out {-@ newtype Embed a = Embed a @-} fixes the problem, then that doesn't exactly work for me--see the examples below, of which four is the most interesting--somehow running liquid first with the newtype annotation, then without, and finally with --diff causes it to emit "SAFE".

All of the "Commands" scripts below are executed using sh in this repository under this branch https://github.com/einargs/dep-lang/tree/liquid-issue-reproduction after running nix-shell. If desired, I can create something that doesn't rely on nix.

The only difference between the Repro2-has-newtype.hs and Repro2-no-newtype.hs files mentioned in the scripts below is whether {-@ newtype @-} is commented out:

-- Repro2-has-newtype.hs {-@ newtype Embed a = Embed a @-}-- disabled:-- {-@ newtype Embed a = Embed a @-}

1.

Commands:

rep1.sh

echo "rm -rf src/.liquid" rm -rf src/.liquid

echo "without newtype" rm ./src/Repro2.hs cp ./Repro2-no-newtype.hs ./src/Repro2.hs cat ./src/Repro2.hs

echo "stack exec liquid -- src/Repro2.hs" stack exec liquid -- src/Repro2.hs

Error:

:1:1-1:1: Error crash: SMTLIB2 respSat = Error "line 31 column 101: unknown sort 'Repro2.LTT'"

1.

Commands:

rep2.shecho "rm -rf src/.liquid"

rm -rf src/.liquid echo "use newtype" rm ./src/Repro2.hs cp ./Repro2-has-newtype.hs ./src/Repro2.hs cat ./src/Repro2.hs echo "stack exec liquid -- src/Repro2.hs" stack exec liquid -- src/Repro2.hs

Error:

$CENSORED/dep-lang/src/Repro2.hs:19:46-56: Error: Uh oh.

19 | isLttDev (Pi (Embed t1) t2) = isLttDev t2 || isLttDev t1 ^^^^^^^^^^^

 addC: malformed constraint:

forall a . a <: {VV : Repro2.LTT | autolen VV < autolen ds_d1YE && autolen VV >= 0}

1.

Commands:

rep4.shecho "rm -rf src/.liquid"

rm -rf src/.liquid echo "use newtype" rm ./src/Repro2.hs cp ./Repro2-has-newtype.hs ./src/Repro2.hs cat ./src/Repro2.hs echo "stack exec liquid -- src/Repro2.hs" stack exec liquid -- src/Repro2.hs echo "remove newtype" rm ./src/Repro2.hs cp ./Repro2-no-newtype.hs ./src/Repro2.hs cat ./src/Repro2.hs echo "stack exec liquid -- src/Repro2.hs" stack exec liquid -- src/Repro2.hs echo "stack exec liquid -- src/Repro2.hs --diff" stack exec liquid -- src/Repro2.hs --diff

Error: first I get a weirdly formatted trace and a SAFE message:

RESULT: SAFE **

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1490?email_source=notifications&email_token=AAMS4OBJ34A36AG5R2ISJNDQCOIUXA5CNFSM4HMW2BTKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD3MLPFA#issuecomment-517519252, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OFXCDFYYVHXFDHI2UTQCOIUXANCNFSM4HMW2BTA .

einargs commented 5 years ago

I can confirm that changing the newtype to data fixes the problem.

ranjitjhala commented 5 years ago

Also after adding the —no-adt , right?

On Tue, Aug 6, 2019 at 6:37 AM Einar Strandberg notifications@github.com wrote:

I can confirm that changing the newtype to data fixes the problem.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1490?email_source=notifications&email_token=AAMS4OEYAQEHLCC43AMU47DQDDFFNA5CNFSM4HMW2BTKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD3TQFTI#issuecomment-518456013, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OCUABWDPC3VLG55GW3QDDFFNANCNFSM4HMW2BTA .

einargs commented 5 years ago

That doesn't seem to make a difference. If I alter Repro2-no-newtype.hs by changing newtype to data, resulting in:

{-@ LIQUID "--exact-data-cons" @-}

module Repro2 () where

-- If you convert `newtype Embed` to `data Embed` the error goes away.
data Embed a = Embed a

{-@ autosize LTT @-}
{-@ data LTT = Pi { piTyA :: Embed LTT, piTyB :: LTT }
             | Universe
             | Var @-}
data LTT = Pi (Embed LTT) LTT
         | Universe
         | Var

{-@ measure isLttDev @-}
isLttDev :: LTT -> Bool
isLttDev (Pi (Embed t1) t2) = isLttDev t2 || isLttDev t1
isLttDev Universe = True
isLttDev Var = False
stack exec liquid -- src/Repro2.hs

And do sh rep1.sh on a modified rep1.sh script that has the -v flag added to liquidhaskell:

# rep1.sh
echo "rm -rf src/.liquid"
rm -rf src/.liquid

echo "without newtype"
rm ./src/Repro2.hs
cp ./Repro2-no-newtype.hs ./src/Repro2.hs
cat ./src/Repro2.hs

echo "stack exec liquid -- -v src/Repro2.hs"
stack exec liquid -- -v src/Repro2.hs

I get the console output in the attached file: log.txt (which ends with a SAFE message)

yiyunliu commented 4 years ago

Here's a minimal example I can produce for this issue. The use case arises when defining instance functions of the form: Semigroup a => Semigroup (Dual a) where Dual is a newtype:

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

newtype MyId a = MyId a

{-@ data U a = U {unU :: a -> ()} @-}
data U a = U {unU :: a -> ()}

newtype Id a = Id a

-- crash: SMTLIB2 respSat = Error "line 316 column 73: Sorts Int and (Main.Id Int) are incompatible"
{-@ bad :: x:U a -> y:Id a -> {x /= x} @-}
bad :: U a -> Id a -> ()
bad (U unU) (Id y) = unU y

-- succeed and no smtlib crash
{-@ ok0 :: x:U a -> y:Id a -> () @-}
ok0 :: U a -> Id a -> ()
ok0 (U unU) (Id y) = unU y

-- fail but no smtlib crash
{-@ ok1 :: x:U a -> y:a -> {x /= x} @-}
ok1 :: U a -> a -> ()
ok1 (U unU) y = unU y
nikivazou commented 4 years ago

@yiyunliu I pushed a PR-fix; waiting for travis, but let me know if it fixes your original problem.