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