`export`ed declarations may cause ambiguity without warning

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

If a declaration Foo.bar is exported to, for example, the root namespace, and then a subsequent declaration bar is created. Lean does not warn the user that (a synonym for) the declaration already exists. This leads to ambiguity errors when trying to use bar, and then the user must supply the prefix (either Foo.bar or _root_.bar). Likewise, if _root_.baz is declared, then Foo.baz is created and then we export (Foo) baz, there is no warning.

Context

This was found in the context of Classical.not_imp and _root_.not_imp on the Lean Zulip by @jcommelin.

Steps to Reproduce

theorem Foo.bar : True := .intro

export Foo (bar)

theorem bar : True := .intro

/-
ambiguous, possible interpretations 
  _root_.bar : True
  
  Foo.bar : True
-/
example : True := bar



theorem baz : True := .intro

theorem Foo.baz : True := .intro

export Foo (baz)

/-
ambiguous, possible interpretations 
  _root_.baz : True
  
  Foo.baz : True
-/
example : True := baz

Expected behavior: When creating synonyms with export or when adding declarations to the environment, Lean should warn the user if doing so results in ambiguity.

Actual behavior: Lean issues no such warning and the user only finds out when trying to use the ambiguous names.

Versions

4.12.0-nightly-2024-09-04

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal Lean reproducer from the issue against a current nightly release and confirm the two export-order cases. Trace the declaration and export handling involved in name resolution. Done means both cases emit a warning when the synonym creates ambiguity, rather than failing only when the ambiguous name is used.