Which is the difference between these polymorphic types?

Question

In System F, what is the difference between the following 3 types:

Reproduced in text here:

∀X.((X → X) → (X → X))
∀X.((X → X) → ∀X.(X → X))
((∀X.X → X) → (∀X.X → X))

Is the second one more general than the first?

Answer 1

Depends on how tight forall quantifier binds. Lets assume that it binds on next terminal expression (variable or ()-block).

The first will become (X0 -> X0) -> (X0 -> X0) where X0 is a fresh type variable.

The second will become (X0 -> X0) -> forall X1. (X1 -> X1) where X0 and X1 are fresh.

The third - (bot -> X) -> (bot -> X) where X is the old binding and bot is the uninhabited forall X. X.