`resolveUniqueNamespace` fails even when all namespace resolution candidates are equal

Prerequisites

• 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

resolveUniqueNamespace errors with "ambiguous namespace" if the candidates are not a singleton list. However, it can happen that the list is non-singleton, but contains all identical entries (for example, if the opened namespace appended to the current namespace is a namespace, and the open decls produce the same namespace). This affects e.g. open hiding occasionally, which relies on resolveUniqueNamespace.

This can happen when the current namespace is opened:

namespace Foo.Bar
-- register namespace(s)
end Foo.Bar

open Foo
namespace Foo

/-- error: ambiguous namespace `Bar`, possible interpretations: `[Foo.Bar, Foo.Bar]` -/
#guard_msgs in
open Bar hiding foo

Context

This occurs because in resolveNamespace we simply prepend any successful return of resolveNamespaceUsingScope? to what resolveNamespaceUsingOpenDecls gives us, even if it already exists in the list:

def resolveNamespace (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List Name :=
  match resolveNamespaceUsingScope? env id ns with
  | some ns => ns :: resolveNamespaceUsingOpenDecls env id openDecls
  | none => resolveNamespaceUsingOpenDecls env id openDecls

and then demand a singleton list inside of resolveUniqueNamespace.

Steps to Reproduce

1. Open a namespace ns and set it as the current namespace.
2. Try to resolve as a unique namespace a name n such that ns ++ n is a namespace.

Expected behavior: We resolve to ns ++ n.

Actual behavior: We error, claiming that ns ++ n is ambiguous due to producing the resolutions [ns ++ n, ns ++ n].

Versions

Lean 4.31.0-nightly-2026-04-09
(Lean web)

Additional Information

The duplication in the output of resolveNamespace also results in duplicate OpenDecls in the scope after ordinary opens, but this doesn't seem to be an issue.

Impact

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

Start with the minimal Lean example in the issue and read resolveNamespace and resolveUniqueNamespace, especially how scope and open-declaration results are combined. Confirm the reproduced [Foo.Bar, Foo.Bar] case and use it as a regression test; done means the example resolves Foo.Bar without an ambiguous-namespace error.