# first-class polymorphism beats rank-2 polymorphism

**Simon Peyton-Jones
**
simonpj@microsoft.com

*Tue, 12 Mar 2002 01:55:55 -0800*

|* 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