feat: ignore unquoted identifiers in prechecked quotations

src/Lean/Elab/Quotation/Precheck.lean

@@ -49,9 +49,9 @@ partial def precheck : Precheck := fun stx => do
   if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then
     if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; true) (fun _ => false) then
       return
-  if stx.isAntiquot then
+  if stx.isAnyAntiquot then
     return
-  if !hasIdent stx then
+  if !hasQuotedIdent stx then
     return  -- we only precheck identifiers, so there is nothing to check here
   if let some stx' ← liftMacroM <| Macro.expandMacro? stx then
     precheck stx'
@@ -59,11 +59,13 @@ partial def precheck : Precheck := fun stx => do
   throwErrorAt stx "no macro or `[quotPrecheck]` instance for syntax kind '{stx.getKind}' found{indentD stx}
 This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check."
 where
-  hasIdent stx := do
-    for stx in stx.topDown do
-      if stx.isIdent then
-        return true
-    return false
+  hasQuotedIdent
+    | Syntax.ident .. => true
+    | stx =>
+      if stx.isAnyAntiquot then
+        false
+      else
+        stx.getArgs.any hasQuotedIdent
 
 def runPrecheck (stx : Syntax) : TermElabM Unit := do
   let opts ← getOptions

src/Lean/Syntax.lean

@@ -412,5 +412,8 @@ def mkAntiquotSuffixSpliceNode (kind : SyntaxNodeKind) (inner : Syntax) (suffix
 def isTokenAntiquot (stx : Syntax) : Bool :=
   stx.isOfKind `token_antiquot
 
+def isAnyAntiquot (stx : Syntax) : Bool :=
+  stx.isAntiquot || stx.isAntiquotSplice || stx.isAntiquotSuffixSplice || stx.isTokenAntiquot
+
 end Syntax
 end Lean

tests/lean/StxQuot.lean

@@ -101,6 +101,8 @@ open Parser.Term
 #eval run ``(x)
 #eval run ``(id)
 #eval run ``(pure)
+syntax "foo" term : term
+#eval run ``(foo $(Syntax.missing))  -- syntax with no quoted identifiers should be ignored
 #eval run ``(fun x => x)
 #eval run ``(fun x => y)
 #eval run ``(fun x y => x y)

tests/lean/StxQuot.lean.expected.out

@@ -49,7 +49,8 @@ fun (a : ?m) => sorry : (a : ?m) → ?m a
 StxQuot.lean:101:13-101:14: error: unknown identifier 'x'
 "`id._@.UnhygienicMain._hyg.1"
 "`pure._@.UnhygienicMain._hyg.1"
+"(termFoo_ \"foo\" <missing>)"
 "(Term.fun \"fun\" (Term.basicFun [`x._@.UnhygienicMain._hyg.1] \"=>\" `x._@.UnhygienicMain._hyg.1))"
-StxQuot.lean:105:22-105:23: error: unknown identifier 'y'
+StxQuot.lean:107:22-107:23: error: unknown identifier 'y'
 "(Term.fun\n \"fun\"\n (Term.basicFun\n  [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n  \"=>\"\n  (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))"
 "(Term.fun\n \"fun\"\n (Term.basicFun\n  [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n  \"=>\"\n  `x._@.UnhygienicMain._hyg.1))"