Kernel rejects unification solution with max universes

[Janno]

Description of the problem

The example below fails at Qed time instead of during unification. Using apply eq_refl does not help.
It's not clear to me at all that it should fail but if it should indeed fail anywhere then it shouldn't be during Qed.

Small Coq file to reproduce the bug

Definition test1@{u} := unit.
Definition test2@{u} := unit.
Goal Type@{max(Set,test1.u)} = Type@{test2.u}.
Proof. Set Printing Universes. refine eq_refl. Qed.

Version of Coq where this bug occurs

8.16.0, 8.19.1

Last version of Coq where the bug did not occur

No response

[SkySkimmer]

Around

coq/pretyping/evarsolve.ml

Line 1820 in 4352c71

let evd', body = refresh_universes pbty env evd' body in

we are supposed to produce evk := body but instead produce evk := body' with body <= body'.
Removing the refresh entirely results in failure at the Definition command (I think it fails to unify the implicit argument of eq with the type of Type@{max(...)})
Doing the refresh only when pbty <> None (ie when we are up to cumulativity instead of conversion) results on failure at refine eq_refl (probably what we expect?), not sure if there are any bad consequences. There are a couple test failures (#4095 and #4957).

But TBH IDK if it's worth caring about bugs with explicit algebraics until #18903

[Janno]

But TBH IDK if it's worth caring about bugs with explicit algebraics until #18903

That makes sense and I am fine keeping this unresolved for now.

The reason I reported this bug is because I was trying to debug a unification failure and those algebraic universes were the terms involved in that unification problem. I didn't chose to use algebraic universes; they were generated by Coq.

[SkySkimmer]

A version of the report without the explicit algebraics may be useful then.

[Janno]

Sorry I should have been more explicit: In the end, the unification failure itself was not a bug. But debugging it was problematic because of this issue here.