compiler plugin doesn't work due to dated Hackage package

[gshen42]

I followed the tutorial for compiler plugin, but failed to compile package liquidhaskell with the following error message:

src/Language/Haskell/Liquid/GHC/Misc.hs:59:82: error:
    Module ‘Type’ does not export ‘isClassPred’
   |
59 | import           Type                                       (expandTypeSynonyms, isClassPred, isEqPred, liftedTypeKind)
   |                                                                                  ^^^^^^^^^^^

src/Language/Haskell/Liquid/GHC/Misc.hs:59:95: error:
    Module ‘Type’ does not export ‘isEqPred’
   |
59 | import           Type                                       (expandTypeSynonyms, isClassPred, isEqPred, liftedTypeKind)
   |                    

The problem is caused by the fact that the latest liquidhaskell on Hackage is compiled against ghc-8.8, whereas the compiler plugin requires ghc-8.10.1 (which I'm using), and there's a breaking API change in ghc-8.10.1 (function isClassPred and isEqPred are moved from module Type to Predicate), so the package from Hackage fails to compile.

Aside from update the package on Hackage, is there a workaround to try the compiler plugin, or am I missing anything?

[ranjitjhala]

Hi @gshen42,

Unfortunately yes the only workaround is to use GHC 8.10 as the plugin requires features that were just added to that version of GHC.

The simplest way would be to follow these instructions:

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/INSTALL.md#step-2-install-liquid-from-source

LMK if that works!

• Ranjit.

[gshen42]

Thanks, @ranjitjhala. The standalone liquid executable works, but that's not the compiler plugin way I hope to use.

I somehow managed to get the latest liquidhaskell by listing the GitHub repo in the extra-deps field of my stack.yaml. It looks like this:

extra-deps:
...
- github: ucsd-progsys/liquid-fixpoint
  commit: 18ddfac7dafbe7472c1962a1e986677fbcd27515
- github: ucsd-progsys/liquidhaskell
  commit: 3bc467162ba285bf2c1529dafce21a20bb9aab8e
  subdirs:
  - liquid-ghc-prim
  - liquid-base
  - liquid-bytestring
  - liquid-prelude
  - liquid-vector
  - liquid-containers
  - liquid-parallel
  - liquid-platform
  - .

The liquidhaskell package builds successfully, however, when I try to type check this code:

{-@ one :: {v:Int | v > 0} @-}
one :: Int
one = 42

, I get this error:

/home/gshen/LH-playground/[src/Main.hs:6:12-27: Error: Illegal type specification for `Main.one`
     Main.one :: {v : GHC.Types.Int | v > 0}
     Sort Error in Refinement: {v : GHC.Types.Int | v > 0}
     The sort GHC.Types.Int is not numeric
  because
The sort GHC.Types.Int is not numeric]

Is there a way to fix this?

[ranjitjhala]

Wow that’s surprising - how are you running LH to get that error?

Did you try

$ stack exec — liquid path/to/File.hs

Or something else?

On Tue, Jun 16, 2020 at 9:59 PM Gan Shen notifications@github.com wrote:

Thanks, @ranjitjhala https://urldefense.com/v3/__https://github.com/ranjitjhala__;!!Mih3wA!VmNFtKbErMNSsu1fLn1E03OslX_7GmXRZ0EbRfBXV64juH3yPkKHJFcth1vc7QBs$. The standalone liquid executable works, but that's not the compiler plugin way I hope to use.

I somehow managed to get the latest liquidhaskell by listing the GitHub repo in the extra-deps field of my stack.yaml. It looks like this:

extra-deps: ...

• github: ucsd-progsys/liquid-fixpoint commit: 18ddfac7dafbe7472c1962a1e986677fbcd27515
• github: ucsd-progsys/liquidhaskell commit: 3bc467162ba285bf2c1529dafce21a20bb9aab8e subdirs:
  • liquid-ghc-prim
  • liquid-base
  • liquid-bytestring
  • liquid-prelude
  • liquid-vector
  • liquid-containers
  • liquid-parallel
  • liquid-platform
  • .

The liquidhaskell package builds successfully, however, when I try to type check this code:

{-@ one :: {v:Int | v > 0} @-} one :: Int one = 42

, I get this error:

/home/gshen/LH-playground/[src/Main.hs:6:12-27: Error: Illegal type specification for Main.one Main.one :: {v : GHC.Types.Int | v > 0} Sort Error in Refinement: {v : GHC.Types.Int | v > 0} The sort GHC.Types.Int is not numeric because The sort GHC.Types.Int is not numeric]

Is there a way to fix this?

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1689*issuecomment-645150698__;Iw!!Mih3wA!VmNFtKbErMNSsu1fLn1E03OslX_7GmXRZ0EbRfBXV64juH3yPkKHJFcth7ti23Sp$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OCWKI5G4GO453HHXTLRXBERLANCNFSM4N7J4TDA__;!!Mih3wA!VmNFtKbErMNSsu1fLn1E03OslX_7GmXRZ0EbRfBXV64juH3yPkKHJFcthy4-iLBC$ .

[gshen42]

Yes, running stack exec -- liquid ... works, so I guess it's maybe a bug in the compiler plugin or I missed something.

I just upload my project (https://github.com/gshen42/LH-playground) to the GitHub in case you want to reproduce the error. What I'm trying to do is simply run stack build then my code will be type checked and compiled.

[ranjitjhala]

Hi @adinapoli can you provide some insight here? Maybe there is something in the docs we can clarify?

[ranjitjhala]

(or is this the package path thing?)

[adinapoli]

@ranjitjhala It might be something ever simpler. If I understand what @gshen42 is trying to achieve by looking at his example project, he's trying to actually use the plugin (which is great).

Unfortunately this made me realise we didn't clarify something that for us it's obvious, but that we totally neglected documentationwise: the use of the "mirror packages".

@gshen42 What you need to do is to replace your base dependency in your .cabal manifest with the liquid-base "mirror" package that actually ships module re-exports that allows you to use stuff from base plus all the Liquid refinements. At the moment these "mirror" packages are in alpha version, which means we are adding stuff as we see need, so we do not cover all base but the most parts (definitely enough for what you need, I think).

In the same vein, we provide some very simple "mirror" packages for containers, vector and bytestring all with the liquid-* prefix, but the ecosystem is quite in its infancy at this stage (pull requests are welcome, of course 😉 ).

Sorry for the confusion! We sort of hint about this in the tutorial but we should make this much more obvious (I will make sure this piece of information is much more visible).

[gshen42]

Thanks @adinapoli for the clarification. Now everything works perfectly.

[adinapoli]

Great, happy to have been useful, and sorry if you had to be the guinea pig for this 😉

[ranjitjhala]

Ah, got it thanks Alfredo and apologies Gary!

On Thu, Jun 18, 2020 at 12:39 AM Alfredo Di Napoli notifications@github.com wrote:

Great, happy to have been useful, and sorry if you had to be the guinea pig for this 😉

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1689*issuecomment-645840187__;Iw!!Mih3wA!U8l0IqOAjxtfRtg7FQPo642guP4eISu1w-eJiE7dJHmfxFr5YcnqU-oTLDpWAZkX$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4ODOWUNNKBHZPHCCMB3RXHAEZANCNFSM4N7J4TDA__;!!Mih3wA!U8l0IqOAjxtfRtg7FQPo642guP4eISu1w-eJiE7dJHmfxFr5YcnqU-oTLJn_859j$ .