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

refactor: replace isImplicitReducible with Meta.isInstance in shouldInline (#12759)

Browse source 
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 <noreply@anthropic.com>
This commit is contained in:
Leonardo de Moura 2026-03-02 13:49:46 -08:00 • committed by GitHub
parent d66aaebca6
commit 584d92d302
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 17 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean
View file

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

1
stage0/src/stdlib_flags.h
View file

@ -1,3 +1,4 @@
// update me
#include "util/options.h"
namespace lean {