perf: optimizations for the simp compiler pass

src/Lean/Compiler/LCNF/Passes.lean

@@ -94,7 +94,7 @@ def builtinPassManager : PassManager := {
     Pass.checkMeta,
     pullInstances,
     cse (shouldElimFunDecls := false),
-    simp,
+    simp { simpCtor := false },
     floatLetIn,
     findJoinPoints,
     pullFunDecls,

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

@@ -41,5 +41,10 @@ structure Config where
   annotated with inlining attributes.
   -/
   inlineDefs := true
+  /--
+  If `simpCtor` is `true`, then scalar constructor applications with a matching discriminant are
+  replaced with a reference to the discriminant. Otherwise, only non-scalar constructor
+  applications are affected (see `simpCtorDiscr?`).
+  -/
+  simpCtor := true
   deriving Inhabited
-

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

@@ -59,7 +59,11 @@ def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do
   | some { value := .lit (.nat n), .. } =>
     return some <| .natVal n
   | some { value := .const declName _ args, .. } =>
-    let some (.ctorInfo val) := (← getEnv).find? declName | return none
+    let some (.ctorInfo val) := (← getEnv).find? declName |
+      -- always consider scalar constructors like `true` / `false`
+      -- we don't consider non-scalar constructors here because touching them can break reuse
+      let some c@(.ctor _ #[]) := (← read).discrCtorMap.get? fvarId | return none
+      return some c
     return some <| .ctor val args
   | _ => return (← read).discrCtorMap.get? fvarId
 

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

@@ -47,7 +47,16 @@ def simpAppApp? (e : LetValue .pure) : OptionT SimpM (LetValue .pure) := do
   | .proj .. | .lit .. => failure
 
 def simpCtorDiscr? (e : LetValue .pure) : OptionT SimpM (LetValue .pure) := do
-  let .const declName _ _ := e | failure
+  let .const declName _ args := e | failure
+  /-
+  Don't replace scalar constructors like `true` / `false` in the first pass to avoid the following
+  kind of situation (which occurred e.g. in the `charactersIn` benchmark):
+  1. `instDecidableEqBool x true` gets converted to `instDecidableEqBool x y` by this function
+  2. `pullFunDecls` moves `instDecidableEqBool x y` into a place where `y` is no longer known
+     to be `true`
+  3. `instDecidableEqBool` is inlined as usual, producing an unnecessary branch on `y`
+  -/
+  if !(← read).config.simpCtor && args.isEmpty then failure
   let some (.ctorInfo _) := (← getEnv).find? declName | failure
   let some fvarId ← simpCtorDiscrCore? e.toExpr | failure
   return .fvar fvarId #[]