Jason Dagit wrote:
Tom Hawkins wrote:
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?
Equal :: Expr a -> Expr a -> Expr Bool
Makes the type parameter 'a' an existential type. You can think of it like this: data Expr a = Equal (forall a. Expr a Expr a)
I think that forall is in the right place.
You mean data ExprBool = forall a. Equal (Expr a) (Expr a)
This means that when you use the (Equal a b) pattern the 'a' has to be instantiated to some distinct rigid type, and similarly (Equal x y) instantiates 'a' again to some distinct rigid type. This is where your a1 and a2 in the error message come from.
So, in other words, in order to test whether terms constructed with Equal are equal, you have to compare two terms of different type for equality. Well, nothing easier than that: (===) :: Expr a -> Expr b -> Bool Const === Const = True (Equal a b) === (Equal a' b') = a === a' && b === b' _ === _ = False instance Eq (Expr a) where (==) = (===) Chances are that the equality test with different types is more useful in the rest of your program as well. Regards, apfelmus