5
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ 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? $\endgroup$ Aug 7 at 19:46

1 Answer 1

4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.