[Haskell-cafe] Re: Comparing GADTs for Eq and Ord

[apfelmus]

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