ucsd-progsys / liquidhaskell

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

Make --exact-data-cons the default #2290

Closed facundominguez closed 4 months ago

facundominguez commented 4 months ago

--exact-data-cons is a source of confusion for users that try to reflect functions every now and then.

In this PR I'm enabling it by default.

Note that I'm also removing the flag --exact-data-cons and adding a flag --no-exact-data-cons, which might not be your preference if you care about backward compatibility of the command line.

facundominguez commented 4 months ago

Any drawbacks of merging something like this?

facundominguez commented 4 months ago

Hm, CI is revealing some issue with ProofCombinators.

Multiple specifications for `Language.Haskell.Liquid.ProofCombinators.Admit` :
     Conflicting definitions at
     .       
     * src/Language/Haskell/Liquid/ProofCombinators.hs:76:12
     .       
     * src/Language/Haskell/Liquid/ProofCombinators.hs:79:14

This is fixable by using --no-exact-data-cons in ProofCombinators.

facundominguez commented 4 months ago

There are several files that fail to verify with obscure errors when exact-data-cons is enabled. Enabling the flag by default would expose the users to all of those, which I'm deeming worse than the current situation where we get an error about an undefined symbol when --exact-data-cons needs to be enabled.

Example errors with --exact-data-cons enabled by default:

[160 of 224] Compiling Holes            ( pos/Holes.hs, /home/facundo/tweag/liquidhaskell2/dist-newstyle/build/x86_64-linux/ghc-9.8.2/tests-0.1.0.0/x/unit-pos-2/build/unit-pos-2/unit-pos-2-tmp/Holes.o )

**** LIQUID: ERROR *************************************************************

<no location info>: error:
    Sorry, unexpected panic in liquid-fixpoint!
[176 of 224] Compiling Jeff             ( pos/Jeff.hs, /home/facundo/tweag/liquidhaskell2/dist-newstyle/build/x86_64-linux/ghc-9.8.2/tests-0.1.0.0/x/unit-pos-2/build/unit-pos-2/unit-pos-2-tmp/Jeff.o )

<no source information>:1:1: error:
    Unknown type constructor `GHC.ForeignPtr.ForeignPtr`
    matchTyCon: GHC.ForeignPtr.ForeignPtr
[184 of 224] Compiling LambdaEval       ( pos/LambdaEval.hs, /home/facundo/tweag/liquidhaskell2/dist-newstyle/build/x86_64-linux/ghc-9.8.2/tests-0.1.0.0/x/unit-pos-2/build/unit-pos-2/unit-pos-2-tmp/LambdaEval.o )

**** LIQUID: ERROR *************************************************************

<no location info>: error:
    Sorry, unexpected panic in liquid-fixpoint!
[185 of 224] Compiling LambdaEvalMini   ( pos/LambdaEvalMini.hs, /home/facundo/tweag/liquidhaskell2/dist-newstyle/build/x86_64-linux/ghc-9.8.2/tests-0.1.0.0/x/unit-pos-2/build/unit-pos-2/unit-pos-2-tmp/LambdaEvalMini.o )

**** LIQUID: ERROR *************************************************************

<no location info>: error:
    Sorry, unexpected panic in liquid-fixpoint!
[186 of 224] Compiling LambdaEvalSuperTiny ( pos/LambdaEvalSuperTiny.hs, /home/facundo/tweag/liquidhaskell2/dist-newstyle/build/x86_64-linux/ghc-9.8.2/tests-0.1.0.0/x/unit-pos-2/build/unit-pos-2/unit-pos-2-tmp/LambdaEvalSuperTiny.o )

**** LIQUID: ERROR *************************************************************

<no location info>: error:
    Sorry, unexpected panic in liquid-fixpoint!
[187 of 224] Compiling LambdaEvalTiny   ( pos/LambdaEvalTiny.hs, /home/facundo/tweag/liquidhaskell2/dist-newstyle/build/x86_64-linux/ghc-9.8.2/tests-0.1.0.0/x/unit-pos-2/build/unit-pos-2/unit-pos-2-tmp/LambdaEvalTiny.o )

**** LIQUID: ERROR *************************************************************

<no location info>: error:
    Sorry, unexpected panic in liquid-fixpoint!

Until these error messages are improved, I propose that we don't change the default.