Solved: Typing problems with polymorphic recursion and typeclasses

[Simon Peyton-Jones]

| First, let us distill the problem to the following few lines:
|=20
| > f:: (Show fa) =3D> fb -> fa
| > f =3D undefined
| >
| > g:: (Show ga) =3D> ga -> gb
| > g =3D undefined
| >
| > -- h:: (Show fa) =3D> t -> fa
| > h b =3D f (g (h b))
|=20
| This code loads and checks. If we ask the compiler for the type of h,
| we get the type of h that was commented out in the code above. If we
| remove the comment and reload the code, we get an error:
|=20
|     Ambiguous type variable(s) `fa' in the constraint `Show fa'
|     arising from use of `h' at /tmp/p.lhs:12
|     In the first argument of `g', namely `(h b)'
|     In the first argument of `f', namely `(g (h b))'
|=20
| This behavior seems rather puzzling: the compiler refuses to accept
| its own type. The problem is that the compiler is slightly lying to
| us. When we ask for the type
|     *Main> :type h
|     forall fa t. (Show fa) =3D> t -> fa
|=20
| the real type of h is
|     forall t. t -> (function-of-t)

I don't agree with that.  h really is polymorphic.  Its result is the
result of f, which is any type at all so long as it is Showable.

| Perhaps even more stunning is that we can test our hypothesis. We can
| explicitly specify the functional dependence between types. We will
| use lexically-scoped type variables, described in the eponymous paper
| by Simon Peyton-Jones and Mark Shields. The following works in GHC
| 5.04.1, given -fglasgow-exts flag.
|=20
| > h1:: (Show t2) =3D> t1 -> t2
| > h1 b :: g1a
| >  =3D (f (g ((h1 b)::g1a)))

This is nothing to do with dependent types.  Your type signature simply
constrains the result of (h1 b) to have the type g1a, and which is
specified by the LHS to be the type of the result to the whole call.  So
now the recursive call has=20
	an argument b which is the same as the argument to the
definition of h1
	and a result whose type is the same as the type of the result of
h1
so the recursive call has the same type as the main function; so the
situation is identical to the case where there is no type signature, and
the recursive call is at the same type as the function being defined.


Consider the well known
	show (read s)
This is ambiguous unless we add a signature to make the result of 'read'
less polymorphic:
	show ((read s) :: Int)

But giving an explicit type signature for h makes it *more* polymorphic,
and that in turn leads to ambiguity in this particular case.

Simon