From 8b28467655f636faa798528ea30a3d464cca489f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 30 Oct 2025 17:02:45 +0100
Subject: [PATCH] perf: better detection of repeated branching on same value
 (#11020)

This PR improves the detection of situations where we branch multiple
times on the same value in the
code generator. Previously this would only consider repeated branching
on function arguments, now on
arbitrary values.


Closes: #11018
---
 src/Lean/Compiler/LCNF/Simp/DiscrM.lean |  3 +--
 tests/lean/run/double_match.lean        | 22 ++++++++++++++++++++++
 2 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/double_match.lean

diff --git a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean
index 500a9fd10b..7e4f1bcb39 100644
--- a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean
+++ b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean
@@ -61,8 +61,7 @@ def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do
   | some { value := .const declName _ args, .. } =>
     let some (.ctorInfo val) := (← getEnv).find? declName | return none
     return some <| .ctor val args
-  | some _ => return none
-  | none => return (← read).discrCtorMap.get? fvarId
+  | _ => return (← read).discrCtorMap.get? fvarId
 
 def findCtorName? (fvarId : FVarId) : DiscrM (Option Name) := do
   let some ctorInfo ← findCtor? fvarId | return none
diff --git a/tests/lean/run/double_match.lean b/tests/lean/run/double_match.lean
new file mode 100644
index 0000000000..b944c7cdb8
--- /dev/null
+++ b/tests/lean/run/double_match.lean
@@ -0,0 +1,22 @@
+/--
+trace: [Compiler.saveMono] size: 6
+    def foo f x : Option Nat :=
+      let _x.1 := f x;
+      cases _x.1 : Option Nat
+      | Option.none =>
+        return _x.1
+      | Option.some val.2 =>
+        let _x.3 := Nat.add val.2 val.2;
+        let _x.4 := some ◾ _x.3;
+        return _x.4
+-/
+#guard_msgs in
+set_option trace.Compiler.saveMono true in
+def foo (f : Nat → Option Nat) (x : Nat) : Option Nat :=
+  if let some val := f x then
+    if let some val2 := f x then
+      some <| val + val2
+    else
+      none
+  else
+    none