Qq bug: declaration has metavariable `_unsafe_rec`

Stream: lean4

[Vasilii Nesterov]

Hi there! I ran into a strange bug while using Qq:

import Qq

open Qq Lean

opaque Foo {α β : Type} (f : α → β) : Prop

-- (kernel) declaration has metavariables 'proveFoo._unsafe_rec'
partial def proveFoo {α β : Q(Type)} (f : Q($α → $β)) :
    MetaM Q(Foo $f) := do
  match β with
  | ~q(Nat) => failure
  | ~q(Int) =>
    let t : Q(Prop) := sorry
    let ~q(@Foo $α'' $β'' $f'') := t | failure
    let pf : Q(Foo $f) ← proveFoo q($f)
    failure

Lean complains that proveFoo contains metavariables. Can someone explain why this is happening?