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

@@ -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 =>

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

tests/compiler/reduceArity_overapp.lean.expected.out

@@ -0,0 +1 @@
+a