Fix #648: cyclic type aliases produce [E132] at check time

CHANGELOG.md

@@ -6,6 +6,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+## [0.0.149] - 2026-05-12
+
+### Fixed
+
+- **[#648](https://github.com/aallan/vera/issues/648)** — cyclic type aliases now produce a clean `[E132]` diagnostic at `vera check` time instead of crashing `vera compile` with `RecursionError`.  Pre-fix `vera/checker/registration.py::_register_alias` resolved aliases one at a time; when `type A = B` was processed before `B` was registered, the forward-reference fallback in `_resolve_type` returned a placeholder rather than chasing the chain, so the resolved-type representation reached the post-registration state with no observable cycle.  Codegen later stored the raw AST `type_expr` and `vera/codegen/core.py::_type_expr_to_wasm_type` chased the chain through the AST, blowing the stack with `RecursionError: maximum recursion depth exceeded`.  Post-fix `_register_all` calls a new `_check_alias_cycles` pass that walks every alias's AST `type_expr` chain (following `NamedType`-of-alias references through `RefinementType` wrappers, mirroring codegen's recursion shape) and emits `[E132]` ("Cyclic type alias") with the originating decl location, the full cycle path (`A -> B -> C -> A`), and a `Fix:` paragraph pointing at `data`-declared ADTs as the alternative for self-referential types.  Defensive cycle guards on the alias-walking helpers in `vera/wasm/inference.py` (closed in #633) remain as belt-and-braces.  Closes `#648`.
+
 ## [0.0.148] - 2026-05-12
 
 ### Fixed
@@ -2171,7 +2177,8 @@ Small docs sweep — closes six aging documentation issues in one PR.  No code c
 - Grammar: handler body simplified to avoid LALR reduce/reduce conflict
 - `pyproject.toml`: corrected build backend, package discovery, PEP 639 compliance
 
-[Unreleased]: https://github.com/aallan/vera/compare/v0.0.148...HEAD
+[Unreleased]: https://github.com/aallan/vera/compare/v0.0.149...HEAD
+[0.0.149]: https://github.com/aallan/vera/compare/v0.0.148...v0.0.149
 [0.0.148]: https://github.com/aallan/vera/compare/v0.0.147...v0.0.148
 [0.0.147]: https://github.com/aallan/vera/compare/v0.0.146...v0.0.147
 [0.0.146]: https://github.com/aallan/vera/compare/v0.0.145...v0.0.146

HISTORY.md

@@ -293,6 +293,7 @@ Stage 12 opens on the morning v0.0.138 shipped: the residual GC-rooting bug in #
 | v0.0.146 | 12 May | Refinement-of-Array element inference — closes [#655](https://github.com/aallan/vera/issues/655) Shape B. |
 | v0.0.147 | 12 May | Cross-module `_fn_ret_type_exprs` propagation — closes [#628](https://github.com/aallan/vera/issues/628). |
 | v0.0.148 | 12 May | Type-alias arity check ([E133]) — closes [#660](https://github.com/aallan/vera/issues/660) and [#661](https://github.com/aallan/vera/issues/661). |
+| v0.0.149 | 12 May | **Cyclic type aliases now produce [E132]** ([#648](https://github.com/aallan/vera/issues/648)). |
 
 ---
 
@@ -333,4 +334,4 @@ Alongside the compiler, editor support and AI discoverability infrastructure wer
 | Spec chapters | 7 | 10 | 11 | 12 | 13 | 13 | 13 |
 | Code coverage | — | — | — | 90% | 91% | 96% | 96% |
 
-Total: **810+ commits, 148 tagged releases, 58 active development days.**
+Total: **810+ commits, 149 tagged releases, 58 active development days.**

KNOWN_ISSUES.md

@@ -8,7 +8,6 @@ Bugs and limitations tracked against the [issue tracker](https://github.com/aall
 |-----|-------|
 | Tail-call optimization disabled for allocating functions — `return_call` would discard the GC epilogue and leak shadow-stack slots, so allocating functions fall back to plain `call`. Workaround: restructure to allocate outside the recursion, or iterate via `array_fold` / `array_map` (which compile to WASM loops). | [#549](https://github.com/aallan/vera/issues/549) |
 | Conservative GC scan can spuriously retain heap objects via the host-handle field of a wrapper ADT (#573 latent). Phase 2b scans wrapper payloads word-by-word; the `handle` at offset 4 is a small i32 that stays below `gc_heap_start` (~147 KiB) for typical programs, so the heap-range check rejects it. Long-running programs (>100K host-store allocations in a single `execute()`) could see a handle exceed the threshold and (with the right alignment) be falsely classified as a heap pointer, retaining an unrelated heap object. Retention bug, not correctness — no use-after-free, no corruption. Issue body lists four candidate fix designs (self-describing wrappers, header skip-scan flag, wrap-table cross-reference, max-handle lower-bound check). | [#578](https://github.com/aallan/vera/issues/578) |
-| Cyclic type aliases (`type A = B; type B = A;`) pass `vera check` cleanly then crash `vera compile` with `RecursionError` in `vera/codegen/core.py:_type_expr_to_wasm_type`.  The type checker masks the cycle at alias-registration time (when `A` is registered before `B`, the unresolved-import fallback returns a placeholder `AdtType`), but codegen stores raw AST `type_expr` nodes and chases the chain through them.  The proper fix is a post-registration cycle-detection pass in `vera/checker/registration.py` emitting `[E132] Cyclic type alias` with location and rationale.  Defensive cycle guards on the alias-walking helpers in `vera/wasm/inference.py` (`_resolve_base_type_name`, closed in #633) are belt-and-braces for the same family. | [#648](https://github.com/aallan/vera/issues/648) |
 | Nested type aliases (alias-of-alias via `Array<…>`, e.g. `type Row = Array<Int>; type Grid = Array<Row>;`) cause silent codegen skip when indexed through both layers.  `vera check` accepts the program; codegen drops the function with a generic `[E602]` skip, and downstream `vera run` reports the now-missing function as `unknown func: $caller` at WAT validation — pointing at *callers* of the skipped function rather than the skipped function itself.  Single-layer aliases work; substituting the fully-expanded `Array<Array<Int>>` at every use site also works.  Likely interacts with the new `_array_elem_triad_or_skip` helper (#658) — leg 1's `_infer_concat_elem_type` doesn't recurse through the alias chain.  May be partially improved already by Layer 3's per-node `[E602]` spans; verify the diagnostic precision before deciding whether the misleading-caller-error symptom still surfaces. | [#559](https://github.com/aallan/vera/issues/559) |
 
 ## Limitations

README.md

@@ -181,7 +181,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.0.148 — 810+ commits, 148 releases, 3,820 tests, 96% code coverage, 86 conformance programs, 34 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.0.149 — 810+ commits, 149 releases, 3,825 tests, 96% code coverage, 86 conformance programs, 34 examples, and a 13-chapter specification. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
 The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [13 chapters](spec/).
 

ROADMAP.md

@@ -4,7 +4,7 @@ Where the project is going.  See [HISTORY.md](HISTORY.md) for what's been built
 
 ## Where we are
 
-3,820 tests, 86 conformance programs, 34 examples, 13 spec chapters.
+3,825 tests, 86 conformance programs, 34 examples, 13 spec chapters.
 
 ## What's next
 

TESTING.md

@@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d
 
 | Metric | Value |
 |--------|-------|
-| **Tests** | 3,820 across 29 files (~51,141 lines of test code; 3,806 passed, 14 skipped) |
+| **Tests** | 3,825 across 29 files (~51,234 lines of test code; 3,811 passed, 14 skipped) |
 | **Compiler code coverage** | 96% of 15,149 statements (CI minimum: 80%) |
 | **Conformance programs** | 86 programs across 9 spec chapters, validating every language feature |
 | **Example programs** | 34, all validated through `vera check` + `vera verify` |
@@ -56,7 +56,7 @@ python scripts/fix_allowlists.py --fix               # auto-fix stale allowlists
 |------|------:|------:|----------------|
 | `test_parser.py` | 128 | 968 | Grammar rules, operator precedence, parse errors |
 | `test_ast.py` | 127 | 1,130 | AST transformation, node structure, serialisation, string escape sequences, ability declarations |
-| `test_checker.py` | 516 | 5,822 | Type synthesis, slot resolution, effects, effect subtyping, contracts, exhaustiveness, cross-module typing, visibility, error codes, string built-ins, generic rejection, IO operation types, Markdown types, Regex types, abilities, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, removed legacy name regression |
+| `test_checker.py` | 521 | 5,939 | Type synthesis, slot resolution, effects, effect subtyping, contracts, exhaustiveness, cross-module typing, visibility, error codes, string built-ins, generic rejection, IO operation types, Markdown types, Regex types, abilities, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, removed legacy name regression |
 | `test_verifier.py` | 145 | 2,079 | Z3 verification, counterexamples, tier classification, call-site preconditions, branch-aware preconditions, pipe operator, cross-module contracts, match/ADT verification, decreases verification, mutual recursion, refined Bool/String/Float64 param sorts, **@Nat subtraction underflow obligation** (#520 — Path-A obligation discharge via requires/path-conditions/path-aware Z3 refutation, pure-literal exclusion, Int-Int and Nat-Int → Int exemptions) |
 | `test_codegen.py` | 1,101 | 18,191 | WASM compilation, arithmetic, Float64, Byte, arrays (incl. compound element types), ADTs, match (incl. nested patterns), generics, State\<T\>, Exn\<E\> handlers, control flow, strings, string escape sequences, IO (read\_line, read\_file, write\_file, args, exit, get\_env, sleep, time, stderr), bounds checking, quantifiers, assert/assume, refinement type aliases, pipe operator, string built-ins, built-in shadowing, parse\_nat Result, GC, Markdown host bindings, Regex host bindings, Map collection, Set collection, Decimal type, Json type, Html type, Http effect, Inference effect, Random effect, example round-trips, GC shadow stack overflow, **WASM tail-call optimization** (#517 — `return_call` emission for tail-position calls, 50K- and 1M-iteration stress, structural assertions on `return_call`/plain `call` boundary, allocating-function fallback, postcondition-fallback regression, analyzer unit tests covering Block-trailing / IfExpr-both-branches / MatchExpr-arm-bodies / let-value-NOT-marked / call-args-NOT-marked / ExprStmt-statement-NOT-marked / IfExpr-condition-NOT-marked / MatchExpr-scrutinee-NOT-marked) |
 | `test_codegen_contracts.py` | 32 | 576 | Runtime pre/postconditions, contract fail messages, old/new state postconditions |

docs/index.html

@@ -265,7 +265,7 @@ <h1 class="hero-tagline">A programming language designed for LLMs to write, not
         <a href="/SKILL.md" rel="agent-instructions" type="text/markdown" class="btn btn-ghost">For Agents → SKILL.md</a>
       </div>
       <p class="version">
-        <span>v<a href="https://github.com/aallan/vera/releases/tag/v0.0.148">0.0.148</a></span>
+        <span>v<a href="https://github.com/aallan/vera/releases/tag/v0.0.149">0.0.149</a></span>
         <a href="https://github.com/aallan/vera/actions/workflows/ci.yml" aria-label="CI status"><img src="https://github.com/aallan/vera/actions/workflows/ci.yml/badge.svg" alt="CI" style="height:18px"></a>
       </p>
     </div>

docs/index.md

@@ -4,7 +4,7 @@
 
 From the Latin *veritas* — truth. In Vera, verification is a first-class citizen.
 
-**Current version:** [0.0.148](https://github.com/aallan/vera/releases/tag/v0.0.148)  ·  [GitHub](https://github.com/aallan/vera)  ·  [SKILL.md](https://veralang.dev/SKILL.md) (agent language reference)
+**Current version:** [0.0.149](https://github.com/aallan/vera/releases/tag/v0.0.149)  ·  [GitHub](https://github.com/aallan/vera)  ·  [SKILL.md](https://veralang.dev/SKILL.md) (agent language reference)
 
 ## Why?
 

docs/llms-full.txt

@@ -2,7 +2,7 @@
 
 > Vera is a statically typed, purely functional programming language designed for large language models to write. It uses typed slot references (@T.n) instead of variable names, requires contracts on every function, and compiles to WebAssembly.
 
-This file contains the core Vera language documentation — language reference, agent instructions, FAQ, error codes, and formal grammar — compiled into a single document. Version 0.0.148. For the full documentation index including the 13-chapter specification and supplementary docs, see llms.txt.
+This file contains the core Vera language documentation — language reference, agent instructions, FAQ, error codes, and formal grammar — compiled into a single document. Version 0.0.149. For the full documentation index including the 13-chapter specification and supplementary docs, see llms.txt.
 
 
 ========================================================================
@@ -2810,6 +2810,7 @@ Every diagnostic has a stable error code. Codes are grouped by compiler phase:
 - **E125**: Call-site effect mismatch
 - **E130**: Unresolved slot reference
 - **E131**: Result ref outside ensures
+- **E132**: Cyclic type alias
 - **E133**: Type alias arity mismatch
 - **E140**: Arithmetic requires numeric operands
 - **E141**: Arithmetic requires matching numeric types

docs/llms.txt

@@ -4,7 +4,7 @@
 
 Vera uses De Bruijn indexing for bindings: `@Int.0` is the most recent `Int` binding, `@Int.1` the one before. There are no variable names. Contracts are mandatory — every function must declare `requires(...)`, `ensures(...)`, and `effects(...)`. The Z3 SMT solver verifies contracts statically where possible; remaining contracts become runtime assertions. All side effects (IO, Http, State, Exceptions, Async, Inference, Random) are tracked in the type system via algebraic effects.
 
-Current version: 0.0.148. The reference compiler is written in Python. Install with `pip install -e .` from the repository.
+Current version: 0.0.149. The reference compiler is written in Python. Install with `pip install -e .` from the repository.
 
 ## Homepage
 

pyproject.toml

@@ -1,6 +1,6 @@
 [project]
 name = "vera"
-version = "0.0.148"
+version = "0.0.149"
 description = "Vera: a programming language designed for LLMs, with full contracts, algebraic effects, and typed slot references"
 readme = "README.md"
 license = "MIT"

tests/test_checker.py

@@ -5499,6 +5499,123 @@ def test_alias_zero_args_when_zero_expected_ok(self) -> None:
 public fn current(@Unit -> @Year)
   requires(true) ensures(true) effects(pure)
 { 2026 }
+""")
+
+    # =================================================================
+    # #648 — cyclic type aliases must produce [E132] at check time
+    # =================================================================
+
+    def test_cyclic_alias_two_way_e132(self) -> None:
+        """`type A = B; type B = A` produces [E132] at check time
+        instead of crashing codegen with RecursionError (#648).
+
+        Also pins the diagnostic *payload* (cycle path + fix
+        message) on this representative test — the other cyclic-
+        alias tests below check error_code only, since the
+        payload-shape contract is uniform across them.
+        """
+        errs = _check_err("""
+type A = B;
+type B = A;
+
+public fn id(@A -> @A)
+  requires(true) ensures(true) effects(pure)
+{
+  @A.0
+}
+""", "Cyclic type alias")
+        e132 = [e for e in errs if e.error_code == "E132"]
+        assert e132, (
+            f"Expected at least one diagnostic with error_code=E132; "
+            f"got: {[(e.error_code, e.description) for e in errs]}"
+        )
+        # Pin the cycle-path rendering in the description and the
+        # `data`-as-alternative suggestion in the fix hint.  A
+        # future refactor that changes the rendering would still
+        # emit E132 but the payload contract these messages embody
+        # — "you can tell *which* aliases form the cycle" and
+        # "here's the alternative that supports self-reference" —
+        # would silently regress without these assertions.
+        assert "A -> B -> A" in e132[0].description, (
+            f"Expected cycle path 'A -> B -> A' in description; "
+            f"got: {e132[0].description!r}"
+        )
+        assert "data" in e132[0].fix, (
+            f"Expected fix hint to suggest `data` as the alternative "
+            f"for self-referential types; got: {e132[0].fix!r}"
+        )
+
+    def test_cyclic_alias_self_e132(self) -> None:
+        """`type A = A` is the degenerate self-cycle case (#648)."""
+        errs = _check_err("""
+type A = A;
+
+public fn id(@A -> @A)
+  requires(true) ensures(true) effects(pure)
+{
+  @A.0
+}
+""", "Cyclic type alias")
+        e132 = [e for e in errs if e.error_code == "E132"]
+        assert e132, (
+            f"Expected at least one diagnostic with error_code=E132; "
+            f"got: {[(e.error_code, e.description) for e in errs]}"
+        )
+
+    def test_cyclic_alias_three_way_e132(self) -> None:
+        """`A -> B -> C -> A` three-way cycle also flagged (#648)."""
+        errs = _check_err("""
+type A = B;
+type B = C;
+type C = A;
+
+public fn id(@A -> @A)
+  requires(true) ensures(true) effects(pure)
+{
+  @A.0
+}
+""", "Cyclic type alias")
+        e132 = [e for e in errs if e.error_code == "E132"]
+        assert e132, (
+            f"Expected at least one diagnostic with error_code=E132; "
+            f"got: {[(e.error_code, e.description) for e in errs]}"
+        )
+
+    def test_cyclic_alias_refinement_e132(self) -> None:
+        """Cycles through a `RefinementType` wrapper (`type A = { @B
+        | true }; type B = A`) also flagged.  Pins the
+        `_alias_chain_target` helper's `RefinementType.base_type`
+        peeling — codegen's `_type_expr_to_wasm_type` recurses
+        through refinements unconditionally, so a cycle hidden
+        behind one is still a codegen-crash cycle (#648)."""
+        errs = _check_err("""
+type A = { @B | true };
+type B = A;
+
+public fn id(@A -> @A)
+  requires(true) ensures(true) effects(pure)
+{
+  @A.0
+}
+""", "Cyclic type alias")
+        e132 = [e for e in errs if e.error_code == "E132"]
+        assert e132, (
+            f"Expected at least one diagnostic with error_code=E132; "
+            f"got: {[(e.error_code, e.description) for e in errs]}"
+        )
+
+    def test_acyclic_alias_chain_ok(self) -> None:
+        """`type IntAlias = Int; type Pair = IntAlias` is an
+        acyclic chain — must pass without false-positive E132 (#648)."""
+        _check_ok("""
+type IntAlias = Int;
+type Pair = IntAlias;
+
+public fn id(@Pair -> @Pair)
+  requires(true) ensures(true) effects(pure)
+{
+  @Pair.0
+}
 """)
 
     # Line 84: Array/Tuple without type_args