Sadly, this is not a good solution here, as it leads you to universe inconsistencies in the elaborated term: recall we must have ?A : for id ?A to type-check, but the type of forall A : A -> A is which is what the type-checker complains about. 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 : A -> A) A. It then starts by inferring a type for id ?A, which is ?A -> ?A (learning along the way that we must have ?A : Now to type-check id ?A id, it first infers a type for id, which is forall A : A -> A. In the first definition, Coq generates a metavariable, called ?A for the hole. Let me try and give a more precise idea of what happens. In short, in the first definition Coq takes the heuristic solution of letting your hole be unified with forall A : 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.
Mike Shulman got it right: this is a tricky question of how Coq solves unification problems.
However, why will Coq automatically conduct this expansion? Moreover, why Coq won't do this in the first (failed) definition of selfid? This $\eta$-conversion does make the definition of selfid valid. Selfid = id (forall A : A -> A) (fun A : => id A) Moreover, it seems that Coq automatically $\eta$-expanded the second id in the definition of selfid: Set Printing Universes. Unexpectedly, this command does not fail. To have type "?A" (unable to find a well-typed instantiation for "?A": cannotĮnsure that is a subtype of a variant to the failed definition Definition selfid := id (forall A : Type, A -> A) id. The term "id" has type "forall A : A -> A" while it is expected The command has indeed failed with message: 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.
0 kommentar(er)
