The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Dear Jeremy,

There was a thread started by Vadim Zaliva on Nov. 30th, 2019 with
subject "universe inconsistency on inport". That thread developed into a
discussion on how to debug universe inconsistencies, e.g., by naming the
universes introduced by key (monomorphic) definitions. Maybe it can
serve as a starting point?

Hope that helps!

Christian

On 1/13/20 6:37 AM, Jeremy Dawson wrote:
> Hi,
>
> Following the problem described in the message below, I've spent a very 
> great deal of time inserting Polymorphic in various definitions, 
> more-or-less randomly, and it often seems to make a difference, 
> sometimes by avoiding an error but sometimes by producing similar errors 
> somewhere else.  This doesn't help, and as a result it's making Coq 
> virtually unusable for me.
>
> Trying random changes to see if it works isn't my idea of how to go 
> about doing proofs (or anything else), and certainly not something I'd 
> recommend and certainly  so I really would appreciate some guidance on this.
>
> In particular, the latest error I've got is
>
> Unable to unify
>   "seqrel@{Top.598 Top.602 Top.600} (singleton_rel ([], [Imp C D]) ([C], 
> [D]))
>      c2 x" with "seqrel@{Top.775 Set Top.772} ?R c2 x"
>
> what does seqrel@{Top.598 Top.602 Top.600} mean?
>
> And I get the following
> can_trf_ImpRinv_ImpL' < Check seqrel.
> seqrel@{Top.777 Top.778
> Top.779}
>       : forall W : Type@{Top.778},
>         (rel (list W) -> rel (list W) -> Type@{Top.779}) ->
>         relationT@{lntT.6 Top.777} (Seql W)
> (* {Top.779 Top.778 Top.777 Top.775 Top.772 Top.749} |=
>     Set <= Top.602
>     Set <= Top.749
> (and about a screenful more of similar inequalities)
>
> I've seen a bit about universe inequality constraints in
> http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html
> but apart from that, what does this mean?
>
> Thanks for any help
>
> Jeremy
>
>
> On 25/12/19 11:15 pm, Jeremy Dawson wrote:
>> Hi,
>>
>> I've got the following error message
>>
>> The term "rr" has type
>>    "(rel (list W) -> rel (list W) -> Type@{Top.890}) -> Type@{Top.889}"
>> while it is expected to have type
>>    "(rel (list W) -> rel (list W) -> Type@{k4.86}) -> Type@{Top.897}"
>> (universe inconsistency: Cannot enforce k4.86 <= Top.890 because Top.890
>> < Top.688 <= gstep.624 = k4.86).
>>
>> How do I find out why Coq wants Top.890 < Top.688 and Top.688 <=
>> gstep.624 and gstep.624 = k4.86 ?
>>
>> Is this the sort of error which is likely to be solved by putting
>> Set Universe Polymorphism?  (When I tried this it led to errors
>> elsewhere so I didn't pursue this idea).
>>
>> Thanks
>>
>> Jeremy Dawson
>>