type class problem

[oleg at pobox.com]

Dean Herington wrote:
> Can someone explain why the following doesn't work?

> {-# OPTIONS -fglasgow-exts #-}

> class R r where
>   rId :: r -> String

> class (R r) => RT r t where
>   rtId :: r -> t -> String

> data RPair r1 r2 = RPair r1 r2

> instance (R r1, R r2) => R (RPair r1 r2) where
>   rId (RPair r1 r2) = "RPair " ++ rId r1 ++ " " ++ rId r2

> class TPair t t1 t2 where
>   prj :: t -> (t1,t2)
>   inj :: (t1,t2) -> t

> instance (RT r1 t1, RT r2 t2, TPair t t1 t2) => RT (RPair r1 r2) t where
>  rtId (RPair r1 r2) t = "RT (RPair " ++ rtId r1 t1 ++ " " ++ rtId r2 t2 ++")"
>    where (t1,t2) = prj t

You need a functional dependency. For example:

class TPair t t1 t2 | t->t1 t2 where
  prj :: t -> (t1,t2)
  inj :: (t1,t2) -> t

with this definition, the typechecker is satisfied.

Without the dependency, the compiler assumes that there may be several
instances:
	TPair t t1 t2
and
	TPair t t1' t2'

You claimed that RT r1 t1 and RT r2 t2 holds. But you didn't promise
that RT r1 t1' and RT r2 t2' will also hold. In other words,
	(RT r1 t1, RT r2 t2, TPair t t1 t2)
reads as
	(exists t1 t2. RT r1 t1, RT r2 t2, TPair t t1 t2)
rather than
	(forall t1 t2. RT r1 t1, RT r2 t2, TPair t t1 t2)
(which you need to guarantee that the definition of (t1,t2) = prj t
can be typechecked). Notice that forall is _inside_ of parentheses,
on the assumption side (the negative side).