From 3ea59e15b8ebd9b0b6fc2ccc9bf64eaeb0ba6499 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Sun, 1 Mar 2026 17:39:17 +1100
Subject: [PATCH] fix: set implicitReducible on grandparent subobject
 projections (#12701)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a gap in how `@[implicit_reducible]` is assigned to parent
projections during structure elaboration.

When `class C extends P₁, P₂` has diamond inheritance, some ancestor
structures become constructor subobject fields even though they aren't
direct parents. For example, in `Monoid extends Semigroup, MulOneClass`,
`One` becomes a constructor subobject of `Monoid` — its field `one`
doesn't overlap with `Semigroup`'s fields, and `inSubobject?` is `none`
during `MulOneClass` flattening.

`mkProjections` creates the projection `Monoid.toOne` but defers
reducibility to `addParentInstances` (guarded by `if !instImplicit`).
However, `addParentInstances` only processes direct parents from the
`extends` clause. Grandparent subobject projections fall through the gap
and stay `semireducible`.

This causes defeq failures when `backward.isDefEq.respectTransparency`
is enabled (#12179): at `.instances` transparency, the semireducible
grandparent projection can't unfold, so two paths to the same ancestor
structure aren't recognized as definitionally equal.

Fix: before `addParentInstances`, iterate over all `.subobject` fields
and set `implicitReducible` on those whose parent is a class.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
---
 src/Lean/Elab/Structure.lean                 | 10 +++++
 tests/elab/grandparentImplicitReducible.lean | 43 ++++++++++++++++++++
 2 files changed, 53 insertions(+)
 create mode 100644 tests/elab/grandparentImplicitReducible.lean

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 81948b3dec..7ccc9bffd3 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -1549,6 +1549,16 @@ def elabStructureCommand : InductiveElabDescr where
                     if fieldInfo.kind.isInCtor then
                       enableRealizationsForConst fieldInfo.declName
                   if view.isClass then
+                    -- Set implicitReducible on subobject projections to class parents.
+                    -- mkProjections defers reducibility to addParentInstances, but
+                    -- addParentInstances only handles direct parents. Subobject fields
+                    -- for non-direct parents (grandparents promoted to constructor
+                    -- subobjects during diamond flattening) also need implicitReducible
+                    -- to be unfoldable at .instances transparency.
+                    for fieldInfo in fieldInfos do
+                      if let .subobject parentName := fieldInfo.kind then
+                        if isClass (← getEnv) parentName then
+                          setReducibilityStatus fieldInfo.declName .implicitReducible
                     addParentInstances parentInfos
                   -- Add field docstrings here (after @[class] attribute is applied)
                   -- so that Verso docstrings can use the class.
diff --git a/tests/elab/grandparentImplicitReducible.lean b/tests/elab/grandparentImplicitReducible.lean
new file mode 100644
index 0000000000..2398b7e8ea
--- /dev/null
+++ b/tests/elab/grandparentImplicitReducible.lean
@@ -0,0 +1,43 @@
+import Lean
+
+/-!
+# Grandparent subobject projections should be `@[implicit_reducible]`
+
+When `class C extends P₁, P₂` has diamond inheritance, some ancestor structures
+end up as constructor subobject fields even though they aren't direct parents.
+These grandparent projections need `@[implicit_reducible]` so they unfold at
+`.instances` transparency.
+
+For example, with `MyMonoid extends MySemigroup, MyMulOneClass` where both share
+`MyMul`, the structure `MyOne` becomes a constructor subobject of `MyMonoid`
+(it has no overlap with `MySemigroup`). So `MyMonoid.toMyOne` is created by
+`mkProjections` as a subobject projection, but it is NOT a direct parent —
+it's a grandparent reached through `MyMulOneClass`.
+
+Previously, `addParentInstances` only set `@[implicit_reducible]` on direct
+parent projections. This test verifies that grandparent subobject projections
+also receive `@[implicit_reducible]`.
+-/
+
+-- Minimal hierarchy with a diamond via MyMul
+class MyOne (α : Type _) where one : α
+class MyMul (α : Type _) where mul : α → α → α
+class MyMulOneClass (M : Type _) extends MyOne M, MyMul M
+class MySemigroup (G : Type _) extends MyMul G
+class MyMonoid (M : Type _) extends MySemigroup M, MyMulOneClass M
+
+open Lean in
+def showReducibility (n : Name) : CoreM Unit := do
+  IO.println s!"{n}: {repr (← getReducibilityStatus n)}"
+
+/--
+info: MyMonoid.toMySemigroup: Lean.ReducibilityStatus.implicitReducible
+MyMonoid.toMyMulOneClass: Lean.ReducibilityStatus.implicitReducible
+MyMonoid.toMyOne: Lean.ReducibilityStatus.implicitReducible
+-/
+#guard_msgs in
+#eval do
+  showReducibility ``MyMonoid.toMySemigroup
+  showReducibility ``MyMonoid.toMyMulOneClass
+  -- Grandparent subobject projection should also be implicitReducible
+  showReducibility ``MyMonoid.toMyOne