LiquidHaskell: Analyzing DataCon

In my last post I wrote about how I arrived to a new error: GHC and Liquid specifications have different numbers of fields for `Basic.C:VEq`.

I ran a few experiments. I will document the results.

The first thing to notice is that the error comes from the inconsistencies between the variables dts (the type arguments to the constructor) and dcArgs (pairs of LHName and SpecType) in the function makePluggedDataCon, in Plugged.hs.

When I trace both variables I get the following:

-- Pretty printed because it has no Show instance
dts: [a -> ()]

dcArgs: [
  (LHNResolved (LHRGHC Basic.$p1VEq{v rOQ}) "Basic.$p1VEq", (Basic.MyEq a##aEh)),
  (LHNResolved (LHRGHC Basic.lawRefl{v rEe}) "Basic.lawRefl", v:a##aEh -> {VV : _ | Basic.eq v v == true})
]

My first thought was that dcArgs had more data than it should. However, when tracing the same variables in LH GHC8 I got this:

dts: [Basic.MyEq a, a -> ()]

dcArgs: [
  ("Basic.$p1VEq",(Basic.MyEq a##alt)),
  ("Basic.lawRefl",v:a##alt -> {VV : _ | Basic.eq v v == true})
]

The surprising thing here is that dts actually contains an extra element: Basic.MyEq a.

So, maybe the right solution would be to add the extra information to dts instead of removing elements from dcArgs.

Trying to decide whether we have missing or unnecessary information, I tried one more experiment:

{-@ LIQUID "--typeclass" @-}
{-@ LIQUID "--reflection" @-}
module Basic where

class MyEq a where
    {-@ eq :: a -> a -> Bool @-}
    eq :: a -> a -> Bool

class MyEq2 a where
    {-@ eq2 :: a -> a -> Bool @-}
    eq2 :: a -> a -> Bool

class (MyEq a, MyEq2 a) => VEq a where
    {-@ lawRefl :: v:a -> {eq v v <=> eq2 v v} @-}
    lawRefl :: a -> ()

I ran the checker in GHC8 and noticed that both dts and dcArgs had 3 terms now, which is reasonable.

What would happen if I change VEq to the following?

- class (MyEq a, MyEq2 a) => VEq a where
+ class MyEq a => VEq a where
    {-@ lawRefl :: v:a -> {eq v v <=> eq2 v v} @-}
    lawRefl :: a -> ()

Turns out that now, neither variable has Basic.MyEq2 a present. I was expecting a different result, and maybe that could have been an indicator for how to solve the present issue, but it wasn’t.

So, at this point I think either way would work: adding the typeclass dependency to dts or removing typeclasses from dcArgs, as long as the solution is consistent. I might try to do the filtering, simply because I think it could be easier, but I am open to do the other option if it happens to be more useful down the road.