On Mon, Sep 15, 2008 at 11:01 AM, 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?
The reason this doesn't work is rather hard to see. You correctly noticed that changing the above definition to "Expr a" fixes the problem. The reason this fixes the problem is because: 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. 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. But, your proposed fix: Equal :: Expr a -> Expr a -> Expr a Means that the 'a' is no longer existential and so everything works the way you expect. Except that your equal constructor really should return Expr Bool. I'm not sure what the best way to fix this is. It will be interesting to see what others suggest. Jason