Assertion failure in local_context_adapter.cpp

[eric-wieser]

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

lean/src/frontends/lean/local_context_adapter.cpp

Lines 56 to 61 in 3526539

	expr local_context_adapter::translate_to(expr const & e) const {
	lean_assert(!has_local_ref(e));
	expr r = replace_locals(e, m_locals, m_local_refs);
	lean_assert(!has_regular_local(r));
	return r;
	}

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)

lean/src/frontends/lean/local_context_adapter.cpp

Lines 63 to 68 in 3526539

	expr local_context_adapter::translate_from(expr const & e) const {
	lean_assert(!has_regular_local(e));
	expr r = replace_locals(e, m_local_refs, m_locals);
	lean_assert(!has_local_ref(r));
	return r;
	}

Reproduces how often: Every time

Versions

Lean (version 3.45.0, commit 3526539, Debug)

[eric-wieser]

It would be a lot easier to debug this if I could get lean to pretty-print the value of e or r at this point: but the gdb pretty-printign only seems to work for me in VSCode with

`python print(list(gdb.selected_frame().block())[2].value(gdb.selected_frame()))

and I can't wokr out how to get hold of a formatter object inside translate_to in order to use the lean expr printing.