Unexpected error: index out of bounds caused by the mere presence of a function

[PeterKementzey]

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

I get an error: index out of bounds because of this function even though I am not even calling it anywhere in the code. If the debug trace is enabled the issue disappears.

Steps to Reproduce

def foo (array : Array Nat) : Nat -> Nat
  | 0 => 0
  | n + 1 =>
    let array := array.filter (!.==5) -- This seems to be necessary to reproduce, the condition does not matter

    if array.isEmpty then 0 else
      let arrayOfLast := #[array.back]
      -- let arrayOfLast := dbgTrace (toString arrayOfLast) (fun _ => arrayOfLast)
      -- Error: if the line above that doesn't do anything is commented out then I get an `Error: index out of bounds message` when running.
      foo arrayOfLast n

def main : IO Unit :=
  IO.println ("hi")

1. leanpkg build bin
2. run the executable

Expected behavior: Nothing (printing hi).

Actual behavior: Error: index out of bounds

Reproduces how often: Always

Versions

Lean (version 4.0.0-nightly-2021-06-16, commit 7485ab5, Release)

OS:
Description: Ubuntu 20.04.2 LTS
Release: 20.04
Codename: focal

Running on WSL 2

[Kha]

The current eager extraction of closed terms does not mesh well with panics. This will be fixed with #467; in the mean time, I'd advise to compile the code with set_option compiler.extract_closed false, which usually does not introduce significant overhead.