`#check` does not issue deprecation warning or handle overloaded definitions

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

#check ident does not issue a warning if ident is deprecated. It also does not print all definitions of overloaded constants, and does not issue an error in this case.

Context

Zulip discussion

Steps to Reproduce

@[deprecated] def A := 0
@[deprecated] def B.A := 0
open B

#check A

Expected behavior: Warns that A is deprecated. Either raises an error that says A is overloaded or print types of both A and B.A. Both of these are done if the user does #check (A) instead.

Actual behavior: #check prints the type of B.A without warning

Versions

Lean version 4.13.0-rc3

Impact

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

Start by running the minimal reproducer from the issue against the Lean nightly release and compare #check A with #check (A). Use the linked Zulip discussion for context. Done means deprecated identifiers produce a warning and overloaded definitions are either reported as ambiguous or both types are printed.