Skip to content

v0.0.5: Type checker#2

Merged
aallan merged 1 commit intomainfrom
type-checker
Feb 23, 2026
Merged

v0.0.5: Type checker#2
aallan merged 1 commit intomainfrom
type-checker

Conversation

@aallan
Copy link
Copy Markdown
Owner

@aallan aallan commented Feb 23, 2026

Summary

  • Type checker (vera/types.py, vera/environment.py, vera/checker.py): Tier 1 decidable type checking — validates expression types, slot reference resolution, effect annotations, and contract well-formedness
  • Two-pass architecture: pass 1 registers all declaration signatures (forward references, mutual recursion), pass 2 checks bodies
  • Expression type synthesis for all AST node types, De Bruijn slot resolution with alias opacity, generic type argument inference, handler effect discharge, error accumulation with UnknownType propagation
  • vera check now runs the full pipeline (parse → AST → typecheck); vera typecheck added as explicit alias
  • 91 new tests across 19 test classes (284 total, up from 193)
  • All 13 example programs type-check cleanly

Test plan

  • All 284 tests pass (pytest tests/ -q)
  • All 13 examples pass vera check (11 clean, 2 with only unresolved-name warnings)
  • vera check examples/factorial.vera prints "OK"
  • vera typecheck examples/factorial.vera prints "OK"
  • Type error diagnostics include description, location, rationale, fix, spec_ref

🤖 Generated with Claude Code

@aallan @claude
v0.0.5: Type checker — 91 new tests, vera typecheck command
89e0733 
Tier 1 decidable type checking: expression types, slot resolution,
effect annotations, and contract well-formedness. Two-pass architecture
with error accumulation and LLM-oriented TypeError diagnostics.
All 13 example programs type-check cleanly.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@aallan aallan merged commit fc76f0d into main Feb 23, 2026
3 checks passed
@aallan aallan deleted the type-checker branch February 23, 2026 07:32
@aallan aallan mentioned this pull request Apr 16, 2026
Closed
aallan added a commit that referenced this pull request Apr 23, 2026
@aallan
Address fourth CodeRabbit review round (2 findings)
407772b 
Both findings real, both fixed.

Predicate hoist (#2):
- Extracted the canonical ASCII whitespace predicate into a
  module-level helper emit_is_ascii_whitespace(byte_local, indent)
  in vera/wasm/helpers.py.  Single-source-of-truth for the
  branchless {space(32) | (byte - 9) < 5} encoding of Python's
  str.isspace() ASCII set {tab(9), LF(10), VT(11), FF(12), CR(13),
  space(32)}.  Replaced four open-coded copies with calls to the
  helper:
    1. _translate_is_whitespace (~10 LOC → 1 line)
    2. _is_ws_inline closure inside _translate_trim
    3. _translate_structural_split count pass (string_words)
    4. _translate_structural_split emit pass (string_words)
- Helper docstring documents the historical context (PR #510 round 2
  caught _translate_strip's divergent narrow predicate; round 4
  hoisted the helper) and warns against re-encoding the byte set.
- Direct application of the byte-literal-collision review rule (memory
  file feedback_review_heuristics.md): two functions sharing a
  predicate routed through one helper from day 1 prevents future
  divergence.

Browser regression (#1):
- New tests/test_browser.py::TestBrowserStringUtilities::
  test_string_strip_vt_ff: compiles and runs a program that calls
  string_strip("\\u{0B}\\u{0C}hi \\u{0B}") and asserts the output
  is "hi".  Pins the strip→trim delegation contract under the
  browser runtime — if a future refactor accidentally re-opens the
  old narrow predicate for strip, this assertion breaks.

All 3,487 tests pass; mypy clean; doc count check + site asset
check + spec/SKILL/conformance/example checks all green.

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request Apr 23, 2026
@aallan
Extend SKILL.md Known Bugs table with #515/#516/#517 (PR #518 CR #2)
dc010e5 
CodeRabbit caught that the Known Bugs and Workarounds table only had
rows for #514/#475/#487 but KNOWN_ISSUES.md and the ROADMAP short-term
queue already tracked #515/#516/#517 as well.  Added three new rows:

- GC collect faults (#515): collector walks past heap_ptr under
  allocation pressure.
- Runtime trap diagnostics (#516): 'Runtime contract violation'
  label conflates contract-fail with OOM/overflow/etc.
- No tail-call optimization (#517): tail-recursive iteration blows
  the call stack at ~tens of thousands of frames.

Also rewrote the existing #514 row with the agent's sharpened
characterization (closures + any heap capture, not 'nested
closures'), and rewrote the trailing diagnostic-hint paragraph to
map each common symptom to the specific issue it's likely caused
by.  No stale labels remain; the section mirrors the KNOWN_ISSUES.md
Bugs table in scope.

Co-Authored-By: Claude <noreply@anthropic.invalid>
aallan added a commit that referenced this pull request Apr 27, 2026
@aallan
PR #533 review fixes: stderr wiring + JSON key clarity + counts
835dc68 
Five real findings from CodeRabbit, one rabbit-incorrect:

1. (real) HISTORY.md line 294: '119 tagged releases' -> 120.
2. (real) KNOWN_ISSUES line 17: clarified the JSON envelope key is
   trap_kind, distinct from WasmTrapError.kind (the Python attribute).
3. (rabbit-incorrect) README.md '32 examples' is correct (filesystem
   count via ls examples/*.vera = 32). Not changed; replied.
4. (real) ROADMAP.md line 39: same kind/trap_kind clarification as #2.
5. (real) Added test_json_mode_includes_stderr_in_envelope.
6. (real, the important one) cmd_run never passed capture_stderr=True
   to execute(), so WasmTrapError.stderr and the JSON envelope's
   stderr field were permanently empty. Wired through:

   a. cmd_run now passes capture_stderr=True (parallel to stdout's
      always-on capture)
   b. Success path replays exec_result.stderr to sys.stderr (text)
      or includes it in the envelope (JSON)
   c. Existing WasmTrapError handler now actually populates these
      fields on the trap path
   d. Preserved the original 'stdout suppresses value-printing'
      behaviour (stderr does not suppress value-printing -- it's
      independent in its own stream)

Plus lint fix: 'uv lock --check' was failing because pyproject.toml
version bumped 0.0.119 -> 0.0.120 but uv.lock still pinned 0.0.119.
Ran 'uv lock' to sync.

Test count: 3536 -> 3537 (+1 from new stderr test); doc counts
and TESTING.md row updated accordingly.

Co-Authored-By: Claude <noreply@anthropic.invalid>
@aallan aallan mentioned this pull request May 7, 2026
Merged
9 tasks
aallan added a commit that referenced this pull request May 8, 2026
@aallan
Review-pass fixes on PR #631 — close cross-cutting findings from 4 ag…
0afd4e2 
…ents + CodeRabbit

Four review agents (code-reviewer, pr-test-analyzer, comment-analyzer,
silent-failure-hunter) plus three CodeRabbit comments produced a
batch of cross-cutting findings.  This commit addresses them all
in one pass to avoid the iterative round-trip cost the bug class
itself was filed to eliminate.

**Critical fixes:**

1. **Closure body E615 harvest gap (silent-failure-hunter C1).**
   `_compile_lifted_closure` constructed its own WasmContext but
   never harvested `_interp_inference_failures` — closure bodies
   with E615-triggering interpolation segments were silently
   dropped, producing call_indirect→missing-table-entry WASM
   validation traps with no source-located diagnostic.  Extracted
   the harvest into `CodeGenerator._harvest_interp_inference_failures`
   on the codegen base and called it from both functions.py and
   closures.py.  Removed the now-disproved `# pragma: no cover —
   defensive` claim on closures.py's body-instrs-None path.  New
   regression test `test_e615_in_closure_body_emits_diagnostic`.

2. **`_canonical_named_type` type_args from terminal NamedType
   (CodeRabbit #3 + code-reviewer I1).**  The walker's
   `outer_type_args` capture rule (always read from first NamedType)
   lost type_args when alias_map substitution bound a generic
   param to a parameterised type.  Empirically reachable today via
   `type Mapper<A, B> = fn(A -> B); Mapper<Int, Array<Int>>` etc.
   Fix: drop the "outermost" rule, return type_args from the
   terminal NamedType reached.  All 21 existing #602-class
   regression tests still pass.  New regression test
   `test_canonical_named_type_terminal_args_propagation`.

3. **HISTORY.md footer (CodeRabbit #1).**  141 tagged releases →
   142 to match the v0.0.142 row added in PR #631.

**UX fix:**

4. **Multiple E615 per function (silent-failure-hunter H2).**
   Pre-this-fix `_translate_interpolated_string` returned None on
   the first failing segment, requiring N round-trips for N bad
   segments in one interpolation.  Now collects every failing
   segment via `had_failure` flag, then bails at the end.  New
   regression test `test_multiple_e615_in_one_interpolation`.

**Doc-quality fixes (comment-analyzer):**

5. **Trigger-count drift** in `operators.py:491-494` —
   "every canonicalisation gap (#602 and ten subsequent triggers)"
   implied 11; rewrote to "the ten triggers of the #602 bug class
   accumulated across PRs #627 + #629".

6. **`_format_named_type_canonical` docstring drift** — claim
   "matches the pre-#630 fallback shape" was empirically wrong
   (pre-#630 resolved through aliases, post-#630 fallback doesn't).
   Rewrote to acknowledge the deliberate behavioural change.

7. **"Future closure-arg shapes plug in here without further
   dispatch ladder"** — overstatement.  Adding a `FnCall`
   returning a closure still needs an `elif`; what's saved is
   canonicalisation logic, not dispatch logic.  `IfExpr` between
   closures has no single `return_type` field — example was
   misleading.  Rewrote in both `_infer_fncall_vera_type` and
   `_infer_apply_fn_return_type`.

8. **`_canonical_wasm_type` docstring** — added explicit `Unit →
   None` documentation; clarified that `None` (no WASM type) and
   `"i64"` (unreachable-NamedType default) are distinct return
   shapes that callers must not conflate.

**Tests added (besides the regressions tied to fixes):**

9. **`test_per_function_isolation_of_failures_list`** — pins
   that a clean function and a dirty function in the same source
   produce independent `_interp_inference_failures` lists.

10. **`test_e615_fires_on_result_in_interpolation`** — adjacent
    ADT shape (Result vs Option) so a future Option-handling
    broadening doesn't accidentally regress the parallel Result
    path.

11. **`test_array_map_refinement_returning_closure`** — pins the
    previously-unaudited `_infer_closure_return_vera_type` path
    in `calls_arrays.py`, which the #630 migration broadened to
    handle refinements.

**Test enhancements:**

12. **E615 ordering before matching E602** in the existing test
    (CodeRabbit #2) — pinned via `warnings.index(e615[0])` <
    `warnings.index(matching_e602)`.  Filtered to the E602 that
    mentions the offending function so prelude-skip E602s don't
    confound the assertion.

13. **E615 source-location attached** in the existing test —
    softened to "line > 0" (any location) because SlotRef-inside-
    InterpolatedString spans are unreliable today (#634, separate
    follow-up).  Tightening to "line points at the segment" is
    the natural acceptance test for that follow-up.

**Skipped with reasons:**

- **Cycle-guard regression on `_resolve_base_type_name`** —
  test-analyzer C1 / code-reviewer S4.  Verified pre-existing
  and dead-code-safe today (cycles crash an upstream resolver
  first).  Filed as #633.

- **`_canonical_wasm_type`'s `i64` default for unhandled
  apply_fn / call_indirect shapes** — silent-failure-hunter H1.
  Bigger refactor parallel to Tier 2 but for the WASM-side
  dispatch.  Filed as #632.

- **SlotRef-inside-InterpolatedString span fidelity** —
  surfaced when writing the E615 source-location assertion.
  Diagnostic-quality concern, separate from #630's
  canonicalisation scope.  Filed as #634.

- **`_canonical_named_type` worked-example docstring**
  (comment-analyzer I6) — superseded by fix #2 above (semantics
  changed; docstring rewritten with concrete examples).

- **Per-context isolation prose-vs-test** (comment-analyzer I4)
  — addressed via fix #9 (test added).

- **`_resolve_i32_pair_ret_te` 30-line upper docstring** —
  comment-analyzer style nit.  The prose is load-bearing
  context (#628 cross-module narrative); trimming would lose
  history without obvious gain.  Defer.

**Follow-ups:** #632 (apply_fn / call_indirect E616), #633
(_resolve_base_type_name cycle guard), #634 (interpolation
SlotRef source spans).  Added to KNOWN_ISSUES.md alongside #628.

Counts: 3,792 tests (3,778 passed, 14 skipped) — six new tests
under `TestE615LoudInterpolationFallthrough630`.  CHANGELOG +
KNOWN_ISSUES + ROADMAP + TESTING.md + HISTORY footer all
synced.  mypy clean.

Co-Authored-By: Claude <noreply@anthropic.invalid>
@aallan aallan mentioned this pull request May 8, 2026
Merged
8 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@aallan