`MkIffOfInductiveProp` produces proofs with metavariable issues and type mismatch issues

The following code that makes use of mk_iff attribute produces a code that cannot be added by the kernel due to metavariable issues and type mismatch in the application.

import Mathlib.Tactic.MkIffOfInductiveProp

/--
error: (kernel) application type mismatch
  @test1_functor.mk α✝ a✝⁴ a✝³ a✝¹ w✝ left✝¹
argument has type
  a✝³ w✝ w✝
but function has type
  a✝⁴ a✝¹ w✝ → a✝³ w✝ w✝ → @test1_functor α✝ a✝⁴ a✝³ a✝¹ a✝¹
-/
#guard_msgs in
@[mk_iff] inductive test1_functor.{u_1} : {α : Sort u_1} → (α → α → Prop) → (α → α → Prop) → α → α → Prop where
| mk : ∀ {α : Sort u_1} (r call : α → α → Prop) {a b : α},
  r a b → call b b → test1_functor r call a a

/-- error: (kernel) declaration has metavariables 'test2_functor_iff' -/
#guard_msgs in
@[mk_iff] inductive test2_functor.{u_1} : {α : Sort u_1} → (α → α → Prop) → α → (α → Prop) → α → Prop where 
  | mk : ∀ {α : Sort u_1} (r : α → α → Prop) (a : α) (call : α → Prop) {b : α},
  r a b → call b → test2_functor r a call a

Expected behaviour:
The code generated by MkIffOfInductiveProp should be accepted by the kernel.

Actual behaviour:
The errors described above

Lean version:
4.24.0-rc1 on live.lean-lang.org

Start with the reproducer in the issue and inspect the Mathlib.Tactic.MkIffOfInductiveProp implementation it imports. Confirm the generated declarations for both inductive examples and trace the metavariables and application types involved; done means the examples are accepted by the kernel without the reported errors.