Name collision between fields and parameters in struct declaration

[Rotsor]

Prerequisites

• [x] 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

Definition is rejected with a strange error message, indicating likely scope hygiene violation:

structure str (x : bool) := (x : bool) -- invalid return type for 'str.mk'
structure str (x : bool) := (x : nat)
/-
type mismatch at application
  str x
term
  x
has type
   ℕ
but is expected to have type
  bool
 -/

Steps to Reproduce

1. structure str (x : bool) := (x : bool)
2. structure str (x : bool) := (x : nat)

Expected behavior:

Both definitions are individually accepted, parameter x is ignored. Alternatively, they are rejected with a specific (identical) error message.

Actual behavior:

Bad error message. See Description.

Reproduces how often:

Always

Versions

Lean (version 3.3.0, commit fa9c868ed2bb, Release) Windows 10 Pro

Additional Information

[Rotsor]

I guess it would be nice if "invalid return type" printed the actual return type too when it's not available in the source code.