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