The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hello,

I already had used "Set Printing Universes". As far as I can tell, the
only thing "Set Printing Universes" does is cause "Print/Check term." to
print the universe levels of all occurrences of "Type" occurring in a
particular definition as well as the constraints enforced by a
particular definition.

I have a constraint system with thousands of constraints arising from
hundreds of definitions and I would like to know which constraints
contribute to the inconsistency and which definitions/lemmas give rise
to a given constraint.

For instance, Print Universes might mention
"Coq.Relations.Relation_Definitions.1" which I could correctly guess is
the first argument of "relation":

relation =
fun A : Type@{Coq.Relations.Relation_Definitions.1} => A -> A -> Prop
     : Type@{Coq.Relations.Relation_Definitions.1} ->
       Type@{max(Coq.Relations.Relation_Definitions.1,Set+1)}

But its not always that easy to guess the definitions introducing a
particular universe index and even harder to guess which definition or
lemma enforces a given constraint.

Best,
Christian


On 05/09/18 20:42, Gaëtan Gilbert wrote:
> 1) yes
> 
> 2) and 3)
> if you enable printing of universes (Set Printing Universes. in
> coqtop/proof general/etc, some GUI toggle in coqide) universe
> inconsistencies should print that information
> 
> Gaëtan Gilbert
> 
> On 05/09/2018 17:57, Christian Doczkal wrote:
>> Hello everyone,
>>
>> We have a large development where we have generic structures and some
>> concrete instances for them. One of these is for relations (X -> Y ->
>> Prop) with (X,Y : Set).
>>
>> Now I was trying to generalize this to all instances with (X,Y : Type).
>> This leads to a universe inconsistency thousands of lines down the road.
>> I would hope that this is merely a problem of making certain things
>> universe polymorphic, but I don't manage to come up with a minimal
>> example reproducing the problem.
>>
>> At first, I only got the rather uninformative "Universe Inconsistency"
>> error when trying to load two separately compiled parts of the library.
>>
>> With some trial and error I got to the point where I have statement that
>> type checks before the generalized instances are imported and fails to
>> type check afterwards. This gives me an Error of the form:
>>
>> "... cannot ensure that "Type@{foo.2}" is a subtype of Type@{bar.3}"
>>
>> I can use "Print Universes" before and after the Import, but that yields
>> thousands of constraints and even the diff is not too enlightening.
>>
>> If I understand the universe mechanism and the error message correctly,
>> this actually means that assuming "foo.2 <= bar.3" is inconsistent with
>> the current collection of universe constraints. So here are some
>> questions:
>>
>> 1) Is my understanding correct?
>>
>> 2) If yes, is there a way to obtain a minimal (or at least sufficiently
>> small) subset of the current collection of constraints, proving that
>> "foo.2 <= bar.3" cannot be consistently added.
>>
>> 3) What other things can I do to shed some light onto what is happening?
>>
>> Any help would be appreciated.
>>
>> Best,
>> Christian
>>