Assertion failure in local_context_adapter.cpp

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

The following code (from this Zulip thread) produces an assertion failure:

set_option old_structure_cmd true

class has_nat_cast (R : Type) :=
(nat_cast : ℕ → R)

class add_monoid_with_one (R : Type) extends has_nat_cast R :=
(nat_cast := sorry)
(nat_cast_zero : R := nat_cast 0)

Steps to Reproduce

1. Obtain a debug build of lean
2. Run lean test.lean on the file above

Expected behavior: No assertion error

Actual behavior: Two assertion errors:

LEAN ASSERTION VIOLATION
File: /workspace/lean/src/frontends/lean/local_context_adapter.cpp
Line: 59
Task: /workspace/lean/test.lean: parsing at line 6
!has_regular_local(r)
(C)ontinue, (A)bort/exit, (S)top/trap
c

https://github.com/leanprover-community/lean/blob/3526539070ea6268df5dd373deeb3ac8b9621952/src/frontends/lean/local_context_adapter.cpp#L56-L61

LEAN ASSERTION VIOLATION
File: /workspace/lean/src/frontends/lean/local_context_adapter.cpp
Line: 64
Task: /workspace/lean/test.lean: parsing at line 6
!has_regular_local(e)
(C)ontinue, (A)bort/exit, (S)top/trap
S
Aborted (core dumped)

https://github.com/leanprover-community/lean/blob/3526539070ea6268df5dd373deeb3ac8b9621952/src/frontends/lean/local_context_adapter.cpp#L63-L68

Reproduces how often: Every time

Versions

Lean (version 3.45.0, commit 3526539070ea6268df5dd373deeb3ac8b9621952, Debug)

Start with src/frontends/lean/local_context_adapter.cpp at the assertions on lines 56-61 and 63-68, then reproduce the failure using the Lean snippet in the issue with a debug build. Trace why the structure declarations create locals that fail the regular-local checks. Done means the reproducer completes without assertion errors.