Failed to synthesize instance with a reducible definition, despite the exact instance existing

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

In the following MWE I've defined an instance instToStringToTypeFoo (foo : Foo) : ToString (foo.toType), where Foo.toType is a reducible definition. Then, when attempting to synthesize an instance of type ToString (?foo.toType), which should match exactly the instance just defined, we get a "failed to synthesize error".

Note that if we remove the reducible annotation on Foo.toString, then synthesis does work as expected.

inductive Foo
  | nat
  | int

@[reducible]
def Foo.toType : Foo → Type
  | .nat => Nat  
  | .int => Int

instance instToStringToTypeFoo (foo : Foo) : ToString (foo.toType) :=
  match foo with
  | .nat => inferInstanceAs <| ToString Nat
  | .int => inferInstanceAs <| ToString Int

/- This is fine; the instance certainly exists -/
#check (instToStringToTypeFoo _ : ToString <| Foo.toType ?foo)

/-
Yet, the following fails to synthesize, despite it matching exactly the type of the instance above

failed to synthesize
  ToString (Foo.toType ?foo)
-/
#synth ToString (Foo.toType ?foo)

https://live.lean-lang.org/#codez=FASwdgJgrgxgLiAbgUwAQDED2nitQH1TAEM5cDVwzgABAbQCdloYQAjAG2QF1gJkAZhmwA6OJgAqATwAOaAFzDMqQEmEqaXPKERJOKgC8APlQA5Uni2oRVA8YCSYauADOcYmBhoXcCZgDKcAzgAOa+GshYygAUAtioipEAlPHq/oEhqDGi4uHJ8vrkALakMAAWqLHKAO4gcKWWOuZGlGACyAwOru6eAILOqAA8hL4BQWDBpqQNNs3gbR1gXR7IfYPDaWMTDtQA9AC06qUg/ccV4MgA3Kh1Xotuy6ieDG7gHFKoyAAex3D9ezvAADEZWQMAA1plvCN0uMwrIInEAPopaGbNZKMSSeGoAD8lUSwGA+2AAE1kHAADTXUpoWIcDiYGrjCrEEAcfriVDOKSOGnOEAAL2QVP4zhktS8emKcDKGS+xHgb2paDg2MwQhuLSWnlQxDYmBQhIErK4EGuym5vOQ/KF5FRGSikUx4Vx+OA/yBlrqqVGDqdOWxeOwiSAA

Steps to Reproduce

1. Define a typeclass instance where the type uses a reducible definition
2. Attempt to synthesize an instance of exactly the same type
3. Observe failure

Expected behavior: I'd expect typeclass synthesis to succeed, given that an instance of exactly the expected type exists.

Actual behavior: "failed to synthesize" error

Versions

On live.lean-lang.org:

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

and

Lean 4.20.0-nightly-2025-04-16
Target: x86_64-unknown-linux-gnu

Both have the same behaviour.

Impact

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

Start with the self-contained Foo example in the issue and run it against the listed Lean versions or the linked live.lean.org reproduction. Compare synthesis with the reducible and non-reducible definitions, then verify that the expected ToString instance is synthesized without regressing the existing #check case.