specialization can put expensive computations in loops

[digama0]

def build (n : Nat) : Array Unit := do
  let mut out := #[]
  for _ in [0:n] do
    out := out.push ()
  out

@[noinline] def size : IO Nat := pure 50000

def bench (f : ∀ {α : Type}, α → IO Unit := fun _ => ()) : IO Unit := do
  let n ← size
  let arr := build n
  timeit "time" $
    for _ in [:30] do
      f $ #[1, 2, 3, 4].map fun ty => arr[ty]

#eval bench -- 2.5 s

Looking at the trace, it appears that the evaluation of let arr := build n is lowered into the function, as if it were written:

def bench (f : ∀ {α : Type}, α → IO Unit := fun _ => ()) : IO Unit := do
  let n ← size
  timeit "time" $
    for _ in [:30] do
      f $ #[1, 2, 3, 4].map fun ty => (build n)[ty]

which causes the large array to be constructed 120 times.