Inconsistent behavior in typeclass resolution (local vs top-level instance)

Prerequisites

• 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

class C (α: Type)

structure T1

@[implicit_reducible]
def T2 := T1

def p [C T1]: Prop := True

-- works
theorem test_local [C T2]: p = True := rfl

instance: C T2 where

/--
error: failed to synthesize instance of type class
  C T1

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
theorem test_toplevel: p = True := rfl

-- workaround
instance [C T2]: C T1 := inferInstanceAs (C T2)
-- now succeeds
theorem test_toplevel': p = True := rfl

In test_local, Lean searches for an instance of C T1, and tries every instance in the local context that matches C ?_. So it tries the instance of C T2 and succeeds because C T1 and C T2 are defeq at implicit transparency.

In test_toplevel, however, a top-level instance of C T2 is defined, and because now typeclass resolution works by doing a lookup in a discrimination tree, Lean does not even try the defeq check, and fails.

To work around this, one can add an instance of C T1 derived from an instance of C T2.

(Thanks to this workaround, this issue is not a blocker: I am opening it so that it is documented somewhere)

Context

Code minimized from typeclasses appearing in Bob DyLean. The behavior of typeclass resolution trying defeq with each local instance was discussed with @Kha and @nomeata at SVIL26 last week.

Steps to Reproduce

Expected behavior: test_local and test_toplevel should either both succeed, or both fail. I think probably they should both fail.

Actual behavior: test_local succeeds and test_toplevel fails

Versions

• 4.30.0-rc2
• 4.31.0-nightly-2026-04-28

Impact

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

Start with the minimal Lean reproduction in the issue and run it against the stated nightly version, using set_option trace.Meta.synthInstance true to inspect resolution. Trace the local-context and top-level instance paths, then make their behavior consistent and verify both test_local and test_toplevel produce the intended result.