LiquidHaskell: Comparing approaches to plugging DataCon

We have figured out the fact that the module Language.Haskell.Liquid.Bare.Plugged throws an error in the makePluggedDataCon function because the dts and dcArgs variables differ in the number of arguments. This is because in recent GHC versions, the superclass is not included in the type arguments while it is in the arguments of the data constructor.

So, the two options are: remove superclasses from dcArgs or add it to dts.

I tried both approaches and, while they don’t solve the typeclass issue yet, they do yield slightly different error messages.

First, let’s look at the approach of removing the superclass from dcArgs:

   where
     (tArgs, tRes)     = plugMany allowTC  embs tyi ldcp (das, dts, dt) (dcVars, dcArgs, dcpTyRes dcp)
     (das, _, dts, dt) = Ghc.dataConSig dc
-    dcArgs            = reverse $ filter (not . (if allowTC then isEmbeddedClass else isClassType) . snd) (dcpTyArgs dcp)
+    dcArgs            = reverse $ filter (not . isClassType . snd) (dcpTyArgs dcp)
     dcVars            = if isGADT
                           then padGADVars $ L.nub (dcpFreeTyVars dcp ++ concatMap (map ty_var_value . freeTyVars) (dcpTyRes dcp:(snd <$> dcArgs)))
                           else dcpFreeTyVars dcp

This will always filter out class types, even when the typeclass flag is enabled. The next error message with this fix is:

typeclasses/pos/Basic.hs:9:1: error:
    Specified type does not refine Haskell type for `Basic.C:VEq` (Plugged Init types new - TC allowed)
The Liquid type
.
    a##aEh -> (a##aEh -> _) -> (Basic.VEq a)
.
is inconsistent with the Haskell type
.
    a -> (a -> ()) -> Basic.VEq a
.
defined at typeclasses/pos/Basic.hs:(9,1)-(11,22)
.
Specifically, the Liquid component
.
    a##aEh
.
is inconsistent with the Haskell component
.
    a
.

HINT: Use the hole '_' instead of the mismatched component (in the Liquid specification)
  |
9 | class MyEq a => VEq a where
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^...

On the other hand, there is the fix that adds the superclass:

   where
     (tArgs, tRes)     = plugMany allowTC  embs tyi ldcp (das, dts, dt) (dcVars, dcArgs, dcpTyRes dcp)
-    (das, _, dts, dt) = Ghc.dataConSig dc
+    (das, theta, originDts, dt) = Ghc.dataConSig dc
+    dts               = consClassArgs ++ originDts
+    consClassArgs     = if allowTC then filter (not . GM.isEmbeddedDictType) theta else []
     dcArgs            = reverse $ filter (not . (if allowTC then isEmbeddedClass else isClassType) . snd) (dcpTyArgs dcp)
     dcVars            = if isGADT
                           then padGADVars $ L.nub (dcpFreeTyVars dcp ++ concatMap (map ty_var_value . freeTyVars) (dcpTyRes dcp:(snd <$> dcArgs)))
                           else dcpFreeTyVars dcp

And this yields the following error.

typeclasses/pos/Basic.hs:9:1: error:
    Specified type does not refine Haskell type for `Basic.C:VEq` (Plugged Init types new - TC allowed)
The Liquid type
.
    a##aEh -> (Basic.MyEq a##aEh) -> (a##aEh -> _) -> (Basic.VEq a)
.
is inconsistent with the Haskell type
.
    a -> Basic.MyEq a -> (a -> ()) -> Basic.VEq a
.
defined at typeclasses/pos/Basic.hs:(9,1)-(11,22)
.
Specifically, the Liquid component
.
    a##aEh
.
is inconsistent with the Haskell component
.
    a
.

HINT: Use the hole '_' instead of the mismatched component (in the Liquid specification)
  |
9 | class MyEq a => VEq a where
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Notice how the underlying error in both cases is the same: there is an issue when comparing type variables, making a different than a##aEh.

The only difference is whether the LH type as well as the Haskell type is considered to include the predicate Basic.MyEq a/Basic.MyEq a##aEh or not.

I’ll just stick to one solution for the moment being, and hopefully moving forward in the solution will shed some light on which one might be the better option.