18

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?

perror
  • 7,071
  • 16
  • 58
  • 85
augurar
  • 12,081
  • 6
  • 50
  • 65
  • 5
    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](http://www.konne.me/2015/08/17/paradoxes.html)). – Konstantin Weitz Aug 23 '15 at 19:57
  • 2
    Note that `-type-in-type` only works for Coq 8.5 beta (not for the currently stable 8.4 version) – Catalin Hritcu Sep 13 '15 at 21:41

1 Answers1

21

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.

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • 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. – hugomg Sep 14 '16 at 23:37
  • 1
    @hugomg Add `Set Universe Polymorphism.` before `nat`'s definition. That should solve the problem. – Anton Trunov Jan 13 '17 at 17:58
  • @hugomg Instead of defining addition as `n succ m`, you can define it as `λ f. λ x. n f (m f x)`. – augurar Jan 14 '17 at 01:24
  • sure, but you can't do something similar with exponentiation. You have to define it as iterated multiplication. – hugomg Jan 14 '17 at 16:19
  • 1
    @hugomg You can define exponentiation *without* iterated multiplication. See the [Church encoding](https://en.wikipedia.org/wiki/Church_encoding) entry on Wikipedia. It's almost the same in Coq, you just need to figure out the type parameters. – Anton Trunov Mar 22 '18 at 17:55
  • @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. – LeonidR Mar 04 '19 at 05:31
  • @LeonidR `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 _).`. – Anton Trunov Mar 04 '19 at 08:30
  • @AntonTrunov Thank you! Now I understand that Coq's type inferences is more subtle (powerful) than what I'm used to. – LeonidR Mar 04 '19 at 18:57