Slow typechecking at `rewrite`

Stream: mathlib4

[Gareth Ma]

Hi, I am back for more bugs. I am not sure why the following is slow. What is the "type checking" in question? Isn't everything just Nat? lol. Also, if you remove the rewrite, the problem goes away. If you replace digitsLen with a simpler function like fun a => a + 1, the problem goes away. If you make 128 bigger, it gets even worse.

import Mathlib.Data.Nat.Digits
import Mathlib.Algebra.BigOperators.Ring

open Nat Finset BigOperators

set_option profiler true

def digitsLen : ℕ → ℕ := fun a ↦ (digits 10 a).length

/- type checking took 6.1s -/
example : ∑ k in range 128, digitsLen k * 2 < 977778 := by
  rewrite [←sum_mul]
  done

[Gareth Ma]

Not sure if this is related.

[Kyle Miller]

Don't forget that propositions are types, and theorems have types, etc.

Probably something is being unfolded, but I didn't look into it beyond noticing that if you give arguments explicitly it's fast:

example : ∑ k in range 128, digitsLen k * 2 < 977778 := by
  rewrite [← sum_mul (s := range 128) (f := digitsLen) (b := 2)]
  done

[Gareth Ma]

I see, I also think the sum over the range is unfolded, but not sure why it is happening. Your fix works so thanks! :)