fix: show error messages on name conflicts in mutual blocks

src/Lean/Elab/MutualDef.lean

@@ -981,6 +981,21 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let newHeaders ← (process).run' 1
   newHeaders.mapM fun header => return { header with type := (← instantiateMVarsProfiling header.type) }
 
+/--
+Ensures that all declarations given by `preDefs` have distinct names.
+Remark: we wait to perform this check until the pre-definition phase because we must account for
+auxiliary declarations introduced by `where` and `let rec`.
+-/
+private def checkAllDeclNamesDistinct (preDefs : Array PreDefinition) : TermElabM Unit := do
+  let mut names : Std.HashMap Name Syntax := {}
+  for preDef in preDefs do
+    let userName := privateToUserName preDef.declName
+    if let some dupStx := names[userName]? then
+      let errorMsg := m!"'mutual' block contains two declarations of the same name '{userName}'"
+      Lean.logErrorAt dupStx errorMsg
+      throwErrorAt preDef.ref errorMsg
+    names := names.insert userName preDef.ref
+
 def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
@@ -1014,6 +1029,7 @@ where
         checkLetRecsToLiftTypes funFVars letRecsToLift
         (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc headers else withUsed vars headers values letRecsToLift) fun vars => do
           let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+          checkAllDeclNamesDistinct preDefs
           for preDef in preDefs do
             trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
           let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamTypesPreDecls preDefs

src/Lean/Elab/MutualInductive.lean

@@ -960,6 +960,30 @@ private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabS
         mkInjectiveTheorems e.view.declName
     return res
 
+/-- Ensures that there are no conflicts among or between the type and constructor names defined in `elabs`. -/
+private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) : TermElabM Unit := do
+  let throwErrorsAt (init cur : Syntax) (msg : MessageData) : TermElabM Unit := do
+    logErrorAt init msg
+    throwErrorAt cur msg
+  -- Maps names of inductive types to to `true` and those of constructors to `false`, along with syntax refs
+  let mut uniqueNames : Std.HashMap Name (Bool × Syntax) := {}
+  for { view, .. } in elabs do
+    let typeDeclName := privateToUserName view.declName
+    if let some (prevNameIsType, prevRef) := uniqueNames[typeDeclName]? then
+      if prevNameIsType then
+        throwErrorsAt prevRef view.declId m!"cannot define multiple inductive types with the same name '{typeDeclName}'"
+      else
+        throwErrorsAt prevRef view.declId m!"cannot define an inductive type and a constructor with the same name '{typeDeclName}'"
+    uniqueNames := uniqueNames.insert typeDeclName (true, view.declId)
+    for ctor in view.ctors do
+      let ctorName := privateToUserName ctor.declName
+      if let some (prevNameIsType, prevRef) := uniqueNames[ctorName]? then
+        if prevNameIsType then
+          throwErrorsAt prevRef ctor.declId m!"cannot define an inductive type and a constructor with the same name '{typeDeclName}'"
+        else
+          throwErrorsAt prevRef ctor.declId m!"cannot define multiple constructors with the same name '{ctorName}'"
+      uniqueNames := uniqueNames.insert ctorName (false, ctor.declId)
+
 private def applyComputedFields (indViews : Array InductiveView) : CommandElabM Unit := do
   if indViews.all (·.computedFields.isEmpty) then return
 
@@ -1016,6 +1040,7 @@ def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Uni
   let (elabs, res) ← runTermElabM fun vars => do
     let elabs ← inductives.mapM fun (modifiers, stx) => mkInductiveView modifiers stx
     elabs.forM fun e => checkValidInductiveModifier e.view.modifiers
+    checkNoInductiveNameConflicts elabs
     let res ← elabInductiveViews vars elabs
     pure (elabs, res)
   elabInductiveViewsPostprocessing (elabs.map (·.view)) res

tests/lean/run/6694.lean

@@ -0,0 +1,169 @@
+/-!
+# Duplicate definition names in `mutual` blocks
+
+https://github.com/leanprover/lean4/issues/6694
+
+Definitions with conflicting names in `mutual` blocks should report errors rather than silently
+failing or producing invalid entries in the environment.
+-/
+
+/--
+error: 'mutual' block contains two declarations of the same name 'foo'
+---
+error: 'mutual' block contains two declarations of the same name 'foo'
+-/
+#guard_msgs in
+mutual
+def foo := ()
+
+def foo := ()
+end
+/-- error: unknown identifier 'foo' -/
+#guard_msgs in #check foo
+
+/--
+error: 'mutual' block contains two declarations of the same name 'foo'
+---
+error: 'mutual' block contains two declarations of the same name 'foo'
+-/
+#guard_msgs in
+mutual
+private def foo := ()
+
+def foo := ()
+end
+/-- error: unknown identifier 'foo' -/
+#guard_msgs in #check foo
+
+/--
+error: 'mutual' block contains two declarations of the same name 'y.z'
+---
+error: 'mutual' block contains two declarations of the same name 'y.z'
+-/
+#guard_msgs in
+mutual
+def y :=
+  let rec z := 3
+  z + 2
+
+def y.z := 42
+end
+/-- error: unknown identifier 'y' -/
+#guard_msgs in #check y
+/-- error: unknown identifier 'y.z' -/
+#guard_msgs in #check y.z
+
+/--
+error: 'mutual' block contains two declarations of the same name 'a.b'
+---
+error: 'mutual' block contains two declarations of the same name 'a.b'
+-/
+#guard_msgs in
+mutual
+def a :=
+  let rec b := 4
+  b + 2
+
+def a.b := 42
+end
+/-- error: unknown identifier 'a' -/
+#guard_msgs in #check a
+/-- error: unknown identifier 'a.b' -/
+#guard_msgs in #check a.b
+
+/--
+error: cannot define an inductive type and a constructor with the same name 'Bar.foo'
+---
+error: cannot define an inductive type and a constructor with the same name 'Bar.foo'
+-/
+#guard_msgs in
+mutual
+  inductive Bar
+  | foo : Bar
+
+  inductive Bar.foo
+  | mk : Bar.foo
+end
+/-- error: unknown identifier 'Bar' -/
+#guard_msgs in #check Bar
+/-- error: unknown identifier 'Bar.foo' -/
+#guard_msgs in #check Bar.foo
+/-- error: unknown identifier 'Bar.foo.mk' -/
+#guard_msgs in #check Bar.foo.mk
+
+/--
+error: cannot define multiple inductive types with the same name 'Private'
+---
+error: cannot define multiple inductive types with the same name 'Private'
+-/
+#guard_msgs in
+mutual
+  private inductive Private
+  | mk
+
+  inductive Private
+  | mk
+end
+/-- error: unknown identifier 'Private' -/
+#guard_msgs in #check Private
+/-- error: unknown identifier 'Private.mk' -/
+#guard_msgs in #check Private.mk
+
+/--
+error: cannot define an inductive type and a constructor with the same name 'PrivateConstructor.priv'
+---
+error: cannot define an inductive type and a constructor with the same name 'PrivateConstructor.priv'
+-/
+#guard_msgs in
+mutual
+  inductive PrivateConstructor
+  | private priv
+
+  inductive PrivateConstructor.priv
+  | mk
+end
+/-- error: unknown identifier 'PrivateConstructor' -/
+#guard_msgs in #check PrivateConstructor
+/-- error: unknown identifier 'PrivateConstructor.priv' -/
+#guard_msgs in #check PrivateConstructor.priv
+
+/--
+error: cannot define multiple constructors with the same name 'Baz.foo.mk'
+---
+error: cannot define multiple constructors with the same name 'Baz.foo.mk'
+-/
+#guard_msgs in
+mutual
+  inductive Baz
+  | foo.mk : Baz
+
+  inductive Baz.foo
+  | mk : Baz.foo
+end
+/-- error: unknown identifier 'Baz' -/
+#guard_msgs in #check Baz
+/-- error: unknown identifier 'Baz.foo' -/
+#guard_msgs in #check Baz.foo
+/-- error: unknown identifier 'Baz.foo.mk' -/
+#guard_msgs in #check Baz.foo.mk
+
+/--
+error: cannot define multiple inductive types with the same name 'Foo'
+---
+error: cannot define multiple inductive types with the same name 'Foo'
+-/
+#guard_msgs in
+mutual
+  inductive Foo
+  | bar : Foo
+
+  inductive Foo
+  | bar : Foo
+  | foo : Foo → Foo
+end
+/-- error: unknown identifier 'Foo' -/
+#guard_msgs in #check Foo
+/-- error: unknown identifier 'Foo.bar' -/
+#guard_msgs in #check Foo.bar
+/-- error: unknown identifier 'Foo.foo' -/
+#guard_msgs in #check Foo.foo