(libc++abi) lean::exception: incomplete case

Stream: lean4

[Sébastien Michelland]

The following snippet triggers a C++ exception which looks like a bug on Lean's side. The core of the problem seems to be splitting EQ with a tactic (in makePair?) then trying to use the resulting value in a computation (in usePair).

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
-- libc++abi: terminating with uncaught exception of type lean::exception: incomplete case

The bug was found by @Siddharth Bhat on leanprover/lean4:nightly-2022-05-17. I tested this minimized version on today's nightly leanprover/lean4:nightly-2022-06-29. Cc @Leonardo de Moura I suppose.

[Leonardo de Moura]

@Sébastien Michelland Thanks for creating the mwe. I pushed a fix for this issue:
https://github.com/leanprover/lean4/commit/a888b21bce4000322f1de4b975edf43840240896