feat: add throwUnexpectedSyntax

@kha From now on, let's use `throwUnexpectedSyntax` instead of `unreachable!` at
`match_syntax`. The `unreachable!` makes sense when the syntax was
created by our parser, but ill-formed syntax may be created by macros,
and we have no control on how users will create the resulting syntax object.

src/Init/Lean/Elab/BuiltinNotation.lean

@@ -13,24 +13,24 @@ namespace Term
 @[builtinTermElab dollar] def elabDollar : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `($f $ $a) => `($f $a)
-| _          => unreachable!
+| _          => throwUnexpectedSyntax stx "application"
 
 @[builtinTermElab dollarProj] def elabDollarProj : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `($term $.$field) => `($(term).$field)
-| _                 => unreachable!
+| _                 => throwUnexpectedSyntax stx "$."
 
 @[builtinTermElab «if»] def elabIf : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `(if $h : $cond then $t else $e) => let h := mkTermIdFromIdent h; `(dite $cond (fun $h => $t) (fun $h => $e))
 | `(if $cond then $t else $e)      => `(ite $cond $t $e)
-| _                                => unreachable!
+| _                                => throwUnexpectedSyntax stx "if-then-else"
 
 @[builtinTermElab subtype] def elabSubtype : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `({ $x : $type // $p }) => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : $type) => $p))
 | `({ $x // $p })         => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : _) => $p))
-| _                       => unreachable!
+| _                       => throwUnexpectedSyntax stx "subtype"
 
 @[builtinTermElab anonymousCtor] def elabAnoymousCtor : TermElab :=
 fun stx expectedType? => do
@@ -58,7 +58,7 @@ match expectedType? with
 @[builtinTermElab «show»] def elabShow : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `(show $type from $val) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $thisId) $val)
-| _                       => unreachable!
+| _                       => throwUnexpectedSyntax stx "show-from"
 
 def elabInfix (f : Syntax) : TermElab :=
 fun stx expectedType? => do

src/Init/Lean/Elab/Term.lean

@@ -116,15 +116,19 @@ match ref.getPos with
   | some macro => pure macro
   | none       => pure ref
 
+private def prettyPrint (stx : Syntax) : TermElabM Format :=
+match stx.reprint with -- TODO use syntax pretty printer
+| some str => pure $ format str
+| none     => pure $ format stx
+
 private def addMacroStack (msgData : MessageData) : TermElabM MessageData := do
 ctx ← read;
 if ctx.macroStack.isEmpty then pure msgData
 else
-  pure $ ctx.macroStack.foldl
-    (fun (msgData : MessageData) (macro : Syntax) =>
-      match macro.reprint with -- TODO use pretty printer
-      | some str => msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ str)
-      | none     => msgData ++ Format.line ++ "while expanding macro")
+  ctx.macroStack.foldlM
+    (fun (msgData : MessageData) (macro : Syntax) => do
+      macroFmt ← prettyPrint macro;
+      pure (msgData ++ Format.line ++ "while expanding" ++ MessageData.nest 2 (Format.line ++ macroFmt)))
     msgData
 
 /--
@@ -136,6 +140,12 @@ msgData ← addMacroStack msgData;
 msg ← mkMessage msgData MessageSeverity.error ref;
 throw (Exception.error msg)
 
+def throwUnexpectedSyntax {α} (ref : Syntax) (expectedMsg : Option String := none) : TermElabM α := do
+refFmt ← prettyPrint ref;
+match expectedMsg with
+| none    => throwError ref ("unexpected syntax" ++ MessageData.nest 2 (Format.line ++ refFmt))
+| some ex => throwError ref ("unexpected syntax, expected '" ++ ex ++ "'" ++ MessageData.nest 2 (Format.line ++ refFmt))
+
 protected def getCurrMacroScope : TermElabM Nat := do
 ctx ← read;
 pure ctx.currMacroScope

src/Init/Lean/Elab/TermApp.lean

@@ -328,7 +328,7 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
           s ← observing $ elabAppLVals ref f (lvals' ++ lvals) namedArgs args expectedType? explicit;
           pure $ acc.push s)
         acc
-    | _ => unreachable!
+    | _ => throwUnexpectedSyntax id "identifier"
   | _ => do
     f ← elabTerm f none;
     s ← observing $ elabAppLVals ref f lvals namedArgs args expectedType? explicit;

src/Init/Lean/Elab/TermBinders.lean

@@ -123,12 +123,12 @@ fun stx _ => match_syntax stx.val with
   elabBinders binders $ fun xs => do
     e ← elabType term;
     mkForall stx.val xs e
-| _ => unreachable!
+| _ => throwUnexpectedSyntax stx.val "forall"
 
 @[builtinTermElab arrow] def elabArrow : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `($dom:term -> $rng) => `(forall (a : $dom), $rng)
-| _                    => unreachable!
+| _                    => throwUnexpectedSyntax stx "->"
 
 @[builtinTermElab depArrow] def elabDepArrow : TermElab :=
 fun stx _ =>