open is confused

Stream: lean4

[Kenny Lau]

I've found a very interesting behaviour, not sure if it's intended or not:

theorem Nat.foo : 37 = 51 := sorry

namespace Foo

theorem Nat.my_test : 39 = 21 := sorry

open Nat in
theorem bar : 37 = 29 := by
  rw [foo] -- unknown identifier 'foo'

end Foo

Here Lean complains that it has no idea what foo means, until you comment out Nat.my_test above it!

[Kenny Lau]

presumably Lean saw the additional declaration Foo.Nat.my_test and decided that open Nat means open Foo.Nat?

[Kenny Lau]

(I suppose the intended solution is to replace Nat.my_test with instead _root_.Nat.my_test

[Kyle Miller]

Odd, open Nat is supposed to open every Nat that can be opened, if I remember correctly.

[Aaron Liu]

weird

[Aaron Liu]

is Nat resolved in the current namespace?

[Aaron Liu]

this properly opens Nat

theorem Nat.foo : 37 = 51 := sorry

namespace Foo

theorem Nat.my_test : 39 = 21 := sorry

open _root_.Nat in
theorem bar : 37 = 29 := by
  rw [foo] -- unknown identifier 'foo'

end Foo

[Kyle Miller]

Yes, it seems to be resolved. If you do open Nat in #where you can see open Foo.Nat.

[Kyle Miller]

I guess the deal is that resolveNamespace returns just a single resolution here.

import Lean

theorem Nat.foo : 37 = 51 := sorry

namespace Foo

theorem Nat.my_test : 39 = 21 := sorry

#eval Lean.resolveNamespace (Lean.mkIdent `Nat)
-- [`Foo.Nat]

[Kyle Miller]

docs#Lean.ResolveName.resolveNamespaceUsingScope? only looks for a single resolution, using the largest prefix of the current namespace.

(This sort of problem that reusing namespace components can cause.)

[Jovan Gerbscheid]

I think this kind of resolution is correct when it comes to identifiers. Because priority is given to those that can be obtained using the namespaces and without the opens. (so that e.g. in namespace CategoryTheory, Functor is unambiguous). But when opening namespaces, this seems wrong.

[Michael Stoll]

See also #lean4 > open not opening a namespace @ 💬