fix: match_expr parser

closes #3989
closes #3990

src/Lean/Parser/Term.lean

@@ -870,7 +870,7 @@ def matchExprElseAlt (rhsParser : Parser) := leading_parser "| " >> ppIndent (ho
 def matchExprAlts (rhsParser : Parser) :=
   leading_parser withPosition $
     many (ppLine >> checkColGe "irrelevant" >> notFollowedBy (symbol "| " >> " _ ") "irrelevant" >> matchExprAlt rhsParser)
-    >> (ppLine >> checkColGe "irrelevant" >> matchExprElseAlt rhsParser)
+    >> (ppLine >> checkColGe "else-alternative for `match_expr`, i.e., `| _ => ...`" >> matchExprElseAlt rhsParser)
 @[builtin_term_parser] def matchExpr := leading_parser:leadPrec
   "match_expr " >> termParser >> " with" >> ppDedent (matchExprAlts termParser)
 

tests/lean/3989_1.lean

@@ -0,0 +1,3 @@
+def foo (ty : Expr) : MetaM Expr :=
+  match_expr ty with
+  | Nat => sorry

tests/lean/3989_1.lean.expected.out

@@ -0,0 +1 @@
+3989_1.lean:4:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`

tests/lean/3989_2.lean

@@ -0,0 +1,6 @@
+def foo (ty : Expr) : MetaM Expr :=
+  match_expr ty with
+  | Nat => sorry
+  | BitVec n => sorry
+
+#check Nat

tests/lean/3989_2.lean.expected.out

@@ -0,0 +1,2 @@
+3989_2.lean:6:0: error: expected else-alternative for `match_expr`, i.e., `| _ => ...`
+Nat : Type