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

[kim-em]

Prerequisites

• 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 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).

[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?