From f20fc6328c38baa71acf90140929df2e3af38a32 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Mar 2021 16:26:26 -0700 Subject: [PATCH] fix: better error message when `cases` fails and there are no alternatives --- src/Lean/Meta/Match/Match.lean | 10 +++++++++- tests/lean/matchMissingCasesAsStuckError.lean | 3 +++ .../matchMissingCasesAsStuckError.lean.expected.out | 2 ++ 3 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 tests/lean/matchMissingCasesAsStuckError.lean create mode 100644 tests/lean/matchMissingCasesAsStuckError.lean.expected.out diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index db30fafea0..5024b76436 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -319,7 +319,15 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do | [] => unreachable! | x :: xs => do let subgoals? ← commitWhenSome? do - let subgoals ← cases p.mvarId x.fvarId! + let subgoals ← + try + cases p.mvarId x.fvarId! + catch ex => + if p.alts.isEmpty then + /- If we have no alternatives and dependent pattern matching fails, then a "missing cases" error is bettern than a "stuck" error message. -/ + return none + else + throw ex if subgoals.isEmpty then /- Easy case: we have solved problem `p` since there are no subgoals -/ pure (some #[]) diff --git a/tests/lean/matchMissingCasesAsStuckError.lean b/tests/lean/matchMissingCasesAsStuckError.lean new file mode 100644 index 0000000000..9b1a4bccfd --- /dev/null +++ b/tests/lean/matchMissingCasesAsStuckError.lean @@ -0,0 +1,3 @@ +example (a : α) (f : α → Option α) : Bool := by + match h:f a with + | some _ => exact true diff --git a/tests/lean/matchMissingCasesAsStuckError.lean.expected.out b/tests/lean/matchMissingCasesAsStuckError.lean.expected.out new file mode 100644 index 0000000000..e8e5d28026 --- /dev/null +++ b/tests/lean/matchMissingCasesAsStuckError.lean.expected.out @@ -0,0 +1,2 @@ +matchMissingCasesAsStuckError.lean:2:2-2:7: error: missing cases: +none, _