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-extension... 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@haskell.org [mailto:glasgow-haskell-users- | bounces@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@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users