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