Rank-2 polymorphism & type inference
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
(Of course, this isn't a very useful example, but it's the smallest one
that shows up the problem.)