exponential blow-up in `isDefEq` when unifying nested `List.map` calls

Prerequisites

• 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

In the following example, the (failing) isDefEq check between the two propositions takes about 1.7s, increasing 2x with every additional nested .map call:

module
import Init

set_option trace.profiler true
set_option trace.profiler.threshold 5

set_option maxHeartbeats 800000
example (xs : List Nat)
    (h : 0 < (xs.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)
      |>.map (· + 1)).length) :
    0 < xs.length := by
  exact h

Expected behavior:

The example should fail, but faster. These expressions should be checked for definitional equality in reasonable time: They superficially aren't highly dependently typed.

Actual behavior:

The runtime is exponential in the number of nested List.map calls.

Versions

Lean 4.30.0-nightly-2026-03-18
Target: x86_64-unknown-linux-gnu

(Lean 4 Web)

Additional Information

I'm not fully sure, but the problem seems to be in whnfImp.

• First, whnfCore runs and it tries reduceMatcher? for (inner_expr).map. Finally, reduceMatcher? e gets stuck and so whnfCore returns e.
• Later in whnfImp, unfoldDefinition? again delta-unfolds List.map and again tries to reduce.

Both of these compute the WHNF of the same inner map expression, apparently without profiting from a cache.

Now this goes down fifteen layers of List.map calls. On each layers, the number of whnf calls doubles, leading to exponential blow-up.

Impact

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

Start by running the minimal reproducer with profiler tracing and inspect whnfCore, reduceMatcher?, and whnfImp around the repeated List.map reduction. Compare the duplicated WHNF work across added map layers; done means the example still fails as expected without exponential runtime, with a regression test covering the behavior.