[Haskell-cafe] Comparing GADTs for Eq and Ord

[Tom Hawkins]

Hi,

How do I compare a GADT type if a particular constructor returns a
concrete type parameter?

For example:

data Expr :: * -> * where
 Const :: Expr a
 Equal :: Expr a -> Expr a -> Expr Bool      -- If this read Expr a,
the compiler has no problem.

instance Eq (Expr a) where
  Const == Const = True
  (Equal a b) (Equal x y) = a == x && b == y
  _ == _ = False

GHC throws:

    Couldn't match expected type `a1' against inferred type `a2'
      `a1' is a rigid type variable bound by
           the constructor `Equal' at Test.hs:9:3
      `a2' is a rigid type variable bound by
           the constructor `Equal' at Test.hs:9:18
      Expected type: Expr a1
      Inferred type: Expr a2
    In the second argument of `(==)', namely `x'
    In the first argument of `(&&)', namely `a == x'

I believe I understand the reason for the problem; even though Equal
has a type Expr Bool, two Equal expressions could have parameters of
different types.  But I'm not sure how to get around the problem.  Any
suggestions?

Thanks,

Tom