first-class polymorphism beats rank-2 polymorphism

[Ralf.Laemmel@cwi.nl]

Simon Peyton-Jones wrote:

> In fact GHC does "forall-lifting" on type signatures to bring the
> foralls to the front.  But there's a bug in 5.02's forall-lifting...
> ...
> Perhaps you can try the 5.03 snapshot release?

Certain things work there.
In fact, it is fascinating.

But now I did a new experiment ... 
It seems that forall-lifting does not work 
as expected for type synonyms in 5.03.

Here is an example
from my upcoming ICFP submission :-)

Here is an innocent type synonym for generic 
functions with three parameters of kind * -> *:

type Generic i o m = forall x. i x -> m (o x)

This is a good candidate for all the parameters:

type Id x = x

Now I tried to define sequential composition.
In fact, the following type deals with a very
restricted case for simplicity:

sequ :: forall t.
        (Generic t t Id)
     -> (Generic t t Id)   
     -> (Generic t t Id)   
sequ f g = undefined

Looking at the type of sequ,
the foralls for t end up at the top.
Hence, I have no chance to define sequential
composition.

Main> :t sequ
forall t x1 x11 x.
(t x1 -> Id (t x1)) -> (t x11 -> Id (t x11)) -> t x -> Id (t x)
Main>

Please let me know if this is a bug.
Please don't fix it too soon :-) because otherwise
I had to rewrite some material which is now based
on first-class polymorphism and datatypes for i, o, and m.
Such code will probably look better in proper rank-2
style with type synonyms for type constructor parameters.

I just realized that type synonyms in GHC seem to be valid
arguments even when not completely instantiated? This is
wonderful. It is not supported in hugs. How difficult is
it to cope with this? Does it make a real difference for the
type system?

Ralf