first-class polymorphism beats rank-2 polymorphism

[Simon Peyton-Jones]

| type Generic i o =3D forall x. i x -> o x
|=20
| type Id x =3D x
|=20
| comb ::=20
|         (Generic Id Id)
|      -> (Generic Id Id)  =20
|      -> (Generic Id Id)  =20
| comb =3D undefined

| So now let's ask for the type of comb in ghc.
| It turns out to be the rank-1 (!!!) type I captured as=20
| explicit type annotation for comb'. I would have expected a=20
| rank-2 type because the forall is scoped by the type synonym=20
| Generic. So why should I like to see the forall going to the=20
| top? I still would say that THIS IS A BUG. Here is why the=20

Yes, indeed this is a bug.  Thank you for finding it.  It turned out
that in liberalising GHC's treatment of type synonyms (which you
remark is a good thing) I had failed to cover a case.   Fortunately,
an ASSERT caught the bug in my build, and the fix is easy.

| yacomb1 :: (forall x. x -> x)=20
|	-> (forall x. x -> x)=20
|	-> (forall x. x -> x)=20
| yacomb1 =3D  (.)
|
| yacomb2 :: forall x y z. (x -> x) -> (y -> y) -> (z -> z)
| yacomb2 =3D undefined
|
| Now let's try to define yacomb2 in terms of yacomb1, that is:
|
| yacomb2 =3D yacomb1
|
| This works. Let us not wonder why.

We should wonder why.  It's plain wrong.  yacomb1's type signature
is more restrictive than that of yacomb2.   This is a bug in the 5.03
snapshot, which fortunately I fixed a week or two ago.  The compiler
in the respository rejects the definition.


Bottom line: you found two bugs, for which much thanks.  But I stand
by forall-lifting!   (But note that the foralls are lifted only from
*after*
the arrow, not before.   (forall a.a->a) -> Int   is not the same as
(forall a.  (a->a) -> Int).)

Simon