"Invalid return type" error when definining inductive propositions can be attached to more suitable text range

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When defining inductive propositions (probably for types as well, but I haven't checked), "invalid return type" error is not attached to the text range of the actual erroneous return type, making it harder to understand.

Steps to Reproduce

Here is a code that you can paste into a new file:

structure relation :=
(c : Type) -- c for "carrier"
(holds : c → c → Prop)

inductive trans_closure (r : relation) : r.c → r.c → Prop
| base : ∀ {x y : r.c}, r.holds x y → trans_closure x y
| step : ∀ {x y z : r.c}, r.holds x y → trans_closure y z → r.holds x z

Expected behavior: [What you expect to happen]

Red squiggly line in VSCode is under the r.holds x z

Actual behavior: [What actually happens]

Red squiggly line in VSCode is under the word inductive, which makes the actual mistake harder to spot:

Reproduces how often: [What percentage of the time does it reproduce?]

Reproduces consistently from limited testing.

Versions

Lean (version 3.50.3, commit 855e5b74e3a5, Release), Linux Mint.

Start by reproducing the Lean 3.50.3 example from the issue and confirm the diagnostic range shown in VSCode. The payload names no source files or tests, so locating the compiler diagnostic handling for inductive declarations will require project familiarity. Done means the error highlights the invalid r.holds x z return type rather than inductive.