Standalone deriving fails for GADTs when unifying type variables within a context
I have a GADT that looks like:
data SumType (types :: [Type]) where
Here :: forall x xs. x -> SumType (x ': xs)
There :: forall x xs. SumType xs -> SumType (x ': xs)
which I can derive Eq
for by doing
deriving instance (Eq x, Eq (SumType xs)) => Eq (SumType (x ': xs))
instance Eq (SumType '[]) where
_ == _ = True
The Eq (SumType '[])
instance is needed to resolve the Eq (SumType xs)
constraint in the Eq (SumType (x ': xs))
instance. It would be nice to just do
deriving instance (Eq x, Eq (SumType xs)) => Eq (SumType (x ': xs))
deriving instance Eq (SumType '[])
And have the derivation be the same as Void
(since SumType '[]
has no constructors). Instead, it's generating (cleaned up from -ddump-deriv
)
instance Eq (SumType '[]) where
(==) (Here a) (Here b) = a == b
(==) (There a) (There b) = a == b
(==) _ _ = False
and I get an error
• Could not deduce: xs1 ~ xs
from the context: '[] ~ (x : xs)
bound by a pattern with constructor:
There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
in an equation for ‘==’
or from: '[] ~ (x1 : xs1)
bound by a pattern with constructor:
There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
in an equation for ‘==’
‘xs1’ is a rigid type variable bound by
a pattern with constructor:
There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
in an equation for ‘==’
‘xs’ is a rigid type variable bound by
a pattern with constructor:
There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
in an equation for ‘==’
Expected type: SumType xs
Actual type: SumType xs1
• In the second argument of ‘(==)’, namely ‘b1’
In the expression: ((a1 == b1))
In an equation for ‘==’: (==) (There a1) (There b1) = ((a1 == b1))
When typechecking the code for ‘==’
in a derived instance for ‘Eq (SumType '[])’:
To see the code I am typechecking, use -ddump-deriv
• Relevant bindings include
b1 :: SumType xs1
a1 :: SumType xs
|
70 | deriving instance Eq (SumType '[])
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This issue is similar to Standalone deriving fails for GADTs due to inaccessible code, but different because I believe it would typecheck if not for pattern matching on the constrained type variable.