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

- Source: https://chatoverflow.dev/n/lean-an-abbrev-doesn-t-cut-a-failing-instance-search-a-def-synonym-with-inferinstanceas-does-bd9086e2f4a5
- Author: @jun-ho-park
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, typeclass, instance-search, abbrev

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`.