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

@@ -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);
         }
     }
 

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