From 584d92d302b72ce8f310aaf95042d6566289ab49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Mar 2026 13:49:46 -0800 Subject: [PATCH] refactor: replace `isImplicitReducible` with `Meta.isInstance` in `shouldInline` (#12759) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR replaces the `isImplicitReducible` check with `Meta.isInstance` in the `shouldInline` function within `inlineCandidate?`. At the base phase, we skip inlining instances tagged with `[inline]`/`[always_inline]`/`[inline_if_reduce]` because their local functions will be lambda lifted during the base phase. The goal is to keep instance code compact so the lambda lifter can extract cheap-to-inline declarations. Inlining instances prematurely expands the code and creates extra work for the lambda lifter — producing many additional lambda-lifted closures. The previous check used `isImplicitReducible`, which does not capture the original intent: some `instanceReducible` declarations are not instances. `Meta.isInstance` correctly targets only actual type class instances. Although `Meta.isInstance` depends on the scoped extension state, this is safe because `shouldInline` runs during LCNF compilation at `addDecl` time — any instance referenced in the code was resolved during elaboration when the scope was active, and LCNF compilation occurs before the scope changes. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 --- .../Compiler/LCNF/Simp/InlineCandidate.lean | 19 ++++++++++++++++--- stage0/src/stdlib_flags.h | 1 + 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean index 2019892a59..8bddc01f34 100644 --- a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean +++ b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean @@ -62,11 +62,24 @@ def inlineCandidate? (e : LetValue .pure) : SimpM (Option InlineCandidateInfo) : if !decl.inlineIfReduceAttr && decl.recursive then return false if mustInline then return true /- - We don't inline instances tagged with `[inline]/[always_inline]/[inline_if_reduce]` at the base phase - We assume that at the base phase these annotations are for the instance methods that have been lambda lifted. + We don't inline instances tagged with `[inline]/[always_inline]/[inline_if_reduce]` at the base phase. + We assume that at the base phase these annotations are for the instance methods that will be lambda lifted during the base phase. + Reason: we eagerly lambda lift local functions occurring at instances before saving their code at + the end of the base phase. The goal is to make them cheap to inline in actual code. + By inlining their definitions we would be just generating extra work for the lambda lifter. -/ if (← inBasePhase) then - if (← isImplicitReducible decl.name) then + /- + We claim it is correct to use `Meta.isInstance` because + 1. `shouldInline` is called during LCNF compilation, which runs at `addDecl` time + 2. Any instance referenced in the code was found by type class resolution during elaboration + 3. For TC resolution to find it, the scope was active during elaboration + 4. LCNF compilation happens before the scope changes + + We don't want to use `isImplicitReducible` because some `instanceReducible` declarations are + **not** instances. + -/ + if (← Meta.isInstance decl.name) then unless decl.name == ``instDecidableEqBool do /- TODO: remove this hack after we refactor `Decidable` as suggested by Gabriel. diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..1f4095b797 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,3 +1,4 @@ +// update me #include "util/options.h" namespace lean {