a code suggestion bug

[fonqL]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

def aaaaa := 1

#eval ([1,2,3].map λ c => a).length

When I type a in the lambda, LSP only suggests the symbols in the namespace of List, not global symbols.

Context

Zulip discussion

Steps to Reproduce

1. Paste the code above in vscode.
2. Put the cursor in the character a in the lambda.
3. Trigger suggestion.

Expected behavior:

Show global symbols, including aaaaa.

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

Only show symbols in List namespace.

Versions

4.9.0-rc1

Additional Information

Impact

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

[fonqL]

Sorry, I seems to report in a wrong place..

[mhuisi]

No, I think this is the right place!