fix: use the correct calling convention when over-applying a closure in lean_apply_m

This PR fixes a crash when more than 16 arguments are applied at once to a closure whose arity is at most 16. Deeply nested monad stacks can produce such applications, and the result was memory corruption rather than a clean call.

`lean_apply_m` handles applications of more than 16 arguments. Its over-application branch invoked the closure through `FNN`, which passes arguments as an array. That convention is only correct for closures whose arity exceeds `LEAN_CLOSURE_MAX_ARGS`; below that the generated code takes its arguments separately, so the callee received the argument array in its first parameter and register garbage in the rest. The fixed-arity `lean_apply_N` functions already guard this, `lean_apply_15` even asserting `arity > 16` immediately before its `FNN` call. The over-application branch now applies the first `arity - fixed` arguments via `lean_apply_n`, which dispatches on the count and consumes the closure, and continues with the remainder.

Author: Kha

src/runtime/apply.cpp

@@ -890,12 +890,21 @@ if (arity == fixed + n) {
   lean_dec_ref(f);
   return r;
 } else if (arity < fixed + n) {
-  obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
-  for (unsigned i = 0; i < fixed; i++) { lean_inc(fx(i)); args[i] = fx(i); }
-  for (unsigned i = 0; i < arity-fixed; i++) args[fixed+i] = as[i];
-  obj * new_f = FNN(f)(args);
-  lean_dec_ref(f);
-  return lean_apply_n(new_f, n+fixed-arity, &as[arity-fixed]);
+  unsigned m = arity - fixed;
+  obj * new_f;
+  if (arity > LEAN_CLOSURE_MAX_ARGS) {
+    // `f`'s code takes its arguments as an array
+    obj ** args = static_cast<obj**>(LEAN_ALLOCA(arity*sizeof(obj*))); // NOLINT
+    for (unsigned i = 0; i < fixed; i++) { lean_inc(fx(i)); args[i] = fx(i); }
+    for (unsigned i = 0; i < m; i++) args[fixed+i] = as[i];
+    new_f = FNN(f)(args);
+    lean_dec_ref(f);
+  } else {
+    // `f`'s code takes `arity` separate arguments, so it must not be invoked through `FNN`;
+    // `lean_apply_n` dispatches on `m` and consumes `f`.
+    new_f = lean_apply_n(f, m, as);
+  }
+  return lean_apply_n(new_f, n - m, &as[m]);
 } else {
   return fix_args(f, n, as);
 }