Termination check not preserved under let binding.

Stream: lean4

[Siddharth Bhat]

When f is a recursive function, changing an application of f x to let name := x; f name can cause the termination checker to fail on nightly "4.0.0-nightly-2022-04-26".

MWE:

import Lean
#eval Lean.versionString

section events
universe u v

-- | Polymorphic to and sum.
def pto (E: Type → Type u) (F: Type → Type v) :=
  ∀ T, E T → F T
def psum (E: Type → Type u) (F: Type → Type v) :=
  fun T => E T ⊕ F T
inductive PVoid: Type -> Type u
infixr:40 " ~> " => pto
infixr:60 " +' " => psum
end events



/- finite interaction trees -/
inductive Fitree (E: Type → Type u) (R: Type) where
  | Ret (r: R): Fitree E R
  | Vis {T: Type} (e: E T) (k: T → Fitree E R): Fitree E R

/-
Describe the ability to split a sum type L + R into LR.
-/
class SumSplit (L: Type -> Type) (LR: Type -> Type) (R: Type -> Type)  where
  redSplit: LR ~> L +' R

instance {L: Type -> Type}: SumSplit L  L PVoid where
  redSplit := fun T l => Sum.inl l

instance {L: Type -> Type} {R: Type -> Type}: SumSplit L (L +' R) R where
  redSplit := fun T lr => lr

/- peel an itree along a split -/
def splitTree [SumSplit EL ELR ER] (t: Fitree ELR X): Fitree (EL +' ER) X :=
  match t with
  | Fitree.Ret x => Fitree.Ret x
  | @Fitree.Vis _ _ T e k =>
     Fitree.Vis (SumSplit.redSplit _ e) (fun t' =>
        let kt := (k t')
        splitTree kt)
        -- splitTree (k t'))

Error

"4.0.0-nightly-2022-04-26"
mwe-split-tree.lean:37:4: error: fail to show termination for
  splitTree
with errors
argument #6 was not used for structural recursion
  failed to eliminate recursive application
    splitTree kt

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

Desired Behavior

Changing the final line from splitTree kt into splitTree (k t') makes the definition succeed. It would be nice if both versions succeed the termination checker.

[Leonardo de Moura]

Pushed a fix for this issue: https://github.com/leanprover/lean4/commit/7c427c1ef27d65cec81c5b78e4737eaf312d21d4