feat: better error message

src/Lean/Elab/Structure.lean

@@ -639,7 +639,8 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
       return result
     let declVal ← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType))
     let declName := structName ++ mkToParentName (← getStructureName parentType)
-    -- TODO: nice error message if `declName` already exists
+    if env.contains declName then
+      throwError "failed to create coercion '{declName}' to parent structure '{parentStructName}', environment already contains a declaration with the same name"
     addAndCompile <| Declaration.defnDecl {
       name        := declName
       levelParams := levelParams

tests/lean/diamond5.lean

@@ -0,0 +1,15 @@
+class A (α : Type) where
+  one  : α
+  zero : α
+
+class B (α : Type) extends A α where
+  add : α → α → α
+
+class C (α : Type) extends A α where
+  mul : α → α → α
+
+set_option structureDiamondWarning false
+
+def D.toC (x : Nat) := x
+
+class D (α : Type) extends B α, C α

tests/lean/diamond5.lean.expected.out

@@ -0,0 +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