Implicit 'forall' in data declarations

[Simon Peyton-Jones]

| > In a data type decl
| >    data Foo = Foo (Eq a => a)
| > the "top of the type" is done separately for each argument.  After
| > all, Foo (Eq a => a) isn't a type.  So you get
| >    data Foo = Foo (forall a. Eq a => a)
| 
| This was a surprise as
| 
|      data Bar = Bar (a -> a)
| 
| is illegal and *not* equivalent to
| 
|      data Bar = Bar (forall a . a -> a)

Darn, that's quite right. In fact what really happens is that the "top of a type" thing is triggered by a "=>", which is why Bar (a->a) is treated differently than Bar (Eq a => a -> a).

The rule I originally gave would indeed treat
	data Bar a = Bar aa
as meaning
	data Bar a = Bar (forall aa. aa)
which is almost certainly not right.

So GHC's behaviour is probably about right, but the description is wrong.

Let's try again:

  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'

  At each implicit quantification point 'ty', working outside in,
  GHC finds all the type variables a,b,c in 'ty' that are not already
  in scope, and transforms 'ty' to (forall a,b,c. ty).

Note that
* the argument of a constructor is not an implicit quantification point
* implicit quantification points may be nested but the inner ones are
	effectively no-ops.  Example
	 f :: Int -> (Eq a => a -> a) -> Int
    There are two quantification points: the whole type, and the (Eq a => ...)
    But when the outer quantification point wraps forall a around it,
    the inner quantification point has no free variables to quantify. So we
    get
        f :: forall a. Int -> (Eq a => a -> a) -> Int

Is that better?  

Simon


| 
| (at least in GHC 6.12.3)
| 
| This lead me into thinking that the type class context causes
| quantification which was apparently wrong.
| 
| In fact, I think according to the documentation of implicit
| quantification it is unclear if the definitions of Foo and Bar
| (without explicit forall) are legal. I expected both to be illegal and
| am surprised that one is legal and the other is not.
| 
| If "the top level of user written types" includes data constructor
| arguments, then probably both should be legal. On the other hand it
| would probably be surprising if one could write
| 
|      data Id type = Id typ
| 
| without getting an error message.
| 
| > Suppose you wrote
| >
| >     bar :: (Eq a => a) -> a
| >
| > Then which of these two do you want?
| >
| > 	bar :: forall a. (forall a. Eq a => a) -> a
| >      bar :: forall a. (Eq a => a) -> a
| >
| > And then what's the rule lexically scoped tyvars?
| 
| I'm afraid I don't understand your question. But I'm fine with the
| current behaviour of implicit quantification in function types.
| 
| Sebastian