feat: enforce correct syntax kind in macros

doc/macro_overview.md

@@ -302,7 +302,7 @@ To see the desugared definition of the actual expansion, we can again use
 ```lean
 
 set_option trace.Elab.definition true in
-macro "exfalso" : tactic => `(apply False.elim)
+macro "exfalso" : tactic => `(tactic| apply False.elim)
 
 /-
 Results in the expansion:

src/Init/Conv.lean

@@ -242,11 +242,11 @@ which only unfolds `@[reducible]` definitions). -/
 macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s)
 
 /-- `args` traverses into all arguments. Synonym for `congr`. -/
-macro "args" : conv => `(congr)
+macro "args" : conv => `(conv| congr)
 /-- `left` traverses into the left argument. Synonym for `lhs`. -/
-macro "left" : conv => `(lhs)
+macro "left" : conv => `(conv| lhs)
 /-- `right` traverses into the right argument. Synonym for `rhs`. -/
-macro "right" : conv => `(rhs)
+macro "right" : conv => `(conv| rhs)
 /-- `intro` traverses into binders. Synonym for `ext`. -/
 macro "intro" xs:(colGt ident)* : conv => `(conv| ext $xs*)
 

src/Init/Notation.lean

@@ -110,17 +110,17 @@ end Lean
 Maximum precedence used in term parsers, in particular for terms in
 function position (`ident`, `paren`, ...)
 -/
-macro "max"  : prec => `(1024)
+macro "max"  : prec => `(prec| 1024)
 /-- Precedence used for application arguments (`do`, `by`, ...). -/
-macro "arg"  : prec => `(1023)
+macro "arg"  : prec => `(prec| 1023)
 /-- Precedence used for terms not supposed to be used as arguments (`let`, `have`, ...). -/
-macro "lead" : prec => `(1022)
+macro "lead" : prec => `(prec| 1022)
 /-- Parentheses are used for grouping precedence expressions. -/
 macro "(" p:prec ")" : prec => return p
 /-- Minimum precedence used in term parsers. -/
-macro "min"  : prec => `(10)
+macro "min"  : prec => `(prec| 10)
 /-- `(min+1)` (we can only write `min+1` after `Meta.lean`) -/
-macro "min1" : prec => `(11)
+macro "min1" : prec => `(prec| 11)
 /--
 `max:prec` as a term. It is equivalent to `eval_prec max` for `eval_prec` defined at `Meta.lean`.
 We use `max_prec` to workaround bootstrapping issues.
@@ -128,13 +128,13 @@ We use `max_prec` to workaround bootstrapping issues.
 macro "max_prec" : term => `(1024)
 
 /-- The default priority `default = 1000`, which is used when no priority is set. -/
-macro "default" : prio => `(1000)
+macro "default" : prio => `(prio| 1000)
 /-- The standardized "low" priority `low = 100`, for things that should be lower than default priority. -/
-macro "low"     : prio => `(100)
+macro "low"     : prio => `(prio| 100)
 /-- The standardized "medium" priority `med = 1000`. This is the same as `default`. -/
-macro "mid"     : prio => `(1000)
+macro "mid"     : prio => `(prio| 1000)
 /-- The standardized "high" priority `high = 10000`, for things that should be higher than default priority. -/
-macro "high"    : prio => `(10000)
+macro "high"    : prio => `(prio| 10000)
 /-- Parentheses are used for grouping priority expressions. -/
 macro "(" p:prio ")" : prio => return p
 
@@ -476,7 +476,8 @@ macro_rules
 -- Declare `this` as a keyword that unhygienically binds to a scope-less `this` assumption (or other binding).
 -- The keyword prevents declaring a `this` binding except through metaprogramming, as is done by `have`/`show`.
 /-- Special identifier introduced by "anonymous" `have : ...`, `suffices p ...` etc. -/
-macro tk:"this" : term => return Syntax.ident tk.getHeadInfo "this".toSubstring `this []
+macro tk:"this" : term =>
+  return (⟨(Syntax.ident tk.getHeadInfo "this".toSubstring `this [])⟩ : TSyntax `term)
 
 /--
 Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.

src/Init/NotationExtra.lean

@@ -77,12 +77,15 @@ end Lean
 
 open Lean
 
+section
+open TSyntax.Compat
 macro "∃ " xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Exists xs b
 macro "exists" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Exists xs b
 macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Sigma xs b
 macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``PSigma xs b
 macro:35 xs:bracketedExplicitBinders " × " b:term:35  : term => expandBrackedBinders ``Sigma xs b
 macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders ``PSigma xs b
+end
 
 -- enforce indentation of calc steps so we know when to stop parsing them
 syntax calcStep := ppIndent(colGe term " := " withPosition(term))

src/Init/System/IO.lean

@@ -209,7 +209,7 @@ def sleep (ms : UInt32) : BaseIO Unit :=
   return t.get
 
 local macro "nonempty_list" : tactic =>
-  `(exact Nat.zero_lt_succ _)
+  `(tactic| exact Nat.zero_lt_succ _)
 
 /-- Wait until any of the tasks in the given list has finished, then return its result. -/
 @[extern "lean_io_wait_any"] opaque waitAny (tasks : @& List (Task α))

src/Init/Tactics.lean

@@ -257,13 +257,13 @@ syntax (name := refl) "eq_refl" : tactic
 This is supposed to be an extensible tactic and users can add their own support
 for new reflexive relations.
 -/
-macro "rfl" : tactic => `(eq_refl)
+macro "rfl" : tactic => `(tactic| eq_refl)
 
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).
 -/
-macro "rfl'" : tactic => `(set_option smartUnfolding false in with_unfolding_all rfl)
+macro "rfl'" : tactic => `(tactic| set_option smartUnfolding false in with_unfolding_all rfl)
 
 /--
 `ac_rfl` proves equalities up to application of an associative and commutative operator.
@@ -283,16 +283,16 @@ a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but
 you can double check if a theorem depends on `sorry` by using
 `#print axioms my_thm` and looking for `sorryAx` in the axiom list.
 -/
-macro "sorry" : tactic => `(exact @sorryAx _ false)
+macro "sorry" : tactic => `(tactic| exact @sorryAx _ false)
 
 /-- `admit` is a shorthand for `exact sorry`. -/
-macro "admit" : tactic => `(exact @sorryAx _ false)
+macro "admit" : tactic => `(tactic| exact @sorryAx _ false)
 
 /--
 `infer_instance` is an abbreviation for `exact inferInstance`.
 It synthesizes a value of any target type by typeclass inference.
 -/
-macro "infer_instance" : tactic => `(exact inferInstance)
+macro "infer_instance" : tactic => `(tactic| exact inferInstance)
 
 /-- Optional configuration option for tactics -/
 syntax config := atomic(" (" &"config") " := " term ")"
@@ -360,7 +360,7 @@ macro (name := rwSeq) "rw" c:(config)? s:rwRuleSeq l:(location)? : tactic =>
   match s with
   | `(rwRuleSeq| [$rs,*]%$rbrak) =>
     -- We show the `rfl` state on `]`
-    `(tactic| rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl)))
+    `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
   | _ => Macro.throwUnsupported
 
 /--
@@ -647,7 +647,7 @@ it is defined as `repeat sorry`.
 It is useful when working on the middle of a complex proofs,
 and less messy than commenting the remainder of the proof.
 -/
-macro "stop" tacticSeq : tactic => `(repeat sorry)
+macro "stop" tacticSeq : tactic => `(tactic| repeat sorry)
 
 /--
 The tactic `specialize h a₁ ... aₙ` works on local hypothesis `h`.
@@ -706,7 +706,7 @@ when working on a long tactic proof, by using `save` after expensive tactics.
 (TODO: do this automatically and transparently so that users don't have to use
 this combinator explicitly.)
 -/
-macro (name := save) "save" : tactic => `(skip)
+macro (name := save) "save" : tactic => `(tactic| skip)
 
 /--
 The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing.

src/Init/WFTactics.lean

@@ -10,7 +10,7 @@ import Init.WF
 /-- Unfold definitions commonly used in well founded relation definitions.
 This is primarily intended for internal use in `decreasing_tactic`. -/
 macro "simp_wf" : tactic =>
-  `(simp [invImage, InvImage, Prod.lex, sizeOfWFRel,
+  `(tactic| simp [invImage, InvImage, Prod.lex, sizeOfWFRel,
           measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
 /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"

src/Lean/Elab/Macro.lean

@@ -33,8 +33,9 @@ open Lean.Parser.Command
       let macroRulesCmd ← if rhs.getArgs.size == 1 then
         -- `rhs` is a `term`
         let rhs := ⟨rhs[0]⟩
-        `($[$doc?:docComment]? macro_rules | `($pat) => $rhs)
+        `($[$doc?:docComment]? macro_rules | `($pat) => Functor.map (@TSyntax.raw $(quote cat.getId.eraseMacroScopes)) $rhs)
       else
+        -- TODO(gabriel): remove after bootstrap
         -- `rhs` is of the form `` `( $body ) ``
         let rhsBody := ⟨rhs[1]⟩
         `($[$doc?:docComment]? macro_rules | `($pat) => `($rhsBody))

src/lake

@@ -1 +1 @@
-Subproject commit b843041aa4589ee093a67794967421e347f33482
+Subproject commit 8546900b81abb8df291d95bd615819a28b4fdc15

tests/lean/run/allGoals.lean

@@ -39,7 +39,7 @@ theorem Weekday.nextOfPrevious'' (d : Weekday) : previous (next d) = d ∧ next
   apply And.intro <;> cases d <;> rfl
 
 open Lean.Parser.Tactic in
-macro "rwd " x:term : tactic => `(tactic| rw [$x:term]; done)
+macro "rwd " x:term : tactic => `(tactic| (rw [$x:term]; done))
 
 theorem ex (a b c : α) (h₁ : a = b) (h₂ : a = c) : b = a ∧ c = a := by
   apply And.intro <;> first | rwd h₁ | rwd h₂

tests/lean/run/newfrontend1.lean

@@ -63,7 +63,7 @@ by {
   assumption
 }
 
-macro "intro3" : tactic => `(tactic| intro; intro; intro)
+macro "intro3" : tactic => `(tactic| (intro; intro; intro))
 macro "check2" x:term : command => `(#check $x #check $x)
 macro "foo" x:term "," y:term : term => `($x + $y + $x)
 

tests/lean/run/precDSL.lean

@@ -8,8 +8,8 @@ macro_rules
 #check id fn x => x + 1
 #check id function x => x + 1
 
-macro "addPrec" : prec => `(65)
-macro "mulPrec" : prec => `(70)
+macro "addPrec" : prec => `(prec| 65)
+macro "mulPrec" : prec => `(prec| 70)
 
 infix:addPrec " +' " => Nat.add
 infix:mulPrec " *' " => Nat.mul