design: ratify 19a-arc in DESIGN.md (tidy)
Per CLAUDE.md tidy-iter at family boundaries. ailang-architect flagged the canonical 'DESIGN.md silent' finding for the entire 19a-arc — same shape as family-20's 20e tidy. Decision 10 schema-additions block gained 'Iter 19b — FnDef.suppress' entry. New subsection 'Advisory diagnostics — Iter 19a-arc' documents the over-strict-mode lint rule (incl. heap-type filter rationale), Severity::Warning introduction, CLI exit-on-Error gating, and the suppress mechanism. New subsection 'Why advisory + suppress instead of inference' pins the three substantive reasons (annotation-states-intent, drift-bremse, LLM-authoring forcing function) so future iters can't reopen the decision without engaging the recorded rationale. Migration plan extended with step 7 covering 19a/19a.1/19b. Decision 10's mandatory-annotation rule is explicitly reaffirmed as unchanged. No code changes. Two architect findings deferred (codegen FnDef fan-out, snapshot-fixture coupling). Data model (MVP) drift predates 19b — separate iter.
This commit is contained in:
@@ -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<Suppress> ; 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 <code>: <because>` 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)
|
||||
|
||||
|
||||
Reference in New Issue
Block a user