From 683ecb2d656d5a85a53ccaf8c6b4ad57b16d23d5 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 29 Apr 2021 10:07:12 +0200
Subject: [PATCH] feat: ignore unquoted identifiers in prechecked quotations

---
 src/Lean/Elab/Quotation/Precheck.lean | 16 +++++++++-------
 src/Lean/Syntax.lean                  |  3 +++
 tests/lean/StxQuot.lean               |  2 ++
 tests/lean/StxQuot.lean.expected.out  |  3 ++-
 4 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
index 072212e275..e6efc96063 100644
--- a/src/Lean/Elab/Quotation/Precheck.lean
+++ b/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
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index decd0578cd..024ab614f5 100644
--- a/src/Lean/Syntax.lean
+++ b/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
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 4c1da4c570..7f749fff83 100644
--- a/tests/lean/StxQuot.lean
+++ b/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)
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 9985cd27c6..bae67764e8 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/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))"