diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index d0c8e1b507..2bb56fc7ff 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/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
diff --git a/tests/lean/diamond5.lean b/tests/lean/diamond5.lean
new file mode 100644
index 0000000000..8bbf84b5a3
--- /dev/null
+++ b/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 α
diff --git a/tests/lean/diamond5.lean.expected.out b/tests/lean/diamond5.lean.expected.out
new file mode 100644
index 0000000000..d65a684fc4
--- /dev/null
+++ b/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