Type error when ascribing a valid forall type to a let-bound variable

Question

Is this a bug in the type checker?

Prelude> let (x :: forall a. a -> a) = id in x 3

<interactive>:0:31:
    Couldn't match expected type `forall a. a -> a'
                with actual type `a0 -> a0'
    In the expression: id
    In a pattern binding: (x :: forall a. a -> a) = id

The fact that the above fails to type check, but this contortion succeeds:

Prelude> let (x :: (forall a. a -> a) -> Int) = (\f -> f 3) in x id
3

leads me to think that "weak prenex conversion" (see page 23 of this paper) might be related somehow. Embedding a forall in a contravariant position where it can't be "floated out" seems to keep it safe from this weird error.

Answer 1

What I think is happening here is this: In standard Damas–Milner type inference, let bindings are the only place where generalization of a type happens. The type signature that your failing example uses is a pattern type signature which "constrains the type of the pattern in the obvious way". Now, in this example, it is not "obvious" whether this constraining should happen before or after generalization, but your failing example demonstrates, I think, that it gets applied before generalization.

Put more concretely: in a let binding let x = id in ..., what happens is that id's type forall a. a->a gets instantiated into a monotype, say a0 -> a0, which is then assigned as x's type and is then generalized as forall a0. a0 -> a0. If, as I think, the pattern type signature is checked before generalization, it's essentially asking the compiler to verify that the monotype a0 -> a0 is more general than the polytype forall a. a -> a, which it isn't.

If we move the type signature to the binding level, let x :: forall a. a-> a; x = id in ... the signature is checked after generalization (since this is expressedly allowed in order to enable polymorphic recursion), and no type error ensues.

Whether it is a bug or not is, I think, a matter of opinion. There doesn't seem to be an actual spec that would tell us what the right behaviour here is; there's only our expectations. I would suggest discussing the matter with the GHC people.

Answer 2

Not a real answer, but too long for a comment:
It may well be a bug. Playing around a bit with the expression, unsurprisingly

let x :: forall a. a -> a; x = id in x 3

works if writing explicit foralls is enabled. It's a bog-standard rank 1 type, though. Some other variation:

$ ghci-6.12.3 -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3
3

Okay, that works, I don't know why the lambda behaves differently, but it does. However:

$ ghci -ignore-dot-ghci -XRankNTypes -XScopedTypeVariables
Prelude> let (x :: forall a. a -> a) = \y -> id y in x 3

<interactive>:0:31:
    Couldn't match expected type `t0 -> t1'
                with actual type `forall a. a -> a'
    The lambda expression `\ y -> id y' has one argument,
    but its type `forall a. a -> a' has none
    In the expression: \ y -> id y
    In a pattern binding: (x :: forall a. a -> a) = \ y -> id y

(7.2.2; 7.0.4 gives the same error). That is surprising.