Interpreter crash with `unreachable`

[mirkootter]

Prerequisites

• [X] 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)

[Kha]

This is an interesting disagreement of whether infinite recursion is an observable effect between IR phases.

[elim_dead_branches]
def some_work_in_progress_code (x_1 : obj) (x_2 : obj) (x_3 : obj) : obj :=
  let x_4 : u8 := 1;
  let x_5 : obj := sorryAx ◾ x_4;
  let x_6 : obj := some_work_in_progress_code x_1 x_2 x_5;
  case x_6 : obj of
  Prod.mk →
    ⊥

ElimDeadBranches (unintentionally?) assumes that infinite recursion necessarily leads to unreachable code...

[boxing]
def some_work_in_progress_code (x_1 : @& obj) (x_2 : @& obj) (x_3 : @& obj) : obj :=
  ⊥

... but Boxing disagrees

[Kha]

Whether this code should have been produced and run in the first place is a completely different question of course

[leodemoura]

@Kha I didn't read this issue yet. If it is relevant to the new code generator, could you please tag it with "depends on new code ..."?

[Kha]

Not sure. The direct issue of "we probably shouldn't even try to run this code" is rather in the frontend. The optimization issue depends on whether the compiler reimplementation will touch the mentioned phases.

[gebner]

I think the syntax error is a red herring here. Minimized:

partial def swipc (_ : Unit) : Nat × Nat :=
  let (a, b) := swipc ()
  (a, b)

(EDIT: now without syntax error)

[gebner]

From what I can tell, the issues are all in the part of the compiler which is already written in Lean.

[Kha]

I think the syntax error is a red herring here

It's a legitimate bug in itself though. There is no unguarded recursion in the original input, it was made up by the elaborator.

[leodemoura]

I think the syntax error is a red herring here

It's a legitimate bug in itself though. There is no unguarded recursion in the original input, it was made up by the elaborator.

So, there are two bugs :( The example in @gebner's comment is exposing a bug at ElimDeadBranches.lean that you pointed out above.