JOURNAL: Iter 18c.2 — linearity check + suggested_rewrites

Records what shipped in 18c.2 (activation gate, two diagnostic
codes, position model, the new parse_term / term_to_form_a
round-trip in ailang-surface, gate on clean-typecheck), the
three known false negatives that are deliberate scope cuts
(missing-consume-of-Own, lam captures conservative, pattern
bindings start fresh), and the dispatch for 18c.3 (uniqueness
inference + codegen inc/dec — the iter where RC actually starts
collecting memory).

docs/JOURNAL.md

@@ -6141,3 +6141,166 @@ informative — design discipline corrupts faster than I notice
 when I let "implementer-friendly" creep into the slot reserved
 for "language-honest". The CLAUDE.md rule exists so the next
 session catches this earlier.
+
+## Iter 18c.2 — linearity check + suggested_rewrites
+
+Pure diagnostic addition. New module `ailang-check::linearity`
+walks every fn whose `param_modes` are all explicit (`Borrow`
+or `Own`, no `Implicit`); tracks per-binder consume/borrow state
+through the AST; emits `use-after-consume` and
+`consume-while-borrowed` diagnostics with form-A
+`suggested_rewrites`. No IR change, no codegen change, no runtime
+change. Existing fixtures (all `Implicit`) untouched; the
+all-explicit `borrow_own_demo` fixture passes the check
+unchanged.
+
+### Activation gate
+
+The check is opt-in *by signature*: a fn has to have spelled
+every param mode explicitly (none `Implicit`) and have at least
+one param. Any `Implicit` in the signature skips the fn's body
+entirely. This is the back-compat lane Decision 10 promised —
+LLMs that want linearity guarantees opt in by writing modes;
+hand-written or transitional code keeps the old behaviour.
+
+### Diagnostics
+
+Two codes, both at `Severity::Error`, both with
+`ctx = {"binder": "<n>"}`:
+
+- `use-after-consume` — a binder is referenced after a previous
+  reference already consumed it. Replacement: `(clone <n>)` at
+  the *earlier* site, so the later site stays the unique
+  consume.
+
+- `consume-while-borrowed` — a binder is consumed while a borrow
+  of it is still live (a sibling subterm in the same call passed
+  it to a `Borrow` param earlier; or, for a `Borrow` parameter
+  of the enclosing fn, the caller's outer borrow is always live
+  for the body's whole duration). Replacement: `(clone <n>)` at
+  the offending consume site.
+
+### Position model
+
+Each `Term::Var` occurrence is in either `Consume` or `Borrow`
+position, computed from its parent term:
+
+- `App.callee` → Consume.
+- `App.args[i]` → Borrow if the resolved callee type's
+  `param_modes[i] == Borrow`; otherwise Consume (Own / Implicit
+  / unknown all default to Consume).
+- `Clone.value` → Borrow (clone reads + bumps RC, doesn't move).
+- `Match.scrutinee` → Borrow.
+- Everything else (`Let.value`, `If.cond`, `Ctor.args[*]`,
+  `Do.args[*]`, `Lam`-captures, …) → Consume.
+
+For `App` whose callee is a fn-typed `Var`: when an arg slot
+takes a *bare* `Term::Var { name }` in Borrow position, we bump
+`borrow_count[name]` *before* evaluating subsequent args, and
+release after the call. So a sibling Consume of the same binder
+within the same call triggers `consume-while-borrowed`.
+
+### `suggested_rewrites`
+
+New `Diagnostic` field, always serialised (`[]` when empty —
+stable JSON shape for `ail check --json` consumers). Currently
+populated only by the linearity codes; everything else emits
+`[]`. Each `SuggestedRewrite` carries a free-form `description`
+and a `replacement` string. The replacement is form-A AILang —
+parseable by `ailang_surface::parse_term`, the new
+single-term entrypoint added in this iter alongside the dual
+`term_to_form_a`. The round-trip is a contract guarded by tests:
+the workspace integration tests parse every emitted replacement
+and panic if any fail.
+
+### Why a new `parse_term` / `term_to_form_a` pair
+
+Parser and printer previously only had whole-`Module`
+entrypoints. The linearity check produces snippet-sized
+suggestions, which forced either (a) ad-hoc string formatting
+inside the check, or (b) a fully-fledged single-term
+parser/printer pair. Choice (b) is right because the
+`replacement` field is part of the diagnostic's *contract* — if
+any future code path produces a string that the surface refuses
+to parse, the round-trip test catches it before it ships.
+
+The pair is now public surface API of `ailang-surface` and is
+the canonical way for any tool to produce form-A snippets that
+round-trip cleanly.
+
+### Why gate on clean-typecheck before running
+
+`check_workspace` skips the linearity pass on any module that
+already produced a typecheck diagnostic. Running on a partly-
+defined IR (unresolved `Var` lookups, mismatched ctor arities)
+would produce noise that competes with the upstream errors the
+author actually has to fix first. Cleanly-typechecked modules
+with at least one all-explicit fn are the surface this check is
+designed to inspect.
+
+### Known false negatives (deferred to 18c.3)
+
+- **Missing-consume-of-Own.** An `Own` param matched by
+  `Term::Match` but never moved out of the body is not flagged.
+  Matching is a Borrow-position read by the position model;
+  catching "you declared `own`, you have to consume" requires a
+  must-consume analysis that the assignment kept out of scope.
+  18c.3 will see it because uniqueness inference computes a
+  per-binder must-be-consumed bit anyway.
+
+- **Lam captures conservatively in Consume.** A `Term::Lam` body
+  is walked with each capture in Consume position; we don't
+  model "the closure borrows its capture for the closure's
+  lifetime". For 18c.2 this means closures over an explicit-mode
+  param effectively consume the param at the lam site, which
+  matches the conservative thing to flag if anyone tries to use
+  the param after closing over it. Full closure-borrow
+  discipline is 18c.3.
+
+- **Pattern bindings start fresh.** `Match` arm patterns bind
+  fresh names with default state; we don't propagate ownership
+  from the scrutinee into the pattern bindings. False positives
+  could only arise if a pattern re-binds a name already in scope
+  in the enclosing all-explicit fn — none in shipping fixtures.
+
+These three are deliberate scope cuts, not bugs. 18c.3's
+uniqueness inference subsumes the first two by construction; the
+third is rare enough that an explicit shadow-warning isn't worth
+the schema cost.
+
+### Tests
+
+- `crates/ailang-check/src/linearity.rs` — 3 unit tests
+  (`explicit_fn_with_no_uses_is_clean`, `implicit_fn_is_exempt`,
+  `mixed_implicit_explicit_is_exempt`).
+- `crates/ailang-check/tests/workspace.rs` — 3 integration tests
+  (`use_after_consume_on_own_param_is_reported`,
+  `consume_while_borrowed_in_sibling_arg_is_reported`,
+  `borrow_own_demo_is_linearity_clean`). Each negative test
+  asserts diagnostic kind, def, `ctx.binder`, AND that every
+  emitted `replacement` parses via `parse_term` (the contract
+  test).
+- 1 unit test for `suggested_rewrites` JSON serialisation in
+  `diagnostic.rs`.
+
+`cargo build --workspace` clean, `cargo test --workspace` green.
+E2E unchanged (52 → 52); ailang-check unit 34 → 38; ailang-check
+integration 5 → 8.
+
+### Next
+
+Iter 18c.3: uniqueness inference + codegen `inc`/`dec`
+emission. A dataflow over the AST computes, per binder, the
+"unique" / "shared" status; codegen under `--alloc=rc` emits
+`ailang_rc_inc` / `ailang_rc_dec` calls at the appropriate
+seams (most notably: a single `inc` for every `Term::Clone`
+inserted by 18c.2's suggested rewrites, and a `dec` at the last
+use of each binder leaving scope). This is the iter where RC
+actually starts collecting memory; 18b's leak-everything
+behaviour ends here.
+
+The check from 18c.2 stays as the *user-visible* enforcement
+surface; 18c.3's inference is internal codegen-side bookkeeping.
+The two layers communicate only through the explicit
+`Term::Clone` markers in the source — the linearity check
+demands them, the codegen pass honours them.