Slow elaboration of lets

Stream: lean4

[Chris Bailey]

Someone in the San Francisco thread had an issue that I think can be minimized to the code below (their example involved GetElem). There seems to be something nonlinear happening when there are a lot of local vars 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.

Nothing in the diagnostics or pp.all output jump out. Can anyone shed some light on what might be going on?

-- 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

[Kim Morrison]

I wonder if this is the same as lean#5108.

[Kim Morrison]

No, seems to be different. lean#5108 appears to be caused by cases accumulating copies of let binding.

This example isn't in tactic mode, and indeed if you change it to tactic mode you see linear behaviour again!