[Task 54] Type checker: handler typing + E0220 one-shot linearity#20
Conversation
Plan B Task 54 — full handler typing (effect registry, op-arm env extension, body-row extension, cross-arm overall-type unification) plus the one-shot linearity check (E0220). Per Task 53 review item 11 (preferred option), E0133 / E0134 stay live as the staged-feature gates so well-formed effect / handle programs cannot reach the CPS-pending codegen path until Task 55 lands the lowering. - Effect registry: Tc.effects: BTreeMap<String, EffectDecl> built in the top-level pre-pass; exposed via CheckedProgram.effects for Task 55. Duplicate effect names emit E0136; duplicate ops within an effect emit E0137. First declaration wins (mirrors A3 type / ctor pre-pass convention). - check_perform: non-IO dispatch through the registry; param / return tys resolve under the effect's generic substitution; arg unification through unify_ty (E0042 / E0043 / E0044). IO branch unchanged (Task 57's job). - check_handle: three-phase walk — dispatch table (E0138 / E0139 / E0140 / E0141 + per-handle effect substitution cache); body walk under extended row pushed against handler_scopes stack so body's perform sites share the handler's substitution; arm walks with snapshot/restore env scope, fresh handler-overall type variable, cross-arm unification, and one-shot linearity check. Task 53 review item 10 closed: arm-param + k + return-arm bindings are installed before walking arm bodies, even when registry lookup failed (Ty::Unit fallback) so structural diagnostics surface alongside the registry diagnostic. - E0220: count_continuation_uses helper. Path-max syntactic counting (sum on sequential composition; max on if / match / nested handle arms; lambda-body capture saturates to 2 unconditionally). Lexical shadowing in patterns / nested handle arm k_names / let stmts suspends counting. Multi-shot arms (resumes: many) skip the check. See [DEVIATION Task 54] for the path-max vs path-uniform interpretation choice and the conservative-lambda rationale. - Catalog: E0136 / E0137 / E0138 / E0139 / E0140 / E0141 / E0220 added with full long-form text + fix examples. - Tests: 30 new typecheck unit tests (registry diagnostics, env extension regressions, handler overall-type, body-row extension, perform-via-registry, full E0220 matrix including direct unit tests on the counter helper). 376 → 410 compiler lib tests. All prior Task 53 staged-stub tests still pass under the new internal typing path. Codegen: unchanged. The Item::Effect → return true short-circuit in contains_apply_or_generic_ref and the Expr::Handle => unreachable! arms in lower_expr / type_of_expr stay in place; E0133 + E0134 prevent any well-formed program from reaching them, so the unreachable!s never fire. Task 55's PR lifts both gates and replaces the unreachable!s with the CPS expansion in a single focused change. PLAN_B_DEVIATIONS.md gains two entries before this commit (per plan's commit discipline): "E0133 / E0134 staged-feature gates remain live through Task 54" (codegen-gate alignment with Task 55) and "One-shot linearity check uses path-max syntactic counting; lambda capture is conservative" (algorithm choice + interpretation rationale). PLAN_B_PROGRESS.md flips Task 51 / 52 / 53 done-pending-ci → done with squash-merge hashes and adds Task 54 done-pending-ci [HEAD]. Pod-verify clean.
Code Review — Task 54 handler typing + E0220High-quality PR overall. Three-phase walk is well-isolated, cascade prevention via Please address the following before merging. Bugs / correctness1. Body row sorted alphabetically drops insertion order. body_row.sort();
body_row.dedup();Rows are treated as sets via 2. 3. 4. Continuation Test coverage gaps5. No test for nested handles (E0220 propagation through 6. No test for 7. No test for the Style / nits8. EffectDecl cloned per Strengths worth keeping
|
Review — context-aware passVerdict: merge-with-fixes. Mechanical sweep clean, substantive design correct including handler-partial-discharge. Two must-fix items are documentation honesty (PR body and DEVIATIONS.md make claims that don't match what's on disk); three follow-ups for hygiene/test coverage. Per-task
Mechanical (all green)
Handler exhaustiveness — resolved as non-issueThe pre-registered Stage 6 worry list flagged this as the highest-stakes item. Resolved cleanly: design doc Forward concern for Task 56's design: Substantive findings (clean)Cross-checked the substantive correctness items against
Must-fix before merge1. PR body falsely claims the no-E0001 sweep was extended for the 7 new codes. PR body says "376 → 410 compiler lib tests overall (+34: 30 new tests + 4 from the catalog discipline test now covering the 7 new error codes)." The 2. PLAN_B_DEVIATIONS.md cites a Follow-up (Task 55 PR or small follow-up commit)
Deferred (correctly)
RegressionsNone. All prior 376 tests still pass; new total 410/410. Once items 1 and 2 land, this is ready to merge. Items 3-5 should be noted in |
|
Promoting all follow-up items to must-fix. The marginal cost of landing the three test additions now is lower than letting them slip across the PR boundary, and they each close a real coverage gap on load-bearing mechanism (sequential-sum counting, cross-arm Combined must-fix list for this PR
|
Addresses all must-fix items from PR #20's review (the consolidated list in the third review comment, plus the now-low-cost items from the first review that close real coverage gaps): Must-fix (review comment 3): 1. **No-E0001 sweep extension.** Added 7 new programs to `no_user_facing_error_uses_e0001` covering each of the new user-facing codes (E0136-E0141 + E0220) so the discipline rule "no user-facing diagnostic uses E0001" actually covers all reachable diagnostics from this PR. 2. **`linearity_shadowed_k_does_not_count` test.** New direct unit test on `count_continuation_uses` exercising `count_in_block`'s `Stmt::Let`-shadow suspension logic (block: `let k = 1; k + k` should return 0). The full-pipeline equivalent (a `let k = 5` inside a handler arm body whose arm declares `k`) trips the typechecker's `env_insert` debug-assert against shadowing, so the direct unit test exercises the linearity-counter logic without coupling to that env-side invariant. The DEVIATIONS entry's coverage list now matches what's on disk. 3. **`linearity_count_in_block_sums_uses` direct counter test.** Closes the sequential-sum gap in the direct-counter unit-test matrix: `Block { stmts: [Stmt::Expr(k), Stmt::Expr(k)] }` -> count = 2 (saturates). 4. **Cross-arm `effect State[A]` generic-param consistency test (`cross_arm_state_generic_param_consistency_fires_e0044`).** Pins the load-bearing `effect_substs` cache mechanism for generic effects. `State.get(k) => k(42)` pins `A = Int`; the sibling arm `State.set(v, k) => use_str(v)` therefore sees `v: Int` and fires E0044 because `use_str` expects `String`. If the cache were broken (per-arm fresh `Ty::Var` for `A`), the program would silently typecheck — that would be a soundness regression. Test asserts E0044 fires. 5. **`handle_arm_k_call_with_wrong_arg_is_e0044`.** Locks down `k`'s binding type at the arm env-extension site. `k` is typed as `Fn(op_ret_ty) -> handler_overall ![caller_row]`; calling with the wrong arg type fires E0044 via the normal call-site arg unification. Bonus (review comment 1): 6. **Dropped redundant `body_row.sort()` / `dedup()`.** The contains-check above the loop already prevents duplicates from appearing in the new tail entries; the surface row is dedup'd by the parser. Sort had no semantic value. 7. **IO arity-mismatch recovery comment.** Documents why the IO branch returns `Some(Ty::Unit)` (it matches `IO.println`'s actual declared return type, and Task 57's IO-into-registry refactor will collapse both branches into the same `op_ret_ty`-driven recovery shape). 8. **`handler_overall` unsolved-var TODO note.** Task 55 needs to decide before lifting E0134: pin the unsolved var via the body's perform-call return type's constraint chain, or surface a clearer "cannot infer handler return type" diagnostic (E0132-style ambiguous polymorphism). Today the gate fires first so this case is unreachable in user-visible output. 9. **Nested-handle linearity test (`linearity_nested_handle_inner_arm_shadow_does_not_count_outer_k`).** Exercises the `Expr::Handle` case in `count_in_expr` (walk body, skip arms that re-bind `k_name`) — previously implemented but unexercised. Tests that an inner handle's arm rebinding `k` shadows the outer continuation for linearity purposes. Test deltas: 410 -> 415 compiler lib tests (+5 new). All prior tests still pass; pod-verify clean.
|
Review-fixup pushed at Must-fix items (review comment 3)
Comment 1 items
Comment 1 deferrals (style nits)
Test deltas
Pod-verifyClean on CI polling on the new push. Forward-looking concern from comment 2 (Task 56's runtime semantics for "handler frame for E exists but has no arm for E.unhandled_op") noted for inclusion in Task 56's PR description — not a Task 54 bug, design point that needs an explicit decision when the runtime walk lands. |
Re-review — mergeSpot-check confirms all directives from both review comments addressed; CI green on all 4 lanes at Comment 3 (consolidated must-fix list)
Comment 1 (no-context reviewer)
Mechanical / CI
Merge. Squash-merge SHA lands in |
Implements Plan B Task 54 — full handler typing for
handle ... with { ... }plus the one-shot linearity check (E0220). Per Task 53's PR #19 review item 11 (preferred option),E0133andE0134stay live as the staged-feature gates so well-formed effect / handle programs cannot reach the still-CPS-pending codegen path until Task 55 lands the lowering.Plan reference:
in-progress/2026-04-21-sigil-effects.mdTask 54.What landed
Effect registry
Tc.effects: BTreeMap<String, EffectDecl>populated in the top-level pre-pass; exposed viaCheckedProgram.effectsso Task 55's CPS transform can look up operation signatures without re-scanning the program.check_performregistry dispatchperformsites now dispatch throughTc.effects. Parameter and return types resolve under the effect's generic substitution; arg unification routes throughunify_tyso HM inference flows correctly. The IO branch is unchanged — Task 57 refactors it into the registry.Option<Ty>return type (was());Stmt::PerformandExpr::Performcall sites updated.![Foo]plus aperform Foo.bar(...)lands a diagnostic pointing at the missing decl rather than silent acceptance.Expr::Handletypecheck arm — full handler typingReplaces the Task 53 staged-stub walker with
check_handle, a three-phase walk:body_row = caller_row ∪ discharged_effects. Pushed against aTc.handler_scopesstack soperform Effect.op(...)sites inside the body share the handle's substitution.kbindings into a snapshot/restore env scope (caller-row scope, since discharged effects are NOT in scope inside arm bodies). Arm body unifies with a fresh handler-overall var; the body's type (or the optionalreturn(v) => ...arm's body) flows in too. One-shot linearity check (E0220) runs on cleanly-resolved arms.Task 53 review item 10 closed: even arms whose registry lookup failed get
Ty::Unit-fallback bindings + walked bodies so structural diagnostics inside the arm surface alongside the registry diagnostic instead of cascading intoE0046s on the params /kreferences.One-shot linearity check (E0220)
count_continuation_uses(expr, k_name)helper: path-max syntactic counting. Branching constructs (if,match, nestedhandlearm bodies) take the max across branches; sequential composition (block stmts, binary ops, call args) takes the sum; both saturate at 2 (the > 1 vs <= 1 distinction is what the linearity rule needs).kfrom inside alambdabody saturates to 2 immediately. A lambda's call frequency is not statically known — capturingkinto a closure could invoke it any number of times.k_names/letstmts suspends counting.effect E resumes: many) skip the check.See
[DEVIATION Task 54] One-shot linearity check uses path-max syntactic counting; lambda capture is conservativefor the path-max vs path-uniform interpretation choice and the conservative-lambda rationale.Codegen-gate alignment with Task 55 (Task 53 review item 11)
Codegen unchanged.
Item::Effect → return trueshort-circuit incontains_apply_or_generic_refand theExpr::Handle => unreachable!arms inlower_expr/type_of_exprstay in place; E0133 + E0134 prevent any well-formed effect / handle program from reaching codegen, so theunreachable!s never fire. Task 55's PR lifts both gates and replaces theunreachable!s with the CPS expansion in a single focused change.See
[DEVIATION Task 54] E0133 / E0134 staged-feature gates remain live through Task 54for the rationale and the alternative (extending the codegen walker to short-circuitExpr::Handle) we declined.Tests
35 new typecheck unit tests (30 in the initial commit + 5 added in the review-fixup commit). The catalog gains 7 entries (E0136 through E0141 + E0220), each covered by a dedicated user-reachable program in the
no_user_facing_error_uses_e0001discipline sweep.duplicate_effect_decl_is_e0136,duplicate_op_in_effect_decl_is_e0137,handle_unknown_effect_arm_is_e0138,handle_unknown_op_on_known_effect_is_e0139,duplicate_handle_arm_is_e0140,handle_arm_arity_mismatch_is_e0141.handle_arm_param_bindings_no_spurious_e0046,handle_arm_k_binding_no_spurious_e0046,handle_return_arm_v_binding_no_spurious_e0046,handle_arm_param_typed_from_op_decl,handle_arm_k_call_with_wrong_arg_is_e0044.handle_body_can_perform_discharged_effect,handle_arm_body_perform_of_discharged_effect_fires_e0042.performvia registry:perform_via_registry_typechecks,perform_via_registry_arity_mismatch_is_e0043,perform_via_registry_arg_type_mismatch_is_e0044.cross_arm_state_generic_param_consistency_fires_e0044— pins the load-bearingeffect_substscache mechanism foreffect State[A]-style effects.linearity_zero_uses_is_fine,linearity_one_use_is_fine,linearity_two_uses_in_sequence_is_e0220,linearity_branches_use_k_independently_is_fine,linearity_branch_then_extra_use_is_e0220,linearity_lambda_capturing_k_is_e0220,linearity_multi_shot_skips_check,linearity_zero_uses_with_branches_is_fine,linearity_shadowed_k_does_not_count,linearity_nested_handle_inner_arm_shadow_does_not_count_outer_k, plus 5 direct unit tests on the counter helper (count_in_expr_zero_in_lit,count_in_expr_saturates_at_two,count_in_expr_lambda_capture_returns_two,count_in_expr_branches_take_max,count_in_block_sums_uses).handle_overall_type_is_body_type_without_return_arm,handle_overall_type_uses_return_arm_when_present,handle_arm_body_unifies_with_handler_overall.All 5 pre-existing Task 53 staged-stub tests still pass under the new internal typing path. 376 → 415 compiler lib tests (+39 net: 35 new tests + 4 from the catalog discipline ordering).
Pod-verify
Clean:
cargo fmt --check,cargo check --workspace,cargo clippy -p sigil-runtime,cargo clippy -p sigil-compiler,cargo test -p sigil-runtime --lib,scripts/check-no-interior-pointers.sh, all discipline greps.Plan B progress
done(squash hash2ed6628).done(squash hash6305bcb, wasdone-pending-ci [HEAD]).done(squash hash6305bcb, wasdone-pending-ci [HEAD]).done-pending-ci [HEAD](this PR).Stage 6 still in progress: Tasks 55 (CPS transform), 56 (runtime), 57 (IO refactor + Raise[ArithError]), 58 (multi-shot rigor), 59 (catch / state / choose examples), 60 (perf floor), 61 (P18-P20 prompts).
Test plan
cargo test -p sigil-compiler --lib -- --test-threads=1).ubuntu-24.04andmacos-14(build + test, cold-checkout test) at020aa43(initial push).dc8e86a(review-fixup commit).Notes for the reviewer
[HEAD]placeholders with this PR's squash hash.handler_scopesstack is the cross-perform / cross-arm consistency mechanism for generic effects. Non-generic effects (the common case) don't use the cache — every empty subst flows through unchanged. The stack matters foreffect State[A] { get: () -> A, set: (A) -> Unit }style effects so thatperform State.get()in the body andState.set(x, k) => k(())in an arm both reference the same freshA-instantiation. The newcross_arm_state_generic_param_consistency_fires_e0044test pins this mechanism.QUESTIONS.md's open[PLAN-B] Task 54: revisit handler arm surface (qualified-only vs bare-op-as-sugar)entry stays open. Task 54 ergonomic data was thin (we have noTask 59examples yet); revisit at the Stage 6 review checkpoint.