From ed4d453346c223546289d4b2d3bd8d2b4d1cf551 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 15 Oct 2025 12:10:52 +0200
Subject: [PATCH] refactor: processLeaf: Only look at first alt (#10774)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR lets match compilation look only at the first remaining
alternative in `processLeaf`. At this point we have no further variables
we can split on, so if the first one isn’t applicable, match compilation
should fail.
---
 src/Lean/Meta/Match/Match.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 818cfb078b..83acec06a2 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -328,9 +328,9 @@ where
         trace[Meta.Match.match] "missing alternative"
         p.mvarId.admit
         modify fun s => { s with counterExamples := p.examples :: s.counterExamples }
-    | alt :: alts =>
+    | alt :: _ =>
       unless (← solveCnstrs p.mvarId alt) do
-        go alts
+        throwErrorAt alt.ref "Dependent match elimination failed: Could not solve constraints"
 
 private def processAsPattern (p : Problem) : MetaM Problem := withGoalOf p do
   let x :: _ := p.vars | unreachable!