From 0f184a8c9394143244158e303df9638a29e72f55 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Aug 2021 06:51:50 -0700
Subject: [PATCH] fix: binder annotation for class diamond coercions

---
 src/Lean/Elab/Structure.lean          | 11 ++++++-----
 tests/lean/diamond2.lean.expected.out |  3 +--
 tests/lean/diamond3.lean.expected.out |  2 +-
 tests/lean/diamond4.lean              | 18 ++++++++++++++++++
 tests/lean/diamond4.lean.expected.out |  4 ++++
 5 files changed, 30 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/diamond4.lean
 create mode 100644 tests/lean/diamond4.lean.expected.out

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 341b3d3738..11b410561a 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -611,15 +611,16 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
       setReducibleAttribute declName
 
 private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentType : Expr) : MetaM Unit := do
+  let env ← getEnv
   let structName := view.declName
-  let sourceFieldNames := getStructureFieldsFlattened (← getEnv) structName
+  let sourceFieldNames := getStructureFieldsFlattened env structName
   let structType ← mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
-  -- TODO: binder annotation for instances
-  withLocalDeclD `source structType fun source => do
-    let declType ← mkForallFVars params (← mkArrow structType parentType)
+  let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
+  let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
+  withLocalDecl `self binfo structType fun source => do
+    let declType ← mkForallFVars params (← mkForallFVars #[source] parentType)
     let declType := declType.inferImplicit params.size true
     let rec copyFields (parentType : Expr) : MetaM Expr := do
-      let env ← getEnv
       let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
       let parentCtor := getStructureCtor env parentStructName
       let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs
diff --git a/tests/lean/diamond2.lean.expected.out b/tests/lean/diamond2.lean.expected.out
index af734bec51..b6af9fdbbd 100644
--- a/tests/lean/diamond2.lean.expected.out
+++ b/tests/lean/diamond2.lean.expected.out
@@ -3,5 +3,4 @@ Foo2.mk : {α : Type} → Bar (α → α) → (β : Type) → (α → β) → α
 def Foo2.toBar : {α : Type} → Foo2 α → Bar (α → α) :=
 fun α self => self.1
 def Foo2.toBoo2 : {α : Type} → Foo2 α → Boo2 α :=
-fun α source =>
-  { toBoo1 := { toBaz := { a := source.toBar.a, β := _, b := source.b }, x1 := source.x1 }, x2 := source.x2 }
+fun α self => { toBoo1 := { toBaz := { a := self.toBar.a, β := _, b := self.b }, x1 := self.x1 }, x2 := self.x2 }
diff --git a/tests/lean/diamond3.lean.expected.out b/tests/lean/diamond3.lean.expected.out
index eded9a403e..7cc457450d 100644
--- a/tests/lean/diamond3.lean.expected.out
+++ b/tests/lean/diamond3.lean.expected.out
@@ -1,2 +1,2 @@
 def D.toC : D → C :=
-fun source => { toA := source.toB.toA, w := source.w }
+fun self => { toA := self.toB.toA, w := self.w }
diff --git a/tests/lean/diamond4.lean b/tests/lean/diamond4.lean
new file mode 100644
index 0000000000..89d476bafd
--- /dev/null
+++ b/tests/lean/diamond4.lean
@@ -0,0 +1,18 @@
+class A (α : Type) where
+  one  : α
+  zero : α
+
+class B (α : Type) extends A α where
+  add : α → α → α
+
+class C (α : Type) extends A α where
+  mul : α → α → α
+
+set_option structureDiamondWarning false
+
+class D (α : Type) extends B α, C α
+
+set_option pp.all true
+
+#print D.toB
+#print D.toC
diff --git a/tests/lean/diamond4.lean.expected.out b/tests/lean/diamond4.lean.expected.out
new file mode 100644
index 0000000000..cc6eaed440
--- /dev/null
+++ b/tests/lean/diamond4.lean.expected.out
@@ -0,0 +1,4 @@
+def D.toB : {α : Type} → [self : D α] → B α :=
+fun (α : Type) [self : D α] => self.1
+def D.toC : {α : Type} → [self : D α] → C α :=
+fun (α : Type) [self : D α] => @C.mk α (@B.toA α (@D.toB α self)) (@D.mul α self)