bug: stuck at solving universe constraint "while trying to unify `α : Type u` with `α : Type u`" message

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The error message that is shown when universe unification does not make sense in some cases.

Steps to Reproduce

Run this in Lean 4 Web:

inductive Y (α' β) where
| y : α' → β → Y α' β

def predicate {α' β} :
  Y.{u + 1, v + 1} α' β → Prop := sorry

def weird_cast {α'' α' : Type u} (x : α'') : α' :=
  sorry

example {α : Type u} {x : α} (h : predicate (weird_cast x)) :
    Unit := ()

(I know, the example is really contrived. This is due to the minimization.)

Expected behavior:

The code is obviously underdetermined (and nonsensical). It compiles after passic explicit arguments (β := α) (α := α) to predicate.

I imagine the error message should describe the failure to determine α, β or α first. As long as they are undetermined, this seems to be the more instructive kind of error than a universe unification error.

If a universe unification error needs to be shown, it should clearly indicate what is being unified and why it fails. The user should be convinced from the error message that there's a problem.

Actual behavior:

I get this error message:

stuck at solving universe constraint
  max ?u.520 ?u.521 =?= u
while trying to unify
  α : Type u
with
  α : Type u

I find it confusing because α : Type u should definitely unify with itself, and it certainly has nothing to do with the maximum of two level metavariables.

Versions

Lean 4.19.0-rc2
Target: x86_64-unknown-linux-gnu

using Lean 4 Web.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal example in Lean 4 Web and compare the reported universe constraint with the expected underdetermined implicit arguments. Trace the diagnostic path for universe unification and implicit-argument elaboration. Done means the example reports the unresolved arguments clearly, or explains the actual failed constraint in terms users can understand.