How to get Eq for GADT with non-standard parameter like phantom

Question

For example, trying to compile the following code

{-# LANGUAGE StandaloneDeriving, KindSignatures, DataKinds, GADTs#-} data ExprTag = Tag1 | Tag2 data Expr (tag :: ExprTag) where Con1 :: Int -> Expr tag Con2 :: Expr tag -> Expr tag Con3 :: Expr tag -> Expr Tag2 deriving instance Eq (Expr a) 

gives an error like

 Could not deduce (tag1 ~ tag) from the context (a ~ 'Tag2) bound by a pattern with constructor Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2, in an equation for `==' at Bar.hs:11:1-29 or from (a ~ 'Tag2) bound by a pattern with constructor Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2, in an equation for `==' at Bar.hs:11:1-29 `tag1' is a rigid type variable bound by a pattern with constructor Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2, in an equation for `==' at Bar.hs:11:1 `tag' is a rigid type variable bound by a pattern with constructor Con3 :: forall (tag :: ExprTag). Expr tag -> Expr 'Tag2, in an equation for `==' at Bar.hs:11:1 Expected type: Expr tag1 Actual type: Expr tag In the second argument of `(==)', namely `b1' In the expression: ((a1 == b1)) When typechecking the code for `==' in a standalone derived instance for `Eq (Expr a)': To see the code I am typechecking, use -ddump-deriv 

I see why this does not work, but is there some solution that does not require me to manually create instances of Eq (and Ord)?

Answer 1

As others have found out, the key to the problem is an existentially quantized tag in type Con3 . When you try to identify

 Con3 s == Con3 t = ??? 

there is no reason s and t should be expressions with the same tag .

But maybe you don't care? You can perfectly define a heterogeneous equality test that gladly compares the Expr construct, regardless of tags.

 instance Eq (Expr tag) where (==) = heq where heq :: Expr a -> Expr b -> Bool heq (Con1 i) (Con1 j) = i == j heq (Con2 s) (Con2 t) = heq st heq (Con3 s) (Con3 t) = heq st 

If you don't care, then you might be advised to equip Con3 with a Con3 time witness to the existentially quantified tag . The standard way to do this is with a singleton design.

 data SingExprTag (tag :: ExprTag) where SingTag1 :: SingExprTag Tag1 SingTag2 :: SingExprTag Tag2 

Analysis of the case on the value in the SingExprTag tag will determine exactly what a tag . We can skip this additional information in Con3 as follows:

 data Expr' (tag :: ExprTag) where Con1' :: Int -> Expr' tag Con2' :: Expr' tag -> Expr' tag Con3' :: SingExprTag tag -> Expr' tag -> Expr' Tag2 

Now we can check if the tags match. We could write heterogeneous equality for singleton tags like this ...

 heqTagBoo :: SingExprTag a -> SingExprTag b -> Bool heqTagBoo SingTag1 SingTag1 = True heqTagBoo SingTag2 SingTag2 = True heqTagBoo _ _ = False 

... but to do this would be completely useless, since it gives us only a value like Bool , not Bool what that value means and what its truth can give us. Knowing that heqTagBoo ab = True does not tell typechecker anything useful about tags that a and b are witnesses to. The boolean bit is uninformative.

We can write essentially the same test, but in the positive case we prove that the tags are equal.

 data x :=: y where Refl :: x :=: x singExprTagEq :: SingExprTag a -> SingExprTag b -> Maybe (a :=: b) singExprTagEq SingTag1 SingTag1 = Just Refl singExprTagEq SingTag2 SingTag2 = Just Refl singExprTagEq _ _ = Nothing 

Now we are cooking gas! We can implement an Eq instance for Expr' that uses the ExprTag comparison to justify the recursive call for two children of Con3' when the tags were shown as matching.

 instance Eq (Expr' tag) where Con1' i == Con1' j = i == j Con2' s == Con2' t = s == t Con3' as == Con3' bt = case singExprTagEq ab of Just Refl -> s == t Nothing -> False 

The general situation is that advanced types require singleton types associated with them (at least until we get the right Π types), and we need proof for heterogeneous equality tests for these singleton families, so we can compare two singleton and get at the level of knowledge, when they become witnesses to the same level values. Then, as long as your GADTs carry single witnesses for any existential factors, you can evenly test equality, ensuring that positive test results using a singleton test give a bonus of unifying types for other tests.

Answer 2

This is an existential problem, not an elevated view. One solution in this case would be to provide an untyped representation

 data UExpr = UCon1 Int | UCon2 UExpr | UCon3 UExpr deriving (Eq, Ord) 

you just need a function

 toUExpr :: Expr t -> UExpr toUExpr (Con1 x) = UCon1 x (Con2 x) = UCon2 $ toUExpr x (Con3 x) = UCon3 $ toUExpr x 

and easily identify the instances you need

 instance Eq (Expr x) where (==) = (==) `on` toUExpr instance Ord (Expr x) where compare = compare `on` toUExpr 

do better than this will almost certainly require Template Haskell.