fix: structure command diamond support

Fixes issue described at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structure.20diamond.20error

src/Lean/Elab/Structure.lean

@@ -310,11 +310,12 @@ where
     else
       return none
 
+/-- Auxiliary method for `copyNewFieldsFrom`. -/
 private def getFieldType (infos : Array StructFieldInfo) (parentStructName : Name) (parentType : Expr) (fieldName : Name) : MetaM Expr := do
   withLocalDeclD (← mkFreshId) parentType fun parent => do
     let proj ← mkProjection parent fieldName
     let projType ← inferType proj
-    /- Eliminate occurrences of `parent`. This may happen when structure contains dependent fields -/
+    /- Eliminate occurrences of `parent`. This may happen when structure contains dependent fields. -/
     let visit (e : Expr) : MetaM TransformStep := do
       if let some fieldName ← isProjectionOf? e parentStructName parent then
         -- trace[Meta.debug] "field '{fieldName}' of {e}"
@@ -322,8 +323,8 @@ private def getFieldType (infos : Array StructFieldInfo) (parentStructName : Nam
         | some existingFieldInfo => return TransformStep.done existingFieldInfo.fvar
         | none => throwError "unexpected field access {indentExpr e}"
       else
-        return TransformStep.visit e
-    Meta.transform projType (pre := visit)
+        return TransformStep.done e
+    Meta.transform projType (post := visit)
 
 private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility := do
   if isProtected (← getEnv) fieldInfo.projFn then

tests/lean/run/diamond5.lean

@@ -0,0 +1,10 @@
+class Semigroup (G : Type u) extends Mul G
+
+class Numeric (α : Type u)
+
+class Monoid (M : Type u) extends Semigroup M, Numeric M where
+  mul_one (m : M) : m * m = m
+
+class AddMonoid (A : Type u) extends Numeric A
+
+class Semiring (R : Type u) extends AddMonoid R, Monoid R