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

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.

Start by running the minimized foo reproduction from the issue with Lean 4.16.0-nightly-2024-12-24 and confirm the kernel error. Compare it with the expected successful definition, then trace how let rec in the decreasing_by clause is handled; done means the reproduction completes without errors.