From a888b21bce4000322f1de4b975edf43840240896 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jun 2022 06:56:17 -0700
Subject: [PATCH] fix: compiler bug at `And.casesOn`

Fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28libc.2B.2Babi.29.20lean.3A.3Aexception.3A.20incomplete.20case/near/287839995
---
 src/library/compiler/lcnf.cpp     |  4 +++-
 tests/lean/run/andCasesOnBug.lean | 28 ++++++++++++++++++++++++++++
 2 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/andCasesOnBug.lean

diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp
index 0459e38cde..af2af42452 100644
--- a/src/library/compiler/lcnf.cpp
+++ b/src/library/compiler/lcnf.cpp
@@ -362,7 +362,9 @@ public:
                 minor = args[3];
             else
                 minor = args[4];
-            return visit(mk_app(minor, pr_a, pr_b), root);
+            expr new_e = mk_app(minor, pr_a, pr_b);
+            new_e      = mk_app(new_e, args.size() - 5, args.data() + 5);
+            return visit(new_e, root);
         }
     }
 
diff --git a/tests/lean/run/andCasesOnBug.lean b/tests/lean/run/andCasesOnBug.lean
new file mode 100644
index 0000000000..cd7f6ab7fc
--- /dev/null
+++ b/tests/lean/run/andCasesOnBug.lean
@@ -0,0 +1,28 @@
+inductive FinInt: Nat → Type :=
+  | nil: FinInt 0
+  | next: Bool → FinInt n → FinInt (n+1)
+deriving DecidableEq
+
+def zero (sz: Nat): FinInt sz :=
+  match sz with
+  | 0 => .nil
+  | sz+1 => .next false (zero sz)
+
+inductive Pair :=
+  | mk (sz: Nat) (lhs rhs: FinInt sz)
+
+def makePair?: (n m: (sz: Nat) × FinInt sz) → Option Pair
+  | ⟨sz, lhs⟩, ⟨sz', rhs⟩ =>
+      if EQ: true /\ sz = sz' then
+            have rhs' : FinInt sz := by {
+                cases EQ;
+                case intro left right =>
+                simp [right];
+                exact rhs;
+            };
+            some (Pair.mk sz lhs rhs')
+      else none
+
+def usePair: Pair → Bool := fun ⟨sz, lhs, rhs⟩ => lhs = rhs
+
+#eval (makePair? ⟨8, zero 8⟩ ⟨8, zero 8⟩).map usePair