Defining Eq instance for Haskell GADTs

Question

I have a GADT that's a lot like this:

data In a where
  M :: MVar a -> In a
  T :: TVar a -> In a
  F :: (a -> b) -> In a -> In b

It wraps various input primitives, but the last constructor also allows for a Functor instance:

instance Functor In where
  fmap f (F g v) = F (f . g) v
  fmap f x = F f x

The point of this type, BTW, is to support:

read :: In a -> IO a
read (M v) = takeMVar v
read (T v) = atomically (readTVar v)
read (F f v) = f <$> read v

What I want to be able to do is define the obvious Eq instance on this type, something like:

instance Eq (In a) where
  (M x) == (M y) = x == y
  (T x) == (T y) = x == y
  (F _ x) == (F _ y) = x == y
  _ == _ = False

The problem is the third case, which fails because x and y don't necessarily have the same type at that point. I understand that. In my own code I can make a long work-around, but it feels like there should be a way to define Eq directly. In my mind the solution is something like "keep drilling through the F constructors until you hit M or T, then if they're the same constructor (i.e. both M or both T) and same type, do the equality comparison", but I'm not sure how I could write that.

Answer 1

I'm highly suspicious about your equality since it only really tests half of the F, but if that's what you really want, here's how you can do it. Note that the cast serves as a test for type equality, since you can only compare the two Fs if the types of the existentially quantified a inside are the same.

data In a where
  M :: MVar a -> In a
  T :: TVar a -> In a
  F :: (Typeable a) => (a -> b) -> In a -> In b
  deriving (Typeable)


instance Eq (In a) where
  (M x) == (M y) = x == y
  (T x) == (T y) = x == y
  (F _ x) == (F _ y) = Just x == cast y
  _ == _ = False

Or maybe this isn't what you want either? Reading your motivation again it seems like you want a function where an In Int can be equal to an In Double.

How would you like these two to compare F floor r and F id r (if r is M x :: In Double)?

Answer 2

At one point, you need to test whether two things of different type are equal. There are two ways to do that:

1. The Typeable class.
2. A GADT data Equal a b where Eq :: Equal a a.

Since MVar and TVar don't support 2, you will have to use the Typeable class. In other words, you will have to augment your data type with Typeable constraints.

Fortunately, you have some freedom as to where to put the constraints. For instance, you can put them as follows:

data In a where
    M :: Typeable a => MVar a -> In a
    T :: Typeable a => TVar a -> In a
    F :: (a -> b) -> In a -> In b

equal :: In a -> In b -> Bool
equal (M x) (M y)     = Just x == cast y
equal (T x) (T y)     = Just x == cast y
equal (F _ x) (F _ y) = x `equal` y
equal _ _             = False

instance Eq (In a) where
    (==) = equal

This way, you get to keep the Functor instance.