Rank-2 polymorphism & type inference

[Tom Pledger]

Adrian Hey writes:
 > On Thu 07 Dec, Simon Peyton-Jones wrote:
 [...]
 > > |   Forall a,b. [a] -> (b -> Bool, [a])  and
 [...]
 > > 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?

Section 7.3.2 of the Hugs user guide demonstrates the difference,
using simpler examples.

Among other things, it says "quantifiers can only appear in the types
of function arguments, not in the results."  So the second one (forall
a.  [a] -> forall b.(b -> Bool, [a])) may be invalid.  Something to do
with letting the locally quantified b escape, perhaps?  I'm not sure.

I'm also not sure whether Hugs will allow any function with the type
(forall a. [a] -> (forall b. b -> Bool, [a])) to be applied, because
"Any call to such a function must have at least as many arguments as
are needed to include the rightmost argument with a quantified type."

Regards,
Tom