def _root_... creates literal _root_ namespace

[Kha]

namespace Foo
def _root_.bar := 1
end Foo
#check bar
#check Foo._root_.bar

Expected behavior: for the first #check to work

Actual behavior: the second #check unexpectedly works

[leodemoura]

We should not create a _root_ namespace, and this part is a bug and should be fixed.
This issue also proposes a new feature, the ability to add a declaration to the "root" namespace without closing the current one. I view this feature as a low priority and don't want to think about it right now. For example, what can this feature break? Do we have to change how we process attributes?

[Kha]

Yeah, not accepting the second check is good enough for now

[leodemoura]

@gebner Is this feature important for the mathlib port?

[digama0]

Yes, this feature was implemented in lean 3 and gets some use. It's not incredibly common but there isn't any obvious way for synport to drop in an alternative without significantly changing the surrounding syntax (closing all the namespaces, adding the definition, reopening the namespace and adding all the variables and local things back...)

[gebner]

It's not incredibly common

To give concrete numbers, it occurs 651 times in mathlib.

We might also need it to override instance names in the port: leanprover-community/mathport#106

[leodemoura]

@digama0 @gebner Thanks for the feedback.

Could you please confirm whether the following is the behavior you are expecting?

• Suppose we have open and export active commands in the current namespace/scope. I am assuming they will continue in effect while elaborating def _root_.foo. Correct? The question includes name resolution and scoped attributes. For example

def Bla.z := 1

namespace Foo
open Bla
def x := 10

def _root_.y := x + z -- `x` here is referring to `Foo.x` and `z` to `Bla.z`

• I am assuming it is an error to use scoped attribute with this feature. Example: @[scoped simp] def _root_.foo ... is not accepted.

Any other gotchas?

[digama0]

These are to some extent unexplored questions since the way lean 4 handles namespaced definitions, as though there was a namespace Foo around the definition, is new.

Here's a way that I think can lead to coherent answers to these questions: Imagine that we can write namespace _root_ which acts just like a regular namespace (it is still nesting "inside" namespace Foo and would be closed with end _root_), where the only difference from a regular namespace is that instead of definitions getting the name Foo._root_.y the *._root_ part is removed.

With that model, the name resolution would act as though the open and exports are still in scope, but root-scoped definitions and Bar scoped definitions (in the def _root_.Bar.y case) would take precedence. In your example, x would refer to Foo.x and z would refer to Bla.z like you said.

The behavior of @[scoped attr] should be the same as for @[scoped attr] on a def Bar.foo. I had to check lean to see what it does, and it looks like it makes the attribute active in the namespace Foo, not Bar. Consistency would then suggest to make @[scoped attr] scope the attribute in the namespace Foo (and the current section) even if the definition itself is at _root_.y.