MkIffOfInductiveProp produces proofs with metavariable issues and type mismatch issues #29742
Description
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