`declaration has metavariables` error with matching and recursion

[vasnesterov]

The following code fails with (kernel) declaration has metavariables 'proveFoo._unsafe_rec' error. I'm not sure why this is happening, and can't minimize it further.

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