first-class polymorphism beats rank-2 polymorphism

Simon Peyton-Jones simonpj@microsoft.com
Fri, 8 Mar 2002 04:40:41 -0800


| So I would claim that these two types are the same:
|=20
|   forall x. Class x =3D> (forall y. Class y =3D> y -> y) -> x -> x
|   (forall y. Class y =3D> y -> y) -> (forall x. Class x =3D> x -> x)
|=20
| ...so you should be able to do this:
|=20
|   combinator :: (forall y. Class y =3D> y -> y) -> (forall x.=20
| Class x =3D> x  -> x)
|   combinator f x =3D combinator' f x
|=20
| but for some reason GHC 5.02.2 complains. I think this is a bug.=20

Indeed the two types are the same.  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... it doesn't bring the constraints to the
front too.

I fixed this in 5.03 a while ago, but didn't back-propagate the fix to=20
5.02.  And indeed, 5.03 is happy with the pure rank-2 program.

class Class x where
 combinator' :: (forall y. Class y =3D> y -> y) -> x -> x

combinator :: (forall y. Class y =3D> y -> y)
           -> (forall x. Class x =3D> x -> x)
combinator f =3D combinator' f


It's quite a bit of extra work propagating fixes into the 5.02 branch,
so I probably won't do so for this one, since only a small minority
of people will trip over it.   Perhaps you can try the 5.03 snapshot
release?

Simon