Unexpected eta expansion in constant definition

Question

Start from this example in section 2.1.14: Polymorphic Universes in Coq's reference maunual (slightly modified):

Definition id (A : Type) (a : A) := a.

Set Printing Universes.
Fail Definition selfid := id _ id.
  (*
    The command has indeed failed with message:
    The term "id" has type "forall A : Type@{id.u0}, A -> A" while it is expected
    to have type "?A" (unable to find a well-typed instantiation for "?A": cannot 
    ensure that "Type@{id.u0+1}" is a subtype of "Type@{id.u0}").
  *)

Consider a variant to the failed definition

Definition selfid := id (forall A : Type, A -> A) id.

Unexpectedly, this command does not fail. Moreover, it seems that Coq automatically $\eta$-expanded the second id in the definition of selfid:

Set Printing Universes.
Print selfid.
  (*
    selfid = id (forall A : Type@{selfid.u0}, A -> A) (fun A : Type@{selfid.u0} => id A)
      : forall A : Type@{selfid.u0}, A -> A
    (* {selfid.u0} |= selfid.u0 < id.u0 *)
  *)

This $\eta$-conversion does make the definition of selfid valid. However, why will Coq automatically conduct this expansion? Moreover, why Coq won't do this in the first (failed) definition of selfid?

Answer 1

Mike Shulman got it right: this is a tricky question of how Coq solves unification problems. In short, in the first definition Coq takes the heuristic solution of letting your hole be unified with forall A : Type@{id.u0}, A -> A, which causes universe issues down the road, while in the second case the unification problem is solved by triggering the η-expansion that puzzles you, which is needed because cumulativity is equivariant rather than contravariant on the domains of product types. Let me try and give a more precise idea of what happens.

---

In the first definition, Coq generates a metavariable, called ?A for the hole. It then starts by inferring a type for id ?A, which is ?A -> ?A (learning along the way that we must have ?A : Type@{id.u0}. Now to type-check id ?A id, it first infers a type for id, which is forall A : Type@{id.u0}, A -> A. Finally, this inferred type is compared with the domain of the type of id ?A, namely ?A, for cumulativity, ie the problem is

(forall A : Type@{id.u0}, A -> A) <= ?A

The unification heuristics in such a setting give the "easy" answer to let ?A be forall A : Type@{id.u0}, A -> A. Sadly, this is not a good solution here, as it leads you to universe inconsistencies in the elaborated term: recall we must have ?A : Type@{id.u0} for id ?A to type-check, but the type of forall A : Type@{id.u0}, A -> A is Type@{id.u0+1}, which is what the type-checker complains about.

---

In the second definition, on the contrary, since you write Type a new, fresh level selfid.u0 is first generated. As before, the type-checking of id (forall A : Type@{selfid.u0}, A -> A) happens first, returning the type (forall A : Type@{selfid.u0}, A -> A) -> (forall A : Type@{selfid.u0}, A -> A) (and learning along the way the constraint selfid.u0 < id.u0). Next, it infers a type for id, which is still forall A : Type@{id.u0}, A -> A. Finally, we get the cumulativity problem between the domain of id (forall A : Type@{selfid.u0}, A -> A) and this inferred type, which is now

(forall A : Type@{id.u0}, A -> A) <= (forall A : Type@{selfid.u0}, A -> A)

In Coq’s metatheory, cumulativity is equivariant on product domains, meaning here that the previous cumulativity can only hold if Type@{selfid.u0} and Type@{id.u0} are convertible, which in turn is only true if selfid.u0 = id.u0. But because of the constraint discovered earlier, this cannot hold, and so the problem does not have a solution. Note that if instead cumulativity were contravariant on product domains, since we know that selfid.u0 < id.u0, the cumulativity would hold. This contravariance, while quite common in subtyping for programming languages is not present in Coq because it is not easy to handle in set-theoretic models, which are the standard justification for cumulativity. Even though it is absent, it can still be mimicked by η-expanding functions: while f : A' -> B does have type A -> B only if A and A' are convertible, we still have that fun x : A => f x : A -> B whenever A <= A'. This is exactly what Coq does upon noticing that a cumulativity problem between products does not hold: it η-expands the function and tries again, which, in your case, succeeds.