apfelmus apfelmus at quantentunnel.de
Tue Sep 16 03:55:40 EDT 2008

```Tom Hawkins wrote:
> apfelmus 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  = ...
>

Well,

Const :: a -> Term a

is too general anyway, you do need some information on  a  to be able to compare
different  Const  terms. An  Eq  constraint on  a  is the minimum:

Const :: Eq a => a -> Term a

But that's not enough for  (===)  of course, additional information as suggested
by others is needed.

Regards,
apfelmus

```