Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Debugging Universe Inconsistencies

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Debugging Universe Inconsistencies


Chronological Thread 
  • From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Debugging Universe Inconsistencies
  • Date: Wed, 5 Sep 2018 20:42:36 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay1-d.mail.gandi.net
  • Ironport-phdr: 9a23:Ts9LZB8XuHFmkP9uRHKM819IXTAuvvDOBiVQ1KB42+gcTK2v8tzYMVDF4r011RmVBdqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LXbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUOFeUGIfpYoJP7p1QWrBW+BA2sC/jxxT9Smn/9wKo30+s7Hg7YwAwvBdQOvG7brNX0MKcdSv66zLPUzTjYdPNW2jf86JPLchAgpPGMWKx/cdDLxUkpCQzFkkydpIr4ND2WzuQAq3aX4/diWO61iWMrtxt9riWsy8oikIXFm4YYx17c+Sh43oo5P8C0RFJlbdK+DZdduCKXO5FrTs4gTWxlvjsxxKcctp6hZicKzYwqxx7BZPyDdIiF+gjjW/iVIThihHNpZauziAuo/Uil0OL8V8203ExFriVflNnDq3EN2wbV6seZVvtx5kah2TCR2ADP8uxIP104mKjBJ5Mj3rI8jIcfvEfNEyPshUn7iKGbel0h+uey6uTnZrvmpoWbN49xkgz+Pb4hldKjAesiNAgCRWeb+eW41LL440L5WqlKg+YtkqnasJHaPscbpq+8Aw9QzIkj8QyzDzG439QEhXUHNk5KeAqbj4j1PFHDOOz3DfCmg1i1jDhrw+3GMab6D5XWLnnDla/hcqxn505dzgoz19Ff6IhOBrEPOvKgEnP24dffF1oyNxG+6+fhEtR0kI0ECkyVBarMH6pRrVaO0c0uJ+OBfpNd7Dn0JuQs4bjhjHszlEUBVbKqzIAUaXW9E+4gJUiFNym/yuwdGHsH61JtBNfhj0ePBGYKNiSCGpkk7zR+M7qISILKR4SjmruEhXnpBZ5HfWNHD1WBCzHuepnWAq5QOhLXGddol3k/bZbkU5UojE/8rwzr0LlmK+/Z4GseuI6xjIEotd2Wrgk78HlPN+rY02yJSDspzHkFQzYnheVz50l0y1PF3qF+j/0eE9FPtatE

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




Archive powered by MHonArc 2.6.18.

Top of Page