[Haskell-cafe] GATD and pattern matching

[Daniel Fischer]

On Wednesday 09 June 2010 20:37:22, Dupont Corentin wrote:
> Hello,
>
> I am making a little GATD:
> > {-# LANGUAGE GADTs#-}
> >
> > data Obs a where
> >     Equal :: Obs a -> Obs a -> Obs Bool
> >     Plus :: (Num a) => Obs a -> Obs a -> Obs a
>
> (etc..)
>
> > instance Show t => Show (Obs t) where
> >     show (Equal a b) = (show a) ++ " Equal " ++ (show b)
> >     show (Plus a b) = (show a) ++ " Plus " ++ (show b)
> >
> > instance Eq t => Eq (Obs t) where
> >     a `Equal` b == c `Equal` d = (a == c) && (b == d)
> >     a `Plus` b == c `Plus` d = (a == c) && (b == d)
>
> The Equal constructor causes me problems, while the Plus is fine:
>
> test3.lhs:8:26:
>     Could not deduce (Show a) from the context (t ~ Bool)
>       arising from a use of `show' at test3.lhs:8:26-31
>     Possible fix:
>       add (Show a) to the context of the constructor `Equal'
>     In the first argument of `(++)', namely `(show a)'
>     In the expression: (show a) ++ " Equal " ++ (show b)
>     In the definition of `show':
>         show (Equal a b) = (show a) ++ " Equal " ++ (show b)
>
>
> I guess this is because GADT refines type with pattern matching.
> Since Equal return type is Obs Bool and not Obs a, it cannot bind the
> type variable a to belong to Show.

Right. You can have

(+ 3) `Equal` sin :: Obs Bool

, but how would you show it?

You could add a (Show a) constraint to Equal.

>
> I don't see how to precise the type in the pattern match.
>
> I have another problem:
>
> test3.lhs:12:41:
>     Couldn't match expected type `a' against inferred type `a1'
>       `a' is a rigid type variable bound by
>           the constructor `Equal' at test3.lhs:12:8
>       `a1' is a rigid type variable bound by
>            the constructor `Equal' at test3.lhs:12:23
>       Expected type: Obs a
>       Inferred type: Obs a1
>     In the second argument of `(==)', namely `c'
>     In the first argument of `(&&)', namely `(a == c)'

((+ 3) `Equal` sin) == (True `Equal` False)

Doesn't work.

And you can't make it work, because in

(a `Equal` b) == (c `Equal` d)

, a and b have the same type t1, and c and d have the same type t2 but the 
two types t1 and t2 are generally different, so calling (==) on a and c has 
no chance to type-check. With Equal forgetting the type parameter of its 
arguments, I don't think it's possible.

>
>
> Cheers,
> Corentin