feat: do not inline definitions occurring in instances at the base phase

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -48,6 +48,9 @@ abbrev CompilerM := ReaderT CompilerM.Context $ StateRefT CompilerM.State CoreM
 def getPhase : CompilerM Phase :=
   return (← read).phase
 
+def inBasePhase : CompilerM Bool :=
+  return (← getPhase) matches .base
+
 instance : AddMessageContext CompilerM where
   addMessageContext msgData := do
     let env ← getEnv

src/Lean/Compiler/LCNF/Simp.lean

@@ -46,7 +46,16 @@ partial def Decl.simp (decl : Decl) (config : Config) : CompilerM Decl := do
     Remark: by eta-expanding partial applications in instances, we also make the simplifier
     work harder when inlining instance projections.
     -/
-    config := { config with etaPoly := false, inlinePartial := false }
+    let mut inlineDefs := config.inlineDefs
+    if (← inBasePhase <&&> Meta.isInstance decl.name) then
+      /-
+      At the base phase, we don't inline definitions occurring in instances even if they are tagged with `alwaysInline`.
+      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 definitions we would be just generating extra
+      work for the lambda lifter.
+      -/
+      inlineDefs := false
+    config := { config with etaPoly := false, inlinePartial := false, inlineDefs }
   go decl config
 where
   go (decl : Decl) (config : Config) : CompilerM Decl := do

src/Lean/Compiler/LCNF/Simp/Config.lean

@@ -30,5 +30,10 @@ structure Config where
   phase 1.
   -/
   implementedBy := false
+  /--
+  If `inlineDefs` is `true` then top-level definitions are inlined when they are small are
+  annotated with inlining attributes.
+  -/
+  inlineDefs := true
   deriving Inhabited
 

src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean

@@ -40,13 +40,23 @@ def inlineCandidate? (e : Expr) : SimpM (Option InlineCandidateInfo) := do
   let numArgs := e.getAppNumArgs
   let f := e.getAppFn
   if let .const declName us ← findExpr f then
+    unless (← read).config.inlineDefs do
+      return none
     let some decl ← getDecl? declName | return none
     let inlineIfReduce := hasInlineIfReduceAttribute (← getEnv) declName
-    if !inlineIfReduce && decl.recursive then return none
-    let small ← isSmall decl.value
-    let env ← getEnv
-    unless mustInline || hasInlineAttribute env declName || inlineIfReduce || (small && !hasNoInlineAttribute env declName) do
-      return none
+    let shouldInline : SimpM Bool := do
+      if !inlineIfReduce && decl.recursive then return false
+      if mustInline then return true
+      -- We don't inline instances tagged with `[inline]/[alwaysInline]/[inlineIfReduce]` at the base phase
+      -- We assume that at the base phase these annotations are for the instance methods that have been lambda lifted.
+      if (← inBasePhase <&&> Meta.isInstance decl.name) then return false
+      let env ← getEnv
+      if hasInlineAttribute env declName || inlineIfReduce then return true
+      unless hasNoInlineAttribute env declName do
+        if (← isSmall decl.value) then return true
+      return false
+    unless (← shouldInline) do return none
+    /- check arity -/
     let arity := decl.getArity
     let inlinePartial := (← read).config.inlinePartial
     if !mustInline && !inlinePartial && numArgs < arity then return none