The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Hi Jesper,

It is well known that the release version of Coq is not complete for
universe polymorphism, so your inability to find the problem may have
to do with algorithmic issues in Coq rather than your understanding of
the universes necessary for your code.

Matthieu Sozeau has been working on a Coq version with better universe
treatment.

I haven't looked into your example, but one can sometimes break
universe cycles that are only a Coq artefact by duplicating some
definition (thus creating more fresh universe levels).

BTW, it is not mysterious that "it is always the second one that fails
even if you switch them around." because it is creating a universe
cycle that is the failure, which apparently takes both the definitions
to happen.

Best,
Randy
--
On Mon, Jun 17, 2013 at 8:22 AM, Jesper Bengtson 
<jebe AT itu.dk>
 wrote:
> Dear Coq Club,
>
> I'm having troubles in my current Coq development with Type hierarchies. 
> When defining a Fixpoint, the error message 'Universe Inconsistency' crops 
> up. I have created a small test file that illustrates my problems, but I am 
> having a very hard time understanding what actually is the problem. I have 
> done the hierarchies on paper and they seem to add up.
>
> There are a few things that puzzle me in this example. First of all, I have 
> a definition of a partial function that is never used. If I remove this 
> definition, the universe inconsistencies disappear. Secondly, there are two 
> Fixpoints at the end, and it is always the second one that fails even if 
> you switch them around.
>
> In the file, I have marked the lines that can safely be removed in order to 
> have the whole file compiled. I have also marked which Type uses are the 
> offenders where the Fixpoints start failing so that you don't have to look 
> up the numbers manually. I realise that the constraint system is being 
> built incrementally as new definitions are added to Coq, and here it seems 
> to rear its head by relating definitions that are completely independent 
> (or at least so I think) from each other.
>
> Best regards
>
> /Jesper
>