v0.0.188

Added

• Diagnostic-field discipline is now enforced (#682). spec/00-introduction.md §0.5.1 requires every diagnostic to carry a rationale, a fix, and a spec_ref, but the Diagnostic dataclass defaults all three to "" — so a partially-tagged diagnostic compiled and shipped silently, weakening the "diagnostics as instructions" guarantee (DESIGN.md §Checkability). New scripts/check_diagnostic_fields.py (wired into pre-commit and the CI lint job, mirroring the #597 walker-coverage gate) AST-parses every Diagnostic(...) constructor and self._error(...) / self._warning(...) call under vera/ and fails when one of the three fields is missing — or when a present spec_ref does not resolve to a real spec section/chapter with a matching title (the present-but-wrong case, e.g. citing §4.3 "Operators" when §4.3 is "Slot References"). The exemption surface is explicit and reasoned, never silently inferred (DESIGN.md §"Explicitness over convenience"): a warning is not required to carry a fix (it has no corrected-code template); the codegen _error/_warning helpers — internal-compiler (E699) and "function skipped" diagnostics with no user fix or spec section — are exempt via a documented registry in the script; and a one-off internal/defensive site carries a # diag-fields-exempt: <reason> marker (a dedicated token, deliberately not # noqa:-prefixed so it cannot collide with ruff's suppression namespace). A cheap emission-side check also requires every literal error_code under vera/ to be registered in ERROR_CODES (catching typos / unregistered codes); enforcing each code's uniqueness per concept and its presence is tracked in #828. The pre-commit hook also triggers on spec/**/*.md (not only vera/**/*.py), since the validity pass reads the spec section/chapter titles — a spec-only retitle can invalidate an otherwise-unchanged citation, and now re-runs the check locally rather than only in CI.

Fixed

• Corrected the pre-existing wrong spec_ref citations and documented typed holes (#682). The adversarial audit behind the new validity gate found 30-plus diagnostics across the checker, the parser-error factories, the codegen path, and the verifier whose spec_ref cited the wrong section number or title (e.g. all arithmetic/comparison/logical operator errors cited §4.3 "Operators", but §4.3 is "Slot References" — arithmetic is §4.4, comparison §4.5, logical §4.6) — a misleading instruction is worse than a missing one. Every spec_ref under vera/ now resolves. Typed holes (?) had no spec section at all — W001 (and the codegen E614) cited a fabricated §3.10 "Typed Holes" — so they are now documented in a new spec/04-expressions.md §4.17 "Typed Holes", which both diagnostics cite. Two further citations resolved to a real but semantically wrong section (which the validity gate, checking only that a ref resolves with a matching title, accepts — so they needed reviewer judgment): the unresolved-qualified-call warning E220 cited §7.4.1 "Ambiguous Operations" (the multi-match case) but the error is an unresolved op, so it now cites §7.4 "Performing Effects"; and the type-alias-cycle error E132 cited the unrelated slot-namespace section §3.8 "Type Alias and Reference Resolution" — the rule it actually enforces ("an alias must resolve to a concrete type; the alias chain must be acyclic") had no spec home, so a sentence stating it was added to spec/02-types.md §2.6.3, which E132 now cites. Two fix templates were also corrected for machine-actionability: the unresolved-bare-call diagnostics (E200 and the codegen cross-module backstop) replaced a literal-looking import the.module(f) placeholder with import <module>(f) plus a "replace <module> with that module's path" hint; and the ADT-invariant error (E120) — whose old fix suggested invariant(@Field.0 > 0), a form that cannot resolve (@Field is not a type, and data invariants are NYI, #686) — now points at the documented refinement-type workaround (type Positive = { @Int | @Int.0 > 0 };). Finally, the missing-contract-block error E001 moved from §5.4 "Contract Clauses" (which states the requires/ensures rule but not the effects one) to §5.2 "Function Declaration Syntax" — the one section that shows the complete mandatory block, matching the diagnostic's own fix and the sibling function-structure errors (E1xx in the checker) that already cite it; its three rendered mirrors (README.md, docs/index.html, spec/00-introduction.md) moved in lockstep, pinned by the TestErrorDisplaySync suite.

• Four error_code collisions corrected (#682 review + audit). Each of E130/E210/E320/E600 was shared by two unrelated diagnostics, so a --json consumer keying on error_code would mislabel one of each pair: the slot-resolution E130 (expressions.py) was reused by the "Decimal takes no type arguments" type-application error (resolution.py), now E134 "Type does not take type arguments"; the unknown-constructor E210 (calls.py) by the empty-Tuple() error, now E216 "Empty tuple type"; the unknown-constructor-in-pattern E320 (control.py) by the empty-tuple-pattern error, now E323 "Empty tuple pattern"; and the "unsupported parameter type" E600 (functions.py) by codegen's "refinement base resolves to another refinement" error (contracts.py), now E618 "Nested refinement base unsupported". Each stable code now maps to exactly one diagnostic concept; the new codes are registered in ERROR_CODES, and the three reachable ones (E134, E216, E618) are pinned by collision-regression tests (E323's site is parser-unreachable).

• Five further semantically-wrong spec_refs corrected (exhaustive audit) (#682). A final multi-agent audit of every diagnostic — each finding adversarially verified — caught five more of the resolves-but-wrong-section class the validity gate cannot detect (it checks resolution, not appropriateness): E122 (pure violation) and E002 (missing effects()) cited effect-chapter sections describing how effects work, not the rules they enforce, and now both cite §5.5 "Effect Declaration", which states "Every function MUST declare its effects" and "A function that declares effects(pure) MUST NOT perform any effects" verbatim; the alias-arity error E133 cited the slot-namespace §3.8 and moved to §2.6.3 alongside E132; the @Int→@Nat narrowing obligation E503 cited §4.7 "Let Bindings" (it fires far beyond let) and now cites §2.2.1 "Int and Nat compatibility", where the obligation is stated; and the contract-testing skip warning E701 moved from the chapter-level Chapter 6, "Contracts" to the dedicated §0.5.6 "Contract-Driven Testing".

• spec/04-expressions.md §4.17 "Typed Holes" gains a worked example (#682). The section now shows ? in context (@Int.0 + ?), demonstrating it is inferred to type @Int, type-checks with W001, and is rejected at compile with E614. Validating it exposed that scripts/check_spec_examples.py's check and verify stages treated warning-severity diagnostics as failures (unlike the CLI vera check, and unlike the verify stage's own error-only filter one line later) — both stages now filter to error severity, so a legitimately-checkable warning-emitting example is validated rather than mis-failed.

Changed

• Backfilled 54 under-tagged checker diagnostics (#682). Every self._error(...) site in vera/checker/ (calls, control, expressions, core, resolution) — plus partial direct Diagnostic(...) constructions in the parser-error factories, the tester, the monomorphizer, and the verifier's obligation-fallback — now carries a concrete rationale, a fix template, and a spec_ref. The canonical example from the issue, vera check on a function mixing @Bool.0 + @Int.0 (E140), now emits a Fix: paragraph instead of stopping at the rationale; pinned by tests/test_checker.py::TestErrorCodes::test_E140_carries_a_fix_paragraph_682.

• The TestHostHandleReclamation573 GC-reclamation suite is marked stress (#738). The class compiles and runs full reclamation programs at scale (~minutes locally), so it is now deselected from the default per-PR pytest run and runs under pytest -m stress (and nightly CI), reclaiming local inner-loop time.

• CI hardening — CodeRabbit Pro+ configuration (no compiler or runtime change). .coderabbit.yaml gains three agentic pre-merge checks — changelog covers public-surface changes, spec and implementation move together, and diagnostics carry full metadata — all in warning (advisory) mode, so they surface drift during review without blocking merge. The deterministic floor (mypy, scripts/check_*.py, pre-commit, the conformance suite) remains the only hard gate; these checks complement it and target judgment-gaps it cannot cheaply cover (e.g. "the changelog describes the change", not merely "a bullet exists"). Also raised the GitHub-Checks ingestion timeout to 15 min so CodeRabbit waits for the full multi-OS test matrix before commenting; added AGENTS.md to the Code Guidelines set; linked aallan/vera-bench so a downstream-breaking CLI / exit-code / diagnostic-format change here is flagged during review; and extended the tests/** review guidance to call out the commutative-operations slot-ordering trap. The deterministic counterpart for asserts — ruff flake8-bandit for assert-as-guard (#657) — is tracked as a follow-up; the diagnostic-metadata gate (#682) landed later in this same [Unreleased] cycle (see above), deterministically gating the rationale/fix/spec_ref fields; its interim advisory check was correspondingly narrowed to "Diagnostics carry an error code".