Enforce-or-retract the $-in-authored-binder-names reservation #44

New Issue

2026-05-30T12:51:26+02:00

Brummel commented

2026-05-30 12:51:26 +02:00

Follow-up from the #43 A2b fix (55d76ae) and its raw-buf close audit (b151990).

fresh_binder (ailang-core::desugar) mints shadow-rename binders as <base>$<n>. Collision-freedom rests on a probe against used + in-scope effective names. That probe does NOT see an authored binder literally named <base>$<n> that is out of scope at mint time but later binds under the same (def, name) uniqueness key — the exact collapse class #43 closes. The $-for-synthetic convention is NOT lexer-enforced (ailang-surface/src/lex.rs reserves only .).

Latent today (no fixture uses a $ binder), but it is precisely the robustness-against-hallucinations concern: a hallucinating LLM author could emit a $ binder.

depends on: nothing
context: two candidate closures — (a) enforce the reservation (reject $ in authored binder names, in pre_desugar_validation or the lexer); (b) make the probe complete by seeding used with every authored binder name in the current def before renaming. (a) also retroactively justifies the existing fresh/fresh_lifted machinery. Decide which; it is a real design fork, not a mechanical edit.

Follow-up from the #43 A2b fix (55d76ae) and its raw-buf close audit (b151990). `fresh_binder` (ailang-core::desugar) mints shadow-rename binders as `<base>$<n>`. Collision-freedom rests on a probe against `used` + in-scope effective names. That probe does NOT see an authored binder literally named `<base>$<n>` that is out of scope at mint time but later binds under the same `(def, name)` uniqueness key — the exact collapse class #43 closes. The `$`-for-synthetic convention is NOT lexer-enforced (ailang-surface/src/lex.rs reserves only `.`). Latent today (no fixture uses a `$` binder), but it is precisely the robustness-against-hallucinations concern: a hallucinating LLM author could emit a `$` binder. depends on: nothing context: two candidate closures — (a) enforce the reservation (reject `$` in authored binder names, in pre_desugar_validation or the lexer); (b) make the probe complete by seeding `used` with every authored binder name in the current def before renaming. (a) also retroactively justifies the existing `fresh`/`fresh_lifted` machinery. Decide which; it is a real design fork, not a mechanical edit.

Brummel added the idea label 2026-05-30 12:51:26 +02:00

Brummel referenced this issue

2026-05-30 15:26:30 +02:00

Stale compile_check baseline: check_ms drift +35-47% (pre-existing, confirmed at b151990) #45

Brummel referenced this issue from a commit

2026-05-30 15:27:57 +02:00

spec: reserve `$` in the Form-A lexer (refs #44)

Brummel referenced this issue from a commit

2026-05-30 15:27:57 +02:00

plan: reserved-dollar-in-names — dollar-lexer-reservation (refs #44)

Brummel referenced this issue from a commit

2026-05-30 15:27:57 +02:00