# Rank-2 polymorphism & type inference

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

*Thu, 7 Dec 2000 09:23:37 -0800*

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