Bound vera/addEffect propagation at handlers (#725) - #1259
Conversation
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
📝 WalkthroughWalkthroughThe LSP workflow now stops ChangesHandler-aware effect propagation
Estimated code review effort: 3 (Moderate) | ~20 minutes Sequence Diagram(s)sequenceDiagram
participant add_effect
participant transitive_callers
participant handler_filter
participant effect_rows
add_effect->>transitive_callers: Analyse callers for the requested effect
transitive_callers->>handler_filter: Inspect call sites and handler scopes
handler_filter-->>transitive_callers: Exclude matching handled calls
transitive_callers-->>add_effect: Return callers that still require the effect
add_effect->>effect_rows: Rewrite required top-level effect rows
Possibly related issues
Possibly related PRs
Suggested labels: 🚥 Pre-merge checks | ✅ 7 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (7 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1259 +/- ##
=======================================
Coverage 94.05% 94.06%
=======================================
Files 100 100
Lines 35810 35829 +19
Branches 458 458
=======================================
+ Hits 33682 33701 +19
Misses 2115 2115
Partials 13 13
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 5
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@tests/test_lsp.py`:
- Around line 1049-1066: Add a bare-effect handler fixture alongside
HANDLER_EDGES, using handle[IO] around a call to target, and add a test for
transitive_callers that verifies an IO propagation is bounded while Async still
reaches io_handled. This should exercise the no-type-argument path in
_handled_effect_key and preserve the existing target-only and transitive caller
expectations.
- Around line 1153-1158: Add regression coverage in tests around
transitive_callers: add a whitespace-normalization test using _program(HANDLERS)
and request "State< Int >", then add nested-handler fixtures/tests covering both
a matching handler inside a foreign handler and a foreign handler inside a
matching handler, asserting the matching case prunes while the foreign nested
case does not un-prune.
In `@vera/lsp/workflows.py`:
- Around line 366-375: Update the effect-instance key construction around the
rendered argument loop to detect refinement arguments before calling
format_type_expr and return an unmatchable key when any argument is a
RefinementType. Preserve existing rendering for non-refined arguments, while
ensuring refined effect instances are not collapsed into their base types.
In `@vera/README.md`:
- Line 124: Update the workflows.py code span in the README table to remove
spaces inside the backticks while preserving the surrounding table-cell padding.
- Line 124: Update the README table entry for workflows.py to document the
current 547-line count instead of 502, leaving the surrounding description
unchanged.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 30f4b991-0ebd-404e-b5bf-e91341d986cb
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (10)
CHANGELOG.mdFAQ.mdKNOWN_ISSUES.mdLSP_SERVER.mdREADME.mdROADMAP.mdTESTING.mdtests/test_lsp.pyvera/README.mdvera/lsp/workflows.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
💤 Files with no reviewable changes (1)
- KNOWN_ISSUES.md
7f23559 to
e0b4d84
Compare
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@TESTING.md`:
- Line 173: Escape both literal pipe characters in the inline refinement
examples within the test_lsp.py table row, changing the predicates in Exn<{ `@Int`
| p }> and Exn<Array<{ `@Int` | p }>> to use Markdown-safe escaped pipes while
preserving the surrounding examples.
In `@tests/test_lsp.py`:
- Around line 1212-1217: Extend test_mismatched_type_argument_keeps_the_edge
with a positive-control assertion using the State<Nat> handler fixture,
verifying that a matching State<Nat> request is pruned and does not retain the
caller edge. Keep the existing State<Int> mismatch assertion unchanged so the
test covers both matching and non-matching behavior.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: e8da27f1-a830-41e8-86fa-7cddbffa2861
⛔ Files ignored due to path filters (1)
docs/llms-full.txtis excluded by!docs/**
📒 Files selected for processing (7)
FAQ.mdREADME.mdROADMAP.mdTESTING.mdtests/test_lsp.pyvera/README.mdvera/lsp/workflows.py
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
e0b4d84 to
4c370c2
Compare
|
Thanks — and the body's reachability analysis (the |
4c370c2 to
8bfada7
Compare
|
Tip For best results, initiate chat on the files or code changes.
Keeping the scope to the new test is correct. The pre-existing Reverting the ✏️ Learnings added
You are interacting with an AI system. |
8f58918 to
337d580
Compare
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
KNOWN_ISSUES.md (1)
44-45: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winUpdate issue
#725before removing this row.Issue
#725remains open, although this change implements the fix. Add a closing reference; otherwise retain the row until the issue is closed.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@KNOWN_ISSUES.md` around lines 44 - 45, Update the affected KNOWN_ISSUES entry to reference issue `#725` as the closing issue for the implemented fix; retain the existing row and its current issue reference until the original issue is closed.Source: Path instructions
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@KNOWN_ISSUES.md`:
- Around line 44-45: Update the affected KNOWN_ISSUES entry to reference issue
`#725` as the closing issue for the implemented fix; retain the existing row and
its current issue reference until the original issue is closed.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: ce550d90-12fb-43c4-8c0b-c8cd5fa7c4df
📒 Files selected for processing (1)
KNOWN_ISSUES.md
🔗 Linked repositories identified
CodeRabbit considers these linked repositories for cross-repo context during reviews:
aallan/vera-bench(manual)
|
@aallan You were right that the release merge was the risk, so I trial-rebased onto |
337d580 to
633b16d
Compare
|
Review round complete; the branch carries the contributor's commit (rebased onto post-v0.1.10 Fitness verdict: ACCEPT — no DESIGN violation. The pruning boundary was verified as the compiler's own discharge boundary by execution (a call in a handler's state initialiser fails E125 under a
Gates green across the board (10,330 counted tests / 213 conformance / limitation sync at 2 LSP rows). Remaining before merge: the CI wall on this push and the CodeRabbit pass at this head; merge order stays behind #1279 and #1262 per the queue. |
|
@coderabbitai On the outside-diff finding for |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
echo '--- CLAUDE.md convention ---'
if [ -f CLAUDE.md ]; then
rg -n -i -C 4 'KNOWN_ISSUES|close[sd]?|issue' CLAUDE.md
else
echo 'CLAUDE.md not present at repository root'
fi
echo '--- KNOWN_ISSUES.md issue 725 context ---'
rg -n -C 3 '`#725`|725|addEffect|add_effect' KNOWN_ISSUES.md || true
echo '--- PR `#1259` closing references ---'
gh pr view 1259 --repo aallan/vera --json closingIssuesReferences \
--jq '.closingIssuesReferences[] | {number, title, url, state}'Length of output: 7776
The restored I withdraw the outside-diff finding. 🧠 Learnings usedYou are interacting with an AI system. |
Adversarial review record — PR #1259 (four-lens fitness protocol, 2026-08-13)Reviewed at Fitness verdict
The three fixes
Soundness probes beyond the centerpiece (each run, not reasoned)Nested handlers both orders — pruned correctly, including a call in an inner foreign handler's clause inside an outer matching handler's body (the clause runs in the enclosing context, §7.5.2, executably confirmed by the conformance corpus). Clause bodies calling effectful functions — edge kept, matching the checker. Closures — classified exactly as the checker classifies them (an Reviewer: Opus subagent, four-lens fitness protocol, DESIGN veto first. |
The transitive-caller closure was handler-unaware: a caller that
wrapped its call in handle[E] had E appended to its own effects(...)
row even though the handler discharges it there, so the workflow wrote
rows the program does not need and dragged that caller's own callers in
behind it.
A call site inside a handle[E] body now contributes no edge.
transitive_callers takes an optional effect argument (None keeps the
old handler-unaware closure, which the existing goldens still pin), and
_unhandled_callee_names subtracts the handled sub-tree from
direct_callee_names.
Two cases deliberately still propagate, because the effect really does
escape them: a caller that reaches the callee on any unhandled path as
well, and a call in a handler clause body, which runs outside its own
handler. Both are pinned by tests, and reverting either half of the
bound turns the matching test red.
Containment is structural rather than span arithmetic - identical
answers where both apply, no special case for a node with no span, and
it reuses the existing walk_nodes walker.
The handler has to name the same effect instance, type arguments and
all. The checker discharges against EffectInstance, whose equality
includes type_args, so handle[State<Nat>] does not discharge
State<Int>: pruning that edge on a base-name match would leave the
caller pure, never write the row it actually needs, and fail the whole
candidate on E125. Only an exact match prunes, and every other outcome
keeps the edge - a surviving edge writes a row the program may not
strictly need, which still type-checks. Row identity is a separate
question and stays the base name, so State<Int> is still not appended
beside an existing State<Bool>. Asking the same fixture for
State<Nat> is the positive control: that handler key does prune, so
the surviving State<Int> edge is attributable to the type argument
and not to a key nothing can match.
A refinement argument is one of those distinct instances, and the
narrowest way to get this wrong: format_type_expr renders
{ @int | p } as its bare base type, so a key built straight from it
spells Exn<Int> for a handler that discharges nothing of Exn<Int>, and
the pruned caller would keep pure while its call site fails E125. Any
argument holding a refinement - nested inside another type argument
included, since the renderer recurses - is spelled unmatchably
instead, so the edge survives. handle[Exn<{ @int | p }>] and
handle[Exn<Array<{ @int | p }>>] both check clean, so both are pinned,
end-to-end as well as at the closure.
The two remaining branches of the key are pinned too: an
unparameterised handle[IO] bounding an IO propagation (IO and Async are
what addEffect propagates most), whitespace-insensitive request
spelling, and handler nesting in both orders - a matching handler
inside a foreign one still bounds, and a foreign one inside a matching
one does not un-bound. handle[Mod.IO] is pinned at the key rather than
through a program: effects are only ever registered under an
unqualified name, so a qualified handler always fails E330 and no
program in which that key could prune ever type-checks.
where-block attribution is unchanged: a helper's bare call still
attributes to its containing top-level function, while a helper that
discharges the effect itself bounds the closure at its parent. Row
rewriting is also unchanged, and still top-level-only - a where helper
that needs the new effect does not get one, and the gate refuses that
candidate rather than applying it half-done.
The KNOWN_ISSUES.md and LSP_SERVER.md limitation rows are retired.
Three review fixes on the handler bound. They share lines in the module docstring and the CHANGELOG bullet, so they land together. The handler's STATE INITIALISER was documented as escaping the bound for the clause rule's reason, and nothing pinned it: patching _unhandled_callee_names to prune h.state as well left the whole suite green. It has its own reason - the initialiser is evaluated in the ENCLOSING scope, before the handler is installed, which is why _check_handle synths state.init_expr before it extends env.current_effect_row and why _translate_handle_state evaluates it before pushing the cell. The docstring now derives the two boundaries separately, and two tests pin them: the closure keeps an edge whose only call site is an initialiser (with a body call under the same handler spelling as the positive control that the key does prune), and the checker raises E125 on that call against a pure caller while the identical call in the handler body is clean. The comparison was documented as instance-for-instance in three places. It is not: format_type_expr does not resolve aliases, so the key compares the handle[...] head's SOURCE SPELLING to the request string, and handle[State<MyAlias>] with type MyAlias = Int does not bound a State<Int> propagation even though the checker discharges it. That under-prunes - the caller keeps a row it does not need, which still type-checks - so it is the safe direction and the key is left alone; aallan#1292 owns the swap onto resolved instances. The module docstring, the transitive_callers docstring and LSP_SERVER.md now say spelling, name the under-prune, and cite aallan#1292, and a test pins both halves on one fixture: the program is error-free (only possible if the alias-spelled handler discharges the State<Int> row its callee declares) and the State<Int> request keeps the edge, with the alias-spelled request as the control that does prune. The retired LSP_SERVER.md limitation row stated two things and only one of them is fixed, so the file boundary comes back as its own row. It carries no issue link, being deliberate behaviour rather than tracked work, with a note above the table saying so. Counts and llms-full.txt are refreshed from their oracles. Co-Authored-By: Claude <noreply@anthropic.invalid>
633b16d to
f628d9f
Compare
2 participants
Fixes #725
Summary
vera/addEffectclosed its transitive-caller set over the raw call graph, so a caller that wrapped its call inhandle[E]still gotEappended to its owneffects(...)row. That row is one the program doesn't need, and it dragged the caller's own callers in behind it.handle[E]body now contributes no edge.transitive_callerstakes an optionaleffectargument; withNoneit is bit-for-bit the old handler-unaware closure, which the existing goldens still pin.walk_nodeswalker.Why full-instance identity, not base names
My first cut compared base names, on the reasoning that this is already the identity
effect_row_rewriteuses. That was wrong: the two halves ask different questions.effect_row_rewriteasks whether a row would be a duplicate, where base names suit. The closure bound asks whether the effect is discharged, and the checker answers that with fullEffectInstanceequality, sohandle[State<Nat>]does not dischargeState<Int>.Base names therefore prune an edge the program needs, the caller keeps
effects(pure), and the candidate dies on E125. On a fixture whose only call site sits insidehandle[State<Nat>]while propagatingState<Int>: handler-unaware gaveapplied=Truewith 0 diagnostics, base-name gaveapplied=Falsewith 1. A working edit became a refused one.Same trap one level down.
ast.format_type_exprrenders aRefinementTypeas its base type, sohandle[Exn<{ @Int | @Int.0 >= 0 }>]andExn<Int>produced identical keys, spelled lossily rather than unspellably. That handler passesvera check, and the collapsed key reproduced E125. Any argument containing a refinement now yields an unmatchable key.Two shapes that deliberately still propagate
bodyis pruned.Test plan
handle[State<Nat>]doesn't pruneState<Int>, but nothing established that handler prunes anything, so an implementation returning an unmatchable key for every parameterised handler would satisfy it. The control pins that a matching instance does prune.test_handler_clause_and_foreign_handler_do_not_boundstopped detecting the wrong prune boundary: its discriminating power had been resting on the base-name bug. Re-pointed at the instance its fixture actually handles.vera verifybefore being embedded, so the assertions rest on verified premises rather than strings that merely parse.mypy vera/,ruff check .,check_limitations_sync.py,check_doc_counts.py,check_site_assets.pygreen. Fullpytest tests/andpre-commit run --all-filesgreen.The
KNOWN_ISSUES.mdandLSP_SERVER.mdlimitation rows and the ROADMAP Tier 3 entry are retired.On the release merge
You flagged that #1232 and #1238 rewrote this machinery, so it wouldn't survive the merge. I ran the rebase rather than guess.
git log --full-history origin/main..origin/release/v0.1.10 -- vera/lsp/workflows.pyis empty and the file is the same blob (bfcfe14024) on both branches: #1232 landed inchecker/{calls,control,core,resolution}.pyandwasm/calls_handlers.py, #1238 innaming.py,codegen/*andtypes.py.Trial-rebased onto
release/v0.1.10: zero code conflicts, only doc counts collide, andtests/test_lsp.pyauto-merges because both sides are non-overlapping additions. On that base, the LSP and obligations suites passed (853 tests on the post-release main after the maintainer-side rebase; the full suite is green there too), mypy clean, all 11 handler-bounding legs green, the refinement E125 case still reproducing, and mutation M4 still taking both refinement tests RED.You were right that the ground moved, and it moved in this PR's favour. #1238 is what made
naming.family_namerender refinements distinguishably (Exn<{Int|@Int.0 >= 0}>instead of collapsing toExn<@Int>), which is a better key than the guard here: mine makes every refinement handler unmatchable, so it under-prunes rather than over-prunes.vera/naming.pydoesn't exist onmain, so it can't be used from this PR, but once v0.1.10 lands it would delete the refinement branch, the sentinel, and_effect_instance_keyoutright. Happy to do that rebase whenever you want it.