coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Debugging Universe Inconsistencies, Christian Doczkal, 09/05/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Gaëtan Gilbert, 09/05/2018
- Message not available
- Re: [Coq-Club] Debugging Universe Inconsistencies, Gaëtan Gilbert, 09/06/2018
- Message not available
- Re: [Coq-Club] Debugging Universe Inconsistencies, Christian Doczkal, 09/06/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Jan-Oliver Kaiser, 09/06/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Christian Doczkal, 09/06/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Christian Doczkal, 09/07/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Gaëtan Gilbert, 09/07/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Christian Doczkal, 09/10/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Matthieu Sozeau, 09/10/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Christian Doczkal, 09/11/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Gaëtan Gilbert, 09/10/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Gaëtan Gilbert, 09/07/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Christian Doczkal, 09/07/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Christian Doczkal, 09/06/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Jan-Oliver Kaiser, 09/06/2018
- Re: [Coq-Club] Debugging Universe Inconsistencies, Gaëtan Gilbert, 09/05/2018
Archive powered by MHonArc 2.6.18.