From eba5a5a6ef478086246b5f9ef72bf949a2aed6d5 Mon Sep 17 00:00:00 2001
From: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Date: Mon, 17 Nov 2025 08:51:37 +0100
Subject: [PATCH] fix: consider over-applications in `reduceArity` compiler
 pass (#11185)

This PR fixes the `reduceArity` compiler pass to consider
over-applications to functions that have their arity reduced.
Previously, this pass assumed that the amount of arguments to
applications was always the same as the number of parameters in the
signature. This is usually true, since the compiler eagerly introduces
parameters as long as the return type is a function type, resulting in a
function with a return type that isn't a function type. However, for
dependent types that sometimes are function types and sometimes not,
this assumption is broken, resulting in the additional parameters to be
dropped.

Closes #11131
---
 src/Lean/Compiler/LCNF/ReduceArity.lean       |  8 ++++---
 tests/compiler/reduceArity_overapp.lean       | 21 +++++++++++++++++++
 .../reduceArity_overapp.lean.expected.out     |  1 +
 3 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 tests/compiler/reduceArity_overapp.lean
 create mode 100644 tests/compiler/reduceArity_overapp.lean.expected.out

diff --git a/src/Lean/Compiler/LCNF/ReduceArity.lean b/src/Lean/Compiler/LCNF/ReduceArity.lean
index c3bd67db01..f5c4bc03fa 100644
--- a/src/Lean/Compiler/LCNF/ReduceArity.lean
+++ b/src/Lean/Compiler/LCNF/ReduceArity.lean
@@ -128,10 +128,12 @@ partial def reduce (code : Code) : ReduceM Code := do
   | .let decl k =>
     let .const declName _ args := decl.value | do return code.updateLet! decl (← reduce k)
     unless declName == (← read).declName do return code.updateLet! decl (← reduce k)
+    let mask := (← read).paramMask
     let mut argsNew := #[]
-    for used in (← read).paramMask, arg in args do
-      if used then
-        argsNew := argsNew.push arg
+    for h : i in *...args.size do
+      -- keep over-application
+      if mask.getD i true then
+        argsNew := argsNew.push args[i]
     let decl ← decl.updateValue (.const (← read).auxDeclName [] argsNew)
     return code.updateLet! decl (← reduce k)
   | .fun decl k | .jp decl k =>
diff --git a/tests/compiler/reduceArity_overapp.lean b/tests/compiler/reduceArity_overapp.lean
new file mode 100644
index 0000000000..2ece50f0a5
--- /dev/null
+++ b/tests/compiler/reduceArity_overapp.lean
@@ -0,0 +1,21 @@
+def tuple (types : List Type) : Type :=
+  match types with
+  | [] => Unit
+  | [t] => t
+  | t :: types => t × tuple types
+
+def uncurried ins out := tuple ins -> out
+
+def curried (ins : List Type) out := match ins with
+  | [] => out
+  | (x :: xs) => x -> curried xs out
+
+def curry (f : uncurried ins out) : curried ins out :=
+  match ins with
+  | [] => f ()
+  | [_] => f
+  | (_ :: _ :: _) => λx => curry (λxs => f (x, xs))
+
+def main : IO Unit := do
+  let val : String := curry (ins := [Int, String]) Prod.snd 1 "a"
+  IO.println val
diff --git a/tests/compiler/reduceArity_overapp.lean.expected.out b/tests/compiler/reduceArity_overapp.lean.expected.out
new file mode 100644
index 0000000000..533790e525
--- /dev/null
+++ b/tests/compiler/reduceArity_overapp.lean.expected.out
@@ -0,0 +1 @@
+a