ucsd-progsys / liquidhaskell

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

More/less binders expected when using --typeclass #2269

Open nmeum opened 9 months ago

nmeum commented 9 months ago

Hey, I am new to Liquid Haskell and was interested in using it in conjunction with type classes. For this purpose, I tried the following example from the Liquid Haskell specification:

{-# LANGUAGE RankNTypes #-}
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--typeclass" @-}
{-@ LIQUID "--aux-inline" @-}
{-@ LIQUID "--ple" @-}

import qualified Prelude

class Semigroup a where
    {-@ mappend :: a -> a -> a @-}
    mappend :: a -> a -> a

class Semigroup a => VSemigroup a where
    {-@ lawAssociative :: v:a -> v':a -> v'':a ->
          {mappend (mappend v v') v'' == mappend v (mappend v' v'')} @-}
    lawAssociative :: a -> a -> a -> ()

Running this as:

$ ghci -fplugin=LiquidHaskell semigroup.hs

Gives me the following error message:

GHCi, version 9.2.5: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( semigroup.hs, interpreted )

<no location info>: error:
    • Uh oh.
    Oops, Ghc gave back more/less binders than I expected
    •
Failed, no modules loaded.

This is with liquidhaskell 0.9.2.5.0 and GHC 9.2.5. I also tried this with GHC 9.4.7 and liquidhaskell 0.9.4.7.0 but with this setup I get the same error message. As I said, I am new to liquidhaskell so I suspect I am just using it wrong or is this an expect error given that --typeclass is still considered experimental?

facundominguez commented 9 months ago

Hello! Typeclass support remains experimental. I just reviewed the tests. There are tests like this that were disabled in the move from ghc 8 to ghc 9, so the chances of making it work without hacking on LH are slim. You could try ghc 8, though that is a tad harder to setup as it requires liquid-base in addition to liquidhaskell.

facundominguez commented 9 months ago

Here there are instructions to test with ghc 8 by building an older LH from the github repo.