structural recursion fails when matching on `f x` where `f ` is argument’s subterm

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

Mutual/Nested structural recursion seems to fail on large inductive types.
Consider the following example:

inductive Foo where
  | foo : (String → Option Foo) → Foo

def Foo.map (m : Foo → Foo) : Foo → Foo
  | .foo f => .foo fun s => match f s with
    | none => none
    | some x => map m x
termination_by structural x => x

Despite structural recursion being supported on both large inductive types and nested inductives, mixing the two leads to a failure. In a similar manner, the following function recursing over a large mutual inductive fails with the same error:

mutual
inductive Bar where
  | none
  | some (x : Foo)

inductive Foo where
  | foo : (String → Bar) → Foo
end

def Foo.map (m : Foo → Foo) : Foo → Foo
  | .foo f => .foo fun s => match f s with
    | .none => .none
    | .some x => .some (map m x)
termination_by structural x => x

Expected behavior: No error, these functions get accepted

Actual behavior: Structural recursion fails with the following error:

failed to infer structural recursion:
Cannot use parameter #2:
  failed to eliminate recursive application
    map m x

Versions

Lean 4.12.0-nightly-2024-10-24
Target: x86_64-unknown-linux-gnu

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 two minimal examples from the issue against the Lean nightly release and confirm the structural-recursion error. Then trace the structural recursion handling for recursive calls such as map m x; done means both examples are accepted without the reported elimination failure.