The Coq mailing list

[Jesper Bengtson <jebe AT itu.dk>]

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

Attachment: Test.v
Description: Test.v