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?

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.