# Rank-2 polymorphism & type inference

**Adrian Hey
**
ahey@iee.org

*Fri, 8 Dec 2000 00:45:21 +0000 (GMT)*

On Thu 07 Dec, Simon Peyton-Jones wrote:
>* | < 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])
*>*
*
I thought..
Forall a,b. [a] -> ( b -> Bool, [a])
Forall a. [a] -> Forall b.(b -> Bool, [a])
Forall a. [a] -> (Forall b. b -> Bool, [a])
All mean they same thing, or do they?
Regards
--
Adrian Hey