-
Notifications
You must be signed in to change notification settings - Fork 350
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
rfc: allow universe unification to solve max u v =?= max u ?v
#2297
Comments
Looking at the mathlib PR, I can see two situations where the TypeMax workaround leaks:
theorem one (sf : piOpens F U) : True := ⟨⟩ -- fails
theorem one' (sf : (piOpens F U : TypeMax.{w,v})) : True := ⟨⟩ -- works
variable {C : Type u} [Category.{max w v, u} C] [ConcreteCategory.{max w v, max w v, u} C]
variable {X : TopCat.{w}} (F : Presheaf.{w, max w v, u} C X) {ι : Type w} (U : ι → Opens.{w} X)
def IsCompatible (sf : ∀ i : ι, F.obj (op (U i))) : Prop :=
∀ i j : ι, F.map (infLELeft (U i) (U j)).op (sf i) = F.map (infLERight (U i) (U j)).op (sf j) |
Something to note about the paradigmatic failure above: the universe metavariable is in a candidate instance, not in the type we are trying to synthesize. I appreciate that we should be wary of solving for universes when multiple solutions could exist (i.e. |
…19230) This reverts commit 1336155. These are just too difficult to forward port as is because of the `max u v =?= max u ?v` issue leanprover/lean4#2297. We have another candidate approach to this, using a new `UnivLE` typeclass, and I would prefer if we investigated that without the pressure of the port at the same time. This will delay @hrmacbeth's plans to define meromorphic functions, perhaps. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
My realization from this observation is that, when you have an instance |
The same trick can be used to deal with constraints of the form
|
Actually, UnivLE seems to be the best solution as it only requires one instance for each of the three cases above:
|
I haven't been following, but I sort of suspect you are recapitulating my discovery of the design of |
Yeah, I wasn't following when UnivLE was developed and I'm certainly rediscovering some considerations you had :-) Your choice to use |
This is partially resolved by #3981, although that only enables the approximation outside of typeclass search, so doesn't completely solve the initial problem described here. |
Can you summarize the reasoning for not doing this during typeclass synthesis? |
I think the concern is that as it is an approximation (i.e. might be wrong), but won't be backtracked, it could cause failures. If someone wants to try turning it on during synthesis, and see how much Mathlib complains, I'd be interested to see! |
Breakage incoming: leanprover-community/mathlib4#12522 is waiting until I get back to a machine to figure out what is going on with the non-arm MacOS build. It builds with the custom toolchain. The diff gives an idea of the issues. |
Prerequisites
Description
Currently universe unification will not solve
max u v =?= max u ?v
ormax u v =?= max v ?u
. (Lean 3 would do this.)This is causing some problems in mathlib4.
Steps to Reproduce
Expected behavior:
It would be nice if this all succeeded!
Actual behavior:
Failures with
stuck at max a b =?= max a ?u
.Reproduces how often:
Consistently.
Versions
Additional Information
I have a small patch at #2298, which resolves this issue in a fairly conservative manner.
However changing universe unification seems scary, and I hesitate to suggest this as a solution. It does, however, compile mathlib4 cleanly, with no performance regression (indeed, perhaps a speed-up, although maybe within the margin of error).
See for example leanprover-community/mathlib4#5536 and leanprover-community/mathlib4#5534, which respectively don't use this patch (and hence fail) and do use this patch (and succeed).
The text was updated successfully, but these errors were encountered: