Stream: Coq users

Topic: ✔ Difficult to read universe polymorphism error

Patrick Nicodemus (Apr 23 2022 at 13:10):

I am getting an error which I don't know how to interpret.

Error:
The term
 "{|
    morphism_isomorphic := associator_nat_trans;
    isisomorphism_isomorphic := associator_is_iso
  |}" has type
 "(right_assoc@{Top.AugmentedSimplexCategoryMonoidalStructure.17454
     Top.AugmentedSimplexCategoryMonoidalStructure.17455
     Top.AugmentedSimplexCategoryMonoidalStructure.17452
     Top.AugmentedSimplexCategoryMonoidalStructure.17456
     Top.AugmentedSimplexCategoryMonoidalStructure.17457
     Top.AugmentedSimplexCategoryMonoidalStructure.17458
     Top.AugmentedSimplexCategoryMonoidalStructure.17459
     Top.AugmentedSimplexCategoryMonoidalStructure.17460
     Top.AugmentedSimplexCategoryMonoidalStructure.17461}
     tensor@{Top.AugmentedSimplexCategoryMonoidalStructure.17454
     Top.AugmentedSimplexCategoryMonoidalStructure.17455
    ....

while it is expected to have type
 "(right_assoc@{Top.AugmentedSimplexCategoryMonoidalStructure.16875
     Top.AugmentedSimplexCategoryMonoidalStructure.16876
     Top.AugmentedSimplexCategoryMonoidalStructure.16877
     Top.AugmentedSimplexCategoryMonoidalStructure.16879
     Top.AugmentedSimplexCategoryMonoidalStructure.16880
     Top.AugmentedSimplexCategoryMonoidalStructure.16881
     Top.AugmentedSimplexCategoryMonoidalStructure.16882
     Top.AugmentedSimplexCategoryMonoidalStructure.16883
     Top.AugmentedSimplexCategoryMonoidalStructure.16884}
     tensor@{Top.AugmentedSimplexCategoryMonoidalStructure.16875
     Top.AugmentedSimplexCategoryMonoidalStructure.16876
     Top.AugmentedSimplexCategoryMonoidalStructure.16875
   ...

Patrick Nicodemus (Apr 23 2022 at 13:11):

Where should I start with tracking down the source of this error

Patrick Nicodemus (Apr 23 2022 at 13:11):

I don't know if it's really a universe error or if the error is somewhere else and is just obscured by the massive wall of universes.

Patrick Nicodemus (Apr 23 2022 at 13:16):

Is there a flag i can enable which would suppress all these universes so i can see what else is going on

Paolo Giarrusso (Apr 23 2022 at 13:40):

Universes are hidden by default — you must use Set Printing Universes to show them. (IIRC, Set Printing All does not show them). In Coqide/VSCode/..., you need the corresponding "Display" commands.

Paolo Giarrusso (Apr 23 2022 at 13:41):

Let me assume you have _not_ set some fancy option. Then AFAIK Coq only shows universes if they're relevant.

Patrick Nicodemus (Apr 23 2022 at 13:48):

I see, ok, thank you

Paolo Giarrusso (Apr 23 2022 at 13:49):

Re troubleshooting, I'm fairly clueless on universes but some starting points:

• any change you have a partially applied inductive somewhere? They're a well-known cause of unwarranted universe inconsistencies. IIUC, already this is bad:

Definition f : Type -> Type = option.

replace with

Definition f : Type -> Type = fun x => option x.

• are you mechanizing some large category or such, where you'd expect challenges with universes?
• http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html could be helpful reading.

Paolo Giarrusso (Apr 23 2022 at 13:49):

(I have not seen material on universes in Software Foundations)

Patrick Nicodemus (Apr 23 2022 at 13:50):

Thank you. I turned on Set Printing All and it simplified the message a lot and cleared away the universes

Patrick Nicodemus (Apr 23 2022 at 13:50):

The matter was context dependencies

Notification Bot (Apr 23 2022 at 13:50):

Patrick Nicodemus has marked this topic as resolved.

Patrick Nicodemus (Apr 23 2022 at 13:52):

the type mismatch came from the fact that the term and the type were both borrowing an assumption declared as a context (an instance of a typeclass) but they were two different assumptions declared in two different files.

Last updated: Oct 13 2024 at 01:02 UTC