feat: open _root_.<namespace>

closes #3045

src/Lean/ResolveName.lean

@@ -187,10 +187,17 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
 
 /-! # Namespace resolution -/
 
-def resolveNamespaceUsingScope? (env : Environment) (n : Name) : Name → Option Name
-  | .anonymous    => if env.isNamespace n then some n else none
-  | ns@(.str p _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope? env n p
-  | _             => unreachable!
+def resolveNamespaceUsingScope? (env : Environment) (n : Name) (ns : Name) : Option Name :=
+  match ns with
+  | .str p _ =>
+    if env.isNamespace (ns ++ n) then
+      some (ns ++ n)
+    else
+      resolveNamespaceUsingScope? env n p
+  | .anonymous =>
+    let n := n.replacePrefix rootNamespace .anonymous
+    if env.isNamespace n then some n else none
+  | _ => unreachable!
 
 def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → List Name
   | [] => []

tests/lean/run/3045.lean

@@ -0,0 +1,15 @@
+namespace X
+def test := "test"
+end X
+
+namespace Y
+
+namespace X end X
+
+-- We want to open `X`, not `Y.X`
+open _root_.X  -- should not produce `unknown namespace '_root_.X'`
+/--
+info: X.test : String
+-/
+#guard_msgs in
+#check test