fix(checker): reject where-helper bodies reading the outer function's parameter slot (#969)

[aallan]

Summary

Fixes #969: a where-helper body that references the OUTER function's parameter slot passed vera check and vera verify, then hard-failed vera compile with a dangling-slot E699 — the checker checked helper bodies before the parent's scope popped, while the backends compile each helper as an independent param-rooted scope.

Per spec §5 and DESIGN principles 2 and 5, where-helpers are closed, param-rooted scopes: helpers carry their own mandatory contracts over their own params, and an implicit outer-frame capture would move a value across a contract boundary uncontracted (capture semantics already have their one canonical construct — closures). The fix makes the checker agree with the backends:

• vera/checker/core.py: _check_fn pops the parent's value-slot scope before the where-fn loop, so an outer slot read in a helper body becomes a natural E130. Parent forall type params stay in scope through the loop (generic parents still parameterize helpers — ch09_generic_where_helper stays green).

• vera/checker/expressions.py: the E130 fix text steers to the design's canonical alternative when the failing type is one the parent bound (same narrow-gating pattern as Checker binds handler state into the handled body's slot scope; the backends do not — reconcile #973's hint — count == 0, only inside a helper body, masked everywhere else):

  where-helpers are closed, param-rooted scopes (spec §5): the outer function's @Int slot is not in scope here. Pass it as an explicit argument — add a @Int parameter to the helper and pass the value at the call site.

• vera/wasm/operators.py: with both Checker binds handler state into the handled body's slot scope; the backends do not — reconcile #973 (merged) and where-helper body referencing an outer param slot: check+verify green, compile E699 #969 (this PR) sealed at check time, the dangling-slot E699 guard's two known source routes are gone — the inline comment now records that precisely. The guard itself stays as a defensive net (no exhaustive-unreachability claim).

Evidence

• RED first: new negative conformance fixture ch05_where_helper_outer_slot_rejected.vera (level check, expected_error: E130, the 147th program) wrongly passed check pre-fix; the new unit test got no error. Both flip with the fix.
• Mutation-validated per guard: early value-scope pop disabled → rejection test RED; hint gate widened to always-fire → generic-hint test RED; hint-stack pop disabled → sibling-fn leak test RED. __pycache__ purged; 5/5 green on restore.
• Full gate: 6,860 passed (-m "not stress"), mypy clean (97 files), all 147 conformance programs pass at their level, all 37 examples check + verify.
• One accuracy note from validation: keeping parent type params in scope through the loop is preserved behavior but turned out not to be load-bearing for @T resolution — helper @T resolves via the opaque-typevar fallback and monomorphization reads forall vars from the decl. The regression tests pin it regardless.

Docs lockstep (same commit)

• spec §5 states the closed param-rooted scope rule (type params excepted; pass outer values as arguments).
• where-helper body referencing an outer param slot: check+verify green, compile E699 #969 rows deleted from KNOWN_ISSUES.md and SKILL.md (five bugs remain open).
• CHANGELOG [Unreleased] bullet; counts reconciled across every surface (147 conformance, 15 check-level, 9 negative fixtures, 6,953 tests — including TESTING.md's prose enumeration and FAQ's gate-blind total); CLAUDE.md/AGENTS.md fixture lists updated; site assets regenerated.

Closes #969

Summary by CodeRabbit

• Bug Fixes
  • where-helper bodies are now checked in an isolated value-slot scope, so references to outer function parameter value slots are rejected with clearer E130 guidance to pass values explicitly.
• Documentation
  • Updated where-helper scoping details and refreshed conformance/test totals from 146 to 147 programmes across the changelog and supporting docs.
• Tests
  • Added a new chapter 5 conformance case and expanded checker coverage for helper scoping, diagnostics, and hint selection.

[codecov]

Codecov Report

❌ Patch coverage is 92.30769% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 93.41%. Comparing base (935120a) to head (c0b062b).

Files with missing lines	Patch %	Lines
vera/checker/core.py	90.90%	1 Missing ⚠️

Additional details and impacted files

@@               Coverage Diff               @@
##           release/v0.1.4     #977   +/-   ##
===============================================
  Coverage           93.41%   93.41%           
===============================================
  Files                  96       96           
  Lines               31380    31388    +8     
  Branches              456      456           
===============================================
+ Hits                29314    29322    +8     
  Misses               2053     2053           
  Partials               13       13           

Flag	Coverage Δ
javascript	78.41% <ø> (ø)
python	95.22% <92.30%> (+<0.01%)	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: a869d0cd-fdc7-410e-9352-db07656248c8

📥 Commits

Reviewing files that changed from the base of the PR and between 90241b1 and c0b062b.

📒 Files selected for processing (1)

• TESTING.md

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

---

📝 Walkthrough

Walkthrough

The checker treats where-helper bodies as closed, param-rooted value scopes. Outer parameter slots produce E130 with explicit-argument guidance, while parent generic type parameters remain available. Tests, conformance metadata, specification text, and project documentation reflect the change.

Changes

Where-helper scope validation

Layer / File(s)	Summary
Checker scope boundary and diagnostics vera/checker/core.py, vera/checker/expressions.py, vera/wasm/operators.py	Parent value slots are removed before helper checking; unresolved outer slots receive an explicit-argument hint, and code generation retains a defensive invariant.
Scope regression and conformance coverage tests/test_checker_functions.py, tests/conformance/manifest.json, TESTING.md	Tests cover helper-local slots, rejected outer slots, generic type parameters, hint selection, nested scopes, handler precedence, and state cleanup; the new E130 fixture and suite counts are recorded.
Specification and project documentation spec/05-functions.md, CHANGELOG.md, AGENTS.md, CLAUDE.md, FAQ.md, KNOWN_ISSUES.md, ROADMAP.md, SKILL.md, README.md	Documentation defines closed helper scopes, records the fix, removes the resolved issue entry, and updates conformance and test totals.

Estimated code review effort: 3 (Moderate) | ~20 minutes

Sequence Diagram(s)

sequenceDiagram
  participant TypeChecker
  participant WhereHelper
  participant Diagnostic
  TypeChecker->>TypeChecker: Remove parent value-slot scope
  TypeChecker->>WhereHelper: Check helper body and contracts
  WhereHelper->>Diagnostic: Report unresolved outer slot
  Diagnostic-->>WhereHelper: Return E130 with explicit-argument guidance

Loading

Possibly related PRs

• aallan/vera#975: Both changes extend unresolved-slot diagnostics with context-specific hints in _check_slot_ref.

Suggested labels: compiler, tests, spec, docs

🚥 Pre-merge checks | ✅ 8

✅ Passed checks (8 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly states the main fix: rejecting outer function parameter slot reads in where-helper bodies.
Linked Issues check	✅ Passed	The code and tests match #969 by rejecting outer-slot reads in where-helper bodies with E130 while preserving parent forall type parameters.
Out of Scope Changes check	✅ Passed	The documentation, fixtures, tests, and issue-tracking updates are all directly tied to the where-helper scope fix and its recorded follow-ups.
Docstring Coverage	✅ Passed	Docstring coverage is 86.67% which is sufficient. The required threshold is 80.00%.
Changelog Covers Public-Surface Changes	✅ Passed	CHANGELOG.md explicitly documents the spec §5 where-helper scope rule change: closed, param-rooted helpers, outer slots rejected, values passed as args.
Spec And Implementation Move Together	✅ Passed	PASS: spec/05-functions.md now states where-helpers are closed, param-rooted scopes, and checker code pops the parent value scope plus adds matching E130 hinting.
Diagnostics Carry An Error Code	✅ Passed	PASS: The touched checker diagnostics all still carry explicit stable codes (e.g. E130, E121-124, W001); no new or changed diagnostic path lacks an error_code.

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch fix/969-where-helper-scope

---

_{Comment @coderabbitai help to get the list of available commands.}

[aallan]

@greptileai review

[greptile-apps]

Greptile Summary

Fixes a check/compile scope divergence for where-helper bodies: the checker was validating helper bodies while the parent's value-slot scope was still live, so a helper reading the outer function's parameter slot (e.g. @Int.0 inside a helper whose parent binds @Int) passed vera check and vera verify then crashed vera compile with an E699 dangling-slot error. The parent's value scope is now popped before helper bodies are checked, making such a reference an ordinary E130, with a targeted hint directing the user to pass the value as an explicit argument.

• vera/checker/core.py: _check_fn moves pop_scope() to before the where-fn loop and uses a try/finally-guarded _where_helper_outer_tnames stack to carry the parent's param slot types into the hint logic.
• vera/checker/expressions.py: Adds a narrow E130 hint branch (gated on count == 0, non-empty stack, and the failing type being one the parent bound) that steers users to add an explicit parameter rather than rely on outer-frame capture.
• Tests: 10 new unit tests in TestWhereHelperScope and a new negative conformance fixture (ch05_where_helper_outer_slot_rejected.vera) cover the reported bug, over-pop guard, generic type-param preservation, hint isolation to helpers, contract-clause coverage, nested where-block targeting, and handler/where-helper hint ordering.

Confidence Score: 5/5

The change is safe to merge: it closes a well-understood scope desync between the checker and both backends, is fully mutation-validated, and leaves no known regression surface open.

The core change — moving one pop_scope() call earlier and wrapping the where-fn loop in a narrowly scoped hint-context stack — is minimal, logically sound, and covered by 10 targeted unit tests plus a new negative conformance fixture. The try/finally around the hint stack ensures cleanup even when individual helper checks emit errors. Parent type params are correctly preserved through the separate saved_params save/restore path. All documentation surfaces are updated in lockstep.

No files require special attention.

Important Files Changed

Filename	Overview
vera/checker/core.py	Moves pop_scope() to before the where-fn loop so helper bodies cannot resolve outer parameter slots; adds _where_helper_outer_tnames stack for hint context; uses try/finally to keep the stack clean on errors
vera/checker/expressions.py	Adds a narrowly-gated E130 hint branch for where-helper bodies reading outer-param slot types; correctly places the branch before the generic hint and after the handler-state hint, matching the intended priority order
vera/wasm/operators.py	Updates comment on E699 guard to document that both previously-known source routes (#973, #969) are now sealed at check time; guard is correctly retained as a soundness net
tests/test_checker_functions.py	Adds TestWhereHelperScope with 10 tests covering: the reported bug, over-pop guard, generic type params, unrelated slot type, sibling-fn hint isolation, contract clauses, nested where-block parent/grandparent hint targeting, and handler-hint-wins ordering
tests/conformance/ch05_where_helper_outer_slot_rejected.vera	New negative conformance fixture: outer(@int) with helper(@Bool) that reads @Int.0 in its body; correctly declared at check level with expected_error: E130
tests/conformance/manifest.json	Adds manifest entry for ch05_where_helper_outer_slot_rejected with correct level, spec_ref, expected_error, and feature tags
spec/05-functions.md	Adds a precise prose paragraph to §5.6 codifying the closed param-rooted scope rule for where-helpers, including the type-param exception and the E130 consequence
KNOWN_ISSUES.md	Removes the closed #969 row; adds the new #978 nested-where-blocks bug; keeps the section non-empty per the convention (five bugs remain open)

_{Reviews (5): Last reviewed commit: "docs(testing): last three conformance-co..." | Re-trigger Greptile}

[greptile-apps]

Greptile Summary

This PR closes #969 by making the type checker agree with the WASM backends: a where-helper body can no longer resolve the outer function's parameter slots. Previously the checker checked helper bodies while the parent's value scope was still live, so @Int.0 inside a helper that declared only @Bool silently resolved to the parent's @Int param — passing check and verify before crashing compile with an internal E699 dangling-slot error.

• vera/checker/core.py: moves env.pop_scope() for the parent's value-slot frame to before the where-helper loop; the parent's forall type params stay in scope so generic parents still parameterise their helpers. A try/finally block guarantees _where_helper_outer_tnames cleanup on any exit path.
• vera/checker/expressions.py: adds a narrowly-gated E130 hint branch (fires only when count == 0, inside a helper body, and the unresolved type is one the parent bound) that steers the user to pass the value as an explicit argument instead of the generic "lower index" suggestion.
• vera/wasm/operators.py: updates the E699 defensive guard comment to record that both previously-known source routes are now closed at check time; the guard is intentionally kept as a soundness net.
• Tests: five new unit tests in TestWhereHelperScope cover the bug case, over-pop guard, generic type-params preserved, unrelated-type hint routing, and sibling-function hint isolation; one new negative conformance fixture (ch05_where_helper_outer_slot_rejected) is the 147th conformance program.

Confidence Score: 5/5

The change is a targeted, well-contained scope-reordering in _check_fn: the parent's value frame is popped one step earlier, and the helper-checking loop gains a try/finally to guarantee hint-stack cleanup. All pre-existing tests continue to pass, and five new unit tests together with a new negative conformance fixture exercise every relevant edge case.

The core invariant (parent value scope isolated from helper bodies; parent type scope preserved) is verified by mutation testing described in the PR, and the five new unit tests cross-check each gate condition independently. The try/finally around the hint stack makes the cleanup unconditional. Documentation counts are internally consistent across all updated files. No open questions remain.

No files require special attention.

Important Files Changed

Filename	Overview
vera/checker/core.py	Moves env.pop_scope() for the parent's value-slot frame to before the where-helper loop (was at end of step 9); wraps the helper-check loop in try/finally to guarantee _where_helper_outer_tnames cleanup. The reordering is safe: contracts and body type-checking happen at steps 5–7 before the pop, and parent type params are restored separately at step 9, so generics remain available through the loop.
vera/checker/expressions.py	Adds a narrowly-gated E130 hint branch for the where-helper-outer-slot case, mirroring the pattern from #973. Gate conditions — count == 0, non-empty _where_helper_outer_tnames, and tname in the innermost set — correctly limit the improved message to the exact failure scenario, keeping the generic lower-index hint for unrelated types and sibling functions.
vera/wasm/operators.py	Comment-only update on the E699 dangling-slot guard: documents that both previously-known source routes (#973, #969) are now closed at check time with E130, while explicitly preserving the guard as a soundness net for any future checker/backend scope desync.
tests/test_checker_functions.py	Adds TestWhereHelperScope with five targeted tests: the reported bug, guard against over-pop when helper has its own same-typed param, parent forall type params remaining in scope, unrelated type producing the generic hint, and sibling function not inheriting a stale hint. All necessary corner cases are covered.
tests/conformance/ch05_where_helper_outer_slot_rejected.vera	New negative conformance fixture (the 147th program): helper has @Bool as its parameter but its body references @Int.0, which belongs only to the outer outer(@int -> @int). Registered at level check with expected_error: E130, correctly establishing the check-level rejection as the spec-compliant baseline.
tests/conformance/manifest.json	Adds manifest entry for ch05_where_helper_outer_slot_rejected at chapter 5 with level: check and expected_error: E130. Entry is inserted between ch05_where_fn_higher_order and ch06_requires, maintaining chapter order.
spec/05-functions.md	Adds a spec paragraph formalising the closed-scope rule: helpers resolve slots only against their own params; parent value slots are out of scope; parent forall type params remain in scope; implicit outer-frame capture would cross a contract boundary and is E130.
TESTING.md	Count updates are internally consistent: test total 6,943→6,953 (+10), skipped 65→67 (+2 for the two level-limited skips on the new negative fixture). The skip table gains the two new test_verify and test_run rows for ch05_where_helper_outer_slot_rejected.

_{Reviews (2): Last reviewed commit: "fix(checker): reject where-helper bodies..." | Re-trigger Greptile}

[coderabbitai]

Actionable comments posted: 1

🤖 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/conformance/manifest.json`:
- Around line 808-821: Update the spec_ref field for the
ch05_where_helper_outer_slot_rejected fixture from Section 5.2 to Section 5.6.2,
“Mutual Recursion,” while leaving the remaining manifest metadata unchanged.

🪄 Autofix (Beta)

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: eb4b036a-5500-41fb-a6fc-a97beb154127

📥 Commits

Reviewing files that changed from the base of the PR and between 935120a and 360452b.

⛔ Files ignored due to path filters (6)

• docs/SKILL.md is excluded by !docs/**
• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• tests/conformance/ch05_where_helper_outer_slot_rejected.vera is excluded by !**/*.vera

📒 Files selected for processing (14)

• AGENTS.md
• CHANGELOG.md
• CLAUDE.md
• FAQ.md
• KNOWN_ISSUES.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• spec/05-functions.md
• tests/conformance/manifest.json
• tests/test_checker_functions.py
• vera/checker/core.py
• vera/checker/expressions.py
• vera/wasm/operators.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

💤 Files with no reviewable changes (2)

• SKILL.md
• KNOWN_ISSUES.md

[aallan]

Adversarial review panel + pr-review — record

Five panel lenses (pre/post differential, hint-stack interplay, spec/docs, backend agreement, diagnostic quality) with two adversarial skeptics per finding, plus three review agents (code, tests, docs). All confirmed findings are fixed in f72796f; the review round also surfaced a second new bug, filed as #978.

The #969 fix itself: no correctness findings. The differential lens ran a probe battery at base vs head (own-param helpers, contract-clause reads, let-bound values, sibling helpers, recursive helpers, generic parents) and found only the intended flips — no silent run-result changes, no incomplete flips. The hint-interplay lens could not break the two-hint-stack machinery (a handle inside a helper gets the innermost, correct hint; the where-hint frame consults only the immediate parent). The code reviewer proved contract clauses are isolated along with bodies (a requires(@Int.0 > 0) reading the outer param was check-green/compile-E699 at base, is E130 at head) and that nothing after the moved pop_scope() reads the value scope.

Panel findings (3 confirmed, all minor) — resolved

• The new conformance fixture's header and manifest spec_ref cited §5.2; the closed-scope rule lives at §5.6.2. Corrected (CodeRabbit later reported the manifest half of the same finding).
• Depth-2 nested where-helpers: check-green, vera compile fails with unknown func — the non-generic emission path compiles one level of where_fns while registration recurses (generic parents work via the monomorphize hoist). Pre-existing at base, independently reproduced, filed as #978 with KNOWN_ISSUES + SKILL rows riding this PR and a burndown slot queued.
• The where-helper hint's "add a @Int parameter" mis-articled vowel-initial types; rephrased to avoid the article.

pr-review findings — resolved in f72796f (and the prior comment fix)

• Tests (the sharpest gap): every test exercised a helper BODY read; the contract-clause route — the fix's own motivating rationale — had zero pins, so a narrower body-only reimplementation would have passed the whole suite. Added requires/ensures rejection tests; mutation-validated by reverting the pop placement (both contract pins and the body pin go RED). Also added: nested-where hint pins (immediate-parent hint vs grandparent generic) and a hint-precedence pin (handler-state hint wins inside a helper), and the type-param guard test's docstring no longer overclaims (clearing type params early is provably a no-op — opaque-typevar fallback, call-site-driven monomorphization).
• Docs: the core.py comment cited ch09_generic_where_helper as guarding the type-param retention; the probe shows all 147 conformance programs pass with retention removed. The comment now states the retention is spec-intent, not test-guarded. Everything else verified accurate, including the E699 guard comment's hedged claims and the fifteen/nine TESTING.md enumeration.
• Code: no confirmed findings.

Reviewer scoreboard for this PR so far: panel 3 confirmed (1 unique bug discovery with root cause), pr-review agents 2 confirmed classes (contract-pin gap, comment overclaim), CodeRabbit 1 duplicate-valid (the manifest spec_ref, ~1h behind the panel), Greptile: no output yet.

[coderabbitai]

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 `@README.md`:
- Line 227: Update the active-development metrics sentence in README.md to
report 147 conformance programs instead of 146, keeping it consistent with the
updated test and conformance counts in FAQ.md and ROADMAP.md.

In `@TESTING.md`:
- Line 9: The TESTING.md overview reports an inconsistent test total: 6,860
passed + 26 stress + 67 skipped equals 6,953, not 6,958. Correct the Tests
metric to match the component counts, or document and verify the additional five
tests/statuses against the canonical test collection/count checks.

🪄 Autofix (Beta)

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: e88a776d-4b65-4e7b-ba83-cc041372082d

📥 Commits

Reviewing files that changed from the base of the PR and between 360452b and f72796f.

⛔ Files ignored due to path filters (3)

• docs/SKILL.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• tests/conformance/ch05_where_helper_outer_slot_rejected.vera is excluded by !**/*.vera

📒 Files selected for processing (10)

• FAQ.md
• KNOWN_ISSUES.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• tests/conformance/manifest.json
• tests/test_checker_functions.py
• vera/checker/core.py
• vera/checker/expressions.py

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)

[coderabbitai]

Actionable comments posted: 1

🤖 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`:
- Around line 9-11: Update the stale conformance-program count in the
conformance-suite introduction from 146 to 147, ensuring all references in
TESTING.md match the overview.

🪄 Autofix (Beta)

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: 1d4a6659-400c-4ee0-a705-229662e3ec0b

📥 Commits

Reviewing files that changed from the base of the PR and between f72796f and 90241b1.

📒 Files selected for processing (2)

• README.md
• TESTING.md

🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

• aallan/vera-bench (manual)