From 9a273b85a3ca5f92f0f77585bcbf895abd9ef7f0 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 1 Jun 2022 15:54:00 +0200
Subject: [PATCH] fix: no sorry-warning for missing match cases

---
 src/Lean/Elab/Match.lean                                   | 2 +-
 tests/lean/301.lean.expected.out                           | 1 -
 tests/lean/matchErrorMsg.lean.expected.out                 | 1 -
 tests/lean/matchMissingCasesAsStuckError.lean.expected.out | 1 -
 tests/lean/matchUnknownFVarBug.lean.expected.out           | 1 -
 tests/lean/patvar.lean.expected.out                        | 1 -
 6 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 09627ef40f..a9bb5ad274 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -1112,9 +1112,9 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
     let numDiscrs := discrs.size
     let matcherName ← mkAuxName `match
     let matcherResult ← mkMatcher { matcherName, matchType, discrInfos := discrs.map fun discr => { hName? := discr.h?.map (·.getId) }, lhss := altLHSS }
+    reportMatcherResultErrors altLHSS matcherResult
     matcherResult.addMatcher
     let motive ← forallBoundedTelescope matchType numDiscrs fun xs matchType => mkLambdaFVars xs matchType
-    reportMatcherResultErrors altLHSS matcherResult
     let r := mkApp matcherResult.matcher motive
     let r := mkAppN r (discrs.map (·.expr))
     let r := mkAppN r rhss
diff --git a/tests/lean/301.lean.expected.out b/tests/lean/301.lean.expected.out
index 89ffd24870..fb73864610 100644
--- a/tests/lean/301.lean.expected.out
+++ b/tests/lean/301.lean.expected.out
@@ -1,4 +1,3 @@
-301.lean:1:9-1:17: warning: declaration uses 'sorry'
 301.lean:1:9-1:17: error: missing cases:
 (Nat.succ _)
 301.lean:1:21-1:24: error: type mismatch
diff --git a/tests/lean/matchErrorMsg.lean.expected.out b/tests/lean/matchErrorMsg.lean.expected.out
index 8b7335959a..c648dae646 100644
--- a/tests/lean/matchErrorMsg.lean.expected.out
+++ b/tests/lean/matchErrorMsg.lean.expected.out
@@ -1,3 +1,2 @@
-matchErrorMsg.lean:2:1-4:16: warning: declaration uses 'sorry'
 matchErrorMsg.lean:2:1-2:6: error: missing cases:
 (Prod.mk Nat.zero (Nat.succ _))
diff --git a/tests/lean/matchMissingCasesAsStuckError.lean.expected.out b/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
index 4fd440fedc..08f8c89841 100644
--- a/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
+++ b/tests/lean/matchMissingCasesAsStuckError.lean.expected.out
@@ -1,3 +1,2 @@
-matchMissingCasesAsStuckError.lean:2:2-3:24: warning: declaration uses 'sorry'
 matchMissingCasesAsStuckError.lean:2:2-2:7: error: missing cases:
 none
diff --git a/tests/lean/matchUnknownFVarBug.lean.expected.out b/tests/lean/matchUnknownFVarBug.lean.expected.out
index ebb11bf6e9..cd7e2626a9 100644
--- a/tests/lean/matchUnknownFVarBug.lean.expected.out
+++ b/tests/lean/matchUnknownFVarBug.lean.expected.out
@@ -1,4 +1,3 @@
-matchUnknownFVarBug.lean:2:2-3:19: warning: declaration uses 'sorry'
 matchUnknownFVarBug.lean:2:2-2:7: error: missing cases:
 (some (Nat.succ _)), (some _)
 (some (Nat.succ _)), none
diff --git a/tests/lean/patvar.lean.expected.out b/tests/lean/patvar.lean.expected.out
index 63bedd8635..e3376f8187 100644
--- a/tests/lean/patvar.lean.expected.out
+++ b/tests/lean/patvar.lean.expected.out
@@ -1,4 +1,3 @@
-patvar.lean:3:0-3:22: warning: declaration uses 'sorry'
 patvar.lean:3:0-3:22: error: missing cases:
 (List.cons _ _)
 patvar.lean:10:0-10:16: error: missing cases: