fix: fixes #2178

src/Lean/Elab/Structure.lean

@@ -410,14 +410,15 @@ where
         | none =>
           let some fieldInfo := getFieldInfo? (← getEnv) parentStructName fieldName | unreachable!
           let addNewField : TermElabM α := do
-            let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName
             withLocalDecl fieldName fieldInfo.binderInfo fieldType fun fieldFVar => do
+              let fieldMap := fieldMap.insert fieldName fieldFVar
+              let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName
               let fieldDeclName := structDeclName ++ fieldName
               let fieldDeclName ← applyVisibility (← toVisibility fieldInfo) fieldDeclName
               addDocString' fieldDeclName (← findDocString? (← getEnv) fieldInfo.projFn)
               let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value?,
                                         kind := StructFieldKind.copiedField }
-              copy (i+1) infos (fieldMap.insert fieldName fieldFVar) expandedStructNames
+              copy (i+1) infos fieldMap expandedStructNames
           if fieldInfo.subobject?.isSome then
             let fieldParentStructName ← getStructureName fieldType
             if (← findExistingField? infos fieldParentStructName).isSome then

tests/lean/2178.lean

@@ -0,0 +1,10 @@
+class Zero (α : Type u) where
+  zero : α
+class AddZeroClass (M : Type u) extends Zero M, Add M
+class AddMonoid (M : Type u) extends AddZeroClass M where
+  nsmul : Nat → M → M := fun _ _ => Zero.zero
+class AddCommMonoid (M : Type u) extends Zero M, AddMonoid M
+class AddMonoidWithOne (R : Type u) extends AddMonoid R
+class AddCommMonoidWithOne (R : Type u) extends AddMonoidWithOne R, AddCommMonoid R
+class NonAssocSemiring (α : Type u) extends Zero α, AddCommMonoidWithOne α
+class Semiring (α : Type u) extends Zero α, NonAssocSemiring α