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.