Timeout while generating equations

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

The following code:

import Lean.Elab.ElabRules
import Lean.Meta.Eqns

#eval show Lean.MetaM _ from do
  Lean.Meta.getEqnsFor? ``Lean.Elab.Command.elabElabRulesAux

crashes due to a loose bvar, the backtrace ends in whnf:

#1  0x00007f7bd6f98d03 in __pthread_kill_internal (threadid=<optimized out>, signo=6) at pthread_kill.c:78
#2  0x00007f7bd6f3fd1e in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#3  0x00007f7bd6f27942 in __GI_abort () at abort.c:79
#4  0x00007f7bdcd6510e in lean_panic_fn () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#5  0x00007f7bd8ac7aac in l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfImp___spec__3 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#6  0x00007f7bd8a57d75 in l___private_Lean_Meta_WHNF_0__Lean_Meta_reduceRec___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#7  0x00007f7bd8a89310 in l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore_go___spec__3___lambda__4 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so

comes there from simp:

349 0x00007f7bd955f95a in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___lambda__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#350 0x00007f7bdcd78433 in lean_apply_5 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#351 0x00007f7bd9560481 in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#352 0x00007f7bd9562f55 in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#353 0x00007f7bd95629ba in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#354 0x00007f7bd956563a in l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingImp___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#355 0x00007f7bd8f339f4 in l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_Simp_processCongrHypothesis___spec__2___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#356 0x00007f7bd8f348df in l_Lean_Meta_Simp_processCongrHypothesis () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#357 0x00007f7bd8f35743 in l_Array_forIn_x27Unsafe_loop___at_Lean_Meta_Simp_trySimpCongrTheorem_x3f___spec__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#358 0x00007f7bd8f3d575 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__6 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#359 0x00007f7bd8f3f285 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__7 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#360 0x00007f7bd8f40011 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__8 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#361 0x00007f7bd8f412a8 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__9 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#362 0x00007f7bd8f41751 in l_Lean_Meta_Simp_trySimpCongrTheorem_x3f___lambda__9___boxed () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so

called from the equations code:

#507 0x00007f7bd8f5f76a in l_Lean_Meta_Simp_simpImpl_go () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#508 0x00007f7bd8efa554 in lean_simp () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#509 0x00007f7bd8f61105 in l_Lean_Meta_Simp_main_go () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#510 0x00007f7bd8f62037 in l_Lean_Meta_Simp_main () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#511 0x00007f7bd9833ae5 in l___private_Lean_Meta_Tactic_Split_0__Lean_Meta_Split_simpMatchCore () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#512 0x00007f7bd983409d in l___private_Lean_Meta_Tactic_Split_0__Lean_Meta_Split_simpMatchTargetCore___lambda__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#513 0x00007f7bdcd782dd in lean_apply_5 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#514 0x00007f7bd9573f18 in l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#515 0x00007f7bd8b90be8 in l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#516 0x00007f7bd9865da4 in l_List_foldlM___at_Lean_Meta_Split_splitMatch___spec__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#517 0x00007f7bd98683c6 in l_Lean_Meta_Split_splitMatch___lambda__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#518 0x00007f7bdcd782dd in lean_apply_5 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#519 0x00007f7bd9573f18 in l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#520 0x00007f7bd8b90be8 in l_Lean_MVarId_withContext___at___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthPendingImp___spec__2___rarg () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#521 0x00007f7bdab3c509 in l_Lean_Elab_Eqns_splitMatch_x3f_go () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#522 0x00007f7bdab3fc5c in l_Lean_Elab_Eqns_splitMatch_x3f___lambda__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#523 0x00007f7bdcd782dd in lean_apply_5 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#524 0x00007f7bd986e4d7 in l_Lean_commitWhenSome_x3f___at_Lean_Meta_splitTarget_x3f___spec__1 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#525 0x00007f7bdab79ae0 in l_Lean_Elab_Eqns_mkEqnTypes_go___lambda__2 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#526 0x00007f7bdab7a670 in l_Lean_Elab_Eqns_mkEqnTypes_go___lambda__3 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so
#527 0x00007f7bdab7b3ff in l_Lean_Elab_Eqns_mkEqnTypes_go___lambda__4 () from /home/nix/.elan/toolchains/nightly-2024-12-12/bin/../lib/lean/libleanshared.so

Context

I discovered this in the CI of doc-gen, it has existed there since the 4.15-rc1 update but not before that.

Steps to Reproduce

Expected behavior: No loose bvars

Actual behavior: Loose bvars /o\

Versions

Lean 4.16.0-nightly-2024-12-12
Target: x86_64-unknown-linux-gnu

Impact

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

Start with the minimal #eval example importing Lean.Elab.ElabRules and Lean.Meta.Eqns, then trace Lean.Meta.getEqnsFor? for Lean.Elab.Command.elabElabRulesAux. Inspect the equations-generation path around simp, splitMatch, and whnf. Done means the reproducer no longer crashes and produces no loose bvars on the stated Lean nightly version.