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.