perf: remove @[specialize] from mkBinding (#6019)

This PR removes @[specilize] from `MkBinding.mkBinding`, which is a
function that cannot be specialized (as none of its arguments are
functions). As a result, the specializable function `Nat.foldRevM.loop`
doesn't get specialized, which leads to worse performing code.

As expected, the mathlib bench shows a very small improvement. About 95%
of files show a speedup.
(http://speed.lean-fro.org/mathlib4/compare/e7b27246-a3e6-496a-b552-ff4b45c7236e/to/6033df75-aa53-44d9-819d-51f93fc05e94?hash1=b28f0d7f7e9cc3949a9a3556a6b36513f37f690d)

src/Lean/MetavarContext.lean

@@ -1219,7 +1219,7 @@ private def mkLambda' (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) (etaRed
   Similar to `LocalContext.mkBinding`, but handles metavariables correctly.
   If `usedOnly == true` then `forall` and `lambda` expressions are created only for used variables.
   If `usedLetOnly == true` then `let` expressions are created only for used (let-) variables. -/
-@[specialize] def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) : M Expr := do
+def mkBinding (isLambda : Bool) (lctx : LocalContext) (xs : Array Expr) (e : Expr) (usedOnly : Bool) (usedLetOnly : Bool) (etaReduce : Bool) : M Expr := do
   let e ← abstractRange xs xs.size e
   xs.size.foldRevM (init := e) fun i e => do
       let x := xs[i]!