How to derive Eq for a GADT with a non-* kinded phantom type parameter

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 a type error

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 can see why this doesn't work, but is there some solution that doesn't require me to manually write the Eq (and Ord) instances?

The non-* kind doesn't make a difference here. You get the same error with plain old phantom types. — hammar
The reason is the existential in Con3, it can't recursively call eq because of the existential type. — Philip JF
If you wrote it by hand, what would you write for (Con3 x) == (Con3 y) = ? Note that x :: Expr tagX and y :: Expr tagY don't even have the same type, so even writing it by hand you can't say something like x == y because it won't typecheck. — Lambdageek
@Lambdageek I can write an upcast function (or use unsafeCoerce) to convert an Expr t to an Expr Tag2, and then compare for equality. — Alex R

pigworker pigworker · Accepted Answer · 2012-11-17T13:30:20

As others have identified, the key to the problem is the existentially quantified tag in the type of Con3. When you're trying to define

Con3 s == Con3 t = ???

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

But perhaps you don't care? You can perfectly well define the heterogeneous equality test which is happy to compare Exprs structurally, 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 s t
    heq (Con3 s) (Con3 t) = heq s t

If you do care, then you might be well advised to equip Con3 with a run-time witness to the existentially quantified tag. The standard way to do this is with the singleton construction.

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

Case analysis on a value in SingExprTag tag will exactly determine what tag is. We can slip this extra piece of information into 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 whether the tags match. We could write a heterogeneous equality for tag singletons like this...

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

...but to do so would be perfectly useless, as it only gives us a value of type Bool, with no idea what that value means nor to what its truth might entitle us. Knowing that heqTagBoo a b = True does not tell the typechecker anything useful about the tags which a and b witness. A Boolean is a bit uninformative.

We can write essentially the same test, but delivering in the positive case some evidence 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're cooking with gas! We can implement an instance of Eq for Expr' which uses ExprTag comparison to justify a recursive call on two Con3' children when the tags have been shown to match.

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

The general situation is that promoted types need their associated singleton types (at least until we get proper ∏-types), and we need evidence-producing heterogeneous equality tests for those singleton families, so that we can compare two singletons and gain type-level knowledge when they witness the same type-level values. Then as long as your GADTs carry singleton witnesses for any existentials, you can test equality homogeneously, ensuring that positive results from singleton tests give the bonus of unifying types for the other tests.

How to derive Eq for a GADT with a non-* kinded phantom type parameter

2 Answers