Subtyping variance of dependent product types

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?

What’s the reason product types are invariant in the “index” type?

We generally call it the domain not the index.
It makes model construction easier, for instance in the set model.

How does Coq decide when to η-expand a term to convert it to a certain type?

The coercion system when trying to coerce f : A-> B to A' -> B' tries to produce fun x : A' => coe_B_to_B' (f (coe_A'_to_A x)).
in your example the sub coercions are the identity thanks to cumulativity


see also Activating contravariant subtyping of dependent function types by herbelin · Pull Request #13270 · coq/coq · GitHub

1 Like

From https://inria.hal.science/hal-04077552v2/document

1This restriction comes from the fact that it is difficult to model contravariant cumulativity in set-theoretic models Timany and Sozeau 2018. Whether cumulativity could be contravariant on the left-hand side of an arrow or not is still the subject of ongoing theoretical investigations.

1 Like