diff --git a/docs/DESIGN.md b/docs/DESIGN.md index d3e5def..f336af1 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1074,6 +1074,95 @@ All four are skipped during serialisation when absent / false / None so canonical-JSON hashes of every fixture remain stable until the fixture intentionally adopts the feature. +**Iter 19b — `FnDef.suppress`.** + +```rust +FnDef.suppress: Vec ; advisory diagnostic suppress list + +struct Suppress { + code: String, // diagnostic code being suppressed + because: String, // mandatory non-empty reason +} +``` + +Form-A surface: `(suppress (code "...") (because "..."))` clause +between fn name and `(type ...)`. Multiple clauses allowed; one +per entry. Form-B (prose) renders one +`// @suppress : ` line per entry above the doc +string — lossless, contract metadata. + +Skipped from serialisation when empty so pre-19b fixtures keep +bit-identical canonical-JSON hashes (regression-pinned by +`iter19b_empty_suppress_preserves_pre_19b_hashes` and +`iter19b_schema_extension_preserves_pre_19b_hashes`). + +### Advisory diagnostics — Iter 19a-arc + +The 19a-arc (19a / 19a.1 / 19b) introduces the language's first +**advisory** typechecker diagnostic and the suppression mechanism +that goes with it. Decision 10's mandatory-annotation rule is +unchanged: `param_modes` and `ret_mode` remain author-required; +the typechecker does not infer them. What's new is feedback when +an authored annotation is *stricter than necessary*. + +**The lint: `over-strict-mode` (Iter 19a + 19a.1).** Fires on a +fn-param `p` annotated `(own T)` when: + + 1. `p`'s `consume_count == 0` (uniqueness pass: the body + never consumes `p` as a whole). + 2. For every match arm whose scrutinee is `p`, no + **heap-typed** pattern-binder has `consume_count > 0`. + +The heap-type filter is load-bearing for soundness: +`match xs { Cons(h, t) => h }` records `consume_count(h) == 1`, +but `h: Int` is read by-value — no RC traffic, no heap data +moved out of `xs`'s allocation. Filtering primitive-typed +binders is what lets the lint correctly identify `head_or_zero` +as over-strict (could be `borrow`) while staying silent on +`sum_list` where `t: List` *is* moved out. + +Severity: `Warning`. The first ever Warning-level diagnostic; +prior to 19a all diagnostics were `Error`. CLI exit semantics +adjusted: `ail check`, `ail build`, `ail emit-ir` exit 1 only on +at least one Error. Warnings print but do not abort. + +**The suppression: `mode-strict-because` (Iter 19b).** Authors +who want to keep an over-strict annotation deliberately (e.g. +RC codegen-test fixtures, fns reserved for planned in-place +mutation) attach a `Suppress` entry naming the diagnostic code +and a non-empty reason. The typechecker drops matching +diagnostics from the output. Empty `because` is a hard error +(`empty-suppress-reason`); wrong-code suppresses are silent +no-ops (open-set diagnostic registry — a suppress for a code +that doesn't fire today may exist defensively for a code that +might fire after a future edit). + +### Why advisory + suppress instead of inference + +Three reasons, all anchored in Decision 10's framing: + + 1. **Annotation states intent; inference picks + weakest-supporting.** These often coincide today but are + conceptually different. The annotation captures what the + author committed to (e.g. `(own T)` reserved for a planned + mutation that hasn't landed); inference would silently + relax it. + 2. **Annotation is a drift-bremse.** Body change that flips + the inferred mode produces caller-side breakage at remote + sites. Annotation enforces the local-conflict-error pattern + instead. + 3. **Forcing function for LLM authoring.** Without mandatory + annotation, the LLM never has to commit to ownership intent + before writing the body. The advisory lint plus suppress + lets us flag accidental over-strictness without weakening + the contract. + +The suppress mechanism with mandatory-reason mirrors Rust's +`#[allow(...)]`-style escape hatch but sharpens it: the reason +is required (not optional), and it becomes part of the contract +the next reader sees. CLAUDE.md's "preserve correctness across +development cycles" is what this directly serves. + ### Inference algorithm (Iter 18c) Post-typecheck, post-`lift_letrecs`, pre-codegen pass over the @@ -1203,6 +1292,11 @@ monomorphised copies resolve to concrete drop fns). 6. **Iter 18f:** RC validation bench. If RC within 1.3× of bump on `bench/run.sh`, retire Boehm: flip default to RC, drop `-lgc`, mark Decision 9 historical. +7. **Iter 19a / 19a.1 / 19b:** advisory `over-strict-mode` lint + + precise sub-binder analysis with heap-type filter + + `FnDef.suppress` suppression mechanism with mandatory-reason. + First `Severity::Warning` diagnostic; CLI exit gated on Error + only. Decision 10's mandatory-annotation rule is unchanged. ### Adjacent extensions for mutability (out of Decision 10's scope) diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index bc77c29..84a7e85 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -9442,3 +9442,96 @@ JOURNAL queue: empty again. Three pre-existing 20b deferrals (let-inlining, `print` sugar, deeply-nested-match-on-sub-binder in 19a.1) remain queued; all three need real-corpus signal that hasn't surfaced. + +## 2026-05-08 — 19a-arc tidy-iter (DESIGN.md ratification) + +Per CLAUDE.md "Tidy-iter at family boundaries" — the 19a-arc +(19a + 19a.1 + 19b) closes with a tidy. `ailang-architect` ran +the drift review and reported the canonical "DESIGN.md silent" +finding, identical in shape to the one family-20's tidy-iter +(20e) caught: a substantial new mechanism shipped with no +ratification in the canonical spec. + +### Architect findings + + 1. **DESIGN.md silent on the entire 19a-arc.** Zero hits for + `suppress` / `over-strict-mode` / `empty-suppress-reason` / + `Severity::Warning`. Schema-additions block didn't list + `FnDef.suppress`. Highest-leverage fix. + 2. **Codegen carries `suppress: vec![]` in 7 synthetic FnDef + sites** (`crates/ailang-codegen/src/lib.rs` + lift / desugar + / reuse_shape / uniqueness / pretty). Mechanically correct; + a `FnDef::default()` or `synthetic` constructor would absorb + the fan-out. Bounded; observation, not blocker. + 3. **Snapshot-fixture coupling ratified by recurrence.** 19b + regenerated three pinned `.prose.txt` snapshots — exactly + the cross-family-coupling pattern 20e's item 3 named. + Promote to known structural cost, not a fix. + +### Resolved this iter + +**Item 1 — ratified.** Two edits to `docs/DESIGN.md`: + + - **Schema additions** subsection (Decision 10) gained an + "Iter 19b — `FnDef.suppress`" entry: schema shape, form-A + surface, form-B render, the `skip_serializing_if` / + bit-identity invariant, and the regression-pinning tests. + - **New subsection "Advisory diagnostics — Iter 19a-arc"** + placed between "Schema additions" and "Inference + algorithm". Documents the `over-strict-mode` lint rule + (incl. the heap-type filter rationale), the + `Severity::Warning` introduction, the CLI exit-on-Error + gating, and the `mode-strict-because` suppression with + mandatory-reason. + - **New subsection "Why advisory + suppress instead of + inference"** documents the three substantive reasons that + the user surfaced earlier in the design conversation — + annotation-states-intent vs. inference-picks-weakest, the + drift-bremse role, and the LLM-authoring forcing function. + This pins the rationale so future iters can't reopen the + decision without engaging with the recorded reasons. + - **Migration plan** gained a 7th step covering the 19a-arc. + +The ratification explicitly reaffirms that Decision 10's +mandatory-annotation rule is unchanged. The lint is *advisory*, +the suppress is an *escape hatch with reason*, neither weakens +the contract. + +### Deferred + +**Item 2 (codegen FnDef fan-out).** A `FnDef::default()` / +`synthetic_fn(...)` constructor would absorb the boilerplate +across the seven synthetic sites. Worth doing the next time a +schema-additive `FnDef` field lands; not worth doing speculatively. + +**Item 3 (snapshot-fixture coupling).** Recorded as known +structural cost. The pattern: any iter that touches a fixture +which is pinned by `ailang-prose/tests/snapshot.rs` must also +re-render the `.prose.txt`. Mitigation would require a more +abstract pinning mechanism (e.g. shape-checking instead of +byte-equality), which is itself a substantive design choice and +not on the queue today. + +**Data model (MVP) drift.** DESIGN.md's "Data model (MVP)" +section (around L1280–1325) shows pre-18a / pre-19b shapes for +`FnDef` and `Type::Fn` — no `param_modes`, no `ret_mode`, no +`suppress`. This drift predates 19b by several iters. Bringing +it current is its own iter (touches three or four shape blocks). + +### State of the world + +JOURNAL queue: empty. Both family-20 and the 19a-arc are now +tidied with their respective ratifications recorded in +DESIGN.md. + +Remaining longer-term substantive forks (none queued, none +default): + + - **Boehm retirement** (Decision 9 → Decision 10 endgame). + Validation bench shipped (18f); the orchestrator's call to + actually flip the default has not been made. + - **Family 21+** — language surface expansion (typeclasses, + polymorphic ADTs beyond the heutige form, IO/error + handling). + - **Data model (MVP) refresh.** Cosmetic doc-tidy iter to + bring the schema snapshot current.