gdb.bt

#0  0x000000000061e834 in lean::get_ginductive_num_params(lean::environment const&, lean::name const&) ()
#1  0x000000000095072d in lean::for_each_compatible_constructor(lean::type_context_old&, lean::expr const&, std::function<void (lean::expr const&, lean::buffer<lean::expr, 16u>&)> const&) ()
#2  0x0000000000ad352f in lean::elim_match_fn::process_complete(lean::elim_match_fn::problem const&) ()
#3  0x0000000000acd0a2 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) ()
#4  0x0000000000acde27 in lean::elim_match_fn::process_constructor_core(lean::elim_match_fn::problem const&, bool) ()
#5  0x0000000000acd0c0 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) ()
#6  0x0000000000ad35c4 in lean::elim_match_fn::process_complete(lean::elim_match_fn::problem const&) ()
#7  0x0000000000acd0a2 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) ()
#8  0x0000000000ad048c in lean::elim_match_fn::process_variable_inaccessible(lean::elim_match_fn::problem const&, bool) ()
#9  0x0000000000ad0e26 in lean::elim_match_fn::process_inaccessible(lean::elim_match_fn::problem const&) ()
#10 0x0000000000accfcf in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) ()
#11 0x0000000000acde27 in lean::elim_match_fn::process_constructor_core(lean::elim_match_fn::problem const&, bool) ()
#12 0x0000000000acd0c0 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) ()
#13 0x0000000000ad35c4 in lean::elim_match_fn::process_complete(lean::elim_match_fn::problem const&) ()
#14 0x0000000000acd0a2 in lean::elim_match_fn::process(lean::elim_match_fn::problem const&) ()
#15 0x0000000000ace85b in lean::elim_match_fn::operator()(lean::local_context const&, lean::expr const&) ()
#16 0x0000000000ac210f in lean::elim_match(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) ()
#17 0x0000000000ac2678 in lean::mk_nonrec(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) ()
#18 0x0000000000958431 in lean::compile_equations_core(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) ()
#19 0x0000000000958923 in lean::compile_equations_main(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&, bool) ()
#20 0x0000000000959e21 in lean::compile_equations(lean::environment&, lean::elaborator&, lean::metavar_context&, lean::local_context const&, lean::expr const&) ()
#21 0x00000000007899d2 in lean::elaborator::visit_equations(lean::expr const&) ()
#22 0x00000000007820d9 in lean::elaborator::visit_macro(lean::expr const&, lean::optional<lean::expr> const&, bool) ()
#23 0x0000000000782c76 in lean::elaborator::visit(lean::expr const&, lean::optional<lean::expr> const&) ()
#24 0x00000000007932bd in lean::elaborator::elaborate_with_type(lean::expr const&, lean::expr const&) ()
#25 0x00000000007bcb0c in lean::single_definition_cmd_core(lean::parser_info&, lean::decl_cmd_kind, lean::cmd_meta)::{lambda(lean::expr)#1}::operator()(lean::expr) const ()
#26 0x00000000007be8ae in lean::single_definition_cmd_core(lean::parser_info&, lean::decl_cmd_kind, lean::cmd_meta) ()
#27 0x00000000007c054f in lean::definition_cmd_core(lean::parser&, lean::decl_cmd_kind, lean::cmd_meta const&) ()
#28 0x00000000006fc506 in lean::definition_cmd(lean::parser&, lean::cmd_meta const&) ()
#29 0x00000000006decb5 in std::_Function_handler<lean::environment (lean::parser&, lean::cmd_meta const&), lean::environment (*)(lean::parser&, lean::cmd_meta const&)>::_M_invoke(std::_Any_data const&, lean::parser&, lean::cmd_meta const&) ()
#30 0x00000000006ba00f in lean::parser::parse_command(lean::cmd_meta const&) ()
#31 0x00000000006ba99f in lean::parser::parse_command_like() ()
#32 0x00000000007dca03 in lean::module_parser::parse_next_command_like(lean::optional<std::vector<std::shared_ptr<lean::gtask_cell>, std::allocator<std::shared_ptr<lean::gtask_cell> > > > const&)::{lambda()#1}::operator()() const ()
#33 0x00000000007e120e in lean::task_builder<lean::module_parser_result>::base_task_imp<lean::module_parser::parse_next_command_like(lean::optional<std::vector<std::shared_ptr<lean::gtask_cell>, std::allocator<std::shared_ptr<lean::gtask_cell> > > > const&)::{lambda()#1}>::execute(void*) ()
#34 0x00000000005c75da in lean::library_scopes_imp::execute(void*) ()
#35 0x00000000004d530a in lean::cancellable_task_imp::execute(void*) ()
#36 0x00000000007e29b0 in lean::task_cell<lean::module_parser_result>::execute() ()
#37 0x00000000004d4fc0 in lean::task_queue::execute(std::shared_ptr<lean::gtask_cell> const&) ()
#38 0x00000000005c378f in std::_Function_handler<void (), lean::mt_task_queue::spawn_worker()::{lambda()#1}>::_M_invoke(std::_Any_data const&) ()
#39 0x00000000004d21e5 in lean::lthread::imp::_main(void*) ()
#40 0x0000000000491d1b in start_thread (arg=0x7ffff7ff8700) at pthread_create.c:463
#41 0x0000000000c53c8f in clone ()

gistfile1.txt

$ time lean src/segfault.lean ; echo $? ; time lean --trust=0 src/segfault.lean ; echo $?
Segmentation fault

real    0m0.328s
user    0m0.300s
sys     0m0.031s
139
Segmentation fault

real    0m2.183s
user    0m2.133s
sys     0m0.050s
139

segfault.lean

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

Lean (version 3.18.4, commit f539be1e867c, Release)