"(kernel) declaration has metavariables" error when let rec is in decreasing_by clause

[nesken7777]

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

A definition with let rec inside decreasing_by clause fails with the error: "(kernel) declaration has metavariables".

Context

I ran into this problem when trying to write a bubble sort using tail recursion like this:

def bubbleSort [Ord α] (arr : Array α) : Array α :=
  let rec loop₁ [Ord α] (arr : Array α) (i : Nat) : Array α := -- (kernel) declaration has metavariables 'bubbleSort.loop₁._unary'
    let rec loop₂ [Ord α] (arr : Array α) (i : Nat) (j : Nat) : Array α :=
      if h_index : j < arr.size - 1 - i then
        match Ord.compare arr[j] arr[j + 1] with
        |.gt => loop₂ (arr.swap j (j + 1)) i (j + 1)
        |.lt |.eq => loop₂ arr i (j + 1)
      else
        arr
    if i < arr.size then
      loop₁ (loop₂ arr i 0) (i + 1)
    else
      arr
  termination_by arr.size - i
  decreasing_by
    let rec loop₂_size_eq [Ord α] (arr : Array α) (i j : Nat) : (bubbleSort.loop₁.loop₂ arr i j).size = arr.size := by
      unfold bubbleSort.loop₁.loop₂
      split
      case isTrue =>
        split <;> rw[loop₂_size_eq]
        case h_1 => exact arr.size_swap j (j + 1)
      case isFalse => rfl
    rw[loop₂_size_eq]
    rename_i h
    exact Nat.sub_succ_lt_self arr.size i h
  loop₁ arr 0

In this example, let rec is needed to use rw[loop₂_size_eq]

Steps to Reproduce

Minimized reproduction:

def foo (i : Nat) : Nat := -- (kernel) declaration has metavariables 'foo'
  if i < 10 then
    foo (i + 1)
  else
    10
  termination_by 10 - i
  decreasing_by
    let rec r : 0 = 0 := rfl
    rename_i h
    exact Nat.sub_succ_lt_self 10 i h

Expected behavior: The definition completes without errors

Actual behavior: (kernel) declaration has metavariables error

Versions

#version -- Lean 4.16.0-nightly-2024-12-24

Platform: live.lean-lang.org

Impact

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

[nomeata]

I'm always amused by the kind of unexpected programs users write, and they are absolutely not to blame :-)

My brain runs in circles trying to find out if this can be easily supported given the current implementation of recursive functions. Maybe easiest to just disallow nested recursive definitions in termination_by or decreasing_by.

Oh, and while we are at it we should check what what lean does when trying to call the function of interest from it's own termination or decreasing clause.