The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-12-08 15:54 GMT+01:00 Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>:

Dear all,

May be it is a simple question, but is it possible to bound the Type
hierarchy to some finite number while compiling a proof. The goal
could be for instance to determine the least size of the hierarchy
for a proof to type-check ?

Another way to formulate the question is how can I know the maximum
n such that Type_n is needed in the type-checking of a given proof ?

Of course, this might imply that all the parameters have a fixed
Type index which could be obtained by replacing

forall (X : Type) ...

by

forall (X : Set) ...

for instance.

It seems to me that Set Printing Universes is not enough for that.

Dominique

I

​I am not completely sure of the reply to provide, but you must be aware that:

* now we have universe polymorphisms (we can define the "big" category of all "smaller" categories, for instance)​

​

​* using a library inside of an other project can "insert"​ new levels between already existing ones, and thus would require to change all these computed numbers.

  You can even write a library A which compiles perfectly, and two other libraries B and C which use A and compile perfectly, and then a library D which only

  contains "Require B. Require C." and crashes because of a universe inconsistency (B implies some constraints of universe levels of A which are not compatible

  with those that C implies to A). That is not simply that you get an inconsistant theory, that is really that Coq (hopefully) refuses the theory, because

  the "metatheory" itself becomes inconsistant.