PANIC: Lean.MetavarContext:430:17: unknown metavariable

### Prerequisites

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

* [X] Check that your issue is not already filed:
      https://github.com/leanprover/lean4/issues
  * This could be a duplicate, but is not obviously so.
* [X] Reduce the issue to a minimal, self-contained, reproducible test case.
      Avoid dependencies to Mathlib or Batteries.
* [X] 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 program causes a panic in the language server.

```lean
--import Mathlib.Tactic.ComputeDegree

--set_option diagnostics true

def Chain (I : Type) (n : Nat) (T : Fin (n+1) → Type) :=
  (i : Fin (n+1)) → I → (T i) → Prop

def cons_wit_type (S : Type) (n : Nat) (T : Fin (n+1) → Type) : (i : Fin (n+2)) → Type
  | 0 => S
  | {val := i+1, isLt := _} => sorry
  --| {val := i+1, isLt := _} => T i  --depends on Mathlib.Tactic.ComputeDegree

def ConsChain (I S : Type) (n : Nat) (T : Fin (n+1) → Type) :=
  Chain I (n+1) (cons_wit_type S n T)

def mk_cons (I S : Type) (n : Nat) (T : Fin (n+1) → Type) (relS : I → S → Prop) (r : Chain I n T) :
  ConsChain I S n T
  | 0 => relS
  | {val := i+1, isLt := _} => sorry
  --| {val := i+1, isLt := _} => r i  --depends on Mathlib.Tactic.ComputeDegree

def Base (I S : Type) := Chain I 0 (fun | 0 => S)

def mk_base {I S : Type} (relS : I → S → Prop) : Base I S := (fun | 0 => relS)

infixr:50 " >> " => fun l r => mk_cons l r
postfix:60 " ##" => fun r => mk_base r

def eq (x : Nat) (y : Nat) := x = y

def chain := eq >> (eq ##)
```

### Steps to Reproduce

1. Paste the given program into a new project using Lean v4.19.0-rc2.
2. Mouse over `(eq ##)` on the last line.
3. Observe the panic shown below under **Actual behavior:**.

**Expected behavior:**

Just the following type error without the panic:

Repro.lean:31:13
```
overloaded, errors 
  application type mismatch
    (fun l r ↦ mk_cons l r) eq
  argument
    eq
  has type
    Nat → Nat → Prop : Type
  but is expected to have type
    Type : Type 1
  
  failed to synthesize
    HAndThen (Nat → Nat → Prop) (Base Nat Nat) ?m.3797
  
  Additional diagnostic information may be available using the `set_option diagnostics true` command.
```

(It is a bug to try to use ">>" as the operator name here, which clashes with notation for `HAndThen` in the Prelude. The point is that it shouldn't panic.)

**Actual behavior:**

The expected type error, but also this panic (e.g. in the Output pane of VS Code):

```
PANIC at Lean.MetavarContext.getDecl Lean.MetavarContext:430:17: unknown metavariable
backtrace:
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(+0x7c8c362) [0x7f13a148c362]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_panic+0x4e) [0x7f13a148c27e]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_panic_fn+0x15) [0x7f13a148c3f5]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimMVar+0x46) [0x7f139b114606]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp+0xf19) [0x7f139b10e9e9]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_visit+0x36f) [0x7f139b10f64f]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elim+0x325) [0x7f139b10af55]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_visit+0x36f) [0x7f139b10f64f]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elim+0x79c) [0x7f139b10b3cc]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_MetavarContext_MkBinding_elimMVarDeps+0x53) [0x7f139b11e103]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Nat_foldRevM_loop___at_Lean_MetavarContext_MkBinding_mkBinding___spec__1+0x7b9) [0x7f139b120759]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_MetavarContext_MkBinding_mkBinding+0x1f2) [0x7f139b121842]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_MetavarContext_mkBinding+0x1dc) [0x7f139b1223bc]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_mkForallFVars+0x36c) [0x7f139fd0fc6c]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_InferType_0__Lean_Meta_inferLambdaType___lambda__1+0x20d) [0x7f139f8a1dcd]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_InferType_0__Lean_Meta_inferLambdaType___lambda__1___boxed+0x18) [0x7f139f8a2018]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x3bd) [0x7f13a149f8cd]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process___rarg+0xf6f) [0x7f139fd37dcf]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp___rarg+0x6f) [0x7f139fd3822f]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_lambdaLetTelescope___at___private_Lean_Meta_InferType_0__Lean_Meta_inferLambdaType___spec__1___rarg+0x39) [0x7f139f8a1979]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_inferTypeImp_infer+0x73a) [0x7f139f8ad1ca]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_infer_type+0x2c5a) [0x7f139f893d4a]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_getParamKinds+0xdf) [0x7f139ff782ff]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_delabAppCore+0xabb) [0x7f139ff9fabb]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_delabApp+0x115) [0x7f139ffa22f5]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_7+0x616) [0x7f13a14a3436]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_List_firstM___at_Lean_PrettyPrinter_Delaborator_delabFor___spec__1+0x160) [0x7f13a00de1a0]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_delabFor+0x1be) [0x7f13a00df0be]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_7+0x3cd) [0x7f13a14a31ed]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_orElse___rarg+0xcc) [0x7f13a00c5dec]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_7+0x41c) [0x7f13a14a323c]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_delab___lambda__2+0x305) [0x7f13a00e0c65]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_delab___lambda__3+0x559) [0x7f13a00e2ea9]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_delab___lambda__4+0xac0) [0x7f13a00e5ae0]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_delab___lambda__4___boxed+0x18) [0x7f13a00e7208]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_8+0x21a) [0x7f13a14a48aa]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_Delaborator_delab+0x5f3) [0x7f13a00e6b93]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_7+0x616) [0x7f13a14a3436]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_delabCore___rarg___lambda__1+0x404) [0x7f13a00e7be4]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_delabCore___rarg___lambda__2+0xdd) [0x7f13a00e8d7d]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_delabCore___rarg___lambda__3___boxed+0x22) [0x7f13a00ea3d2]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_6+0x422) [0x7f13a14a1842]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_delabCore___rarg___lambda__4+0x459) [0x7f13a00e99d9]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_delabCore___rarg___lambda__5+0x4b6) [0x7f13a00ea156]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_delabCore___rarg___lambda__6+0xc4) [0x7f13a00ea4c4]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_delabCore___rarg+0x3ee) [0x7f13a00eb1ee]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PrettyPrinter_ppExprWithInfos___lambda__1+0xb0) [0x7f139b138600]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x3bd) [0x7f13a149f8cd]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_withLCtx___at___private_Lean_Meta_Basic_0__Lean_Meta_mkLevelErrorMessageCore___spec__2___rarg+0x17) [0x7f139fd5c3d7]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x3bd) [0x7f13a149f8cd]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l___private_Lean_PrettyPrinter_0__Lean_PrettyPrinter_withoutContext___at_Lean_PrettyPrinter_initFn____x40_Lean_PrettyPrinter___hyg_1096____spec__1+0x10) [0x7f139b1401d0]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x378) [0x7f13a149f888]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_MetaM_run_x27___rarg+0xa2) [0x7f139fcd6c42]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x3bf) [0x7f13a149baef]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_PPContext_runCoreM___rarg+0x478) [0x7f139b1355d8]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x168) [0x7f13a149b898]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_ppExprWithInfos+0x230) [0x7f13a0553aa0]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_ppExprWithInfos+0x1ec) [0x7f139fd5204c]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_ppExpr+0x10) [0x7f139fd522f0]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Info_fmtHover_x3f_fmtTermAndModule_x3f___lambda__1+0x58) [0x7f139b2a0708]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Info_fmtHover_x3f_fmtTermAndModule_x3f___lambda__2+0x3f7) [0x7f139b2a1207]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Info_fmtHover_x3f_fmtTermAndModule_x3f+0xac6) [0x7f139b2a38d6]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_Info_fmtHover_x3f___lambda__5+0x9e) [0x7f139b2a51ae]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_5+0x40e) [0x7f13a149f91e]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Meta_MetaM_run___rarg+0x68) [0x7f139fcd6418]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x3bf) [0x7f13a149baef]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_ContextInfo_runCoreM___rarg___lambda__2+0xac2) [0x7f139ce76c52]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_ContextInfo_runCoreM___rarg+0x499) [0x7f139ce77719]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Elab_ContextInfo_runMetaM___rarg+0x194) [0x7f139ce78eb4]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Server_FileWorker_handleHover___lambda__6+0x49d) [0x7f139b1be3ed]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Server_FileWorker_handleHover___lambda__7+0x192) [0x7f139b1c0142]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Server_FileWorker_handleHover___lambda__7___boxed+0xf) [0x7f139b1c063f]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x70e) [0x7f13a149be3e]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_3+0x69c) [0x7f13a149bdcc]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_2+0x620) [0x7f13a14999b0]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(l_Lean_Server_ServerTask_EIO_mapTaskCheap___rarg___lambda__1+0x10) [0x7f139bc23360]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_2+0x5cc) [0x7f13a149995c]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(+0x7cb48ae) [0x7f13a14b48ae]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x430) [0x7f13a1497cd0]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(lean_apply_1+0x47f) [0x7f13a1497d1f]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(+0x7c96060) [0x7f13a1496060]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(+0x7c96478) [0x7f13a1496478]
/home/daira/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean/libleanshared.so(+0x7c8a2c5) [0x7f13a148a2c5]
/lib/x86_64-linux-gnu/libc.so.6(+0x92083) [0x7f13995b6083]
/lib/x86_64-linux-gnu/libc.so.6(+0x1107b8) [0x7f13996347b8]
```

### Versions

"4.19.0-rc2"
Debian trixie/sid on x86_64

### Impact

Low impact; the problem doesn't occur when the operator name doesn't clash with the Prelude.

Navigation Menu

Uh oh!

PANIC: Lean.MetavarContext:430:17: unknown metavariable #8108

Prerequisites

Description

Steps to Reproduce

Versions

Impact

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Uh oh!

PANIC: Lean.MetavarContext:430:17: unknown metavariable #8108

Description

Prerequisites

Description

Steps to Reproduce

Versions

Impact

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions