From 1587d02dfbe0b4759b7f63657bbc8ac8eb352992 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 29 Oct 2025 14:58:23 +0100 Subject: [PATCH] fix: more stable eager lambda lifting heuristic (#11010) This PR makes the eager lambda lifting heuristic more predictable by blocking it from lifting from any kind of inlineable function, not just `@[inline]`. It also adapts the doc-string to describe what is actually going on. --- src/Lean/Compiler/LCNF/LambdaLifting.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Lean/Compiler/LCNF/LambdaLifting.lean b/src/Lean/Compiler/LCNF/LambdaLifting.lean index 085834962b..fe1648391c 100644 --- a/src/Lean/Compiler/LCNF/LambdaLifting.lean +++ b/src/Lean/Compiler/LCNF/LambdaLifting.lean @@ -169,16 +169,17 @@ def lambdaLifting : Pass where decls.foldlM (init := #[]) fun decls decl => return decls ++ (← decl.lambdaLifting false (suffix := `_lam)) /-- -During eager lambda lifting, we lift -- All local function declarations from instances (motivation: make sure it is cheap to inline them later) -- Local function declarations that take local instances as parameters (motivation: ensure they are specialized) +During eager lambda lifting, we inspect declarations that are not inlineable or instances (doing it +everywhere can accidentally introduce mutual recursion which the compiler cannot handle well at the +moment). We then lift local function declarations that take local instances as parameters from +their body to ensure they are specialized. -/ def eagerLambdaLifting : Pass where phase := .base name := `eagerLambdaLifting run := fun decls => do decls.foldlM (init := #[]) fun decls decl => do - if decl.inlineAttr || (← Meta.isInstance decl.name) then + if decl.inlineable || (← Meta.isInstance decl.name) then return decls.push decl else return decls ++ (← decl.lambdaLifting (liftInstParamOnly := true) (suffix := `_elam))