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

script/apply.lean

@@ -132,12 +132,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);
 }
@@ -186,7 +195,7 @@ Author: Leonardo de Moura
 def mkApplyCpp (max : Nat) : M Unit := do
   mkCopyright
   emit "// DO NOT EDIT, this is an automatically generated file
-// Generated using script: ../../gen/apply.lean
+// Generated using script: script/apply.lean
 #include \"runtime/apply.h\"
 namespace lean {
 #define obj lean_object

src/runtime/apply.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 // DO NOT EDIT, this is an automatically generated file
-// Generated using script: ../../gen/apply.lean
+// Generated using script: script/apply.lean
 #include "runtime/apply.h"
 namespace lean {
 #define obj lean_object
@@ -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);
 }

tests/compile/apply_m_overapp.lean

@@ -0,0 +1,22 @@
+/-!
+This is a regression test reproducer for #14969.
+
+Applying more than `closureMaxArgs` arguments at once to a closure of smaller arity used the
+array calling convention, which is only correct above that arity, and crashed. `Chain` keeps
+every closure at arity 1, and `f` is opaque in `apply20` so that all 20 arguments are applied
+in a single `lean_apply_m` call.
+-/
+
+abbrev Chain : Nat → Type
+  | 0     => Nat
+  | n + 1 => Nat → Chain n
+
+def mk : (n : Nat) → Chain n
+  | 0     => 42
+  | n + 1 => fun _ => mk n
+
+@[noinline] def apply20 (f : Chain 20) : Nat :=
+  f 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
+
+def main : IO Unit :=
+  IO.println (apply20 (mk 20))

tests/compile/apply_m_overapp.lean.out.expected

@@ -0,0 +1 @@
+42