Solved: Typing problems with polymorphic recursion and typeclasses

[oleg@pobox.com]

I think I can explain why Haskell compilers behave as they do with
regards to Levent Erkok's problem, and how to fix it. It seems the
compilers are more powerful than we imagine, but are compelled to
conceal their power and to lie to us.

First, let us distill the problem to the following few lines:

> f:: (Show fa) => fb -> fa
> f = undefined
>
> g:: (Show ga) => ga -> gb
> g = undefined
>
> -- h:: (Show fa) => t -> fa
> h b = f (g (h b))

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:

    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))'

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) => t -> fa

the real type of h is 
    forall t. t -> (function-of-t)

The real type of h is not totally polymorphic : it is dependent!
It goes without saying that such types cannot be expressed in
Haskell. It is stunning that the compiler managed to infer such
a dependent type, albeit it has no way to properly print it. The
compiler could have used the following notation:

    forall fa t | t -> fa. (Show fa) => t -> fa

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.

> h1:: (Show t2) => t1 -> t2
> h1 b :: g1a
>  = (f (g ((h1 b)::g1a)))

Original example by Levent Erkok's also works.