AILang/docs/specs/0057-reserved-dollar-in-names.md

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 <base>$<n>. 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 <base>$<n> 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, <hint>$lr_N from fresh_lifted, <base>$<n> 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 <base>$<n> 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<Vec<Token>, 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:

(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:

(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)

#[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:

(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):

#[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:

        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 <base>$<n> 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.