Rank-2 polymorphism & type inference

[Adrian Hey]

On Fri 08 Dec, Tom Pledger wrote:
> Adrian Hey writes:
>  > 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.

Thanks, I've had a look at the Hugs user guide you mentioned. I'm not
convinced that it does explain the difference, but it certainly lists
a lot of constraints. I don't really understand why nested quantifiers
shouldn't be allowed, for example, or why quantifiers can't appear
in function results. (or why partial application in the example (twice f)
is illegal). Presumably there's some reason why the type of..
 (twice (\x ->[x])) can't be infered as  Forall a. a->[[a]]

To me, pushing all quantifiers 'down the tree' (so to speak) as far as
they can go without leaving a type variable occurence unquantified seems
natural, but maybe my intuition is at fault here.

Making the implicit quantification of a explicit,
 twice :: Forall a. (Forall b. b -> f b) -> a -> f (f a)
Push Forall a 'down the tree'..
 twice ::  (Forall b. b -> f b) -> Forall a. a -> f (f a)
seems to work (informally at least).

Regards
-- 
Adrian Hey