Implicit 'forall' in data declarations

[Sebastian Fischer]

On Oct 21, 2010, at 9:58 PM, Simon Peyton-Jones wrote:

>  A "implicit quantification point" is
>    a) the type in a type signature f :: type, or
>    b) a type of form (context => type), that is not
> 	enclosed by an explicit 'forall'

not quite:

     foo :: forall a . a -> (Ord b => b) -> ()

According to your explanation, there is one implicit quantification  
point: the whole type of `foo`. The type `Ord b => b` is no implicit  
quantification point because it is "enclosed by" an explicit  
'forall' (for a certain definition of "enclosed by"). The new  
explanation implies that the type should be

     foo :: forall b . forall a . a -> (Ord b => b) -> ()

but it is

     foo :: forall a . a -> (forall b . Ord b => b) -> ()

instead.

Apparently, if there is an explicit 'forall' (that does not mention  
`b`) then the implicit 'forall' is inserted at the context. If there  
is no explicit 'forall' then it is inserted at the top level.

My impression is the following:

     An implicit quantification point is
       a) the type in a type signature f :: type or
       b) a type of the form (context => type)
     if it does not start with an explicit 'forall'

Then the only implicit quantification point in the type of `foo` is  
the type `Ord b => b` which matches the behaviour of GHC.

Is this what you meant?

Sebastian