fun_cases: fails with dependent match

This tricky example, based on an example provided by @Rob23oba in https://github.com/leanprover/lean4/issues/8195#issuecomment-2848207869, causes the FunInd code to stumble:

-- set_option trace.Meta.FunInd true

def myTest {α}
  (mmotive : (x : List α) → Sort v)
  (x : List α)
  (h_1 : (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc))
  (h_2 : (x' : List α) → x = x' → mmotive x') : mmotive x :=
  match (generalizing := false) h : x with
  | a :: dc => h_1 a dc h
  | x' => h_2 x' h


/--
error: Failed to realize constant myTest.fun_cases:
  Cannot derive functional cases principle (please report this issue)
  ⏎
    application type mismatch
      motive mmotive x✝ h_1
    argument
      h_1
    has type
      (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
    but is expected to have type
      (a : α) → (dc : List α) → x✝ = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
---
error: unknown identifier 'myTest.fun_cases'
---
error: failed to transform matcher, type error when constructing new pre-splitter motive:
  myTest.match_1 (fun x => motive mmotive x h_1 h_2) x
-/
#guard_msgs in
def foo := @myTest.fun_cases

Versions

Lean 4.20.0, commit 6074ca7452baf54e42de0abc03cdc746af51d5d8

Impact

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

Start by reproducing the dependent-match example in the issue and enable the FunInd trace to inspect functional-cases derivation. Read the handling of the generated myTest.fun_cases principle and the matcher transformation; done means the definition elaborates and #guard_msgs no longer reports the shown errors.