[Haskell-cafe] Comparing GADTs for Eq and Ord

Jason Dagit dagit at codersbase.com
Mon Sep 15 14:42:35 EDT 2008


On Mon, Sep 15, 2008 at 11:01 AM, Tom Hawkins <tomahawkins at gmail.com> wrote:
> 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


More information about the Haskell-Cafe mailing list