From 7ee7ca30b89bf0d0bf2c03cc36a69f87dc60255a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Mar 2022 05:16:19 -0700
Subject: [PATCH] fix: index out of bounds

---
 src/Lean/Meta/Match/MatchEqs.lean | 3 +++
 src/Lean/Meta/Tactic/Split.lean   | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 9937a06bf7..a3d226a453 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -58,6 +58,9 @@ structure MatchEqns where
   splitterAltNumParams : Array Nat
   deriving Inhabited, Repr
 
+def MatchEqns.size (e : MatchEqns) : Nat :=
+  e.eqnNames.size
+
 structure MatchEqnsExtState where
   map : Std.PHashMap Name MatchEqns := {}
   deriving Inhabited
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index 717a3035c6..47ffe0a66a 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -97,6 +97,8 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
     let splitter := mkAppN (mkApp splitter motive) discrsNew
     check splitter
     let mvarIds ← apply mvarId splitter
+    unless mvarIds.length == matchEqns.size do
+      throwError "'applyMatchSplitter' failed, unexpected number of goals created after applying splitter for '{matcherDeclName}'."
     let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do
       let numParams := matchEqns.splitterAltNumParams[i]
       let (_, mvarId) ← introN mvarId numParams