Interpreter crash with `unreachable`

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Lean4 language server crashes with unreachable while I was editing a function in VSCode. Obviously, the code is syntactically malformed, but the observed behaviour seems unexpected.

This is reproducable on both stable and nightly, windows and linux.

I was able to reduce the file to the following:

import Lean
import Lean.Meta

def some_work_in_progress_code (input : Lean.Expr) (vars : Std.HashMap Lean.Expr Nat) :
  Lean.Expr -> (Std.HashMap Lean.Expr Nat) × Lean.Expr
  | L    -- This line is work in progress. I was typing
  | Lean.Expr.app (Lean.Expr.app _ lhs) rhs =>
    let (vars, lhs) :=some_work_in_progress_code input vars lhs
    (vars, .const `stuff [])
  | e => (vars, .const `stuff [])

elab "stuff" : tactic => do
  Lean.Elab.Tactic.withMainContext <| do
    let goal <- Lean.Elab.Tactic.getMainTarget
    if let some (input, lhs, rhs) := <- Lean.Meta.matchEq? goal then
      let vars :=Std.mkHashMap
      let (vars, lhs) :=some_work_in_progress_code input vars lhs
      Lean.logInfo <| lhs

example : ∀ x y : Nat, x = x + y :=by
  intro x y
  stuff
  sorry

Steps to Reproduce

1. Copy the above snippet to VSCode with a Lean4 plugin installed
2. Alternatively, just save the above snippet to a .lean file and call the lean executable on it

Expected behavior:
No crash. Just a red squiggle

Actual behavior:
The lean4 executable crashes with unreachable

Reproduces how often:
Always

Versions

1. Stable on Windows 11: Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
2. Nightly on Gitpod (Ubuntu 20.04.4 LTS) : Lean (version 4.0.0-nightly-2022-08-28, commit cd0dd4cc2fb4, Release)