sequenceDiagram
    participant Program as Program AST
    participant Prelude as Prelude (inject_prelude)
    participant Codegen as Codegen (compile_program)
    participant Reg as RegistrationMixin (_register_builtin_adts)

    Program->>Prelude: provide AST with user declarations
    activate Prelude
    Note over Prelude: compute user_defined_data_names<br/>verify _has_standard_option/_has_standard_result
    Prelude->>Prelude: prepend ADT decls (Option, Result, Ordering, UrlParts)
    Prelude->>Prelude: inject combinator & array-op functions unless shadowed/non-standard
    Prelude->>Program: return augmented AST
    deactivate Prelude

    Program->>Codegen: compile augmented AST
    activate Codegen
    Codegen->>Codegen: snapshot existing_adts/existing_fns
    Codegen->>Reg: request builtin ADT registration (includes UrlParts)
    activate Reg
    Reg->>Reg: add UrlParts layout entry
    deactivate Reg
    Codegen->>Codegen: register injected DataDecls/FnDecls/TypeAliasDecls (skip duplicates)
    deactivate Codegen

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

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 90.95%. Comparing base (d7fec62) to head (4863250).
⚠️ Report is 8 commits behind head on main.

@@            Coverage Diff             @@
##             main     #323      +/-   ##
==========================================
+ Coverage   90.91%   90.95%   +0.03%     
==========================================
  Files          45       45              
  Lines       15394    15416      +22     
==========================================
+ Hits        13996    14021      +25     
+ Misses       1398     1395       -3     

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

@coderabbitai Any comments?

#!/bin/bash
# Show the diff for vera/prelude.py and vera/codegen/core.py on this PR branch
git diff origin/main...HEAD -- vera/prelude.py vera/codegen/core.py

#!/bin/bash
# Show prelude.py with line numbers around the new additions
cat -n vera/prelude.py | sed -n '237,290p'
echo "---"
cat -n vera/prelude.py | sed -n '290,380p'
echo "---"
# Show core.py with line numbers around the new block
cat -n vera/codegen/core.py | sed -n '155,175p'

#!/bin/bash
# Check if _has_nonstandard_data is called anywhere
rg "_has_nonstandard_data" -n

echo "==="
# Check the guard in core.py - what's in existing_adts before inject_prelude runs?
# Look at _register_data and _adt_layouts to understand when it would be pre-populated
rg "_adt_layouts" -n -A2 -B2 vera/codegen/core.py | head -60

echo "==="
# Check _register_all to understand what gets registered in Pass 1
rg "_register_all\|_register_data" -n vera/codegen/core.py | head -30

@aallan: I've dug into both files to trace the specific gaps. Here's the breakdown:

vera/prelude.py — 6 missing lines

Primary issue: _has_nonstandard_data is dead code.

# vera/prelude.py lines 240–247
def _has_nonstandard_data(program: ast.Program, name: str) -> bool:
    """Check if the program defines a data type with the given name
    that does NOT match the standard prelude shape."""
    for tld in program.declarations:
        decl = tld.decl
        if isinstance(decl, ast.DataDecl) and decl.name == name:
            return True
    return False

A rg search confirms this function is defined but never called anywhere in the codebase. The def line itself runs at import time and counts as covered, but the body lines are marked uncovered if the function is never called. That accounts for 5 of the 6 missing lines (lines 243–247). The function looks like a leftover from a refactor — the actual injection logic pivots on _has_standard_option / _has_standard_result and _user_defined_data_names instead.

The 6th missing line is most likely the continue # User's data type shadows the prelude's branch at line 368 of inject_prelude (the case where a user-defined DataDecl name collides with a prelude ADT name) not being exercised through a code path that Codecov measures.

Recommended fix:

• Either remove _has_nonstandard_data (it duplicates what _user_defined_data_names already provides), or wire it up if it was intended to replace one of the isinstance checks.
• Add a test_prelude.py case that verifies a program defining e.g. data Option<T> { None, Just(T) } (non-standard shape) doesn't get a shadowed combinator injected, exercised through inject_prelude directly.

vera/codegen/core.py — 1 missing line

# core.py lines 162–164
elif isinstance(decl, ast.DataDecl):
    if decl.name not in existing_adts:
        self._register_data(decl)  # ← line 164, likely uncovered branch

existing_adts is captured from self._adt_layouts before inject_prelude runs, so the prelude DataDecls (Option, Result, Ordering, UrlParts) are always new and always hit line 164. The uncovered path is the False branch of the guard — i.e., a user-defined ADT that was already registered in Pass 1 is encountered again in the post-injection loop. There's no unit test that drives CodeGenerator through the full compile path with a user-defined data declaration that shadows a prelude type (e.g. data Option<T> { None, Just(T) } compiled end-to-end).

Recommended fix: Add a codegen-level test (or conformance test) that compiles a program containing a user-defined ADT with a prelude-conflicting name.

Learnt from: CR
Repo: aallan/vera PR: 0
File: CLAUDE.md:0-0
Timestamp: 2026-03-20T07:33:16.947Z
Learning: When replying to CodeRabbit review comments, prefix replies with `coderabbitai` so the bot registers the interaction

Learnt from: CR
Repo: aallan/vera PR: 0
File: SKILL.md:0-0
Timestamp: 2026-03-20T07:33:01.566Z
Learning: Applies to **/*.vera : When calling option and result combinators, use typed bindings when the type variable appears only in the return position (e.g., use `let Option<Int> = None;` before calling `option_map`)

Codecov coverage addressed in 79b4511:

• Removed unused _has_nonstandard_data helper (was dead code hurting patch coverage)
• Added 3 new tests exercising the non-standard Result and extra-constructor branches in _has_standard_option/_has_standard_result
• Patch coverage for vera/prelude.py now at 97% (3 remaining uncovered lines are edge cases: user-defined type alias shadowing and early return when everything is shadowed)

@coderabbitai Regarding the atomic bundle injection concern (lines 337-357):

The current design is intentional and has two layers of protection:

1. Bundle-level gate (lines 347-367): The issubset check skips the entire bundle only when the user has defined ALL functions in the group. This prevents partial injection of the source text.

2. Declaration-level filter (lines 374-384): After parsing, individual declarations are filtered out if the user shadows them by name. So if a user defines array_map_go but not array_map, the prelude injects array_map (which calls array_map_go), but the prelude's array_map_go is skipped — the user's version is used.

This is correct behavior: array_map calling the user's array_map_go will fail at type-check time if signatures don't match, which is the right outcome. The internal helpers (array_map_go, OptionMapFn) are private implementation details — a user defining them is deliberately shadowing and should get type errors if incompatible.

Making bundles fully atomic would be worse: if a user defines just array_map (a reasonable name), we'd skip ALL array operations including array_filter and array_fold, which would be surprising.

@coderabbitai Regarding the atomic bundle injection concern (lines 337-357):

The current design is intentional and has two layers of protection:

1. Bundle-level gate (lines 347-367): The issubset check skips the entire bundle only when the user has defined ALL functions in the group.

2. Declaration-level filter (lines 374-384): After parsing, individual declarations are filtered out if the user shadows them by name. So if a user defines array_map_go but not array_map, the prelude injects array_map (which calls array_map_go), but the prelude array_map_go is skipped and the user version is used.

This is correct: array_map calling a user array_map_go will fail at type-check time if signatures mismatch, which is the right outcome. Making bundles fully atomic would be worse: if a user defines just array_map (a reasonable name), we would skip ALL array operations including array_filter and array_fold.

@coderabbitai Regarding core.py line 164 coverage gap:

Investigated — this line (self._register_data(decl)) is architecturally unreachable in the current codebase. All four prelude ADTs (Option, Result, Ordering, UrlParts) are already pre-registered by _register_builtin_adts() in Pass 1, so when the Pass 1.2 loop encounters them, decl.name is always in existing_adts and the registration is skipped. The guard exists as a safety net for future prelude ADTs that might not be pre-registered.

The remaining uncovered lines in prelude.py (268, 384, 392) are similarly edge cases: user-defined type alias shadowing and the early return when every prelude declaration is shadowed. These are correct but rare paths that would require contrived test programs to exercise.

@aallan: That's a clear and well-reasoned design. The two-layer separation makes sense — bundle-level gating on the full set prevents injecting source text with broken internal references, while declaration-level filtering handles partial shadowing at parse time without over-suppressing unrelated operations. The type-checker as a correctness backstop for mismatched array_map_go signatures is the right contract boundary. I'm satisfied with the explanation.

Learnt from: aallan
URL: https://github.com/aallan/vera/pull/323

Timestamp: 2026-03-20T09:04:03.159Z
Learning: In `vera/prelude.py`, the prelude bundle injection uses a deliberate two-layer design:
1. **Bundle-level gate** (lines ~347–367): the `issubset` check skips parsing/injecting an entire source bundle only when the user has defined ALL public functions in that group, preventing partial source-text injection with broken internal references.
2. **Declaration-level filter** (lines ~374–384): after parsing, individual declarations are skipped if the user has defined a name that shadows them. This means a user defining only `array_map_go` (an internal helper) will get prelude `array_map` injected (which calls their `array_map_go`), and a type error fires if signatures are incompatible.
Making bundles fully atomic would be incorrect: a user defining `array_map` alone would suppress `array_filter` and `array_fold`, which is surprising and undesirable.

@aallan: That design rationale is clear and well-reasoned. The two-layer approach is the correct trade-off here:

• Bundle gate as a coarse filter: skipping only when all members are user-defined avoids silently suppressing unrelated operations (e.g. not killing array_filter/array_fold just because the user happened to name something array_map).
• Per-declaration filter as the precise override: lets individual internal helpers (array_map_go, OptionMapFn, etc.) be shadowed without pulling down the whole bundle, with the type-checker acting as the correctness backstop if signatures mismatch.

The type-error-on-mismatch safety net is exactly the right contract for a language with mypy-clean codegen. No changes needed here.

Learnt from: aallan
URL: https://github.com/aallan/vera/pull/323

Timestamp: 2026-03-20T09:04:13.416Z
Learning: In `vera/prelude.py`, the prelude bundle injection uses a deliberate two-layer design:
1. **Bundle-level gate** (around lines 347-367): an `issubset` check skips an entire bundle (e.g. all array ops) only when the user has defined ALL functions in the group — prevents partial injection of the bundle's source text.
2. **Declaration-level filter** (around lines 374-384): after parsing the bundle source, individual declarations are filtered out if the user already defines a declaration with that name — so partial shadowing of internal helpers (e.g. `array_map_go`) is supported. The prelude's public function (e.g. `array_map`) is still injected and will call the user's version; a signature mismatch is caught at type-check time.
Making bundles fully atomic (skip all if any member is shadowed) is intentionally avoided because a user defining `array_map` should not suppress `array_filter`/`array_fold`.

@aallan: That's a clean architectural explanation — thanks for tracing it through. The invariant makes sense: since _register_builtin_adts() runs in Pass 1 and covers all current prelude ADTs, the not in existing_adts branch on line 164 is genuinely unreachable today and the guard is purely forward-compatibility scaffolding.

For the remaining gaps, the standard Python idiom for intentional defensive guards / unreachable-by-design branches is # pragma: no cover with an inline rationale comment, which keeps the coverage signal clean without forcing contrived test programs:

# vera/codegen/core.py
elif isinstance(decl, ast.DataDecl):
    if decl.name not in existing_adts:  # pragma: no cover — safety net for future prelude ADTs not pre-registered by _register_builtin_adts
        self._register_data(decl)

# vera/prelude.py  (lines 268, 384, 392 — type-alias shadowing and all-shadowed early return)
if ...:  # pragma: no cover — reached only when user shadows every prelude declaration
    return

This is purely cosmetic/metrics hygiene — no obligation to change it if you'd rather leave the guards uncommented and accept the small coverage delta.

Learnt from: aallan
URL: https://github.com/aallan/vera/pull/323

Timestamp: 2026-03-20T09:04:28.773Z
Learning: In vera/codegen/core.py, the `self._register_data(decl)` branch inside the post-prelude-injection loop (guarded by `decl.name not in existing_adts`) is architecturally unreachable: all four current prelude ADTs (Option, Result, Ordering, UrlParts) are already pre-registered by `_register_builtin_adts()` in Pass 1, so the guard always evaluates to False. The guard is a forward-compatibility safety net for future prelude ADTs that might not be pre-registered.

Learnt from: aallan
URL: https://github.com/aallan/vera/pull/323

Timestamp: 2026-03-20T09:04:28.773Z
Learning: In vera/prelude.py, the uncovered lines (user-defined type alias shadowing path and the early-return-when-every-prelude-declaration-is-shadowed path) are correct but rare edge cases that would require contrived test programs to exercise. They are intentional defensive guards, not missing test coverage.

@coderabbitai Both findings from review 3980380566 addressed in 4863250:

1. README.md: v0.0.92 -> v0.0.93 in the active development paragraph
2. test_prelude.py: tightened shadowing test — now asserts exactly one user-defined option_map (forall_vars is None) and verifies prelude versions have forall_vars set

@aallan: Confirmed — both fixes look correct:

1. README.md — version string aligned with pyproject.toml and vera/__init__.py.
2. test_prelude.py — the tightened shadowing assertion is a meaningful improvement: distinguishing user-defined option_map (no forall_vars) from prelude-injected versions (with forall_vars set) gives the test real structural teeth rather than just a name-presence check.

Thanks for the thorough follow-through on both.

Learnt from: aallan
Repo: aallan/vera PR: 0
File: :0-0
Timestamp: 2026-03-20T09:04:28.773Z
Learning: In vera/prelude.py, the uncovered lines (user-defined type alias shadowing path and the early-return-when-every-prelude-declaration-is-shadowed path) are correct but rare edge cases that would require contrived test programs to exercise. They are intentional defensive guards, not missing test coverage.

Learnt from: aallan
Repo: aallan/vera PR: 0
File: :0-0
Timestamp: 2026-03-20T09:04:03.159Z
Learning: In `vera/prelude.py`, the prelude bundle injection uses a deliberate two-layer design:
1. **Bundle-level gate** (lines ~347–367): the `issubset` check skips parsing/injecting an entire source bundle only when the user has defined ALL public functions in that group, preventing partial source-text injection with broken internal references.
2. **Declaration-level filter** (lines ~374–384): after parsing, individual declarations are skipped if the user has defined a name that shadows them. This means a user defining only `array_map_go` (an internal helper) will get prelude `array_map` injected (which calls their `array_map_go`), and a type error fires if signatures are incompatible.
Making bundles fully atomic would be incorrect: a user defining `array_map` alone would suppress `array_filter` and `array_fold`, which is surprising and undesirable.

Learnt from: aallan
Repo: aallan/vera PR: 0
File: :0-0
Timestamp: 2026-03-20T09:04:13.416Z
Learning: In `vera/prelude.py`, the prelude bundle injection uses a deliberate two-layer design:
1. **Bundle-level gate** (around lines 347-367): an `issubset` check skips an entire bundle (e.g. all array ops) only when the user has defined ALL functions in the group — prevents partial injection of the bundle's source text.
2. **Declaration-level filter** (around lines 374-384): after parsing the bundle source, individual declarations are filtered out if the user already defines a declaration with that name — so partial shadowing of internal helpers (e.g. `array_map_go`) is supported. The prelude's public function (e.g. `array_map`) is still injected and will call the user's version; a signature mismatch is caught at type-check time.
Making bundles fully atomic (skip all if any member is shadowed) is intentionally avoided because a user defining `array_map` should not suppress `array_filter`/`array_fold`.

Learnt from: aallan
Repo: aallan/vera PR: 0
File: :0-0
Timestamp: 2026-03-20T09:04:28.773Z
Learning: In vera/codegen/core.py, the `self._register_data(decl)` branch inside the post-prelude-injection loop (guarded by `decl.name not in existing_adts`) is architecturally unreachable: all four current prelude ADTs (Option, Result, Ordering, UrlParts) are already pre-registered by `_register_builtin_adts()` in Pass 1, so the guard always evaluates to False. The guard is a forward-compatibility safety net for future prelude ADTs that might not be pre-registered.

Learnt from: CR
Repo: aallan/vera PR: 0
File: SKILL.md:0-0
Timestamp: 2026-03-20T07:33:01.566Z
Learning: Applies to **/*.vera : When calling option and result combinators, use typed bindings when the type variable appears only in the return position (e.g., use `let Option<Int> = None;` before calling `option_map`)