Implicit 'forall' in data declarations
Simon PeytonJones
simonpj at microsoft.com
Wed Oct 20 10:01:26 EDT 2010
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/othertypeextensions.html#implicitquant
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 nototherwisebound 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: glasgowhaskellusersbounces at haskell.org [mailto:glasgowhaskellusers
 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
 higherrank 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 datatype 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
 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list