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

[kim-em]

See issue description at #2297.

[github-actions[bot]]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[tydeu]

@semorrison Should not this be symmetric? That is, if Lean solves max u v =?= max u ?v should it not also solve max u v =?= max ?u v? Or am I missing something makes that unnecessary?

[kim-em]

@tydeu, my understanding is that maxs have already been sorted by the time they arrive here, in a way that ensures the mvars don't appear in the first slot.

[tydeu]

@semorrison Ah, okay, makes sense. 👍

[leodemoura]

@tydeu, my understanding is that maxs have already been sorted by the time they arrive here, in a way that ensures the mvars don't appear in the first slot.

@semorrison You must confirm that. You also need to properly document LevelDefEq.lean and add a Note (in this module) about the change that has been made.

[kim-em]

I'm going to label this as low priority for now, in the context of the UnivLE workaround I developed in Mathlib seeming to work for now. (See https://github.com/leanprover-community/mathlib4/pull/5723, https://github.com/leanprover-community/mathlib4/pull/5724, https://github.com/leanprover-community/mathlib4/pull/5726.) I don't think UnivLE is a complete solution, so this may be worth revisiting later.

One unfortunate aspect of the current set up is that universe unification issues as in the title often appear in error messages that obscure the "actual" error that the user needs to address (usually an instance not being available). We might think about how to improve that situation without changing the unification algorithm, although at present I don't have ideas in that direction. Anyone coming to this issue in the meantime who has been tripped up by the error messages: creating a separate issue about the error message situation would be a great intermediate step.

[kim-em]

Superseded by https://github.com/leanprover/lean4/pull/3981