LiquidHaskell: First approach

So, the first thing is to set up my environment. And I won’t go into the details of that: it’s just configuring my git project to be able to use git worktrees, choosing the right GHC version through GHCup and installing HLS.

I’d already gone through most of these steps before, when exploring the project in order to prepare my proposal for GSoC, but I’ll just document everything here for future reference either way.

Cleaning up tests

The first thing is to re-enable the tests

executable typeclass-pos
    ...

    -- Fails on GHC 9.0.1
-    if impl(ghc < 9)
      other-modules:
                      All
                    , Lib
                    , Lemma
                    , PNat
                    , SemigroupLib

and run them

❯ ./scripts/test/test_plugin.sh typeclass-pos

I get two types of errors.

Name errors. Which are the actual problem that I intend to solve this summer.

typeclasses/pos/All.hs:51:52: error:
    Unknown logic name `mappend`
    Cannot resolve name
    Maybe you meant one of: snd len
   |
51 |     {-@ lawAssociative :: v:a -> v':a -> v'':a -> {mappend (mappend v v') v'' == mappend v (mappend v' v'')} @-}
   |                                                    ^^^^^^^

Illegal type specification errors. I don’t know exactly when those were introduced, maybe it was at the same time that typeclass support got broken, when support for GHC 9 began.

src/GHC/Num_LHAssumptions.hs:9:23: error:
    Illegal type specification for `GHC.Internal.Num.fromInteger`
    GHC.Internal.Num.fromInteger :: forall a .
                                    (Num<[]> a) =>
                                    x:GHC.Internal.Bignum.Integer.Integer -> {v : a | v == x}
    Sort Error in Refinement: {v : a##xo | v == x}
    Unbound symbol a##xo --- perhaps you meant: a##aK8 ?
  because
Cannot unify a##xo with int in expression: v == x
  because
Invalid Relation v == x with operand types a##xo and int
    Just assume

On further inspection of the faulty code, in src/GHC/Num_LHAssumptions.hs, I see the following:

assume fromInteger :: x:Integer -> {v:a | v = x }

assume negate :: (Num a)
               => x:a
               -> {v:a | v = -x}

Comparing the two assumptions, I spot the most likely cause for the issue: a is a type variable which is not being restricted to the proper Num typeclass.

That can be easily fixed:

-assume fromInteger :: x:Integer -> {v:a | v = x }
+assume fromInteger :: (Num a) => x:Integer -> {v:a | v = x }

That indeed fixed the error, I just replicate the same thing for a couple of extra functions that were missing typeclass constraints.

That leaves me with only the unknown name errors. Now I can focus on restoring typeclass support and, the test suite should be a good indicator of how I’m doing.

Fun with flags

I discovered the --dump-pre-normalized-core flag as well. It outputs the Core internal representation (I found this talk, “Haskell to Core: Understanding Haskell Features Through Their Desugaring”, particularly interesting). It might come in handy in the future, we’ll see.

We also have the --verbose flag. It might be useful at some point but, for my small test cases, I didn’t see any difference. A viable alternative is the debugLogs definition in the liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs file:

-- | Set to 'True' to enable debug logging.
debugLogs :: Bool
debugLogs = False

Setting it to True gives a lot of extra information such as dependencies, internal representations, and module information.