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

[Tom Hawkins]

On Mon, Sep 15, 2008 at 3:11 PM, apfelmus <apfelmus at quantentunnel.de> wrote:
>
> 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
>        (==) = (===)

OK.  But let's modify Expr so that Const carries values of different types:

data Expr :: * -> * where
  Const :: a -> Term a
  Equal :: Term a -> Term a -> Term Bool

How would you then define:

Const a === Const b  = ...


-Tom