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?
In Coq, everything has a type.
Type
is no exception: if you ask Coq with theCheck
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 thatType
is not the same as the first one, but a "bigger" one. Formally, everyType
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 thatType_i
has typeType_j
, for any indexj > i
. This is needed to ensure the consistency of Coq's theory: if there were only oneType
, 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 ofnat
is quantified overType_i
, but Coq's logic forcesnat
to be itself of typeType_j
, withj > i
. On the other hand, the applicationn nat
requires thatj <= i
, resulting in a non-satisfiable set of index constraints.