panic on match equality proof

Stream: lean4

[Chris B]

I'm not sure whether the lean 4 repo is open to taking general-purpose issues yet, but I have an mwe for a panic that manifests in vscode's output window:

example (x : Nat) : True :=
match h:x with

-- PANIC at Array.insertAt Init.Data.Array.Basic:679:22: invalid index
-- Lean (version 4.0.0-nightly-2021-09-24, commit 2ca4188fc3d1, Release)

The panic message appears when I hit the h key on the last with, and this only happens if h:x is written with no whitespace. If it's written as h : x there's no panic.

[Chris B]

Somewhat unrelated, but another panic situation:

structure A where
h : Nat := 1
h2 : h ≠ 0 := by

-- PANIC at Lean.Elab.Term.quoteAutoTactic Lean.Elab.Binders:60:28: unreachable code has been reached