# Reserve `$` in the Form-A lexer — Design Spec
**Date:** 2026-05-30
**Status:** Draft — awaiting user spec review
**Authors:** orchestrator + Claude
## Goal
Close the latent collision class flagged by issue #44, the follow-up
to the #43 A2b fix (`55d76ae`) and its raw-buf close audit
(`b151990`).
`Desugarer::fresh_binder` (`crates/ailang-core/src/desugar.rs:537`)
mints shadow-rename binders as `$`. Its collision probe
checks the candidate against `used` (the synthetic-name accumulator)
and `scope` (in-scope *effective* names). It does **not** see an
authored binder literally named `$` that is out of scope at
mint time yet later binds under the same `(def, name)` uniqueness
key — the exact collapse class #43 closes. The `$`-for-synthetic
convention (`$mp_N` from `fresh`, `$lr_N` from `fresh_lifted`,
`$` from `fresh_binder`) is held by discipline only; nothing
in the toolchain rejects an authored `$`.
This cycle makes the convention a **lexically enforced invariant**:
no Form-A *identifier token* may contain `$`. `$` becomes reserved for
the compiler's synthetic namespace, by construction. That makes
`fresh_binder`'s probe sound (a `$` candidate can no longer
alias any authored name, because no authored name can contain `$`) and
retroactively justifies the whole `fresh` / `fresh_lifted` /
`fresh_binder` machinery.
The concern is precisely AILang's robustness-against-hallucinations
identity: latent today (no fixture uses a `$` binder), but a
hallucinating LLM author emitting Form A could mint a `$` name and
silently corrupt the uniqueness table.
### Why the lexer is the correct enforcement point
The threat vector is **Form-A source only**. By project design
(confirmed by the user, 2026-05-30) the client LLM author writes Form
A exclusively; it is *forbidden* from emitting canonical `.ail.json`
directly. The only actor that may hand-author `.ail.json` is the
orchestrator (me), in rare exceptions, as a deliberately
self-responsible channel. Therefore every authored identifier a
hallucinating client could produce passes through the Form-A lexer —
there is no second authoring surface to guard.
This places the invariant exactly at the lexer boundary: **written
source text contains no `$`; synthetic names come into existence only
afterwards** (at desugar) and may freely use `$`. That boundary —
text-in versus AST-internal — coincides with the
`tokenize` boundary. `$` is a *reserved character*, in the same
category as `(` and `)`: it has no legitimate use in any authored
identifier position (verified: zero authored `$` identifiers exist
anywhere in the checked-in `.ail` corpus; the six `$` occurrences are
all inside comments, which are stripped before tokenization). A
reserved character with no positional exceptions belongs in the lexer,
not in a position-aware AST walker.
This is a deliberate reversal of an earlier draft that placed the
reject in the check layer. That draft's load-bearing argument — "a
client could construct `.ail.json` directly, bypassing the lexer" — is
false under the confirmed authoring contract, so the simpler
lexer-local reservation is correct. It also requires no AST-position
machinery: the lexer has no notion of binder-vs-reference, and the
invariant needs none — `$` is banned in *every* identifier uniformly.
### Note on the `.`/`/` precedent (do not mimic it here)
Def-name reservation of `.` lives in the *check* layer
(`CheckError::InvalidDefName`, `crates/ailang-check/src/lib.rs:1534`),
not the lexer — *because* `.` and `/` have legitimate authored uses
(`std_list.map`, `io/print_str` both lex as single idents) and must be
allowed in some positions and rejected in others. That positional
split is exactly what forces a check-layer, AST-aware reject. `$` is
the opposite: no legitimate use anywhere, so no positional split, so
the lexer is right. (The issue's premise "lex.rs reserves only `.`" is
factually wrong on two counts — the lexer reserves no `.` at all, and
the def-name `.` reject is a check-layer concern — and is corrected
here.)
### Explicitly out of scope: the `.ail.json` deserialization path
The canonical `.ail.json` deserialization path is **deliberately not
guarded** by this cycle. Per the authoring contract it is the
orchestrator's self-responsible channel, not a client-reachable
surface. Guarding it would defend against the orchestrator's own
hallucination — a different, lower-priority concern that the user has
explicitly scoped out. This is a documented non-goal, not an
oversight; the honesty-rule consequence is that the spec, the
`fresh_binder` doc-comment, and any future contract text must state
"authored *Form-A* identifiers cannot contain `$`", never the broader
"no `Module` can contain a `$` name".
### Explicitly out of scope: the probe-body simplification
Issue #44's design question 4 asks whether the enforced invariant lets
`fresh_binder` drop a probe check. This cycle **keeps** the probe as
written; only the now-false doc-comment is corrected. Removing a probe
branch would couple `fresh_binder`'s correctness to a separable
property ("`used` is a complete record of every mint") that the fix
does not require. Out of scope.
## Architecture
### Enforcement: the maximal-run classification arm in `tokenize`
`crates/ailang-surface/src/lex.rs` tokenizes by taking maximal
non-paren / non-whitespace / non-`;` runs (string literals and
comments are handled earlier in the scan loop, before a run is formed).
There is **no** `classify_run` helper today: the classification is
**inline in the `tokenize` loop** — after the run is sliced
(`let raw = &input[start..i];`, lex.rs:183) it is classified in place
into `Tok::Int` / `Tok::Float` / `Tok::Ident` (lex.rs:184-230), and
`tokenize` returns `Result, LexError>`. The reservation is
enforced as a new guard **immediately after the run is sliced, before
the `is_int` classification** (i.e. inserted at lex.rs:184): if `raw`
contains `$`, return `Err(LexError::ReservedDollar { … })`.
The plan may either place the guard inline at that point or extract the
run-classification into a small helper as part of this iteration;
inline is the smaller change and the spec's code block (below) is
written inline. Pre-classification placement (rather than only on the
ident arm) is chosen so the message is uniform for every `$`-bearing
run — `x$1`, `$mp_0`, and a malformed `12$3` all report the same
reserved-character violation, rather than `12$3` masquerading as an
`InvalidInteger`. The rule expressed is crisp: *a run that becomes a
token must not contain `$`*.
What is **not** affected, by construction of the scan order:
- **String literals** (`"price: $5"`): handled by the `b'"'` branch in
the scan loop *before* a non-delimiter run is ever sliced. `$` inside
a string stays legal.
- **Comments** (`; loop$lr_0 …`): consumed by the `;`-to-EOL branch and
never tokenized. `$` inside a comment stays legal. (This is why the
six `$`-bearing example files keep parsing.)
### Surfacing: no new wiring
`parse` already converts a `LexError` into `ParseError` via
`ParseError::Lex(#[from] LexError)`
(`crates/ailang-surface/src/parse.rs:101-103`; `parse` propagates it at
`parse.rs:126`, `let toks = tokenize(input)?;`), and the CLI already
converts a surface parse failure into a diagnostic of code
`surface-parse-error` whose message is the error's `Display` — the
`W::SurfaceParse { path, message }` arm in
`crates/ail/src/main.rs:1339-1347`. So a `$`-bearing source flows:
`tokenize` → `Err(ReservedDollar)` → `parse` → `ParseError::Lex` →
`ail check` / `ail parse` print a `surface-parse-error` diagnostic and
exit non-zero. This channel is pinned green by
`crates/ail/tests/ct1_check_cli.rs::ail_check_json_on_ail_with_syntax_error_returns_structured_diagnostic`
(asserts `code == "surface-parse-error"` for a broken `.ail`). No new
error plumbing, no new `CheckError`, no AST walker, no multi-entry-point
wiring is required — a strictly smaller change than the check-layer
alternative.
### Scope: every authored identifier
Because the lexer has no AST, the reservation is uniform across every
identifier token: top-level def/type/ctor names, fn params, `let` /
`lam` / `loop` / `let-rec` binders, `match` pattern variables, **and**
all reference positions and operator-shaped idents. This is a superset
of "all authored binder names" and is the natural granularity; it
needs no enumeration of binder kinds and cannot drift out of sync with
the desugarer's renamable-binder set.
## Concrete code shapes
> The shipped artefact is a *parse-time rejection*. Its empirical
> evidence is therefore (a) a Form-A snippet that `ail check` must
> reject after this cycle, and (b) the two exemption cases that must
> stay accepted forever. The canonical *delivered* code is the
> in-source lexer test, since a must-fail `.ail` cannot live in
> `examples/` (see Testing strategy).
### The must-fail source (what a hallucinating author emits)
A fn whose `let` binder is literally `x$1` — the synthetic shape
`fresh_binder` mints. `$` lexes as an ordinary ident char *today*, so
this snippet parses and checks clean now; this cycle makes the lexer
**reject it at parse time**:
```ail
(module bad
(fn main
(type (fn-type (params) (ret (con Int))))
(params)
(body
(let x$1 7 x$1))))
```
After this cycle, `ail check bad.ail` exits non-zero with a
`surface-parse-error` diagnostic whose message names the reserved `$`
and its byte offset. (Consequently the spec parse-gate, re-run on this
block *after* the feature ships, will exit non-zero — expected; the
block is point-in-time evidence of the accept-today / reject-after
transition.)
### The two exemptions that must stay accepted
`$` inside a string literal (legitimate data) and inside a comment
(the existing six example files) must keep lexing clean — forever, not
just today:
```ail
(module dollar_ok
(fn main
; this comment mentions loop$lr_0 — a synthetic name, must stay legal
(type (fn-type (params) (ret (con Str))))
(params)
(body "price: $5")))
```
### The delivered lexer test (canonical concrete code)
```rust
#[test]
fn dollar_in_ident_is_reserved() {
let err = tokenize("x$1").expect_err("`$` in an ident must be a lex error");
assert!(
matches!(err, LexError::ReservedDollar { ref token, .. } if token == "x$1"),
"expected ReservedDollar(\"x$1\"), got {err:?}",
);
}
#[test]
fn dollar_in_string_literal_is_allowed() {
// The `$` lives inside a string; it must NOT trip the reservation.
let toks = tokenize(r#""price: $5""#).expect("string-internal `$` is legal");
assert!(matches!(toks.as_slice(), [Token { tok: Tok::Str(s), .. }] if s == "price: $5"));
}
#[test]
fn dollar_in_comment_is_allowed() {
// Comment is stripped before tokenization; the ident `x` survives.
let toks = tokenize("x ; mentions loop$lr_0\n").expect("comment `$` is legal");
assert!(matches!(toks.as_slice(), [Token { tok: Tok::Ident(s), .. }] if s == "x"));
}
```
### North-star slice (what the reservation protects)
The legitimate #43 shadowing idiom — the reservation guarantees no
authored name can collide with the rename `desugar_module` produces
(inner `buf` → `buf$1`). This must continue to parse, check, and
compile clean (no regression), because the `buf$1` mint happens at
desugar, never re-lexed:
```ail
(module northstar
(fn f
(type (fn-type (params) (ret (con Int))))
(params)
(body
(let buf 1
(let buf (app + buf 1) buf)))))
```
### Implementation shape — secondary supporting detail
**(1) New `LexError` variant** — `crates/ailang-surface/src/lex.rs`,
appended to the enum (after `InvalidEscape`, ~line 75):
```rust
#[error("reserved character `$` in token {token:?} at byte {start}; \
`$` is reserved for compiler-synthetic names")]
ReservedDollar { token: String, start: usize },
```
**(2) The reject inline in `tokenize`** — immediately after the run is
sliced (`let raw = &input[start..i];`, lex.rs:183), before the `is_int`
classification at lex.rs:184:
```rust
let raw = &input[start..i];
// raw-buf.#44: `$` is reserved for compiler-synthetic names.
if raw.contains('$') {
return Err(LexError::ReservedDollar { token: raw.to_string(), start });
}
// … existing `let first = …; let is_int = …;` classification …
```
**(3) Doc-comment correction (mandatory, honesty rule)** —
`crates/ailang-core/src/desugar.rs:528-536`. The current paragraph
asserts "an authored binder may legally contain `$`" and calls the gap
"tracked as a follow-up". Both become false. The corrected text states
the now-enforced invariant: authored **Form-A** identifiers may not
contain `$` (lexer-enforced in `ailang-surface`), so `fresh_binder`'s
`$` candidates cannot alias any authored name; the probe
against `used` + `scope` now guards only against prior synthetic mints
and in-scope renamed binders. The wording must stay scoped to *Form-A
authored* names (the `.ail.json` path is intentionally unguarded — see
out-of-scope above).
## Components
| Component | File | Change |
|---|---|---|
| `LexError::ReservedDollar` variant | `crates/ailang-surface/src/lex.rs` | add |
| `$`-reject inline in `tokenize` (after `let raw = …`, lex.rs:184) | `crates/ailang-surface/src/lex.rs` | add |
| `fresh_binder` doc-comment | `crates/ailang-core/src/desugar.rs:528-536` | correct |
| lexer must-fail + exemption tests | `crates/ailang-surface/src/lex.rs` (in-source) | add |
| surface-level reject test (optional) | `crates/ailang-surface/tests/` | add |
No change to `ailang-check` (no new `CheckError`, no walker, no entry-
point wiring) and no change to the desugarer logic (doc-comment only).
## Data flow
Authored Form-A text → `tokenize` → **[reject here if any run contains
`$`]** → `parse` → `Module` → `check` → `desugar_module` (mints
synthetic `$` names — never re-lexed) → typecheck → codegen.
The reject sits at the earliest possible point and at the exact
boundary the invariant describes. Everything downstream — including the
compiler's own `$`-bearing synthetic names — is unaffected, because
**no pipeline stage ever re-lexes post-desugar output** (verified: the
only production `tokenize` calls are `parse.rs:126` (`parse`) and
`parse.rs:149` (`parse_term`), fed only by disk-read source or
pre-desugar `print` output; `render`, `merge-prose`, and the round-trip
test all `print` then re-`parse` only *pre-desugar* modules — the
desugar pass runs after parse and its synthetic names never return to
`tokenize`).
## Error handling
A single new lexer error, `LexError::ReservedDollar { token, start }`,
surfaces through the existing `ParseError::Lex` (`parse.rs:103`) →
`W::SurfaceParse` → `surface-parse-error` diagnostic channel
(`main.rs:1339-1347`) with no new code. The message names the offending
token and its byte offset, consistent with the other byte-positioned
lexer errors (`InvalidInteger`, `UnterminatedString`, …).
## Testing strategy
**Must-fail / exemption (new, in-source in `lex.rs`):**
- `dollar_in_ident_is_reserved` — `tokenize("x$1")` → `ReservedDollar`.
- `dollar_in_string_literal_is_allowed` — `$` inside `"…"` lexes clean.
- `dollar_in_comment_is_allowed` — `$` inside a `;` comment is dropped,
surrounding idents lex clean.
- (optional) a `crates/ailang-surface/tests/` integration test feeding
a full `(module …)` with a `$` binder through `parse` and asserting
`Err(ParseError::Lex(LexError::ReservedDollar { … }))`.
**Hard design constraint — no must-fail `$` fixture in `examples/`.**
`crates/ailang-surface/tests/round_trip.rs` parses *every*
`examples/*.ail` with `.expect("parse 1")` and no filter. The existing
must-fail examples (`eq_float_must_fail.ail`, `raw_buf_reject_str.ail`)
survive because they *parse* and fail only later at check/type. A `$`
fixture fails at *parse*, so adding it to `examples/` would panic the
round-trip test. The reject test therefore lives in-source / in surface
`tests/`, never as an `examples/` file.
**No-regression (must stay green):**
- The full round-trip corpus — zero authored `$` idents, so every
example still parses; the six comment-only `$` files
(`local_rec_let_capture.ail` et al.) stay green because comments are
stripped pre-tokenization.
- The 19 existing in-source lexer tests.
- The #43 shadowing north-star slice parses, checks, and compiles clean
(the `buf$1` rename is minted post-parse, never re-lexed).
## Acceptance criteria
1. Any Form-A source containing a `$` in an identifier token (any
position — def/type/ctor name, param, `let`/`lam`/`loop`/`let-rec`
binder, `match` pattern var, or any reference/operator ident) is
rejected by `tokenize` with `LexError::ReservedDollar`, and surfaces
through `ail check` / `ail parse` as a `surface-parse-error`
diagnostic naming the token and its byte offset.
2. `$` inside a string literal is accepted unchanged.
3. `$` inside a comment is accepted unchanged (comment stripped).
4. The `.ail.json` deserialization path is **not** guarded (documented
non-goal); no test asserts it rejects `$`.
5. The full round-trip corpus and the 19 existing lexer tests stay
green; no must-fail `$` fixture is added under `examples/`.
6. The #43 shadowing idiom still parses, checks, and compiles clean;
the `buf$1` rename is unaffected.
7. `fresh_binder`'s doc-comment no longer claims `$` is legal in
authored binders and no longer calls the gap a follow-up; it states
the enforced invariant, scoped to *Form-A authored* identifiers.