Resolution with duplicated namespaces

[Vtec234]

Description

In the following snippet, should the definition that fails actually succeed in resolving Bar?

set_option autoImplicit false

namespace Foo.Bar
abbrev Bar := Nat
end Foo.Bar

open Foo Bar in
def myNat1 : Bar := 10 -- good

namespace Bar
end Bar

open Foo Bar in
/- unknown identifier 'Bar' -/
def myNat2 : Bar := 10

open Foo.Bar in
def myNat3 : Bar := 10 -- good

open Foo Bar in
def myNat4 : Bar.Bar := 10 -- good

A concrete instance of this occurs with Lean.Elab.Tactic.Tactic and a top-level Tactic namespace defined in mathlib4. Another possible solution to avoid confusion might be to forbid defining symbols with the same name as the innermost namespace, in that namespace. For example def Foo.Foo would be forbidden throw an error when an open statement is ambiguous due to multiple possible namespaces (in this case Foo.Bar and Bar) that could be opened.

Steps to Reproduce

1. Run the snippet

Expected behavior: Bar is resolved in all cases, maybe. I am not certain what namespace resolution should do here.

Actual behavior: The first definition fails.

Reproduces how often: 100%

Versions

nightly-2022-06-13

[Vtec234]

My apologies, false alarm. It is actually a mathlib4 issue. Reopening with a new repro.

[leodemoura]

@Vtec234 The behavior is consistent with the spec we have at resolveNamespace?.

/--
Given a name `id` try to find namespace it refers to. The resolution procedure works as follows
1- If `id` is in the scope of `namespace` commands the namespace `s_1. ... . s_n`,
   then return `s_1 . ... . s_i ++ n` if it is the name of an existing namespace. We search "backwards".
2- If `id` is the extact name of an existing namespace, then return `id`

3- Finally, for each command `open N`, return `N ++ n` if it is the name of an existing namespace.
   We search "backwards" again. That is, we try the most recent `open` command first.
   We only consider simple `open` commands.
-/

It would be great to get community consensus before changing it.

[gebner]

Oh yes, the open Tactic issue! Note that we already run into this in core:

import Lean

open Lean Parser Elab Tactic
-- only one of the following works, depending on the order of Parser and Elab!

#check rwRule
#check evalDSimp

FWIW, I would have expected open Tactic to open both Lean.Parser.Tactic and Lean.Elab.Tactic here. I find it counterintuitive if Parser.Tactic.rwRule works but open Parser in Tactic.rwRule doesn't.

Another option that addresses this issue is to reduce the amount of namespaces. I "usually" write open Lean Elab Term Command Meta ... at the beginning of a file, I wouldn't mind if everything was directly in the Lean namespace. Even in core it's rare to use qualified names. We have quite a few definitions that have the same name but are in different namespaces, but I find that more confusing than helpful tbh. For example we have three functions called ppExpr with (sometimes subtly) different behavior and signatures. Or getMVarDecl which comes in two versions, one of which is strictly more useful than the other.

[Kha]

To be honest, for the longest time I wasn't even aware that, unlike with import, we allow relative opens. I'm not really bothered by the verbosity, though I guess @gebner wouldn't be happy with further increasing it 😄 .
One alternative way to decrease it could be to allow more expressive exports after all, such that you e.g. get Lean.Meta for free when opening Lean.Tactic as that is basically always the right thing to do. Not sure what the best practices on module structuring and reexporting in e.g. Rust would say about this.

[Kha]

This change seems to have broken a few documentation examples of the form

namespace Ex
class Inhabited (a : Type _) where
 default : a
export Inhabited (default)

#eval (default : Nat)  -- error: ambiguous, possible interpretations Inhabited.default : Nat, _root_.Inhabited.default : Nat

(which I only found out because I was wondering why the Nix cache was empty 😆 ).

[Kha]

Not sure I want to open this can of worms right now, but I've wondered before whether export should be strengthened to behave as if the exported declarations were declared in the target namespace, i.e. also supported in name resolution such as Ex.default for the example above. I.e. like reexports in other languages such as Rust. Then the expected behavior of the code would be clear at least: the exported default should be preferred just like a direct declaration Ex.default would have been preferred.

[leodemoura]

@Kha I will fix the issue above.