open not opening a namespace

Stream: lean4

[Michael Stoll]

Is the following behavior intended?

def A.foo : Nat := 37

namespace B.A

open A

/- unknown identifier 'foo' -/
#check foo

I would expect open A to open _root_.A even though the current namespace ends with .A.

[Michael Stoll]

Compare with

def A.foo : Nat := 37

namespace B

open A

/- A.foo : Nat -/
#check foo

[Kyle Miller]

I'm a bit surprised by this, because when I last read the open source code, open A opens all namespaces that A resolves to.

[Kenny Lau]

since there has been no feedback for a while, I've done some more digging, and I've traced it back to how Lean interprets syntax itself

import Lean

def A.B.foo1 := 3
def B.foo2 := 3

section Test1
namespace A
-- ... [Lean.Syntax.Preresolved.namespace `A.B]
#eval `(ident|B)
end A
end Test1

section Test2
open A
-- ... [Lean.Syntax.Preresolved.namespace `B, Lean.Syntax.Preresolved.namespace `A.B]
#eval `(ident|B)
end Test2

[Kenny Lau]

Lean decides what to open based on how it interprets the syntax, and in this case we can see that in Test1, at the level of syntax already something has gone wrong, where the namespace `B didn't get detected at all

[Kenny Lau]

and my intuition is that further digging might require reading C++ code

[Kenny Lau]

@Kyle Miller might you have any clue?

[Kenny Lau]

lean4#11014

[Robin Arnez]

I think the reason is that when you have a setup like this:

def foo := 7

namespace A

def foo := 3

#eval foo

end A

we want the #eval foo to use the foo from the inner namespace and not the outer namespace; but if we resolved to both A.foo and _root_.foo, we'd get an "ambiguous identifier" error. So we only resolve to the inner identifier and ignore the outer ones. This might not be the right behavior though when we expect multiple resolutions like in open.

[Kenny Lau]

@Robin Arnez do you have a proposed solution

[Robin Arnez]

Well, we could explicitly distinguish between these two cases in name resolution using some kind of flag but I'm not quite sure whether that's a good idea