Rank-2 polymorphism & type inference

[Simon Peyton-Jones]

| <  p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
| <  q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
| <
| System CT accepts both. No type signature is required.
| 
| The types inferred for p and q are, resp.:
| 
|   Forall a,b. [a] -> (b -> Bool, [a])  and
|   Forall a,b. [a] -> ([a], b -> Bool) 

That's not the type we wanted, though.  We wanted

    Forall a. [a] -> (Forall b. b->Bool, [a])

and similarly the other one.  That's the reason for the type signature
on f, which is short for (forall c. c->Bool).
If you leave out the type signature then all Haskell compilers
are happy.

(Of course, this isn't a very useful example, but it's the smallest one
that shows up the problem.)

Simon