Timeout with large arithmetic expression involving numerals

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 following code timeouts with the default maxHeartbeats setting. It sometimes fails at whnf and sometimes at isDefEq, depending on the specific heartbeat setting used.

theorem foo (x y z p q : Int) : False :=
  have : (1 * x ^ 1 + z ^ 1 * p) *
        (1 / 1 * p ^ 1 * x ^ 1 + 1 * q * p ^ 1 * x * z + 1 * q ^ 1 * p ^ 1 * x ^ 1 +
                            1 * q ^ 1 * p ^ 1 * x * z -
                          1 * q * p ^ 1 * y ^ 1 +
                        1 * q ^ 1 * p ^ 1 * x ^ 1 +
                      1 * q ^ 1 * p ^ 1 * x * z -
                    1 * q ^ 1 * p ^ 1 * y ^ 1 +
                  1 * q ^ 1 * p ^ 1 * x ^ 1 +
                1 * q ^ 1 * p ^ 1 * x * z -
              1 * q ^ 1 * p ^ 1 * y ^ 1 +
            1 * q ^ 1 * x ^ 1 -
          1 * q ^ 1 * p * y ^ 1) +
      z * (1 * y) *
        (-(1 / 1 * p ^ 1 * x * y) + 1 * q * p ^ 1 * z * y - 1 * q ^ 1 * p ^ 1 * x * y +
                  1 * q ^ 1 * p ^ 1 * z * y -
                1 * q ^ 1 * p ^ 1 * x * y +
              1 * q ^ 1 * p ^ 1 * z * y -
            1 * q ^ 1 * p ^ 1 * x * y +
          1 / 1 * q ^ 1 * p ^ 1 * z * y) +
    (-y ^ 1 + p * x * (1 * z) + q * (1 * z ^ 1)) *
      (-(1 / 1 * p ^ 1 * x * z) - 1 * q * p ^ 1 * x ^ 1 - 1 * q ^ 1 * p ^ 1 * x * z -
                1 * q ^ 1 * p ^ 1 * x ^ 1 -
              1 * q ^ 1 * p ^ 1 * x * z -
            1 * q ^ 1 * p ^ 1 * x ^ 1 -
          1 * q ^ 1 * p ^ 1 * x * z -
        1 * q ^ 1 * p * x ^ 1) =
  1 *
        (1 / 1 * p ^ 1 * x ^ 1 + 1 * q * p ^ 1 * x * z + 1 * q ^ 1 * p ^ 1 * x ^ 1 +
                            1 * q ^ 1 * p ^ 1 * x * z -
                          1 * q * p ^ 1 * y ^ 1 +
                        1 * q ^ 1 * p ^ 1 * x ^ 1 +
                      1 * q ^ 1 * p ^ 1 * x * z -
                    1 * q ^ 1 * p ^ 1 * y ^ 1 +
                  1 * q ^ 1 * p ^ 1 * x ^ 1 +
                1 * q ^ 1 * p ^ 1 * x * z -
              1 * q ^ 1 * p ^ 1 * y ^ 1 +
            1 * q ^ 1 * x ^ 1 -
          1 * q ^ 1 * p * y ^ 1) +
      1 *
        (-(1 / 1 * p ^ 1 * x * y) + 1 * q * p ^ 1 * z * y - 1 * q ^ 1 * p ^ 1 * x * y +
                  1 * q ^ 1 * p ^ 1 * z * y -
                1 * q ^ 1 * p ^ 1 * x * y +
              1 * q ^ 1 * p ^ 1 * z * y -
            1 * q ^ 1 * p ^ 1 * x * y +
          1 / 1 * q ^ 1 * p ^ 1 * z * y) +
    1 *
      (-(1 / 1 * p ^ 1 * x * z) - 1 * q * p ^ 1 * x ^ 1 - 1 * q ^ 1 * p ^ 1 * x * z -
                1 * q ^ 1 * p ^ 1 * x ^ 1 -
              1 * q ^ 1 * p ^ 1 * x * z -
            1 * q ^ 1 * p ^ 1 * x ^ 1 -
          1 * q ^ 1 * p ^ 1 * x * z -
        1 * q ^ 1 * p * x ^ 1) := sorry
  sorry

The problem goes away when introducing a new parameter w : Nat and replacing all 1 by w.

set_option diagnostics true shows some interesting type class numbers:

[type_class] used instances (max: 42539, num: 13): ▼
  USize.instOfNat ↦ 42539
  Int.instHPowNat ↦ 42145
  Lean.Omega.IntList.instHMulInt ↦ 21357
  instHMul ↦ 11896
  instPowNat ↦ 8621
  instHSubPos ↦ 5140
  instHAddPosChar ↦ 4084
  Lean.Omega.IntList.instNeg ↦ 845
  instHAdd ↦ 440
  instHSub ↦ 189
  Int.instMul ↦ 90
  Int.instAdd ↦ 31
  Int.instSub ↦ 29

Context

The linear_combination tactic in mathlib is suffering from performance issues, and handling terms that look like the example above seems to be part of the reason why it is so slow.

Steps to Reproduce

1. Copy the above code into the Lean web editor.

Expected behavior: Elaboration should be very fast

Actual behavior: Timeouts

Versions

4.11.0-nightly-2024-07-27 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.

Reproduce the supplied theorem in the Lean web editor with the reported nightly version, then enable set_option diagnostics true and inspect the type-class instance diagnostics around whnf and isDefEq. Compare the original numerals with the w : Nat variant; done means the large expression elaborates quickly without timing out and the behavior is covered by a regression check.