Closed term extraction for large list literals produces large call stacks

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

Closed term extraction for large list and array literals produces a linked list of functions. For example, the code

set_option trace.compiler.ir.result true
def a := [0, 0, 0, 0, 0]

yields

[result]
def a._closed_1 : obj :=
  let x_1 : obj := ctor_0[List.nil];
  let x_2 : obj := 0;
  let x_3 : obj := ctor_1[List.cons] x_2 x_1;
  ret x_3
def a._closed_2 : obj :=
  let x_1 : obj := 0;
  let x_2 : obj := a._closed_1;
  let x_3 : obj := ctor_1[List.cons] x_1 x_2;
  ret x_3
def a._closed_3 : obj :=
  let x_1 : obj := 0;
  let x_2 : obj := a._closed_2;
  let x_3 : obj := ctor_1[List.cons] x_1 x_2;
  ret x_3
def a._closed_4 : obj :=
  let x_1 : obj := 0;
  let x_2 : obj := a._closed_3;
  let x_3 : obj := ctor_1[List.cons] x_1 x_2;
  ret x_3
def a._closed_5 : obj :=
  let x_1 : obj := 0;
  let x_2 : obj := a._closed_4;
  let x_3 : obj := ctor_1[List.cons] x_1 x_2;
  ret x_3
def a : obj :=
  let x_1 : obj := a._closed_5;
  ret x_1

Large list literals have several problems (see for example #5683), but one of the problems is that they will cause the interpreter to overflow its stack when trying to access the list. Since array literals desugar to list literals, this is also true for array literals.

Context

This causes Lean to crash on a test for time zone database parsing that we wanted to add. The workaround is to use small literals instead.

Steps to Reproduce

1. Run lean on this file.

terminate called after throwing an instance of 'lean::throwable'
  what():  deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system)
interpreter stacktrace:
#1 l._closed_4522
#2 l._closed_4523
#3 l._closed_4524
#4 l._closed_4525
#5 l._closed_4526
#6 l._closed_4527
#7 l._closed_4528
#8 l._closed_4529
#9 l._closed_4530
#10 l._closed_4531
#11 l._closed_4532
#12 l._closed_4533
#13 l._closed_4534
#14 l._closed_4535
#15 l._closed_4536
#16 l._closed_4537
#17 l._closed_4538
#18 l._closed_4539
#19 l._closed_4540
#20 l._closed_4541

and so on for a few thousand lines.

Expected behavior: Interpreter can cope with the list.

Actual behavior: See error message above.

Versions

Lean (version 4.15.0-pre, commit bf2e39c2b89a, Release)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.