feat: inline small declarations not tagged with [noinline]

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

@@ -40,10 +40,13 @@ def inlineCandidate? (e : Expr) : SimpM (Option InlineCandidateInfo) := do
   let numArgs := e.getAppNumArgs
   let f := e.getAppFn
   if let .const declName us ← findExpr f then
-    let inlineIfReduce := hasInlineIfReduceAttribute (← getEnv) declName
-    unless mustInline || hasInlineAttribute (← getEnv) declName || inlineIfReduce 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 arity := decl.getArity
     let inlinePartial := (← read).config.inlinePartial
     if !mustInline && !inlinePartial && numArgs < arity then return none

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

@@ -229,10 +229,10 @@ def isOnceOrMustInline (fvarId : FVarId) : SimpM Bool := do
     | _ => return false
 
 /--
-Return `true` if the given local function declaration is considered "small".
+Return `true` if the given code is considered "small".
 -/
-def isSmall (decl : FunDecl) : SimpM Bool :=
-  return decl.value.sizeLe (← getConfig).smallThreshold
+def isSmall (code : Code) : SimpM Bool :=
+  return code.sizeLe (← getConfig).smallThreshold
 
 /--
 Return `true` if the given local function declaration should be inlined.
@@ -241,7 +241,7 @@ def shouldInlineLocal (decl : FunDecl) : SimpM Bool := do
   if (← isOnceOrMustInline decl.fvarId) then
     return true
   else
-    isSmall decl
+    isSmall decl.value
 
 /--
 LCNF "Beta-reduce". The equivalent of `(fun params => code) args`.

tests/lean/linterUnusedVariables.lean.expected.out

@@ -3,8 +3,8 @@ linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unuse
 linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:29:2-29:3: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:34:5-34:6: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables]
 linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x` [linter.unusedVariables]
+linterUnusedVariables.lean:39:2-39:3: warning: unused variable `f` [linter.unusedVariables]
 linterUnusedVariables.lean:42:7-42:8: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:45:8-45:9: warning: unused variable `x` [linter.unusedVariables]
 linterUnusedVariables.lean:49:9-49:10: warning: unused variable `z` [linter.unusedVariables]