FunInd chokes on pattern match with dependent targets

[nomeata]

Lean.Meta.MatcherApp.transform, used by FunInd, chokes upon a dependent match as is produced by

def bar (n : Nat) : Bool :=
  if h : n = 0 then
    true
  else
    have m+1 := n
    bar m
termination_by n

/-
error: failed to transform matcher, type error when constructing new pre-splitter motive:
  bar.match_1
    (fun n h_1 =>
      h = h_1 → (∀ (y : Nat), (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y n → motive y) → motive n)
    x h
---
error: application type mismatch
  h✝ = h
argument
  h
has type
  ¬n✝ = 0 : Prop
but is expected to have type
  ¬x = 0 : Prop
-/
#check bar.induct

The have syntax is desugared to

def baz (n : Nat) : Bool :=
  if h : n = 0 then
    true
  else
    match n, h with
    | m+1, _ => baz m
termination_by n
#check baz.induct

And also affects other types, e.g.

def foo [DecidableEq α] (xs : List α) : Bool :=
  if h : xs = [] then
    true
  else
    have _::ys := xs
    foo ys
termination_by xs
#check foo.induct

Versions

4.9.0-nightly-2024-05-11

Impact

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