fix: enforce choice invariant in ElimDeadBranches (#11398)

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

Closes: #11389 and #11393

Author: hargoniX

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.

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