Implicit 'forall' in data declarations
fischer at nii.ac.jp
Thu Oct 21 04:57:28 EDT 2010
thank you for your explanations. Now I understand why type variables
are quantified at the outermost position in function types.
My confusion was caused by implicit quantifications in data type
declarations. These are not (explicitly) mentioned in the
documentation that you have linked and they only occur when a type
class context is given.
> 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)
(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.
More information about the Glasgow-haskell-users