fix: missing node

src/Lean/Elab/Match.lean

@@ -17,6 +17,23 @@ private def expandSimpleMatchWithType (stx discr lhsVar type rhs : Syntax) (expe
 newStx ← `(let $lhsVar : $type := $discr; $rhs);
 withMacroExpansion stx newStx $ elabTerm newStx expectedType?
 
+/-
+
+```
+def matchDiscr := optIdent >> termParser
+parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
+```
+Remark the `optIdent` must be `none` at `matchDiscr`. They are expanded by `expandMatchDiscr?`.
+-/
+private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
+tryPostponeIfNoneOrMVar expectedType?;
+let discrs := (stx.getArg 1).getArgs.getSepElems.map fun d => d.getArg 1;
+throwError stx ("WIP " ++ stx ++ "\n" ++ toString discrs)
+
+/-- Expand discriminants of the form `h : t` -/
+private def expandMatchDiscr? (stx : Syntax) : MacroM (Option Syntax) := do
+pure none -- TODO
+
 -- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
 @[builtinTermElab «match»] def elabMatch : TermElab :=
 fun stx expectedType? => match_syntax stx with
@@ -24,7 +41,11 @@ fun stx expectedType? => match_syntax stx with
   | `(match $discr:term with | $y:ident => $rhs:term)         => expandSimpleMatch stx discr y rhs expectedType?
   | `(match $discr:term : $type with $y:ident => $rhs:term)   => expandSimpleMatchWithType stx discr y type rhs expectedType?
   | `(match $discr:term : $type with | $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
-  | _ => throwUnsupportedSyntax
+  | _ => do
+    stxNew? ← liftMacroM $ expandMatchDiscr? stx;
+    match stxNew? with
+    | some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+    | none        => elabMatchCore stx expectedType?
 
 end Term
 end Elab

src/Lean/Parser/Term.lean

@@ -106,7 +106,7 @@ withPosition $ fun pos =>
   (if optionalFirstBar then optional "| " else "| ") >>
   sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 
-def matchDiscr := optIdent >> termParser
+def matchDiscr := parser! optIdent >> termParser
 
 @[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
 @[builtinTermParser] def «nomatch»  := parser!:leadPrec "nomatch " >> termParser