Global definition shadowing a local one when using dot-notation

[nnmm]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

I would expect that a "local" definition in the form of a where clause shadows a global definition with the same name. Instead, it appears that the global definition shadows the local definition if dot notation is used.

Context

Zulip chat

Steps to Reproduce

Minimal example (H/T to @eric-wieser)

def foo : Nat := 1

def bar : Nat :=
  foo.add 1
where
  foo := 10

def baz : Nat :=
  .add foo 1
where
  foo := 10

#eval bar -- 2
#eval baz -- 11

Expected behavior: [Clear and concise description of what you expect to happen]

#eval bar returns 11

Actual behavior: [Clear and concise description of what actually happens]

#eval bar returns 2

Versions

Lean (version 4.3.0, commit 8e5cf64, Release)
Ubuntu 22.04.3

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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