Hi Simon,

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.

Sebastian
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Reply via email to