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?

Noway

The non-* kind doesn't make a difference here. You get the same error with plain old phantom types. – Greenburg

I wasn't sure, and I think that the non-* kind rules out some possible solutions, like deriving Data or Generic and then using those. – Noway

The reason is the existential in Con3, it can't recursively call eq because of the existential type. – Cosmonaut

Since all your constructors seem to be functions, I don't see how you could define an Eq instance even if you did it manually. – Hankow

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. – Whitefaced

@PaulJohnson, they're not functions. He's using GADTs – Whitefaced

@Whitefaced I can write an upcast function (or use unsafeCoerce) to convert an Expr t to an Expr Tag2, and then compare for equality. – Noway

Answer 1

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.

Tar

how does that compare to Con3 :: (Typeable tag) => Expr tag -> Expr Tag2? you'd be able to define the equivalent of singExprTagEq with cast right? you also get a "run-time witness" to the type too. I'm new to this type level stuff, so I hope that made sense. – Micrococcus

Indeed, Typeable gives you a source of singleton witnesses that you can test yielding useful equality evidence with eqT. – Tar

Answer 2

This is an issue with existentials, not with the lifted kind. One solution in this case would be to provide an untyped representation

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

then 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 it is easy to define the instances you want

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

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

to do better than this is almost certainly going to require Template Haskell.

Cosmonaut

It would be so nice if I could just derive Eq for Expr Tag2, because then I wouldn't need to write conversion function or to duplicate the ADT... Alas. – Noway

I don't know enough about GADTs to say whether or not it's a good idea, but does deriving instance Eq (Expr Tag2) not work? – Micrococcus