Unable to understand F-omega term

Question

I am reading a paper on F_ω, and cannot understand the reasoning behind this statement:

The type term of type (∀γ:*. F γ → β) shows that F is a constant function that always returns β.

I guess 'F γ → β' is the type term, i.e., an arrow type. This arrow type is the type of a function that takes an argument of type computed by the type application 'F γ' and returns a value of type β.

If this is the case, why should F be a constant (type) function that always returns β? Can't it be any arbitrary type function, one that returns, say, α, and still satisfy the typechecker?

Thanks for your time.

Answer 1

Answering my own question.

I think the reason is parametricity.

If 'F γ' could return any type, for example α, the function (whose type is conveyed by the ∀ type) would have a type of α → β.

Parametricity dictates that all instances of this polymorphic function should have the same behaviour, which is only possible if it is the identity function, i.e., of type β → β, therefore implying that 'F γ' always returns β.