Phase 1 / D6: human-readable error messages (proof/checker failure → "resource X used twice at line N")

[hyperpolymath]

Deliverable 6 of #49. A translation layer from Idris2 proof failures / verifier rejections to actionable, line-anchored messages. The Idris2 type errors surfaced today are unintelligible to non-proof-language users.

Scope

• Map each violation class to a human message carrying a .twasm source span:
  • L7–L10 (aliasing / effects / lifetime / linearity) — e.g. "resource X consumed twice (first at L:C, again at L:C)".
  • L2–L6 (region-binding / type-compat / null / bounds / result-type).
  • The verifier's own error variants: MissingDependentRegions, UnboundAccess, AccessSiteRegionMismatch, AccessSiteFieldMismatch, AccessSiteOutOfOrder, … (proposal 0002 §"Error variants").
• Reuse what already exists: the checker diagnostics in src/parser/Checker.affine and the // E2E: expect-diagnostic <tag> pragmas exercised by tests/e2e/e2e-driver.mjs are the seed for the source-side half.

Acceptance

• Each example's intentional-violation variant yields a message that names the offending resource/field and a source line.
• A catalog/snapshot test pins the message set.

Dependencies

• Source-side half is partially independent (checker diagnostics exist today).
• Proof/verifier-side half benefits from F + D1 (needs emitted modules to reject).

Deliverable: Phase 1 / deliverable 6 (docs/PRODUCTION-PATH.adoc §Phase 1). Part of #49.

[hyperpolymath]

Increment landed in #142 (merged e323f7c): a translation layer (crates/typed-wasm-codegen/src/errors.rs) now maps the verifier's index-keyed rejections — L7/L10 ownership, L10 cross-module, L2 access-site — into actionable, function-name-anchored messages, e.g.:

linearity (L10): in despawn_particle, the own resource parameter #0 is used 2 times — an owned resource must be consumed exactly once (this duplicates / double-frees it).

tw build now self-verifies its own output and surfaces these on any violation (the Phase-2 gate's "an error message they can act on"). Tested in crates/typed-wasm-codegen/tests/errors.rs.

Remaining for this issue: anchoring to a .twasm source line ("…at line N"). That needs source spans from the front-end → IR seam (#127) — the IR is hand-built today and carries no line/column. Keeping this open for the line-anchoring step.

---

Generated by Claude Code