Crash related to equation compiler(?)

[bryangingechen]

Reported by @kodyvajjha on Zulip. The following code crashes both 3.4.2 and the latest 3.5.0c nightly ("nightly-2019-05-17"):

universe u

open nat

variable {α : Type u}
def vec : Type u → ℕ → Type*
| A 0 := punit
| A (succ k) := A × vec A k

inductive dfin : ℕ → Type
| fz {n} : dfin (n+1)
| fs {n} : dfin n → dfin (n+1)

def kth_projn : Π n, vec α n → dfin n → α
| (_) x dfin.fz := x.fst -- crashes lean
| (succ n) (x,xs) (dfin.fs k) := kth_projn n xs k

Curiously, it does not crash when run in the web editor, instead returns the following error message:

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

[bryangingechen]

This crash occurs because of a null pointer dereference here: https://github.com/leanprover-community/lean/blob/master/src/library/inductive_compiler/ginductive.cpp#L240

When I run the debug build of Lean, I get a "LEAN ASSERTION VIOLATION" here: https://github.com/leanprover-community/lean/blob/master/src/library/equations_compiler/elim_match.cpp#L760

(And indeed, line 764 of that file is in the crash backtrace)

Not sure how to proceed...

[cipher1024]

It would be good to know what x_type is in

        lean_assert(is_inductive_app(x_type));

[bryangingechen]

Do you happen to have any tips: e.g. what I could evaluate in the debugger to find out? Entering expr x_type in lldb returns some m_ptr addresses which I don’t know how to interpret.

[Vtec234]

@bryangingechen Do you have gdb installed? There is a pretty-printing module for gdb in lean/bin/lean-gdb.py which makes p x_type print a nicely formatted expression. You need add-auto-load-safe-path /path/to/lean/bin/lean-gdb.py in your .gdbinit to make it work.

Here's what I get before the assertion violation:

> p x_type
$1 = lean::expr[App] = {
  m_fn = lean::expr[App] = {
    m_fn = lean::expr[Constant] = {
      m_name = 'vec',
      m_levels = lean::levels = {(param 'u'), (meta '_mlocal'.'_fresh'.0xc.0x3ce)}
    },
    m_arg = lean::expr[Local] = {
      m_pp_name = 'α',
      m_name = 0x0.'_fresh'.0xc.0x3ba,
      m_bi = {
        m_implicit = 0x1, 
        m_strict_implicit = 0x0, 
        m_inst_implicit = 0x0, 
        m_rec = 0x0
      },
      m_type = lean::expr[Constant] = {
        m_name = 0x1,
        m_levels = lean::levels
      }
    }
  },
  m_arg = lean::expr[Local] = {
    m_pp_name = 'n',
    m_name = 0x0.'_fresh'.0xc.0x52b,
    m_bi = {
      m_implicit = 0x0, 
      m_strict_implicit = 0x0, 
      m_inst_implicit = 0x0, 
      m_rec = 0x0
    },
    m_type = lean::expr[Constant] = {
      m_name = 0x1,
      m_levels = lean::levels
    }
  }
}

[bryangingechen]

I'm having a hell of a time getting gdb to work properly on macOS. That aside, I'm not sure how this function process_constructor_core works so I don't know that I'll be able to debug this further at this time.

[WildCryptoFox]

I hit this segfault while refactoring my code. I hope this can help figure out the cause.

structure bar (x : Type) :=
(data : x)

inductive foo
| q {c} (x : bar c)

namespace foo
  def z : foo → unit
  | (q (⟨tt⟩ : bar bool)) := ()
  | _ := ()
end foo

As a workaround, I'm using @q bool in the pattern.

Curiously the namespace is necessary to trigger the segfault. Without it, I get a different message than the playground.

src/segfault.lean:9:5: error: invalid application, function expected
src/segfault.lean:8:6: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)