fix(checker): re-synth ctor args against partially-generic params so concrete Nat components obligate (#1010)

[aallan]

Restores the static E503 @Nat-narrowing promise for the concrete components of a partially-generic constructor argument.

Root cause

Every re-synthesis in the generic-call argument loop (vera/checker/calls.py) is gated on the whole parameter type being typevar-free. A constructor argument against @Pair<Nat, T> was therefore never re-typed against its instantiated parameter: the concrete Nat component's narrowing target went unrecorded, the verifier's ctor-field walker (which resolves generic fields via the recorded instantiated target, #747) found nothing, and wants(MkPair(0 - 5, None)) checked, verified clean, and silently stored the negative. The fully-concrete @Pair<Nat, Int> analogue obligates correctly — the generic path just never reached the same machinery.

Fix

One block in the argument loop: constructor-expression arguments are re-synthesized against the instantiated parameter even when type variables remain. The #971 bidirectional fill adopts component-wise (typevar components stay unconstrained), and the ctor check records each field's target exactly as on the concrete path. No verifier change needed — its walker already consults the recorded target.

Result parity with the concrete path, all pinned:

• MkPair(0 - 5, None) as @Pair<Nat, T> → E503 (was verify-clean, silent negative)
• MkPair(@Int.0, None) under requires(true) → E503 with counterexample (matches concrete verdict)
• Same under requires(@Int.0 >= 0) → discharges Tier-1
• MkPair(5, None) → verify-clean (no false positive)
• Concrete control pinned to prove both paths share one mechanism

The runtime-guard half for generic fields is unchanged and stays documented under the #754/#757 limitation rows — the static promise is what #1010 restored.

Validation

Five tests in tests/test_verifier_nat_obligations.py (TestGenericCtorParamNatObligation1010), RED-first for the two broken shapes; revert-the-fix mutant killed. Full gate: 7,370 tests green, mypy/ruff clean, 157 conformance, 37 examples, doc-count/limitations-sync/site-asset gates green. Docs: KNOWN_ISSUES + SKILL rows deleted, CHANGELOG [Unreleased] entry, counts reconciled.

Closes #1010

🤖 Generated with Claude Code

Summary by CodeRabbit

• Bug Fixes
  • Restored E503 checks for negative values passed to Nat components within partially generic constructor arguments (issue #1010).
  • Improved runtime trap diagnostics with clearer per-kind guidance and source backtraces, while preserving constant WebAssembly stack usage for tail-recursive iteration.
• Tests
  • Added regression coverage for constructor-argument narrowing and increased totals to 7,370 tests (7,274 passing).
• Documentation
  • Updated changelog/known-bugs entries and refreshed project status/testing metrics across the documentation.

[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: f2de46e5-eaf1-4f65-bfc6-0adc14103347

📥 Commits

Reviewing files that changed from the base of the PR and between 0306a84 and 285e105.

📒 Files selected for processing (2)

• TESTING.md
• tests/test_verifier_nat_obligations.py

🔗 Linked repositories identified

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

• aallan/vera-bench (manual)

---

📝 Walkthrough

Walkthrough

The call checker now re-synthesises partially-generic constructor arguments so concrete Nat components retain E503 obligations. Five regression tests cover affected and control cases, while project documentation and test metrics are updated.

Changes

Nat obligation verification

Layer / File(s)	Summary
Constructor argument re-synthesis vera/checker/calls.py, CHANGELOG.md, KNOWN_ISSUES.md, SKILL.md	Constructor arguments with partially-generic ADT parameter types are re-synthesised against the instantiated type, and related bug documentation records the corrected behaviour and diagnostics.
Regression tests and test metrics tests/test_verifier_nat_obligations.py, TESTING.md, README.md, ROADMAP.md	Tests cover failing, constrained, valid, and fully-concrete Nat components; documented test counts are incremented.

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

Possibly related issues

• aallan/vera#757 — Covers related @Nat handling for generic constructor values, while this change restores the static E503 obligation.

Possibly related PRs

• aallan/vera#994 — Addresses expected-type propagation for nested nullary constructors in a related call-typing path.

Suggested labels: compiler, tests, 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 is specific and accurately reflects the main checker fix for partially generic constructor arguments and issue #1010.
Linked Issues check	✅ Passed	The code change, tests, and verifier behaviour described all align with restoring E503 obligations for concrete Nat components in partially generic constructors.
Out of Scope Changes check	✅ Passed	The documentation and metrics updates appear tied to the same fix and validation work, with no clear unrelated scope creep.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.
Changelog Covers Public-Surface Changes	✅ Passed	All public-surface edits are described: verify --json (#967), Nat widening/narrowing and import tables (#820/#987/#998/#1010), plus where/state/spec changes (#969/#976/#978).
Spec And Implementation Move Together	✅ Passed	Spec already states E503 at constructor-field/generic-instantiation sites; the PR only fixes the checker to realise that behaviour, with runtime-guard limits unchanged.
Diagnostics Carry An Error Code	✅ Passed	PASS: no new diagnostic was introduced; the changed checker path only re-synthesises args, and all diagnostic emissions in vera/checker/calls.py carry explicit error_code values.

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch fix/1010-e503-generic-ctor-param

---

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

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 93.49%. Comparing base (6aa9ff2) to head (285e105).

Additional details and impacted files

@@               Coverage Diff               @@
##           release/v0.1.4    #1011   +/-   ##
===============================================
  Coverage           93.48%   93.49%           
===============================================
  Files                  96       96           
  Lines               31900    31905    +5     
  Branches              456      456           
===============================================
+ Hits                29823    29828    +5     
  Misses               2064     2064           
  Partials               13       13           

Flag	Coverage Δ
javascript	78.41% <ø> (ø)
python	95.27% <100.00%> (+<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]

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/test_verifier_nat_obligations.py`:
- Around line 1550-1612: Strengthen the tests in
test_generic_ctor_param_negative_nat_component_e503,
test_generic_ctor_param_opaque_int_component_obligated,
test_generic_ctor_param_proved_int_component_tier1, and
test_concrete_ctor_param_negative_nat_component_e503 to assert the exact E503
diagnostic for failures and explicitly verify that the constrained case
completes at Tier 1 rather than merely having no errors. Reuse the test helpers
or result fields that expose error_code and verification tier, keeping the
existing diagnostic description 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: 399eaf40-3be7-4165-aeaf-36718dd42b9c

📥 Commits

Reviewing files that changed from the base of the PR and between 6aa9ff2 and 09a8d82.

⛔ Files ignored due to path filters (2)

• docs/SKILL.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**

📒 Files selected for processing (8)

• CHANGELOG.md
• KNOWN_ISSUES.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• tests/test_verifier_nat_obligations.py
• vera/checker/calls.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)

• KNOWN_ISSUES.md
• SKILL.md

[aallan]

Code review (pr-review-toolkit, LIGHT tier) — report

An Opus code-reviewer agent reviewed 09a8d82 via a base-vs-PR differential over ~20 hand-built adversarial programs run through the real check+verify pipeline, plus a revert-mutant check.

Verdict: no findings at confidence ≥ 80; recommended for merge. Per focus area:

• Unconditional re-synth adoption: safe — the whole-type E202 check and A bare None as a call argument never adopts the expected argument type — E202 (generic sibling leak) / E241 (eq-form, even concrete) #993 wildcard still run on the adopted type; no E202 verdict flips anywhere in the differential (wrong-parent expected is a no-op via the expected.name == ci.parent_type guard).
• Double-diagnosis: does not occur — the diagnostic dedup key absorbs the second synth; expected-independent inner errors emit exactly once; E213 stays suppressed in favour of the single call-level E202.
• A bare None as a call argument never adopts the expected argument type — E202 (generic sibling leak) / E241 (eq-form, even concrete) #993 interaction: every A bare None as a call argument never adopts the expected argument type — E202 (generic sibling leak) / E241 (eq-form, even concrete) #993 shape byte-identical between base and PR; bare-typevar params are excluded by the AdtType clause.
• Target provenance: the recorded field target comes from the expected mapping (declared Nat), not the inferred binding — no path where a conflicting inference spoofs a wrong target; a genuine @Int into Pair<T, U> (T inferred Int) stays clean.
• False-E503 sweep: 37 examples + 157 conformance + adversarial legit shapes (nested ctors, Byte components, refined components) all clean; the deeply-nested negative correctly fires E503 and a refined-component negative fires E505 — the fix generalizes consistently with the concrete path.

One ~60%-confidence docs nit (the #993 CHANGELOG entry's now-stale 'tracked in KNOWN_ISSUES' clause) is fixed in the follow-up docs commit.