fix: binder annotation for class diamond coercions

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

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 }

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 }

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

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)