Irene Yoon (Jun 28 2021 at 20:19): Irene Yoon (Jun 28 2021 at 20:19):Hi, I'm running into a problem where if I Require Import typeclass definitions, then it generates different universe constraints than when I inline the definitions in the same file.
The typeclass definitions are in a Section X.
If I put Section X in file A, and try to define the Instances in a Section Y in file B, it throws a universe inconsistency error.
If I put Section X in file B, and try to define the Instances in a Section Y within the same file B, I do not receive the error.
Does anyone know why this might be happening? Thanks!
Paolo Giarrusso (Jun 29 2021 at 14:43):Not a universe expert but you might have different settings (especially for Set Universe Polymorphism and so), possibly coming from your imports... Or this might be a genuine problem with inference heuristics, and then you might need a real expert. I've been told by one of those that e.g. Unset Universe Minimization ToSet. will disable some "unsound" optimizations of inference results, but not sure if they apply here.
Paolo Giarrusso (Jun 29 2021 at 14:43):those optimizations are "unsound" only in the sense that they'll make some clients illegal.
Paolo Giarrusso (Jun 29 2021 at 14:44):BTW I'm guessing that B loads A — otherwise other explanations could apply
Irene Yoon (Jun 29 2021 at 15:20):Ok, I'll try out that flag, thanks!
Christian Doczkal (Jun 29 2021 at 18:39):The last time I encountered a similar issue, which was a few years ago, the culprit was indeed an inference heuristic that was creating an unnecessarily strong universe constraint in one of the lemmas. My solution was to start linearize the development until the error occurred at a lemma statement rather than an import (this seems to not be necessary here). Then I named universes and posed the constraints I would ultimately need to keep the heuristic from adding overly strong constraints. Needless to say, this is not a pleasant process.
Last updated: Sep 30 2023 at 05:01 UTC