The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

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
>