Stream: Coq users

Topic: ✔ Difficult to read universe polymorphism error


view this post on Zulip 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
   ...

view this post on Zulip Patrick Nicodemus (Apr 23 2022 at 13:11):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Apr 23 2022 at 13:48):

I see, ok, thank you

view this post on Zulip Paolo Giarrusso (Apr 23 2022 at 13:49):

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

Definition f : Type -> Type = option.

replace with

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

view this post on Zulip Paolo Giarrusso (Apr 23 2022 at 13:49):

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

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Apr 23 2022 at 13:50):

The matter was context dependencies

view this post on Zulip Notification Bot (Apr 23 2022 at 13:50):

Patrick Nicodemus has marked this topic as resolved.

view this post on Zulip 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: Feb 09 2023 at 00:03 UTC