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