feat: warnings when declarations and export aliases conflict

src/Lean/Elab/BuiltinCommand.lean

@@ -139,7 +139,17 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
     let declName ← resolveNameUsingNamespaces nss idStx
     if (← getInfoState).enabled then
       addConstInfo idStx declName
-    aliases := aliases.push (currNamespace ++ id, declName)
+    let a := currNamespace ++ id
+    aliases := aliases.push (a, declName)
+    -- Is this alias shadowing a declaration?
+    if (← getEnv).contains a then
+      Linter.logLintIf linter.aliasConflict idStx m!"'{.ofConstName a true}' is an existing declaration and this alias may lead to ambiguities"
+    -- Is this alias conflicting with other aliases?
+    let aliases' := getAliases (← getEnv) a (skipProtected := false)
+    unless aliases'.isEmpty do
+      let aliases' := aliases'.map fun alias => m!"'{.ofConstName alias (fullNames := true)}'"
+      Linter.logLintIf linter.aliasConflict (← getRef) m!"\
+        '{a}' already exists as an alias for the following declaration(s) and may lead to ambiguities: {MessageData.joinSep aliases' ", "}"
   modify fun s => { s with env := aliases.foldl (init := s.env) fun env p => addAlias env p.1 p.2 }
 
 @[builtin_command_elab «open»] def elabOpen : CommandElab

src/Lean/Elab/DeclModifiers.lean

@@ -6,15 +6,21 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 prelude
 import Lean.Structure
 import Lean.Elab.Attributes
+import Lean.Linter.Basic
 
 namespace Lean.Elab
 
+register_builtin_option linter.aliasConflict : Bool := {
+  defValue := true
+  descr := "enables warnings when declarations and aliases are in conflict"
+}
+
 /--
 Ensure the environment does not contain a declaration with name `declName`.
 Recall that a private declaration cannot shadow a non-private one and vice-versa, although
 they internally have different names.
 -/
-def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (declName : Name) : m Unit := do
+def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
   let env ← getEnv
   let addInfo declName := do
     pushInfoLeaf <| .ofTermInfo {
@@ -38,6 +44,12 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo
     if env.contains declName then
       addInfo declName
       throwError "a non-private declaration '{.ofConstName declName true}' has already been declared"
+  -- Check for aliases that could conflict with this declaration.
+  let aliases := getAliases env declName (skipProtected := false)
+  unless aliases.isEmpty do
+    let aliases' := aliases.map fun alias => m!"'{.ofConstName alias (fullNames := true)}'"
+    Linter.logLintIf linter.aliasConflict (← getRef) m!"\
+      '{declName}' exists as an alias for the following declaration(s) and may lead to ambiguities: {MessageData.joinSep aliases' ", "}"
 
 /-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/
 inductive Visibility where

tests/lean/run/5258.lean

@@ -0,0 +1,49 @@
+/-!
+# Detect when `export` may lead to ambiguities
+https://github.com/leanprover/lean4/issues/5258
+-/
+
+set_option linter.aliasConflict true
+
+theorem Foo.bar : True := .intro
+
+export Foo (bar)
+
+/-!
+Warning when adding a declaration on top of an alias.
+-/
+/--
+warning: 'bar' exists as an alias for the following declaration(s) and may lead to ambiguities: 'Foo.bar'
+note: this linter can be disabled with `set_option linter.aliasConflict false`
+-/
+#guard_msgs in
+theorem bar : True := .intro
+
+theorem baz : True := .intro
+
+theorem Foo.baz : True := .intro
+
+/-!
+Warning when adding an alias on top of a declaration.
+-/
+/--
+warning: 'baz' is an existing declaration and this alias may lead to ambiguities
+note: this linter can be disabled with `set_option linter.aliasConflict false`
+-/
+#guard_msgs in
+export Foo (baz)
+
+theorem Foo'.baz : True := .intro
+
+/-!
+Warning when adding an alias on top of both an alias and a declaration.
+-/
+/--
+warning: 'baz' is an existing declaration and this alias may lead to ambiguities
+note: this linter can be disabled with `set_option linter.aliasConflict false`
+---
+warning: 'baz' already exists as an alias for the following declaration(s) and may lead to ambiguities: 'Foo.baz'
+note: this linter can be disabled with `set_option linter.aliasConflict false`
+-/
+#guard_msgs in
+export Foo' (baz)