What does "Error: Universe inconsistency" mean in Coq?

Question

I am working through Software Foundations and am currently doing the exercises on Church numerals. Here is the type signature of a natural number:

Definition nat := forall X : Type, (X -> X) -> X -> X.

I have defined a function succ of type nat -> nat. I would now like to define an addition function like so:

Definition plus (n m : nat) : nat := n nat succ m.

However, I get the following error message:

Error: Universe inconsistency.

What does this error message actually mean?

Sheetfed

You can pass the -type-in-type flag to Coq to disable all universe consistency checks. Using this flag is dangerous because it enables Girard's paradox (explained here). – Donohue

Note that -type-in-type only works for Coq 8.5 beta (not for the currently stable 8.4 version) – Parenteau

Answer 1

In Coq, everything has a type. Type is no exception: if you ask Coq with the Check command, it will tell you that its type is... Type!

Actually, this is a bit of a lie. If you ask for more details by issuing the directive Set Printing Universes., Coq will tell you that that Type is not the same as the first one, but a "bigger" one. Formally, every Type has an index associated to it, called its universe level. This index is not visible when printing expressions usually. Thus, the correct answer for that question is that Type_i has type Type_j, for any index j > i. This is needed to ensure the consistency of Coq's theory: if there were only one Type, it would be possible to show a contradiction, similarly to how one gets a contradiction in set theory if you assume that there is a set of all sets.

To make working with type indices easier, Coq gives you some flexibility: no type has actually a fixed index associated with it. Instead, Coq generates one new index variable every time you write Type, and keeps track of internal constraints to ensure that they can be instantiated with concrete values that satisfy the restrictions required by the theory.

The error message you saw means that Coq's constraint solver for universe levels says that there can't be a solution to the constraint system you asked for. The problem is that the forall in the definition of nat is quantified over Type_i, but Coq's logic forces nat to be itself of type Type_j, with j > i. On the other hand, the application n nat requires that j <= i, resulting in a non-satisfiable set of index constraints.

Washbasin

Is there a way to define plus by iterating the succ function, as OP was trying to do, and have it typecheck? The only way I managed to do it was by inlining the definitions of succ and zero, and the result looked absolutely horrible. – Developing

@Developing Add Set Universe Polymorphism. before nat's definition. That should solve the problem. – Snack

@Developing Instead of defining addition as n succ m, you can define it as λ f. λ x. n f (m f x). – Sheetfed

sure, but you can't do something similar with exponentiation. You have to define it as iterated multiplication. – Developing

@Developing You can define exponentiation without iterated multiplication. See the Church encoding entry on Wikipedia. It's almost the same in Coq, you just need to figure out the type parameters. – Snack

@AntonTrunov Could you say more about how to avoid iterated multiplication? I've tried for a bit now but cannot figure out how to tweak the type parameters. – Nereid

@Nereid Definition exp (n m : nat) : nat := fun X => m (X -> X) (n X). Actually, Coq can infer the type arguments, i.e. the following also works Definition exp (n m : nat) : nat := fun X => m _ (n _).. – Snack

@AntonTrunov Thank you! Now I understand that Coq's type inferences is more subtle (powerful) than what I'm used to. – Nereid