The effect system can now discharge an effect, not only track one

[admercs]

Closes the last substantive item on HANDOFF.md's "found and left alone" list: "Effects can be declared, annotated, inferred, and enforced, but never discharged — the effect system has no elimination rule."

Design chosen deliberately: non-resumable handlers, and custom effects must be declared.

Three parts, because none is useful alone

Introduction. Audit.record(x) performs the operation — checked against the signature in the effect block, and it puts audit in the calling function's effect set.

Before this it typechecked as an unknown method returning a fresh variable, accepted any arguments, and died at run time with unknown function `record` . That is the same typechecks-then-does-not-evaluate shape as five earlier bugs this week. An effect block declared operations nothing ever read.

Elimination. handle { body } with Audit { record(e) => … } removes the effect from the block it wraps:

f transcribe(entry: String) -> usize / audit { Audit.record(entry) }

fn summarize_audit(entry: String) -> String {     // pure!
    val n = handle { transcribe(entry) } with Audit { record(e) => len(chars(e)) }
    f"recorded {n} chars"
}

--check reports f transcribe: { audit } and f summarize_audit: pure.

The subtraction is per block, not per function. Calls inside a handled block go into their own bucket, are resolved, and are discharged separately — so an unhandled call sitting beside a handled one still reports. Deleting the effect from the whole function would have been simpler and unsound; there's a test for exactly that.

What the arm itself does is attributed honestly: handling audit by writing a file makes the handling function / fs. A handler exchanges one effect for the effects of handling it, and says so.

Declaration. An effect annotation naming nothing is now an error. / nte used to be accepted as a different effect from / net — enforced perfectly consistently and matching nothing, so a typo invented an effect instead of failing.

What this deliberately is not

Handlers do not resume. An operation dispatches to its arm and returns like an ordinary call, which is what a tree-walking evaluator can do without capturing continuations. resume — and with it generators, backtracking, and async from one mechanism — is the natural next step and is not here.

Handlers are found dynamically (innermost wins) and evaluated lexically (the arm sees the scope the handler was written in). Both are tested, as is the stack discipline that stops a handler outliving its block.

Migration

Surveyed by running the checker over every .mg in the repository rather than guessing at the blast radius. Exactly one file needed a change: effects-showcase gains effect Db {}. It also now demonstrates all three parts, and drops two header claims that are no longer true — including "Not shown, because it does not exist yet: effect handlers."

check-examples.sh caught the example's changed output and refused to bless it silently, which is what that pin is for; the new line is the handle demonstration and the expected answer was updated deliberately.

Verification

• cargo test --release: 1,106, 0 failures. 12 new tests — introduction, elimination, the per-block soundness property, handler-effect attribution, unknown-effect rejection, plus runtime dispatch, innermost-wins, lexical scope, and stack discipline.
• scripts/check-examples.sh green — all 12 typecheck, run, and print their recorded answers.
• scripts/test-all.sh --check-docs green; 45 documented counts match the run.
• 0 clippy warnings across the four owned crates.

Counts move with the suite: prototype 1,094 → 1,106, total 2,802 → 2,814.

🤖 Generated with Claude Code

[admercs]

Found and fixed a bug in this PR before merging it: Audit.recrod(x) — a misspelled operation name — typechecked clean and died at run time with unknown function.

The effect analysis attributes an effect from the receiver alone, so the misspelling was counted as genuinely performing audit, satisfied the annotation, and passed every check. That is the exact bug class this feature was built to eliminate, written into the first version of the feature.

Now checked against the declarations, with the diagnostic naming what does exist:

error: effect `Audit` declares no operation `recrod` (it declares: record)

Counts: prototype 1,106 → 1,107, total 2,814 → 2,815. Re-verified: examples green, --check-docs green at 45 counts, 0 clippy.