rfc: allow universe unification to solve `max u v =?= max u ?v`

[kim-em]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Currently universe unification will not solve max u v =?= max u ?v or max u v =?= max v ?u. (Lean 3 would do this.) This is causing some problems in mathlib4.

Steps to Reproduce

universe u v

-- This is a mock-up of the `HasLimitsOfSize` typeclass in mathlib4.
class HLOS.{a,b} (C : Type b) where
  P : Type a

-- We only have an instance when there is a "universe inequality".
instance HLOS_max : HLOS.{a} (Type max a b) := sorry

example : HLOS.{a} (Type max a b) := HLOS_max.{a, max a b} -- Success
example : HLOS.{a} (Type max a b) := inferInstance -- Fails: stuck at max a b =?= max a ?u

-- In mathlib4 we currently make use of the following workaround:
abbrev TypeMax := Type max u v

instance (priority := high) HLOS_max' : HLOS.{a} (TypeMax.{a, b}) := sorry

example : HLOS.{a} (TypeMax.{a, b}) := HLOS_max'.{a} -- Success
example : HLOS.{a} (TypeMax.{a, b}) := inferInstance -- Success

-- However, these still fail
example : Type max v u = TypeMax.{v} := rfl -- Fails: `max u v =?= max v ?u`
example : Type max v u = TypeMax.{u} := rfl -- Fails: `max u v =?= max u ?u`

-- and there are situations in which, however much we try to use `TypeMax`,
-- we find failing syntheses of: `HLOS.{a} (Type max a b)` 

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

Lean (version 4.0.0-nightly-2023-06-20, commit a44dd71ad62a, Release)

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 https://github.com/leanprover-community/mathlib4/pull/5536 and https://github.com/leanprover-community/mathlib4/pull/5534, which respectively don't use this patch (and hence fail) and do use this patch (and succeed).

[gebner]

Looking at the mathlib PR, I can see two situations where the TypeMax workaround leaks:

1. Type max u v is a category, and that's the expected type of types, so if you use a function [Category C] -> A -> C as a type then it will default to Type max u v.

theorem one (sf : piOpens F U) : True := ⟨⟩ -- fails
theorem one' (sf : (piOpens F U : TypeMax.{w,v})) : True := ⟨⟩ -- works

2. I don't know where to put the workaround in Preshead.IsCompatible:

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)

[kim-em]

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. max u v = max u ?v has solutions ?v := v and ?v = max u v), but this situation is one where we can can be less wary, because typeclass synthesis is just meant to come up with some answer.

[alreadydone]

My realization from this observation is that, when you have an instance C.{u,max u v} that will never file due to this issue, create instead a C.{u,u} instance and a C.{max u v, v} → C.{u, v} instance, then C.{u,max u v} can be found via C.{max u (max u v), max u v} = C.{max u v, max u v}. This works in the category theory library for HasLimitsOfSize, PreservesLimitsOfSize etc. which are Prop-valued, or in other situations where you don't care what v is unified to in max u v. This might alleviate the need for UnivLE and resolution of this issue. The C.{max u v, v} → C.{u, v} instances (where max u v and u pertain to the indexing category) can be achieved using CategoryTheory.ULift.equivalence and doesn't even need the Shrink.equivalence I introduced in mathlib4#7695 which is not as nice definitionally.

[alreadydone]

The same trick can be used to deal with constraints of the form a ≤ b+1, but the solution for a+1 ≤ b. (Not sure whether they come up in practice.) Note that a different "of_max" instance needs to be introduced for each of the three cases.

set_option autoImplicit true

class HLOS.{a,b} (C : Type b) where
  P : Type a

-- instances to implement the constraint `a ≤ b`
instance HLOS_self : HLOS.{a} (Type a) := sorry
instance HLOS_of_max [HLOS.{max a b} (Type a)] : HLOS.{b} (Type a) := sorry
example : HLOS.{a} (Type max a b) := inferInstance -- succeeds
example : HLOS.{a} (Type (a+1)) := inferInstance -- succeeds
example : HLOS.{a} (Type max (a+1) b) := inferInstance -- succeeds
example : HLOS.{a} (Type max a (b+1)) := inferInstance -- succeeds
example : HLOS.{a} (Type (max a b + 1)) := inferInstance -- succeeds

class HLOS1.{a,b} (C : Type b) where
  P : Type a

-- instances to implement the constraint `a+1 ≤ b`
instance HLOS1_succ : HLOS1.{a} (Type (a+1)) := sorry
instance HLOS1_of_max [HLOS1.{max a b} (Type (a+1))] : HLOS1.{b} (Type (a+1)) := sorry
example : HLOS1.{a} (Type (max a b + 1)) := inferInstance -- succeeds
example : HLOS1.{a} (Type max (a+1) b) := inferInstance -- fails

class HLOS2.{a,b} (C : Type b) where
  P : Type a

-- instances to implement the constraint `a ≤ b+1`
instance HLOS2_succ : HLOS2.{a+1} (Type a) := sorry
instance HLOS2_of_max [HLOS2.{max (a+1) b} (Type a)] : HLOS2.{b} (Type a) := sorry
example : HLOS2.{a+1} (Type max a b) := inferInstance -- succeeds
example : HLOS2.{a} (Type a) := inferInstance --succeeds
example : HLOS2.{a} (Type max a b) := inferInstance -- succeeds
example : HLOS2.{a+2} (Type max (a+1) b) := inferInstance -- succeeds
example : HLOS2.{a+2} (Type (max a b + 1)) := inferInstance -- succeeds

[alreadydone]

Actually, UnivLE seems to be the best solution as it only requires one instance for each of the three cases above:

set_option autoImplicit true

@[pp_with_univ]
abbrev UnivLE.{u, v} : Prop := ∀ α : Type u, Small.{v} α
-- see https://github.com/leanprover-community/mathlib4/blob/5015c0b4e8a03ea1e91e095d080c5dfb8953b4d5/Mathlib/Logic/UnivLE.lean#L56
instance univLE_of_max [UnivLE.{max u v, v}] : UnivLE.{u, v} := sorry

class HLOS.{a,b} (C : Type b) where
  P : Type a

-- instances to implement the constraint `a ≤ b`
instance [UnivLE.{a,b}] : HLOS.{a} (Type b) := sorry
example : HLOS.{a} (Type max a b) := inferInstance -- succeeds
example : HLOS.{a} (Type (a+1)) := inferInstance -- succeeds
example : HLOS.{a} (Type max (a+1) b) := inferInstance -- succeeds
example : HLOS.{a} (Type max a (b+1)) := inferInstance -- succeeds
example : HLOS.{a} (Type (max a b + 1)) := inferInstance -- succeeds
example : HLOS.{0} (Type b) := inferInstance -- succeeds

class HLOS1.{a,b} (C : Type b) where
  P : Type a

instance [UnivLE.{a+1,b}] : HLOS1.{a} (Type b) := sorry
example : HLOS1.{a} (Type (max a b + 1)) := inferInstance -- succeeds
example : HLOS1.{0} (Type (b+1)) := inferInstance -- succeeds
example : HLOS1.{a} (Type max (a+1) b) := inferInstance -- succeeds

class HLOS2.{a,b} (C : Type b) where
  P : Type a

instance [UnivLE.{a,b+1}] : HLOS2.{a} (Type b) := sorry
example : HLOS2.{a+1} (Type max a b) := inferInstance -- succeeds
example : HLOS2.{a} (Type a) := inferInstance --succeeds
example : HLOS2.{a} (Type max a b) := inferInstance -- succeeds
example : HLOS2.{a+2} (Type max (a+1) b) := inferInstance -- succeeds
example : HLOS2.{a+2} (Type (max a b + 1)) := inferInstance -- succeeds
example : HLOS2.{1} (Type b) := inferInstance -- succeeds
example : HLOS2.{0} (Type b) := inferInstance -- succeeds

[kim-em]

I haven't been following, but I sort of suspect you are recapitulating my discovery of the design of UnivLE. :-)

[alreadydone]

Yeah, I wasn't following when UnivLE was developed and I'm certainly rediscovering some considerations you had :-) Your choice to use max u v was based on a misconception (that you need it for α → β to be small), but accidentally it makes the instances all work. My observation is mainly that you can replace max u v by u but introduce an instance from UnivLE.{max u v, v} to UnivLE.{u, v} to achieve the same effect. However this weaker UnivLE is not really weaker, because (I think) if u and v are expressions in 0, (+1), max, and universe variables such that u ≤ v no matter what natural numbers are substituted for the variables, then Lean verifies the defeq max u v ≡ v. Therefore, it may not really worth proceeding with the redefinition in #7695, and I might extract generalizations done in #7695 to another PR.

[kim-em]

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.

[mattrobball]

Can you summarize the reasoning for not doing this during typeclass synthesis?

[kim-em]

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!

[mattrobball]

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.