implemented_by unexpectedly sees _unary and fails

[Junology]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

If a function f is defined using well-founded recursion, then implemented_by attribute looks f._unary instead of f.
As a result, it causes a type error if more than one arguments are involved in the termination proof.

Context

Discussed in Zulip

Steps to Reproduce

MWE:

def myfunUnsafe (x : Array α) (i : Fin x.size) : Array α :=
  sorry

/-
Error:
> invalid 'implemented_by' argument 'myfunUnsafe', 'myfunUnsafe' has type
>   {α : Type u_1} → (x : Array α) → Fin (Array.size x) → Array α
> but 'myfun._unary' has type
>   {α : Type u_1} → (x : Array α) ×' Fin (Array.size x) → Array α
-/
@[implemented_by myfunUnsafe]
def myfun (x : Array α) (i : Fin x.size) : Array α :=
  let next := 2*i.1 + 1
  if h : next < x.size then
      have : x.size - next < x.size - i.1 := sorry
      myfun (x.swap i ⟨next,h⟩) ⟨next, (x.size_swap _ _).symm ▸ h⟩
  else
    x
termination_by _ => x.size - i.1

Versions

Lean version: 4.3.0-rc1