Unreasonable "instance problem stuck" due to out-of-order parameter

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

A theorem requires an LE instance, a reflexivity instance for LE and a hypothesis whose type depends on the LE instance. If the hypothesis accidentally comes before the LE (for example because of auto-implicits), Lean shows an error that it cannot infer the reflexivity instance. This is misleading and does not help finding the underlying problem.

Steps to Reproduce

Run this:

def x [LE α] [Std.Refl (α := α) (· ≤ · )]
    (hP : ∀ a : α, a ≤ a) :
    Nat := sorry

/--
error: typeclass instance problem is stuck, it is often due to metavariables
  @Std.Refl α fun x1 x2 => @LE.le α ?m.9 x1 x2
-/
#guard_msgs in
set_option pp.explicit true in
theorem a {hP} [LE α] [Std.Refl (α := α) (· ≤ · )] :
    x (α := α) hP = sorry := by
  sorry

theorem b [LE α] {hP} [Std.Refl (α := α) (· ≤ · )] :
    x (α := α) hP = sorry := by
  sorry

Expected behavior:

a fails, explaining that elaborating hP's type failed because LE cannot be synthesized.

b succeeds.

Actual behavior:

a fails with a misleading error message that does not help finding the underlying problem.

Versions

Lean 4.25.0-nightly-2025-10-13
Target: x86_64-unknown-linux-gnu

Impact

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

No repository files or tests are named. Start by running the minimal reproducer against the specified Lean nightly version and compare theorem a with theorem b. Done means the out-of-order parameter case reports that elaborating hP's type failed because the LE instance cannot be synthesized, rather than showing only a stuck reflexivity instance.