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

[ddrone]

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 855e5b7, Release), Linux Mint.

[ddrone]

By the way, if someone can provide me pointers about the relevant code I'm happy to try to contribute a fix myself.