The manual gives this subtyping rule for product types here:
If E[Γ] ⊢ T =_{βδιζη} U and E[Γ :: (x : T)] ⊢ T' ≤_{βδιζη} U' then E[Γ] ⊢ ∀ x : T, T' ≤_{βδιζη} ∀ x : U, U'.
What surprises me here is the T =_{βδιζη} U where I would have expected T ≥_{βδιζη} U. I think that in programming languages with static typing and subtyping, the function type A → B is usually contravariant in A, but this definition says that in Coq it is invariant.
I tested this code:
Parameter X : Set.
Check X : Type.
Parameter Y : nat -> Set.
Check Y : nat -> Type.
Parameter Z : Type -> nat.
Check Z : Set -> nat.
The result is very surprising to me: the first to Check commands pass, as expected, and the third also passes, but instead of
Z : Set -> nat
Coq says
(fun x : Set => Z x) : Set -> nat
so it seems like Z was automatically η-expanded to yield the right type.
What’s going on behind the scenes here? What’s the reason product types are invariant in the “index” type? How does Coq decide when to η-expand a term to convert it to a certain type? Where can I read more about this?