fix: better error message when cases fails and there are no alternatives

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 #[])

tests/lean/matchMissingCasesAsStuckError.lean

@@ -0,0 +1,3 @@
+example (a : α) (f : α → Option α) : Bool := by
+  match h:f a with
+  | some _ => exact true

tests/lean/matchMissingCasesAsStuckError.lean.expected.out

@@ -0,0 +1,2 @@
+matchMissingCasesAsStuckError.lean:2:2-2:7: error: missing cases:
+none, _