Using open or export does not make names accessible for extended field notation (dot notation)

[kmill]

Description

If you try to use open or export to import names to use for dot notation, it does not work. Confusingly, you can have String.a "x" succeed but "x".a fail.

Context

Zulip thread where this was brought up, during an Advent of Code problem.

Steps to Reproduce

Observe that "x".a produces an error in the following

namespace Common
namespace String

def a (s : String) : Nat := s.length

end String
end Common

open Common (String.a)

#eval String.a "x"

/-
invalid field 'a', the environment does not contain 'String.a'
  "x"
has type
  String
-/
#eval "x".a

export Common (String.a)

/-
invalid field notation, function 'Common.String.a' does not have argument
with type (Common.String ...) that can be used, it must be explicit or
implicit with a unique name
-/
#eval "x".a

Expected behavior: The second and third #evals have the same interpretation as the first.

Actual behavior: Only the first succeeds. The second #eval (when the name is just open) doesn't see String.a at all, and the third #eval (when the name is exported) it sees it but then fails to process it correctly.

Versions

MacOS arm64

/- "4.3.0-rc2" -/
#eval Lean.versionString

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[digama0]

I would love this feature, it would be a way to avoid the name-clash-inducing practice of defining functions outside the project namespace so that you get dot notation on types you don't own. (PS: I would describe this as a feature request / RFC, not a bug.)

[Kha]

I think this is an RFC :) . It is a sensible enhancement suggestion but it is not an accidental oversight in the implementation.

[Kha]

I should also mention a much older proposal of allowing any top-level name in scope as a target for extended field notation. This is especially interesting for typeclasses where it would allow us to use x.toString uniformly instead of the status quo where it only works sometimes depending on whether that exact declaration name was used to construct the instance. It is similar to how in Rust you need to use a trait to get dot access to its members.
It might be that these two proposals are independent(ly desirable) but they are similar enough that I wanted to mention this one in case we say that it would be confusing to have both.

[kmill]

#6189 implements this along with @Kha's suggestion.

New rule: given x : S, then x.f tries resolving S.f with respect to the root namespace. If it can't be resolved, then it tries it with each parent in the resolution order of S as well, if S is a structure.

Additionally, as a last resort, after all attempts of unfolding S to find a resolution, it looks for f in the root namespace (either as an exact match or as an alias) and then does f S. I made it pay no attention to open, since I couldn't think of any examples where you would want that, but it does resolve x.toString to toString x since toString is exported.

(This is all still pending seeing if building mathlib uncovers any problems with this scheme! Edit: Mathlib only needed a few lines changed. Quaternion was using the old version of the aliasing feature, but deleting the export and fully qualifying re in one place fixed it.)