> I expected the type of 'x' to be universally quantified, and thus can be
> unified with 'forall a. a' with no problem

As I get it. 'x' is not universally quantified. f is. [1]
x would be universally quantified if the type of f was :

f :: (forall a. a) -> (forall a. a)

[1] Yet here I'm not sure this sentence is correct. Some heads-up from a type expert would be good.


Would you try:

f :: a -> a
f x = undefined :: a

And tell me if it works? IMO it doesn't.

2012/1/4 Yucheng Zhang <yczhang89@gmail.com>
On Wed, Jan 4, 2012 at 7:58 PM, Yves Parès <limestrael@gmail.com> wrote:
> f :: forall a. a -> a
> f x = x :: forall a. a
>
> Which is obviously wrong: when you have entered f, x has been instatiated to
> a specific type 'a', and then you want it to x to be of any type? That
> doesn't make sense.

I did not expect the type variables to be scoped.

I expected the type of 'x' to be universally quantified, and thus can be unified
with 'forall a. a' with no problem.