From 586ea55c0daa62a2fb0f700034569d186f9d077d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 27 Nov 2025 12:41:43 +0100
Subject: [PATCH] fix: enforce choice invariant in ElimDeadBranches (#11398)

This PR fixes a broken invariant in the choice nodes of
ElimDeadBranches.

Closes: #11389 and #11393
---
 src/Lean/Compiler/LCNF/ElimDeadBranches.lean |  6 +++---
 tests/lean/run/11389.lean                    | 21 ++++++++++++++++++++
 2 files changed, 24 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/11389.lean

diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
index 2fdcb6f180..a05f2b229a 100644
--- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
@@ -84,12 +84,12 @@ choice node further down the tree.
 partial def addChoice (env : Environment) (vs : List Value) (v : Value) : List Value :=
   match vs, v with
   | [], v => [v]
-  | v1@(ctor i1 _ ) :: cs, ctor i2 _ =>
+  | v1@(ctor i1 vs1) :: cs, ctor i2 vs2 =>
     if i1 == i2 then
-      (merge env v1 v) :: cs
+      ctor i1 (Array.zipWith (merge env) vs1 vs2) :: cs
     else
       v1 :: addChoice env cs v
-  | _, _ => panic! "invalid addChoice"
+  | _, _ => panic! s!"invalid addChoice {repr v} into {repr vs}"
 
 /--
 Merge two values into one. `bot` is the neutral element, `top` the annihilator.
diff --git a/tests/lean/run/11389.lean b/tests/lean/run/11389.lean
new file mode 100644
index 0000000000..9c41ba4fef
--- /dev/null
+++ b/tests/lean/run/11389.lean
@@ -0,0 +1,21 @@
+/-!
+Regression tests for #11393 and #11389
+-/
+
+#guard_msgs in
+open System in
+def loadModuleContent : IO Unit := do
+  let lakefile : FilePath := "lakefile.lean"
+
+  if !(← lakefile.pathExists) then
+    IO.println "nope"
+
+  discard <| IO.Process.output {
+    cmd := "ls", args := #[]
+  }
+
+#guard_msgs in
+def test (s : String) : IO Bool := do
+  if s.startsWith "x" then return true
+  let b ← IO.Process.output {cmd := "true", args := #[]}
+  return b.exitCode == 0