feat: allow Lean.Parser.Term.id to be used in binders

cc @Kha

src/Init/Lean/Elab/Binders.lean

@@ -88,24 +88,35 @@ else
   else
     throwUnsupportedSyntax
 
+private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
+ids.getArgs.mapM $ fun id =>
+  let k := id.getKind;
+  if k == identKind || k == `Lean.Parser.Term.hole then
+    pure id
+  else if k == `Lean.Parser.Term.id && id.getArgs.size == 2 && (id.getArg 1).isNone then
+    -- The parser never generates this case, but it is convenient when writting macros.
+    pure (id.getArg 0)
+  else
+    throwError id "identifier or `_` expected"
+
 private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) :=
 match stx with
 | Syntax.node k args =>
-  if k == `Lean.Parser.Term.simpleBinder then
+  if k == `Lean.Parser.Term.simpleBinder then do
     -- binderIdent+
-    let ids  := (args.get! 0).getArgs;
+    ids ← getBinderIds (args.get! 0);
     let type := mkHole stx;
     ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default }
   else if k == `Lean.Parser.Term.explicitBinder then do
     -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
-    let ids         := (args.get! 1).getArgs;
+    ids ← getBinderIds (args.get! 1);
     let type        := expandBinderType (args.get! 2);
     let optModifier := args.get! 3;
     type ← expandBinderModifier type optModifier;
     ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default }
-  else if k == `Lean.Parser.Term.implicitBinder then
+  else if k == `Lean.Parser.Term.implicitBinder then do
     -- `{` binderIdent+ binderType `}`
-    let ids  := (args.get! 1).getArgs;
+    ids ← getBinderIds (args.get! 1);
     let type := expandBinderType (args.get! 2);
     ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.implicit }
   else if k == `Lean.Parser.Term.instBinder then do

src/Init/Lean/Elab/Term.lean

@@ -203,6 +203,12 @@ when (checkTraceOption opts cls) $ logTrace cls ref (msg ())
 def logDbgTrace (msg : MessageData) : TermElabM Unit := do
 trace `Elab.debug Syntax.missing $ fun _ => msg
 
+/-- For testing `TermElabM` methods. The #eval command will sign the error. -/
+def throwErrorIfErrors : TermElabM Unit := do
+s ← get;
+when s.messages.hasErrors $
+  throwError Syntax.missing "Error(s)"
+
 @[inline] def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TermElabM Unit :=
 trace cls Syntax.missing msg
 

tests/lean/run/termElab.lean

@@ -6,12 +6,23 @@ open Lean.Elab.Term
 
 set_option trace.Elab.debug true
 
-def tst : TermElabM Unit := do
+def tst1 : TermElabM Unit := do
 opt ← getOptions;
-stx ← `(fun (a : Nat) => a);
+stx ← `(forall (a b : Nat), Nat);
 dbgTrace "message 1"; -- This message goes direct to stdio. It will be displayed before trace messages.
 e ← elabTermAndSynthesize stx none;
 logDbgTrace (">>> " ++ e); -- display message when `trace.Elab.debug` is true
 dbgTrace "message 2"
 
-#eval tst
+#eval tst1
+
+def tst2 : TermElabM Unit := do
+opt ← getOptions;
+let a := mkTermId `a;
+let b := mkTermId `b;
+stx ← `((fun {$a : Type} (x : $a) => @id $a x) 1);
+e ← elabTermAndSynthesize stx none;
+logDbgTrace (">>> " ++ e);
+throwErrorIfErrors
+
+#eval tst2