Implicit 'forall' in data declarations

[Simon Peyton-Jones]

The current story is this: 

   GHC adds an implicit "forall" at the top of every type
   that foralls all the type variables mentioned in the type
   that are not already in scope (if lexically scoped tyvars is on)

This is stated pretty clearly here
http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/other-type-extensions.html#implicit-quant

Thus, when you write

     bar :: Eq b => (Eq a => a) -> b

you get

     bar :: forall a b. Eq b => (Eq a => a) -> b

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)


So that's what happens.  You could imagine a different design, in which an implicit 'forall' is added at each "=>", forall'ing any not-otherwise-bound type variables.  So if you said

     bar :: Eq b => (Eq a => a) -> b

you'd get

     bar :: forall b. Eq b => (forall a. Eq a => a) -> b

But it's not obvious that's what you want.  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 hope that explains it.  The documentation mentioned above has examples.  I'll gladly improve it if you can suggest concrete wording.

Simon

| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Sebastian Fischer
| Sent: 16 October 2010 02:10
| To: GHC Users
| Subject: Implicit 'forall' in data declarations
| 
| Hello,
| 
| GHC 6.12.3 allows to omit the explicit quantification of
| higher-rank type variables using 'forall' in data types if they
| appear in a type class context
| 
|      {-# LANGUAGE RankNTypes #-}
|      data Foo = Foo (Eq a => a)
| 
| Is this implicit introduction of 'forall' intended? If it is, why
| does it not work in function types? The following is not accepted
| by my GHC:
| 
|      bar :: Eq b => (Eq a => a) -> b
|      bar x = x
| 
| The error message is
| 
|      All of the type variables in the constraint `Eq a'
|      are already in scope (at least one must be universally quantified
| here)
|          (Use -XFlexibleContexts to lift this restriction)
| 
| Using `FlexibleContexts` the signature of `bar` seems to be
| interpreted as
| 
|      bar :: (Eq b, Eq a) => a -> b
| 
| because then the error becomes
| 
|      Couldn't match expected type `b' against inferred type `a'
| 
| So unlike in data-type declarations, a 'forall' in a function type
| must be written explicitly even if the quantified variable appears in
| a local type class constraint.
| 
|      bar :: Eq b => (forall a . Eq a => a) -> b
|      bar x = x
| 
| I have not yet installed GHC 7. Is this inconsistency between data and
| function declarations intended or has it been changed in the new type
| checker?
| 
| Sebastian
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users