SIGSEGV in elaboration

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

test.lean:

@[specialize]
unsafe def map {m : Type v → Type w} [Monad m] (f : α → m β) (sz i : USize) (r : Array NonScalar) : m (Array PNonScalar) := do
  if i < sz then
    let v    := r.uget i lcProof
    let r    := r.uset i default lcProof
    let vNew ← f (unsafeCast ())     
    map f sz (i+1) (r.uset i (unsafeCast vNew) lcProof)
  else
    pure (unsafeCast r)


@[inline]
unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
  let sz := USize.ofNat as.size
  unsafeCast <| map f sz 0 (unsafeCast as)

unsafe def f (arr: Array (IO Nat)) := mapMUnsafe id arr

Running lean test.lean, lean crashes with code 139 (SIGSEGV).

Context

Zulip discussion

Steps to Reproduce

1. copy the above code to a file.
2. run lean filename.lean

Expected behavior:
lean works well.

Actual behavior:
lean crashes.

Versions

4.10.0-rc1

Additional Information

Stacktrace given by Marc Huisinga:

0x00007f8d62c38d90 in lean_inc_ref_cold () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
(gdb) bt
#0  0x00007f8d62c38d90 in lean_inc_ref_cold () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#1  0x00007f8d62b3a181 in lean::lift_loose_bvars(lean::expr const&, unsigned int, unsigned int) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#2  0x00007f8d62b3a1dd in lean::lift_loose_bvars(lean::expr const&, unsigned int) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#3  0x00007f8d62b40ec4 in std::__1::__function::__func<lean::instantiate_rev(lean::expr const&, unsigned int, lean::expr const*)::$_1, std::__1::allocator<lean::instantiate_rev(lean::expr const&, unsigned int, lean::expr const*)::$_1>, lean::optional<lean::expr> (lean::expr const&, unsigned int)>::operator()(lean::expr const&, unsigned int&&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#4  0x00007f8d62b3d947 in lean::replace_rec_fn::apply(lean::expr const&, unsigned int) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#5  0x00007f8d62b3db09 in lean::replace_rec_fn::apply(lean::expr const&, unsigned int) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#6  0x00007f8d62b3d6a0 in lean::replace(lean::expr const&, std::__1::function<lean::optional<lean::expr> (lean::expr const&, unsigned int)> const&, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#7  0x00007f8d62b3f510 in lean::instantiate_rev(lean::expr const&, unsigned int, lean::expr const*) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#8  0x00007f8d62bc58ec in lean::csimp_fn::beta_reduce(lean::expr, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#9  0x00007f8d62bca691 in lean::csimp_fn::reduce_cases_cnstr(lean::buffer<lean::expr, 16ul> const&, lean::inductive_val const&, lean::expr const&, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#10 0x00007f8d62bc64ba in lean::csimp_fn::visit_cases(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#11 0x00007f8d62bc2ff2 in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#12 0x00007f8d62bc01b2 in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#13 0x00007f8d62bc2bb5 in lean::csimp_fn::visit_let(lean::expr) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#14 0x00007f8d62bc014f in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#15 0x00007f8d62bc5a11 in lean::csimp_fn::beta_reduce_cont(lean::expr, unsigned int, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#16 0x00007f8d62bc594f in lean::csimp_fn::beta_reduce(lean::expr, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#17 0x00007f8d62bc5754 in lean::csimp_fn::beta_reduce(lean::expr, lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#18 0x00007f8d62bc9a22 in lean::csimp_fn::try_inline(lean::expr const&, lean::expr const&, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#19 0x00007f8d62bc3452 in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#20 0x00007f8d62bc8ef9 in lean::csimp_fn::merge_app_app(lean::expr const&, lean::expr const&, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#21 0x00007f8d62bc31a7 in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#22 0x00007f8d62bc01b2 in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#23 0x00007f8d62bccb1a in lean::csimp_fn::apply_at(lean::expr const&, lean::expr const&, lean::expr const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#24 0x00007f8d62bc7b9f in lean::csimp_fn::float_cases_on_core(lean::expr const&, lean::expr const&, lean::expr const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#25 0x00007f8d62bc30fa in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#26 0x00007f8d62bc01b2 in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#27 0x00007f8d62bc5bf0 in lean::csimp_fn::beta_reduce_cont(lean::expr, unsigned int, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#28 0x00007f8d62bc594f in lean::csimp_fn::beta_reduce(lean::expr, unsigned int, lean::expr const*, bool) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#29 0x00007f8d62bc5754 in lean::csimp_fn::beta_reduce(lean::expr, lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#30 0x00007f8d62bc3085 in lean::csimp_fn::visit_app(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#31 0x00007f8d62bc01b2 in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#32 0x00007f8d62bc2bb5 in lean::csimp_fn::visit_let(lean::expr) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#33 0x00007f8d62bc014f in lean::csimp_fn::visit(lean::expr const&, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#34 0x00007f8d62bbf4b8 in lean::csimp_fn::visit_lambda(lean::expr, bool, bool) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#35 0x00007f8d62bbe788 in lean::csimp_fn::operator()(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#36 0x00007f8d62bbe11d in lean::csimp_core(lean::environment const&, lean::local_ctx const&, lean::expr const&, bool, lean::csimp_cfg const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#37 0x00007f8d62bf7ed3 in lean::specialize_fn::mk_new_decl(lean::pair_ref<lean::name, lean::expr> const&, lean::buffer<lean::expr, 16ul> const&, lean::buffer<lean::expr, 16ul> const&, lean::specialize_fn::spec_ctx&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#38 0x00007f8d62bf0d40 in lean::specialize_fn::specialize(lean::expr const&, lean::buffer<lean::expr, 16ul> const&, lean::specialize_fn::spec_ctx&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#39 0x00007f8d62bef53a in lean::specialize_fn::visit_app(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#40 0x00007f8d62bef175 in lean::specialize_fn::visit(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#41 0x00007f8d62befe21 in lean::specialize_fn::visit_let(lean::expr) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#42 0x00007f8d62bef1e8 in lean::specialize_fn::visit(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#43 0x00007f8d62befa0f in lean::specialize_fn::visit_lambda(lean::expr) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#44 0x00007f8d62bef1a6 in lean::specialize_fn::visit(lean::expr const&) () from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#45 0x00007f8d62bee86f in lean::specialize_fn::operator()(lean::pair_ref<lean::name, lean::expr> const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#46 0x00007f8d62bedc0e in lean::specialize(lean::environment, lean::list_ref<lean::pair_ref<lean::name, lean::expr> > const&, lean::csimp_cfg const&) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so
#47 0x00007f8d62ba4558 in lean::compile(lean::environment const&, lean::options const&, lean::list_ref<lean::name>) ()
   from /home/mhuisi/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean/libleanshared.so

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with test.lean and run it using lean to reproduce the SIGSEGV. Trace the specialization and simplification path shown in the stack trace, beginning at specialize_fn and csimp_fn, including lift_loose_bvars. Done means the minimal example compiles without crashing and a regression test covers the failure.