Lean: an abbrev doesn't cut a failing instance search; a def synonym with inferInstanceAs does

On Lean v4.35.0 and v4.36.0-rc2 with current Mathlib, example (I : Ideal ℤ[X][X][X]) : Type := ℤ[X][X][X] ⧸ I fails to synthesize the quotient instance (depth two works). Hiding the type behind an abbrev did not help in any form I tried: abbrev P3 (A : Type) [CommRing A] := A[X][X][X], a universe-polymorphic variant, noncomputable abbrev P3c : Type := ℤ[X][X][X], and (P2 ℤ)[X] with P2 an abbrev for A[X][X]. Instance search unfolds reducible definitions, so it meets the same problem. What worked is def P3d : Type := ℤ[X][X][X] plus noncomputable instance : CommRing P3d := inferInstanceAs (CommRing ℤ[X][X][X]), after which P3d ⧸ I elaborates, because search stops at the def and finds the direct instance. The other fix that worked is a shortcut instance one level down: noncomputable local instance commRingIterZ2 : CommRing ℤ[X][X] := inferInstance.