# Unexpected eta expansion in constant definition

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?

• Intriguing. I would guess it has something to do with the explicit Type in the second selfid which gives it another universe parameter. Maybe the eta-expansion happens during checking the second id against the supplied type forall A : Type, A -> A, which doesn't happen in the first case since the known type of id can be synthesized and equated to the implicit argument? Commented Aug 7, 2022 at 19:46

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.