segfault with `by {using}`

[shingtaklam1324]

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

Segfault when running this example

Steps to Reproduce

variable {α : Type}

def with_one (α) := option α

instance : has_one (with_one α) := ⟨none⟩

attribute [irreducible] with_one

lemma ne_one_iff_exists : ∀ {x : with_one α}, x ≠ 1 ↔ ∃ (a : α), x = a
| 1       := ⟨by { using }⟩
| (a : α) := sorry

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

segfault

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

100%

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

3.18.4, seems to crash on Ubuntu and Windows.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[EdAyers]

Can confirm that it also crashes on macOS.

[bryangingechen]

I did some bisection and the example from the OP doesn't crash with Lean 3.10.0c and does crash with Lean 3.11.0c.

I suspect #211 again, see also #372 and the fix in #373.

Here's the lldb backtrace in 3.11.0c:

* thread #3, stop reason = EXC_BAD_ACCESS (code=1, address=0x0)
  * frame #0: 0x000000010043b753 lean`lean::get_ginductive_num_params(lean::environment const&, lean::name const&) + 35
    frame #1: 0x00000001004195fd lean`lean::elim_match_fn::process_constructor_core(lean::elim_match_fn::problem const&, bool) + 973
    frame #2: 0x000000010040adf4 lean`lean::elim_match_fn::process(lean::elim_match_fn::problem const&) + 1204
    frame #3: 0x00000001004076fc lean`lean::elim_match_fn::operator()(lean::local_context const&, lean::expr const&) + 620
    frame #4: 0x00000001004072fe lean`lean::elim_match(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) + 78
    frame #5: 0x00000001004080e3 lean`lean::mk_nonrec(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) + 163
    frame #6: 0x0000000100422cdb lean`lean::compile_equations_core(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) + 2651
    frame #7: 0x0000000100421648 lean`lean::compile_equations_main(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&, bool) + 1336
    frame #8: 0x0000000100421016 lean`lean::compile_equations(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) + 646
    frame #9: 0x0000000100662245 lean`lean::elaborator::visit_equations(lean::expr const&) + 2581
    frame #10: 0x000000010064af5f lean`lean::elaborator::visit_macro(lean::expr const&, lean::optional<lean::expr> const&, bool) + 703
    frame #11: 0x00000001006487d2 lean`lean::elaborator::visit(lean::expr const&, lean::optional<lean::expr> const&) + 1778
    frame #12: 0x000000010066f554 lean`lean::elaborator::elaborate_with_type(lean::expr const&, lean::expr const&) + 372

The appearance of get_ginductive_num_params is reminiscent of #52 and one of the errors when putting the example into the web editor is similar:

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
nested exception message:
cases tactic failed, it is not applicable to the given hypothesis

[shingtaklam1324]

I tried to minimise the example a bit more, didn't find a shorter example but I did find something interesting: If we switch the attribute line and the instance line, then it no longer crashes.

variable {α : Type}

def with_one (α) := option α

instance : has_one (with_one α) := ⟨none⟩

attribute [irreducible] with_one

example : ∀ {x : with_one α}, true | 1 := by { using }

crashes, but

variable {α : Type}

def with_one (α) := option α

attribute [irreducible] with_one

instance : has_one (with_one α) := ⟨none⟩

example : ∀ {x : with_one α}, true | 1 := by { using }

does not.