max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: tighten IR typing rules for applications of closures (#9154)

Browse source 
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`.
This commit is contained in:
Cameron Zwarich 2025-07-02 07:06:24 -07:00 • committed by GitHub
parent 977ae92e43
commit 8954354216
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Compiler/IR/Checker.lean
View file

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

7
src/Lean/Compiler/IR/ToIR.lean
View file

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