From 74bd537465b650eb5796beda971619dcba4824e9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Aug 2021 17:23:18 -0700
Subject: [PATCH] fix: generation of `to*` field names

---
 src/Lean/Elab/Structure.lean                  | 21 +++++-----
 tests/lean/diamond5.lean                      |  2 +
 tests/lean/diamond5.lean.expected.out         |  2 +-
 tests/lean/toFieldNameIssue.lean              | 39 +++++++++++++++++++
 tests/lean/toFieldNameIssue.lean.expected.out |  4 ++
 5 files changed, 58 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/toFieldNameIssue.lean
 create mode 100644 tests/lean/toFieldNameIssue.lean.expected.out

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 1f3813044c11..9ffeb64ceb8f 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -467,8 +467,15 @@ where
       | none => throwError "failed to copied fields from parent structure{indentExpr parentType}" -- TODO improve error message
     return result
 
-private def mkToParentName (parentStructName : Name) : Name :=
-  Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString! -- erase macro scopes?
+private partial def mkToParentName (parentStructName : Name) (p : Name → Bool) : Name := do
+  let base := Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString!
+  if p base then
+    base
+  else
+    let rec go (i : Nat) : Name :=
+      let curr := base.appendIndexAfter i
+      if p curr then curr else go (i+1)
+    go 1
 
 private partial def withParents (view : StructView) (k : Array StructFieldInfo → Array Expr → TermElabM α) : TermElabM α := do
   go 0 #[] #[]
@@ -485,14 +492,12 @@ where
         copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos (copiedParents.push parentType)
         -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure`
       else
-        let toParentName := mkToParentName parentStructName
-        if containsFieldName infos toParentName then
-          throwErrorAt parentStx "field '{toParentName}' has already been declared"
         let env ← getEnv
+        let subfieldNames := getStructureFieldsFlattened env parentStructName
+        let toParentName := mkToParentName parentStructName fun n => !containsFieldName infos n && !subfieldNames.contains n
         let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
         withLocalDecl toParentName binfo parentType fun parentFVar =>
           let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject }
-          let subfieldNames := getStructureFieldsFlattened env parentStructName
           processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => go (i+1) infos copiedParents
     else
       k infos copiedParents
@@ -762,9 +767,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
           result := mkApp result fieldVal
       return result
     let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType)))
-    let declName := structName ++ mkToParentName (← getStructureName parentType)
-    if env.contains declName then
-      throwError "failed to create coercion '{declName}' to parent structure '{parentStructName}', environment already contains a declaration with the same name"
+    let declName := structName ++ mkToParentName (← getStructureName parentType) fun n => !env.contains (structName ++ n)
     addAndCompile <| Declaration.defnDecl {
       name        := declName
       levelParams := levelParams
diff --git a/tests/lean/diamond5.lean b/tests/lean/diamond5.lean
index 8bbf84b5a3aa..c08e31898804 100644
--- a/tests/lean/diamond5.lean
+++ b/tests/lean/diamond5.lean
@@ -13,3 +13,5 @@ set_option structureDiamondWarning false
 def D.toC (x : Nat) := x
 
 class D (α : Type) extends B α, C α
+
+#check @D.toC_1
diff --git a/tests/lean/diamond5.lean.expected.out b/tests/lean/diamond5.lean.expected.out
index d65a684fc487..0fb80ebdc123 100644
--- a/tests/lean/diamond5.lean.expected.out
+++ b/tests/lean/diamond5.lean.expected.out
@@ -1 +1 @@
-diamond5.lean:15:32-15:35: error: failed to create coercion 'D.toC' to parent structure 'C', environment already contains a declaration with the same name
+D.toC_1 : {α : Type} → [self : D α] → C α
diff --git a/tests/lean/toFieldNameIssue.lean b/tests/lean/toFieldNameIssue.lean
new file mode 100644
index 000000000000..abd3f37eb4e1
--- /dev/null
+++ b/tests/lean/toFieldNameIssue.lean
@@ -0,0 +1,39 @@
+structure Foo.A where
+  x : Nat
+
+structure Boo.A extends Foo.A where
+  y : Nat
+
+structure B extends Boo.A where
+  z : Nat
+
+def f1 (x y z : Nat) : B :=
+  { x, y, z }
+
+theorem ex1 (x y z : Nat) : f1 x y z = ⟨⟨⟨x⟩, y⟩, z⟩ :=
+  rfl
+
+theorem ex2 (x y z : Nat) : f1 x y z = B.mk (Boo.A.mk (Foo.A.mk x) y) z :=
+  rfl
+
+#check { x := 0, y := 1, z := 2 : B }
+
+structure Foo.C where
+  x : Nat
+  y : Nat
+
+structure Boo.C where
+  x : Nat
+  z : Nat
+
+structure D extends Foo.C, Boo.C
+
+def f2 (x y z : Nat) : D :=
+  { x, y, z }
+
+theorem ex3 (x y z : Nat) : f2 x y z = D.mk ⟨x, y⟩ z :=
+  rfl
+
+#check { x := 0, y := 1, z := 2 : D }
+
+#print D.toC_1
diff --git a/tests/lean/toFieldNameIssue.lean.expected.out b/tests/lean/toFieldNameIssue.lean.expected.out
new file mode 100644
index 000000000000..97a017679502
--- /dev/null
+++ b/tests/lean/toFieldNameIssue.lean.expected.out
@@ -0,0 +1,4 @@
+{ toA_1 := { toA := { x := 0 }, y := 1 }, z := 2 } : B
+{ toC := { x := 0, y := 1 }, z := 2 } : D
+def D.toC_1 : D → Boo.C :=
+fun self => { x := self.toC.x, z := self.z }