From 7c9158a50e81db0b612bfc142bb24c31a5634de3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Aug 2021 07:45:21 -0700
Subject: [PATCH] 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 |  7 ++++---
 tests/lean/run/diamond5.lean | 10 ++++++++++
 2 files changed, 14 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/diamond5.lean

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 9ffeb64ceb..644bdab741 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/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
diff --git a/tests/lean/run/diamond5.lean b/tests/lean/run/diamond5.lean
new file mode 100644
index 0000000000..25f7f30b61
--- /dev/null
+++ b/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