Implicit 'forall' in data declarations
fischer at nii.ac.jp
Thu Oct 21 10:14:59 EDT 2010
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'
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) -> ()
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?
More information about the Glasgow-haskell-users