diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index aa12a26b5d..8f4857b77c 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -448,6 +448,9 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
       setReducibleAttribute declName
 
 private def elabStructureView (view : StructView) : TermElabM Unit := do
+  view.fields.forM fun field => do
+    if field.declName == view.ctor.declName then
+      throwErrorAt! field.ref "invalid field name '{field.name}', it is equal to structure constructor name"
   let numExplicitParams := view.params.size
   let type ← Term.elabType view.type
   unless validStructType type do throwErrorAt view.type "expected Type"
diff --git a/tests/lean/invalidFieldName.lean b/tests/lean/invalidFieldName.lean
new file mode 100644
index 0000000000..38028a9d8e
--- /dev/null
+++ b/tests/lean/invalidFieldName.lean
@@ -0,0 +1,4 @@
+structure Map (α β : Type) where
+  map    : Type
+  mk     : map
+  insert : map → α → β → map
diff --git a/tests/lean/invalidFieldName.lean.expected.out b/tests/lean/invalidFieldName.lean.expected.out
new file mode 100644
index 0000000000..9120ff47cf
--- /dev/null
+++ b/tests/lean/invalidFieldName.lean.expected.out
@@ -0,0 +1 @@
+invalidFieldName.lean:3:2: error: invalid field name 'mk', it is equal to structure constructor name