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