Some functions using `List.foldr` are specialized for common argument types before the tail-recursive `foldr` is available

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

#eval (List.range 1000000).sum

crashes due to a stack overflow even though List.sum is implemented via List.foldr and a csimp lemma is available for that.

The reason for this is that we define Nat.sum in List/Basic.lean, which creates the specialization of List.foldr for adding natural numbers, and it uses the naive implementation of foldr as the csimp lemma for List.foldr is not available yet. When using List.sum on a list of natural numbers later, Lean will reuse this specialization, even though the csimp lemma is available now.

Similarly, the specialization for adding lists of integers is created when defining Lean.Omega.IntList.sum, and the csimp lemma is not imported there either.

This means that in practice, users using List.sum to sum up lists of natural numbers or integers in their downstream projects will not use a tail-recursive implementation.

Context

This was noticed by @datokrat while doing some benchmarks.

Expected behavior: Summing up lists of Nat and Int should be tail-recursive

Actual behavior: Crashes due to stack overflow

Versions

4.19.0-nightly-2025-03-30 on live.lean-lang.org

Impact

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