search

jprider63 / vrdt

5 stars 0 forks source link

LH says safe when it isn't? #10

Closed jprider63 closed 4 years ago

jprider63 commented 4 years ago

In commit 81a148a, liquid MultiSet.hs returns safe even though the refinement for lawCommutativity doesn't type check. Any idea why this might be @nikivazou?

$ liquid --version
LiquidHaskell Version 0.8.6.0, Git revision 2d3c4009b80a714247648c2234cc34910b855643 (dirty) [develop@2d3c4009b80a714247648c2234cc34910b855643 (Mon Feb 24 13:26:16 2020 +0100)]
nikivazou commented 4 years ago

Interesting. I will have to investigate. Are you using the new PLE? If no, can you pull LH from master and try it both normally and with the oldple flag? Maybe I introduced a bug in the new ple implementation.

jprider63 commented 4 years ago

It was the old PLE. 2d3c4009b80a714247648c2234cc34910b855643 is from develop on Feb 24. I'll try the new one.

I'd be surprised if it's related to PLE since LH wasn't type checking the refinement.

nikivazou commented 4 years ago

oh, you mean the refinement does not typecheck because x is not in scope, correct? I just saw that

jprider63 commented 4 years ago

Right, and the order of arguments is wrong too.

nikivazou commented 4 years ago

ok, I know what is happening: because your refinement is trivially identity, it never reaches the internals of LH: it is treated as true. Could you please make an issue, whenever you can?

jprider63 commented 4 years ago

Ah because the LHS and RHS are equal? I'll make an issue now.

nikivazou commented 4 years ago

yes! also, if you change == to /=, LH will see apply op2 (apply op1 x) /= apply op2 (apply op1 x) as false.

The idea is that for such trivial statements, you do not need to call the SMT to decide.

jprider63 commented 4 years ago

Closing this since we've opened it upstream.