From 895435421634a915c6e09135eaecb26ac41869ee Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Wed, 2 Jul 2025 07:06:24 -0700
Subject: [PATCH] fix: tighten IR typing rules for applications of closures
 (#9154)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR tightens the IR typing rules around applications of closures.
When re-reading some code, I realized that the code in `mkPartialApp`
has a clear typo—`.object` and `type` should be swapped. However, it
doesn't matter, because later IR passes smooth out the mismatch here. It
makes more sense to be strict up-front and require applications of
closures to always return an `.object`.
---
 src/Lean/Compiler/IR/Checker.lean | 6 ++++--
 src/Lean/Compiler/IR/ToIR.lean    | 7 ++-----
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index 269dee3355..3446a54ca9 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -114,8 +114,10 @@ def checkPartialApp (c : FunId) (ys : Array Arg) : M Unit := do
   checkArgs ys
 
 def checkExpr (ty : IRType) : Expr → M Unit
-  | Expr.pap f ys           => checkPartialApp f ys *> checkObjType ty -- partial applications should always produce a closure object
-  | Expr.ap x ys            => checkObjVar x *> checkArgs ys
+  -- Partial applications should always produce a closure object.
+  | Expr.pap f ys           => checkPartialApp f ys *> checkObjType ty
+  -- Applications of closures should always produce a boxed value.
+  | Expr.ap x ys            => checkObjVar x *> checkArgs ys *> checkObjType ty
   | Expr.fap f ys           => checkFullApp f ys
   | Expr.ctor c ys          => do
     if c.cidx > maxCtorTag && (c.size > 0 || c.usize > 0 || c.ssize > 0) then
diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 13a049be88..c7be9aa731 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -138,7 +138,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
   let rec mkExpr (e : Expr) : M FnBody := do
     let var ← bindVar decl.fvarId
     let type ← match e with
-    | .ctor .. | .pap .. | .proj .. => pure <| .object
+    | .ctor .. | .pap .. | .ap .. | .proj .. => pure <| .object
     | _ => toIRType decl.type
     return .vdecl var type e (← lowerCode k)
   let rec mkErased (_ : Unit) : M FnBody := do
@@ -147,10 +147,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
   let rec mkPartialApp (e : Expr) (restArgs : Array Arg) : M FnBody := do
     let var ← bindVar decl.fvarId
     let tmpVar ← newVar
-    let type ← match e with
-    | .ctor .. | .pap .. | .proj .. => pure <| .object
-    | _ => toIRType decl.type
-    return .vdecl tmpVar .object e (.vdecl var type (.ap tmpVar restArgs) (← lowerCode k))
+    return .vdecl tmpVar .object e (.vdecl var .object (.ap tmpVar restArgs) (← lowerCode k))
   let rec tryIrDecl? (name : Name) (args : Array Arg) : M (Option FnBody) := do
     if let some decl ← LCNF.getMonoDecl? name then
       let numArgs := args.size