PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:920:14: unknown metavariable

[eric-wieser]

The following file

import Aesop

universe u
variable {α : Type u}

@[simp]
theorem List.filter_true (l : List α) : filter (fun _ => true) l = l := sorry

structure Finset (α : Type u) where
  val : List α
  nodup : List.Nodup val

namespace Finset

instance : Membership α (Finset α) :=
  ⟨fun a s => a ∈ s.1⟩

protected def Nonempty (s : Finset α) : Prop := ∃ x : α, x ∈ s

instance : Singleton α (Finset α) :=
  ⟨fun a => ⟨[a], sorry⟩⟩

@[simp, aesop safe apply]
theorem singleton_nonempty (a : α) : ({a} : Finset α).Nonempty := sorry

end Finset

example
    (n : List Nat → List Nat)
    (hn : ∀ A, n A = A.filter (fun p => true)) :
    0 ≤ 0 := by
  exact (0, Classical.not_not.1 $ by aesop)

when run as lake lean test/tmp.lean 2>&1 on leanprover/lean4:v4.11.0-rc2, emits 76505 lines of output and 750 panics.

The useful part of the output is:

aesop: internal error: extracted proof has metavariables.
  Proof: Eq.mpr (id Init.Classical._auxLemma.2)
    (?m.1175 (Eq.mp (forall_congr fun A => congrArg (Eq (n A)) (List.filter_true A)) hn))
  Unassigned metavariables: [_uniq.1490, _uniq.1491]

An example panic is:

PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:920:14: unknown metavariable
backtrace:
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7fb99be5832e]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_MkTableKey_normLevel+0x387)[0x7fb99938bd57]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_List_mapM_loop___at_Lean_Meta_SynthInstance_MkTableKey_normExpr___spec__2+0x15d)[0x7fb99938cecd]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0xfe)[0x7fb99938d10e]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x3f4)[0x7fb99938d404]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x3f4)[0x7fb99938d404]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x462)[0x7fb99938d472]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x3f4)[0x7fb99938d404]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_MkTableKey_normExpr+0x3f4)[0x7fb99938d404]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_mkTableKey___at_Lean_Meta_SynthInstance_main___spec__1+0xda)[0x7fb9993d560a]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_SynthInstance_main___lambda__2+0xa0)[0x7fb9993d6080]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x3d4)[0x7fb99be65154]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Core_withCurrHeartbeats___at_Lean_Meta_SynthInstance_main___spec__3+0x29)[0x7fb9993d5cd9]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x3a0)[0x7fb99be66bf0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_withNewMCtxDepthImp___rarg+0x493)[0x7fb99932bb33]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_withNewMCtxDepth___at_Lean_Meta_matchesInstance___spec__1___rarg+0x20)[0x7fb999265090]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_synthInstance_x3f___lambda__4+0x105d)[0x7fb9993e8c2d]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x3a0)[0x7fb99be66bf0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_withTraceNode___at_Lean_Meta_synthInstance_x3f___spec__4+0x295)[0x7fb9993e6f85]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_synthInstance_x3f___lambda__5+0x1cf)[0x7fb9993ee22f]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x1f8)[0x7fb99be63258]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0xe)[0x7fb999c7971e]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0xf)[0x7fb999c7991f]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x149)[0x7fb99be631a9]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_profileit+0x74)[0x7fb99bdbb804]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x60)[0x7fb999c79840]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_synthInstance_x3f+0x156)[0x7fb9993ee506]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_trySynthInstance+0x1a)[0x7fb9993ef25a]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_coerceSimple_x3f+0x803)[0x7fb998f0c363]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_coerce_x3f___lambda__2+0x35e)[0x7fb998f2414e]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_coerce_x3f+0x385)[0x7fb998f25395]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVar___lambda__1+0xa1)[0x7fb99b17d0e1]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVar___lambda__2+0xe18)[0x7fb99b17e998]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVar___lambda__2___boxed+0x27)[0x7fb99b17fd17]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x3e9)[0x7fb99be66c39]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg+0x208)[0x7fb99932e9f8]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_run___spec__1___rarg+0x4f)[0x7fb99abb10bf]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVar+0xb1a)[0x7fb99b17c70a]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_List_filterAuxM___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep___spec__1+0x929)[0x7fb99b17ad19]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeSyntheticMVarsStep+0x2d9)[0x7fb99b178969]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_synthesizeSyntheticMVars_loop+0x13a5)[0x7fb99b174e75]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_synthesizeSyntheticMVars+0xda)[0x7fb99b189fca]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_runTermElab_go___rarg+0x251)[0x7fb99ad0c601]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_runTermElab___rarg___lambda__2+0x86)[0x7fb99ad112b6]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x483)[0x7fb99be69e13]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_runTermElab___spec__2___rarg+0x2830)[0x7fb99ad0f310]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_elabTerm+0x62f)[0x7fb99ad11ccf]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_elabTermEnsuringType+0x100)[0x7fb99ad12d00]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalExact___lambda__1+0x20b)[0x7fb99ad165ab]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_10+0x4b7)[0x7fb99be6a927]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_closeMainGoalUsing___lambda__1+0x324)[0x7fb99ad14d44]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x446)[0x7fb99be66c96]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg+0x208)[0x7fb99932e9f8]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_MVarId_withContext___at_Lean_Elab_Tactic_withMainContext___spec__1___rarg+0x59)[0x7fb99abf3d29]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_withMainContext___rarg+0x28b)[0x7fb99abf414b]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x420)[0x7fb99be69db0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Tactic_evalTactic_eval___spec__2+0x251)[0x7fb99abc0ba1]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_eval___lambda__2+0x254)[0x7fb99abc9174]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x483)[0x7fb99be69e13]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_evalTactic_eval___spec__3+0x2830)[0x7fb99abc4f80]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_eval+0x50d)[0x7fb99abc754d]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_expandEval+0xde1)[0x7fb99abd2c61]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic___lambda__3+0xed)[0x7fb99abdbc4d]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic___lambda__4+0xb24)[0x7fb99abdc7c4]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x420)[0x7fb99be69db0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3+0x355)[0x7fb99abdac05]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x52c)[0x7fb99be652ac]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x260)[0x7fb99be632c0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0xe)[0x7fb999c7971e]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0xf)[0x7fb999c7991f]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x149)[0x7fb99be631a9]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_profileit+0x74)[0x7fb99bdbb804]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg+0x60)[0x7fb999c79840]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic+0xe6)[0x7fb99abccda6]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalSepTactics_goEven___lambda__7+0x45f)[0x7fb99ac4877f]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x4f3)[0x7fb99be69e83]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_withReuseContext___at_Lean_Elab_Tactic_evalWithAnnotateState___spec__3+0x5cc)[0x7fb99ac285cc]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_withNarrowedTacticReuse___at_Lean_Elab_Tactic_evalWithAnnotateState___spec__2+0x27aa)[0x7fb99ac2b37a]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalSepTactics_goEven___lambda__9+0x4f4)[0x7fb99ac4a924]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalSepTactics_goEven+0x69)[0x7fb99ac4aa29]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x420)[0x7fb99be69db0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_withReuseContext___at_Lean_Elab_Tactic_evalWithAnnotateState___spec__3+0x5cc)[0x7fb99ac285cc]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_withNarrowedTacticReuse___at_Lean_Elab_Tactic_evalWithAnnotateState___spec__2+0x27aa)[0x7fb99ac2b37a]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTacticSeq1Indented+0x98)[0x7fb99ac4e8b8]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x420)[0x7fb99be69db0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Tactic_evalTactic_eval___spec__2+0x251)[0x7fb99abc0ba1]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_eval___lambda__2+0x254)[0x7fb99abc9174]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x483)[0x7fb99be69e13]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Term_withoutTacticIncrementality___at_Lean_Elab_Tactic_evalTactic_eval___spec__3+0x2830)[0x7fb99abc4f80]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_eval+0x3e5)[0x7fb99abc7425]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic_expandEval+0xde1)[0x7fb99abd2c61]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic___lambda__3+0xed)[0x7fb99abdbc4d]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Tactic_evalTactic___lambda__4+0xb24)[0x7fb99abdc7c4]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_9+0x420)[0x7fb99be69db0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_withTraceNode___at_Lean_Elab_Tactic_evalTactic___spec__3+0x355)[0x7fb99abdac05]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x52c)[0x7fb99be652ac]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x260)[0x7fb99be632c0]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1+0xe)[0x7fb999c7971e]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed+0xf)[0x7fb999c7991f]
/home/gitpod/.elan/toolchains/leanprover--lean4---v4.11.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x149)[0x7fb99be631a9]