Simple program causes Lean panic with `Batteries.CodeAction.Match` import

[mik-jozef]

The following code panics when I place the text cursor over the last line in vs code. The batteries import is necessary for the issue to manifest.

import Batteries.CodeAction.Match


inductive Foo (n: Nat): Type
| foo {a: Nat}: Foo n

def bar (foo: Foo n): True :=
  foo.rec
    (motive := fun _ => True)
    (@fun | a => sorry)

PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:448:17: unknown metavariable

#version output:

Lean 4.25.0-rc2
Target: x86_64-unknown-linux-gnu

Full error output with backtrace

PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:448:17: unknown metavariable
backtrace:
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9ec116e) [0x7de3a92c116e]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_panic_fn+0x1c) [0x7de3a92c160c]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimMVar+0x3d) [0x7de3a1cdc24d]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp+0x35f) [0x7de3a1cdb07f]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_visit+0x105) [0x7de3a1cdb805]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp_spec__2+0x7d) [0x7de3a1cdbf5d]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp+0x467) [0x7de3a1cdb187]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_visit+0x105) [0x7de3a1cdb805]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elim+0x1e3) [0x7de3a1cd9a23]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_visit+0x105) [0x7de3a1cdb805]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp+0x198) [0x7de3a1cdaeb8]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_MetavarContext_MkBinding_elimMVarDeps+0x53) [0x7de3a1ce33f3]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_MetavarContext_MkBinding_mkBinding+0x5a) [0x7de3a1ce5bda]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_MetavarContext_mkBinding+0x11f) [0x7de3a1ce64ef]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_mkForallFVars+0x2aa) [0x7de3a5cdb93a]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_InferType_0__Lean_Meta_inferLambdaType___lam__0+0x105) [0x7de3a6600a45]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_InferType_0__Lean_Meta_inferLambdaType___lam__0___boxed+0x16) [0x7de3a6600c26]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_7+0x941) [0x7de3a92d68e1]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x86a) [0x7de3a92d3c6a]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process___redArg___lam__0+0x25c) [0x7de3a5d061bc]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process___redArg+0x726) [0x7de3a5d06996]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp+0x7b) [0x7de3a5d06d2b]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_lambdaLetTelescope___at_____private_Lean_Meta_InferType_0__Lean_Meta_inferLambdaType_spec__0___redArg+0x93) [0x7de3a6600783]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_InferType_0__Lean_Meta_inferTypeImp_infer+0x718) [0x7de3a66080b8]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0xa0c) [0x7de3a92d3e0c]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_ContextInfo_runMetaM___redArg___lam__0+0x5f) [0x7de3a39d118f]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x970) [0x7de3a92d0bc0]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_ContextInfo_runCoreM___redArg+0xd47) [0x7de3a39d0437]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_ContextInfo_runMetaM___redArg+0x158) [0x7de3a39d19b8]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c230e2) [0x7de3a90230e2]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c21555) [0x7de3a9021555]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c23396) [0x7de3a9023396]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c21555) [0x7de3a9021555]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c23396) [0x7de3a9023396]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c21555) [0x7de3a9021555]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c24f30) [0x7de3a9024f30]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c1cab7) [0x7de3a901cab7]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c24b97) [0x7de3a9024b97]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9c2486d) [0x7de3a902486d]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_6+0xf3d) [0x7de3a92d59ed]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___Lean_CodeAction_cmdCodeActionProvider_spec__1+0x10d) [0x7de3a8e05cad]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___Lean_CodeAction_cmdCodeActionProvider_spec__2+0x3b4) [0x7de3a8e06bf4]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_CodeAction_cmdCodeActionProvider+0x2c6) [0x7de3a8e076f6]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_4+0x160) [0x7de3a92d1d40]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at___Lean_Server_handleCodeAction_spec__10+0x240) [0x7de3a89e8090]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_Server_handleCodeAction___lam__1+0x16f) [0x7de3a89e914f]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x12a2) [0x7de3a92d14f2]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x12cf) [0x7de3a92d151f]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_2+0x124c) [0x7de3a92cf76c]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(l_Lean_Server_ServerTask_EIO_mapTaskCheap___redArg___lam__0+0xa) [0x7de3a89f388a]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_2+0xbc1) [0x7de3a92cf0e1]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9ee6b2b) [0x7de3a92e6b2b]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x1204) [0x7de3a92cdd14]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x119f) [0x7de3a92cdcaf]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9ecb4f8) [0x7de3a92cb4f8]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9ecba07) [0x7de3a92cba07]
/home/mik-jozef/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/lib/lean/libleanshared.so(+0x9ebefe5) [0x7de3a92befe5]
/lib/x86_64-linux-gnu/libc.so.6(+0x9caa4) [0x7de39f09caa4]
/lib/x86_64-linux-gnu/libc.so.6(+0x129c6c) [0x7de39f129c6c]

[kim-em]

I can't reproduce, on either v4.25.0-rc2, main, or nightly-testing. Can you give more detailed instructions?

[mik-jozef]

I've discovered one more example that reproduces the issue for me (also for v4.27.0-rc1)

import Batteries.CodeAction.Match

def baz: Nat → _
| a => sorry

Here is my setup (changed extensions to .txt to bypass Github whitelist):
lakefile.txt
lake-manifest.json
lean-toolchain.txt
and the example code I have in test.lean, otherwise an empty repo. I just need to place my text cursor on the sorry.

---

I've asked AI, and it produced this solution that does fix the issue for me:

 getMatchHeaderRange?
    -- Isolate the syntax of only the "match" atom to get the starting position:
    let mStx ← matchStx.getArgs.find? (fun s => s.isAtom && s.getAtomVal == "match")
+   if let .original .. := mStx.getHeadInfo then pure () else none
    let startPos ← mStx.getPos? -- begin of 'match' keyword

Gemini 3 says:

The panic occurs because the matchExpand code action in the Batteries library is incorrectly attempting to process the synthetic match expression generated by the @fun macro. This generated code contains metavariables that causes the language server to crash when matchExpand tries to infer types for them.

I have fixed this by modifying Match.lean to ignore synthetic match terms. The code action will now only activate when the match keyword is physically present in the source code (i.e., has "original" source info).

Is this an acceptable change?

Note: I've tried to get the same panic with code that used explicit match statements, and couldn't find anything, with or without the above fix. For example, this is OK:

def bar_explicit (foo: Foo n): True :=
  foo.rec
    (motive := fun _ => True)
    (@fun x => match x with | a => sorry)

[kim-em]

Still can't reproduce. Could you give an example at https://live.lean-lang.org/?