Non-Linear Growth In Elaboration Time With A Number Of Local Vars Declared With Let

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

The elaboration time seems to incease in a non-linear manner as more local vars are declared with let, where the let body involves synthesis of some proof for e.g. bounds checking (I know that in this mwe the proof is unused). Changing the lets to haves elaborates immediately. This also elaborates normally if it is put in tactic mode, or if the h argument of the subtypeSet is removed.

Apparently it looks similar to issue lean#5108 but it is not the same underlying issue.

This is the example code causing a problem:

-- Elaborates normally if the `h` argument is removed.
set_option linter.unusedVariables false in
def subtypeSet (xs : {val : Array UInt64 // val.size = 25}) (i : Nat) (h : i < 25 := by decide) : {val : Array UInt64 // val.size = 25} :=
  xs

set_option linter.unusedVariables false in
def theta (x : {val : Array UInt64 // val.size = 25}) : {val : Array UInt64 // val.size = 25} :=  
  let A := subtypeSet x 0
  let A := subtypeSet x 1
  let A := subtypeSet x 2
  let A := subtypeSet x 3
  let A := subtypeSet x 4
  let A := subtypeSet x 5
  let A := subtypeSet x 6
  let A := subtypeSet x 7
  let A := subtypeSet x 8
  let A := subtypeSet x 9
  let A := subtypeSet x 0
  let A := subtypeSet x 1
  let A := subtypeSet x 2
  let A := subtypeSet x 3
  let A := subtypeSet x 4
  let A := subtypeSet x 5
  let A := subtypeSet x 6
  let A := subtypeSet x 7
  -- Progressively more slow-down as these are uncommented
  let A := subtypeSet x 8
  let A := subtypeSet x 9
  --let A := subtypeSet x 0
  --let A := subtypeSet x 1
  --let A := subtypeSet x 2
  --let A := subtypeSet x 3
  --let A := subtypeSet x 4
  A

Example of the code elaborating normally, when put in tactic mode:

-- Elaborates normally if the `h` argument is removed.
set_option linter.unusedVariables false in
def subtypeSet (xs : {val : Array UInt64 // val.size = 25}) (i : Nat) (h : i < 25 := by decide) : {val : Array UInt64 // val.size = 25} :=
  xs

set_option linter.unusedVariables false in
def theta (x : {val : Array UInt64 // val.size = 25}) : {val : Array UInt64 // val.size = 25} := by 
  let A := subtypeSet x 0
  let A := subtypeSet x 1
  let A := subtypeSet x 2
  let A := subtypeSet x 3
  let A := subtypeSet x 4
  let A := subtypeSet x 5
  let A := subtypeSet x 6
  let A := subtypeSet x 7
  let A := subtypeSet x 8
  let A := subtypeSet x 9
  let A := subtypeSet x 0
  let A := subtypeSet x 1
  let A := subtypeSet x 2
  let A := subtypeSet x 3
  let A := subtypeSet x 4
  let A := subtypeSet x 5
  let A := subtypeSet x 6
  let A := subtypeSet x 7
  -- Progressively more slow-down as these are uncommented
  let A := subtypeSet x 8
  let A := subtypeSet x 9
  --let A := subtypeSet x 0
  --let A := subtypeSet x 1
  --let A := subtypeSet x 2
  --let A := subtypeSet x 3
  --let A := subtypeSet x 4
  exact A

Context

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Slow.20elaboration.20of.20lets/near/468282213

Steps to Reproduce

The code snippets above are enough to reproduce the issue.

Versions

"4.12.0-nightly-2024-09-12"

Additional Information

N/A

Impact

The use case is the implementation of the SHA3 primitive, where there is a lot array accesses. I cannot remove the checks that array accesses are in-bound.

Start by running the provided subtypeSet and theta snippets against the stated Lean nightly version, then compare the term-mode behavior with the tactic-mode and have variants described in the issue. The issue is resolved when repeated let bindings with default bound proofs no longer show non-linear elaboration slowdown without removing the checks.