Cannot derive functional induction principle for a recursive function: 'still depends on' named pattern matches

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

Deriving the functional induction principle for the following function returns an error about the motive 'still depending on' a dependent match inside the function.

Steps to Reproduce

This is a heavily minimised but still meaningful example:

mutual

variable (f: Nat -> Option Nat)

def walk (hf : ∀ n k, f n = some k → k < n) (n : Nat) : Bool :=
  n == 42 ||
  match n with
  | 0 => false
  | m + 1 =>
    match hst : f (m + 1) with
    | some k => step hf (m + 1) k hst
    | none => false
termination_by (n, 1)
decreasing_by exact Prod.Lex.right _ (by omega)

def step (hf : ∀ n k, f n = some k → k < n)
    (n : Nat) (k : Nat) (hst : f n = some k) : Bool :=
  walk hf k
termination_by (n, 0)
decreasing_by exact Prod.Lex.left _ _ (hf _ _ hst)

end

#check @walk.induct   -- returns the error quoted below
#check @step.induct   -- returns the error quoted below (slightly different names)

Expected behavior: A working induction principle should be generated

Actual behavior: The error below is produced instead:

Failed to realize constant walk.induct:
  Cannot derive functional induction principle (please report this issue)
    Type motive
      (PSum.inr
        ⟨m + 1,
          ⟨k,
            hst⟩⟩) of alternative fun m x k hst =>
      id (x (PSum.inr ⟨m + 1, ⟨k, hst⟩⟩) (walk._mutual._proof_2 f m k hst)) still depends on hst

Versions

Lean 4 nightly-2026-04-22 (updated a few minutes ago). Reproducible on live.lean-lang.org as well.

Additional Information

Note that despite the above being a mutual recursion, the mutual induction itself is not the source of bug, as the following simpler recursive function produces an error, but with a slightly different error message:

def walkSolo (f : Nat → Option Nat) (hf : ∀ n k, f n = some k → k < n) (n : Nat) : Bool :=
  n == 42 ||
  match n with
  | 0 => false
  | m + 1 =>
    match hst : f (m + 1) with
    | some k =>
      have : k < m + 1 := hf _ _ hst
      walkSolo f hf k
    | none => false
termination_by n

#check @walkSolo.induct -- returns a slightly different error; see below

The error message is now

failed to transform matcher, type error when constructing new pre-splitter motive: [...] failed with Application type mismatch: [...].

I included the mutual recursion example first because that reproduces the precise error message in my actual use case.

I've tried to debug a bit and noticed that removing the short-circuiting path n==42 will completely resolve the issue, although that is not generally possible in my original function.

#11540 seems to be related, but the example there produces yet another different error message that doesn't seem related to dependent pattern matches.

Note that the first example also witnesses the same issue as in #2920 as well, where the linter reports a false positive on unused variables (hst in step, which is actually used in the termination proof).

Impact

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

Start with the minimal mutual-recursion example in the issue and run #check @walk.induct and #check @step.induct on Lean nightly, then compare with the walkSolo example. Trace the functional-induction derivation around the dependent hst match and short-circuiting path; done means both induction principles are generated without an error, while preserving the reported termination behavior.