From 79bbf4e8d6193db57a64b5048f139a875b983bd6 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Fri, 17 Jul 2026 12:16:27 +0000
Subject: [PATCH 1/2] feat: forbid non-reserved identifiers via `withForbidden`

This PR makes `withForbidden` stop a term at a non-reserved word used as an identifier, not just at a registered token. A parser like `withForbidden "invariant" termParser` now ends the term when it reaches a bare `invariant`, while `invariant` remains usable as an identifier everywhere else.

`identFn` rejects an identifier whose text is in `forbiddenTks`, mirroring the forbidden-token check in `mkTokenAndFixPos`. The check is guarded by `forbiddenTks.isEmpty`, so the common identifier path is unchanged, and it does not affect `rawIdent` (field projections), the parenthesized escape via `withoutForbidden`, or reserved-token forbidding.
---
 src/Lean/Parser/Basic.lean | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 9342d5a938c7..56ad17794c0b 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1295,7 +1295,20 @@ def nameLitNoAntiquot : Parser := {
   info := mkAtomicInfo "name"
 }
 
-def identFn : ParserFn := expectTokenFn identKind "identifier"
+def identFn : ParserFn := fun c s =>
+  if c.forbiddenTks.isEmpty then
+    expectTokenFn identKind "identifier" c s
+  else
+    -- A forbidden token used as an identifier (e.g. a non-reserved clause keyword like
+    -- `invariant`) stops the enclosing term, mirroring `mkTokenAndFixPos`.
+    let iniSz  := s.stackSize
+    let iniPos := s.pos
+    let s := expectTokenFn identKind "identifier" c s
+    if s.hasError then s
+    else match s.stxStack.back with
+      | .ident _ rawVal _ _ =>
+        if c.forbiddenTks.contains rawVal.toString then s.mkErrorAt "forbidden token" iniPos iniSz else s
+      | _ => s
 
 def identNoAntiquot : Parser := {
   fn   := identFn

From 648cffa4df99dcbaf3d044b552ce28c47265bbea Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Fri, 17 Jul 2026 15:22:42 +0000
Subject: [PATCH 2/2] test: forbidden non-reserved identifiers in withForbidden
 scopes

---
 tests/elab/forbiddenIdentifiers.lean | 30 ++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 tests/elab/forbiddenIdentifiers.lean

diff --git a/tests/elab/forbiddenIdentifiers.lean b/tests/elab/forbiddenIdentifiers.lean
new file mode 100644
index 000000000000..34684fd91043
--- /dev/null
+++ b/tests/elab/forbiddenIdentifiers.lean
@@ -0,0 +1,30 @@
+import Lean
+/-!
+`withForbidden` stops a term at a non-reserved word used as a bare identifier, while the word
+stays usable as an identifier (escaped, projected, or a plain declaration name).
+-/
+open Lean Elab Command Parser
+
+namespace ForbiddenIdentTest
+
+-- `#collect e sep e'` parses `e` with the non-reserved word `sep` forbidden, so a bare `sep`
+-- ends `e` without `sep` being a reserved keyword.
+@[command_parser]
+def collectCmd : Parser := leading_parser
+  "#collect " >> withForbidden "sep" termParser >> nonReservedSymbol "sep" >> ppSpace >> termParser
+
+@[command_elab collectCmd]
+def elabCollect : CommandElab := fun _ => pure ()
+
+-- A bare `sep` ends the first term (requires the forbidding; else `a sep` is an application).
+#collect a sep b
+-- A multi-token first term still stops at the bare `sep`.
+#collect f a sep b
+-- Escaped `«sep»` is not forbidden: it is consumed as the first term.
+#collect «sep» sep b
+-- A projection `.sep` (rawIdent path) is not forbidden.
+#collect (id x).sep sep b
+-- The word remains usable as an ordinary identifier.
+def sep : Nat := 0
+
+end ForbiddenIdentTest