fix: recursively copy subfields in diamond extends

src/Lean/Elab/Structure.lean

@@ -446,7 +446,12 @@ where
                 trace[Meta.debug] "composite, {fieldName} := {fieldVal}"
                 copy (i+1) infos (fieldMap.insert fieldName fieldVal) expandedStructNames
             else
-              addNewField
+              let subfieldNames := getStructureFieldsFlattened (← getEnv) fieldParentStructName
+              let fieldName := fieldInfo.fieldName
+              withLocalDecl fieldName fieldInfo.binderInfo fieldType fun parentFVar =>
+                let infos := infos.push { name := fieldName, declName := structDeclName ++ fieldName, fvar := parentFVar, kind := StructFieldKind.subobject }
+                processSubfields structDeclName parentFVar fieldParentStructName subfieldNames infos fun infos =>
+                  copy (i+1) infos (fieldMap.insert fieldName parentFVar) expandedStructNames
           else
             addNewField
       else
@@ -468,7 +473,7 @@ where
     for fieldName in getStructureFields env parentStructName do
       match fieldMap.find? fieldName with
       | some val => result := mkApp result val
-      | none => throwError "failed to copied fields from parent structure{indentExpr parentType}" -- TODO improve error message
+      | none => throwError "failed to copy fields from parent structure{indentExpr parentType}" -- TODO improve error message
     return result
 
 private partial def mkToParentName (parentStructName : Name) (p : Name → Bool) : Name := Id.run <| do

tests/lean/diamond8.lean

@@ -0,0 +1,24 @@
+class One (M : Type u) where one : M
+instance {M} [One M] : OfNat M (nat_lit 1) := ⟨One.one⟩
+
+class Zero (A : Type u) where zero : A
+instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
+
+class Monoid (M : Type u) extends Mul M, One M where
+  mul_one (m : M) : m * 1 = m
+
+class AddCommMonoid (A : Type u) extends Add A, Zero A
+
+class MonoidWithZero (M₀ : Type u) extends Monoid M₀, Zero M₀
+
+class Semiring (R : Type u) extends AddCommMonoid R, MonoidWithZero R, One R
+
+#print Semiring -- only toMonoid field, no duplicate toOne
+
+def oneViaMonoid {M} [Monoid M] : M := 1
+example {R} [Semiring R] : (1 : R) = oneViaMonoid := rfl
+
+example : Semiring Nat where
+  mul_one := by simp
+  zero := 0
+  one := 1

tests/lean/diamond8.lean.expected.out

@@ -0,0 +1,3 @@
+inductive Semiring.{u} : Type u → Type u
+constructors:
+Semiring.mk : {R : Type u} → [toAddCommMonoid : AddCommMonoid R] → [toMonoid : Monoid R] → Semiring R