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