Skip to content

feat(types,hir,mir,codegen): Optional[int] flow-sensitive narrowing (D-199, Part 2 of #747) - #780

Open
rotnov wants to merge 20 commits into
mainfrom
feat/issue-769-optional-narrowing
Open

feat(types,hir,mir,codegen): Optional[int] flow-sensitive narrowing (D-199, Part 2 of #747)#780
rotnov wants to merge 20 commits into
mainfrom
feat/issue-769-optional-narrowing

Conversation

@rotnov

@rotnov rotnov commented Aug 25, 2026

Copy link
Copy Markdown
Owner

Outstanding gate before merge (D-068): the pinned local reviewer
(ievo:deep-review) has not been run against this branch. Skill(skill: "ievo:deep-review") refuses model invocation
(disable-model-invocation: true; "reserved for explicit user invocation")
and this dispatched session has no Task/Agent-style tool to route
around that block — the identical capability gap already logged for
#763/PR #770 (docs/AGENT_RETROSPECTIVE.md, "2026-08-24 — A dispatched
subagent cannot satisfy D-068's local-reviewer dispatch requirement"). A
session that can invoke /ievo:deep-review needs to run it against the
full committed range and resolve any actionable findings before this
merges.

Summary

Implements flow-sensitive Optional[int] narrowing on a top-level
if name is None: / if name is not None: test — Part 2 of #747,
following on from #763/PR #770 (Part 1). Fixes #769.

  • pycc_hir::optional_none_test / pycc_hir::definitely_terminates: a
    shared, environment-independent narrowing-test recognizer and a strict
    terminator predicate, consumed directly by pycc_mir (which cannot
    depend on pycc_types) and re-exported thinly by pycc_types::narrow.
  • pycc_types: overlay-based narrowing state on Environment (clone/
    discard join semantics), applied both to if bodies and to the
    early-return-narrows-the-continuation shape (a guard clause whose body
    definitely terminates narrows every read after it).
  • pycc_mir: a $narrowed:{name} scope-sentinel on the existing scopes
    stack, plus narrowing_snapshot/restore_narrowing/lower_scoped_body
    to recreate the checker's clone-and-discard semantics on MIR's single
    shared scope frame. Deviation from the original dispatched design,
    made and flagged per this task's own "resolve autonomously, flag the
    deviation" instruction: without this, narrowing established inside a
    nested body (e.g. a while loop inside a narrowed if) could leak past
    that body's own close on MIR's shared-frame model, which the checker's
    own clone-and-discard Environment never allows. Covered directly by
    a_nested_scoped_body_entered_while_already_narrowed_still_sees_the_narrowing
    in crates/pycc_mir/src/tests/narrow.rs.
  • MirExpr::OptionalUnwrap (read-side counterpart of OptionalWrap),
    lowered to a single borrowed build_extract_value in codegen — no
    retain at the unwrap site itself. bigint_rc.rs's existing
    retain_if_int_duplicate/int_value_is_a_duplicate_reference
    duplicate-reference classification gained an OptionalUnwrap arm so a
    bigint payload duplicated out of a narrowed binding into a second name
    is still correctly refcounted.
  • docs/decisions/D-199-optional-t-flow-sensitive-narrowing-part2.md,
    docs/TYPE_SYSTEM.md, docs/ROADMAP.md, and
    tests/fixtures/conformance-breadth-manifest.json updated (the
    manifest's narrowing row flips to proven, its existing subset
    marker left unpromoted).

Deliberately out of scope (documented in D-199/TYPE_SYSTEM.md/the
manifest): compound conditions (and/or), narrowing to None itself,
raise as an additional terminator alongside return, and any test more
complex than a top-level is/is not None comparison.

D-014 coverage gate

cargo llvm-cov --workspace --fail-under-lines 100 --fail-under-regions 100
initially failed at 1 missed region
(crates/pycc_codegen/src/bigint_rc.rs:281, the new OptionalUnwrap arm).
Root cause: Cargo compiles pycc_codegen under several distinct metadata
hashes depending on which package links it, and the one uncovered
instantiation (shared by issue_382_exceptions, slice1_codegen_depth,
and the pycc binary) is only reached when a bigint-valued narrowed
Optional[int] read is duplicated into a second binding — the fixture
extension alone didn't close it locally because that scenario in
pep_0604_union.py only reaches this instantiation through
tests/conformance.rs's CPython-oracle comparison, which is skipped
without a pinned python3.14 on PATH. Fixed with
tests/issue_769_optional_narrowing.rs, an oracle-independent
build-and-run integration test (bigint duplicate-binding, smallint
mirror, absent-optional cases), plus the same scenario added to
pep_0604_union.py for when the oracle is available. Final coverage: 0
missed lines/regions/functions across 42836 regions.

Testing

  • cargo test -p pycc_hir --lib: 648 passed, 0 failed.
  • cargo llvm-cov --workspace --fail-under-lines 100 --fail-under-regions 100:
    exit 0, 0 missed lines/regions/functions.
  • cargo test --workspace: 60 test result: ok blocks, 0 failures.
  • ruby scripts/check_roadmap_evidence.rb: passed.
  • python3 scripts/generate_decisions_index.py docs/decisions docs/decisions/README.md --check: up to date.

See docs/sessions/2026-08-25-02-issue-769-optional-narrowing-part2.md
for the full session record.

🤖 Generated with Claude Code

rotnov and others added 8 commits August 25, 2026 06:01
Adds the MIR and codegen halves of flow-sensitive `Optional[int]`
narrowing, on top of the already-merged checker layer:

- pycc_hir::definitely_terminates: extracted as a shared predicate
  (used by both pycc_types::narrow and pycc_mir) since pycc_mir cannot
  depend on pycc_types.
- pycc_mir: MirExpr::OptionalUnwrap (read-side counterpart of
  OptionalWrap), a $narrowed:{name} scope sentinel threaded through
  lower_stmt, and the early-return continuation shape
  (apply_post_if_narrowing / lower_stmt_sequence) mirroring the
  checker's own mechanism.
- pycc_mir: lower_scoped_body isolates narrowing state around every
  *nested* body (if/while/for/try/except/finally/match arms) via a
  snapshot/restore of the $narrowed: sentinel subset, since MIR's
  scopes stack is one shared mutable per-function frame rather than
  per-branch Environment clones like the checker's overlay design --
  without this, narrowing established by a nested early-return guard
  would leak past its own enclosing body. Caught via end-to-end
  execution of the extended fixture, not by a unit test alone; a
  dedicated regression test now covers it directly.
- pycc_codegen: OptionalUnwrap emission (extract_value on the
  Optional struct's payload field) plus the two separate refcount
  classification predicates in bigint_rc.rs (retain_if_int_duplicate's
  own inline match is the one that actually emits the retain call,
  distinct from int_value_is_a_duplicate_reference).
- tests/fixtures/pep_0604_union.py extended with narrowed-use rungs;
  verified byte-for-byte against local CPython 3.14.6 output and
  against the compiled pycc binary.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…narrowing

Documents the flow-sensitive Optional narrowing design (overlay-based
checker state, shared pycc_hir recognizer, MIR scope-sentinel isolation)
and flips the narrowing row in the conformance-breadth manifest to proven
without promoting its subset marker.
Adds direct unit tests for branches that real type-checked programs
cannot reach but that the checker/MIR still code defensively:
- narrow.rs's narrowing_target on a wholly unbound name
- stmt.rs's is-None test on a non-Optional name (narrows neither branch)
- lib.rs's early-return guard on a non-Optional name, and a nested
  scoped body entered while already narrowed
- hir::definitely_terminates's full &&-chain truth table
crates/pycc_codegen/src/bigint_rc.rs's retain_if_int_duplicate has a
distinct compiled instantiation (shared by issue_382_exceptions,
slice1_codegen_depth, and the pycc binary) whose own test traffic never
duplicated a narrowed Optional[int] bigint payload into a second
binding -- the one path that actually reaches its OptionalUnwrap arm.
tests/fixtures/pep_0604_union.py's own narrowing coverage runs only
through tests/conformance.rs's CPython byte-for-byte oracle comparison,
which this environment skips whenever python3.14 isn't on PATH, so it
never contributed to that instantiation's counters here.

Adds tests/issue_769_optional_narrowing.rs: an oracle-independent,
self-contained integration test (same build-and-run pattern as
tests/issue_770_optional_reassignment.rs) that builds and runs a
bigint-payload narrowed duplicate-binding scenario directly, plus a
smallint mirror case and an absent-optional case. Also extends
tests/fixtures/pep_0604_union.py with the same bigint duplicate-binding
scenario so the oracle-backed conformance comparison exercises it too
when the pinned CPython oracle is available.

Full `cargo llvm-cov --workspace --fail-under-lines 100
--fail-under-regions 100` now reports 0 missed lines/regions/functions
across 42836 regions.
Records the implementation, the D-014 coverage-gap diagnosis and fix,
and the D-068 dispatch-capability gap (Skill(ievo:deep-review) refuses
model invocation in this dispatched-subagent context, matching the
identical lesson already logged for #763/PR #770) that leaves review
and merge for a session that can actually run /ievo:deep-review.
@chatgpt-codex-connector

Copy link
Copy Markdown

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.
To continue using code reviews, add credits to your account and enable them for code reviews in your settings.

rotnov and others added 2 commits August 25, 2026 09:16
Finding 1 (blocker, soundness): join_if_branches/join_loop_body/
join_match_branches (pycc_types) and lower_scoped_body's join call sites
(pycc_mir) discarded a narrowing kill from a reassignment inside a nested
branch, letting a stale Optional narrowing survive past that branch's own
close (e.g. `if x is not None: if flag: x = None; print(x + 1)` was
incorrectly accepted). Both crates now reconcile sibling-branch narrowing
states via a sound conservative intersection (a name stays narrowed only
if every supplied branch narrows it to the exact same type): pycc_types
gains narrow::join_narrowed, pycc_mir gains its independent
lib.rs::join_narrowed twin, and lower_scoped_body now returns each nested
body's own ending narrowed state so If/While/ForRange/ForList in stmt.rs
can join branches and re-apply the reconciled result; match/try call
sites are unchanged (deliberately out of scope -- MIR only lowers HIR the
now-sound checker already accepted, and the checker's own join fix for
match/try is a provable subset of "unconditionally keep pre-branch
state"). Verified end-to-end: `pycc check` correctly rejects the blocker
repro with T0021.

Finding 2 (warning, completeness): the checker's if/while fast-path
helpers (check_if_branches_in_place, check_while_body_in_place, and their
_in_function twins) bypassed narrowing-aware statement processing,
spuriously rejecting a nested early-return guard inside an unrelated
outer if. They now route through narrow::check_stmt_sequence /
check_stmt_sequence_in_function like the slow path already did. Verified
end-to-end: `pycc run` on the reported shape now builds and produces the
expected output.

Regression tests: two new pycc_mir::tests::narrow cases proving a
reassignment inside a nested if/while kills narrowing past the nested
body's own close, and seven new pycc_types checker-level tests covering
both findings plus join-reconciliation edge cases (mixed-type sibling
narrowing, partial narrowing across branches).

Also fixes two pre-existing clippy::ptr_arg errors in
apply_post_if_narrowing/restore_narrowing (crates/pycc_mir/src/lib.rs),
confirmed via live CI logs to already exist on the pushed branch before
this pass and to be blocking build-test-coverage/native-build-test/
ci-gate regardless of the review findings; narrowed from &mut Vec<...> to
&mut [...] since neither function calls a Vec-specific method.

cargo test --workspace: 0 failures. cargo llvm-cov --workspace
--fail-under-lines 100 --fail-under-regions 100: 100.00% lines /
100.00% regions (42894 regions, 27848 lines, 0 missed).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
docs/ROADMAP.md's and docs/PYTHON_STANDARDS.md's #769 additions (from
d3ae62f) pushed the llms.txt non-optional-expansion aggregate
(scripts/check-site.sh, issue #207) from 260922 bytes -- already only
1222 bytes under the 262144-byte (256 KiB) ceiling on main -- to 264533
bytes, a genuine PR-caused regression confirmed via live CI logs on the
already-pushed branch (the "build" job's "Validate website" step).
Trimmed both entries to the essential facts (mechanism summary, D-199
pointer, evidence citation) without dropping any distinct claim; local
`GITHUB_PAGES=true sh scripts/check-site.sh` now passes at 261976 bytes.

The remaining 168-byte margin is thin -- worth a follow-up (either a
policy to keep future ROADMAP.md feature-landing paragraphs terser, or
revisiting the 256 KiB ceiling) but out of scope for this review-response
pass.

`ruby scripts/check_roadmap_evidence.rb` still passes after the trim.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@rotnov

rotnov commented Aug 25, 2026

Copy link
Copy Markdown
Owner Author

D-068 review response (98e8c41, b7d0340)

Addressed the pinned ievo:deep-reviewer pass on this branch. Summary below; does not merge.

Finding 1 (blocker, soundness) — fixed

join_if_branches/join_loop_body/join_match_branches (crates/pycc_types/src/lib.rs) and lower_scoped_body's join call sites (crates/pycc_mir/src/lib.rs) discarded a narrowing kill caused by a reassignment inside a nested branch, so a stale Optional narrowing could survive past that branch's own close — e.g.

def f(x: int | None, flag: bool) -> None:
    if x is not None:
        if flag:
            x = None
        print(x + 1)   # unsound: x could be None here

was previously accepted. Both crates now reconcile sibling-branch narrowing via a sound conservative intersection: a name stays narrowed only if every supplied branch narrows it to the exact same type. pycc_types gains narrow::join_narrowed; pycc_mir gains an independent join_narrowed twin (kept separate rather than shared, matching the existing pycc_hir-only-shares-what-both-need precedent, since pycc_mir doesn't depend on pycc_types). lower_scoped_body now returns each nested body's own ending narrowed state so If/While/ForRange/ForList in stmt.rs can join branches and re-apply the reconciled result. match/try call sites are unchanged deliberately: MIR only lowers HIR the now-sound checker already accepted, and the checker's fixed join rule for match/try is a provable subset of "unconditionally keep pre-branch state," so no soundness gap remains there.

Design tradeoff: intersection is not maximally precise (it doesn't special-case an unconditionally-terminating branch the way the ordinary .bindings join does), but it can only shrink or preserve the narrowing set relative to the old always-keep-pre-branch behavior — never grow it — so it cannot introduce new unsoundness. Chosen over a more precise but more intricate join because correctness was the review's actual bar.

Regression tests: pycc_mir::tests::narrow::a_reassignment_inside_a_nested_if_kills_narrowing_past_the_nested_ifs_own_close and a_reassignment_inside_a_nested_while_kills_narrowing_past_the_loops_own_close.

End-to-end verification beyond unit tests: pycc check on the exact repro above now correctly emits error[T0021]: operator Add is not defined for 'int | None' and 'int'.

Finding 2 (warning, completeness) — fixed

The checker's if/while fast-path helpers (check_if_branches_in_place, check_while_body_in_place, and their _in_function twins) bypassed narrowing-aware statement processing, spuriously rejecting a nested early-return guard inside an unrelated outer if, e.g.:

def f(cond: bool, x: int | None) -> int:
    if cond:
        if x is None:
            return 0
        return x
    return 0

All four now route through narrow::check_stmt_sequence/check_stmt_sequence_in_function, matching the slow/clone path's existing behavior.

Regression tests: 7 new checker-level tests in crates/pycc_types/src/tests.rs covering both findings plus join-reconciliation edge cases (mixed-type sibling narrowing, partial narrowing across branches).

End-to-end verification: pycc run on the shape above now builds and runs, printing 5, 0, 0 for f(True, 5), f(True, None), f(False, None).

Finding 3 (doc drift) — no change needed

Checked tests/fixtures/conformance-breadth-manifest.json and D-199's Consequences section against the fixed behavior; both are still accurate now that findings 1 & 2 are resolved.

Incidental fixes (discovered while verifying this branch would actually pass CI)

  • Pre-existing clippy::ptr_arg CI failure in apply_post_if_narrowing/restore_narrowing (crates/pycc_mir/src/lib.rs), confirmed via live CI logs to already exist on the pushed branch before this review pass (traces to 14535c9, part of the original Optional[int] is None / is not None flow-sensitive narrowing (Part 2 of #747) #769 feature work), blocking build-test-coverage, native-build-test (all 4 platforms), and ci-gate regardless of the review findings. Fixed by narrowing both signatures from &mut Vec<HashMap<String, Ty>> to &mut [HashMap<String, Ty>] (verified neither function calls a Vec-specific method). cargo clippy --workspace --all-targets -- -D warnings now passes clean.
  • llms.txt budget regression (D-207): this branch's own docs/ROADMAP.md/docs/PYTHON_STANDARDS.md additions pushed the non-optional-expansion aggregate from 260,922 bytes (main, already only 1,222 bytes under the 262,144-byte ceiling) to 264,533 bytes — a genuine PR-caused regression, not pre-existing. Trimmed both entries to the essential facts; local GITHUB_PAGES=true sh scripts/check-site.sh now passes at 261,976 bytes. The remaining 168-byte margin is thin — worth a follow-up (terser future roadmap entries, or revisiting the 256 KiB ceiling) but out of scope here; noting it rather than filing a new issue since it's a one-line heads-up, not an actionable defect yet.
  • status-page-freshness still fails (this branch's ROADMAP.md change wasn't mirrored into site/status/index.html/site/index.html, per issue P1: Keep the GitHub Pages status/roadmap page in sync on every PR #401/D-156), but that workflow is explicitly documented as not yet a required branch-protection check, so it's flagged here rather than fixed to avoid scope creep into rewriting the status page.

Gate results

  • cargo test --workspace: 0 failures (all test result: lines green, including the 2 new MIR regression tests and 7 new checker tests).
  • cargo llvm-cov --workspace --fail-under-lines 100 --fail-under-regions 100: 100.00% lines / 100.00% regions (42,894 regions, 27,848 lines, 0 missed).
  • ruby scripts/check_roadmap_evidence.rb: passes.
  • GITHUB_PAGES=true sh scripts/check-site.sh: passes.
  • cargo clippy --workspace --all-targets -- -D warnings: passes.

Commits: 98e8c41 (findings 1 & 2 + clippy fix), b7d0340 (llms.txt budget trim).

Not merging — this pass fixed the previously-reviewed findings; a fresh ievo:deep-reviewer pass over these new commits is still needed before merge, and I don't have Agent-tool access in this session to dispatch it myself.

rotnov and others added 4 commits August 25, 2026 10:21
…dies (D-068 re-review of #780, third round)

Two soundness blockers found in a third D-068 pinned-reviewer round against
#780: (1) a `while`/`for` loop body read a name narrowed on loop entry even
though the loop can re-run and a later iteration's read may actually execute
after an earlier iteration's own kill of that name; (2) an `except` handler
was checked against the pre-`try` narrowed state even though the handler is
only ever entered after some (possibly partial) prefix of the `try` body
already ran, including any kill that prefix performed. Both stem from the
narrowing design's single left-to-right source-order pass silently assuming
execution order always matches source order -- true for straight-line code
and `if`/`else`, false for any re-enterable construct.

Fixed uniformly via `pycc_hir::killed_names`, a new shared primitive that
recursively collects every name a body reassigns anywhere within it, and a
new `apply_kill_prescan` in both `pycc_types::narrow` and `pycc_mir` (crate-
local, since `pycc_mir` cannot depend on `pycc_types`) that drops those
names from the narrowing overlay for the *entire* body before the normal
pass runs -- wired into every `while`/`for` loop-body and loop-test call
site (module scope, function scope, and both enum-loop helpers) and into
`check_try_stmt`'s handler-body checking in both crates. `pycc_mir::expr.rs`
has exactly one `narrowed_ty` caller, reading the same `scopes` state the
prescan mutates, so MIR eligibility tracks the checker automatically.

`crates/pycc_types/src/exception.rs` also gains a `check_stmt_sequence_shared`
helper (replacing the old per-statement `check_stmt_shared`) as the vehicle
needed to route the handler-body prescan through a sequence-aware call --
this bundles in the first half of the separate warning-finding fix (routing
`try`'s four body loops through `narrow::check_stmt_sequence[_in_function]`),
since the two changes are interleaved in the same function and cannot be
cleanly split; the second half (the `check_match` case-body routing, plus
the warning-finding regression tests) lands as a separate commit.

Both repros verified empirically against `cargo run --bin pycc` on the
pre-fix branch tip: `check` wrongly exited 0 and `run` executed rejected-in-
principle `int | None` arithmetic without a diagnostic; after this fix both
are rejected with T0021.

New tests: 3 checker-level (two rejection repros plus a completeness guard
proving the prescan does not over-drop narrowing a loop body never kills),
14 direct `pycc_hir::killed_names` unit tests pinning every `HirStmt` match
arm, and 5 MIR-level tests (loop-body read, loop-test read, except-handler
read, plus the MIR completeness guard).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…sequence (D-068 re-review of #780, third round warning finding)

`check_match`'s per-case body loop called `check_stmt`/`check_stmt_in_function`
directly per statement, bypassing `narrow::check_stmt_sequence[_in_function]`
and therefore never running `apply_post_if_narrowing` -- so a nested
early-return guard inside a `match` case body never narrowed the rest of
that same case body, the identical fast-path-bypass defect an earlier D-068
round already fixed for the `if`/`while` fast-path helpers, just never
routed through `match` in the first place. The `try`/`except`/`else`/
`finally` half of this same finding was already fixed in the previous
commit (bundled there because it was inseparable from that commit's
handler-prescan soundness fix in the same function).

New tests: five regression tests proving a nested early-return guard now
narrows the rest of its enclosing `match` case, `try` body, `except`
handler body, and `else` body, plus a sanity check that a `finally` body's
own (unrelated) narrowing behavior is unaffected by the routing change
(`finally` cannot contain a `return`, so this specific fix's own
narrowing-propagation behavior is not itself observable there).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…sequence

D-199's Consequences section claimed "a narrowing fact never survives a
reassignment of the narrowed name" without qualification -- true only for
the constructs D-199 itself covered (straight-line bodies and if/else
joins), never true in general once while/for loops and try/except handlers
entered scope, per the two counterexamples this round's soundness fix
addresses. D-199 is left unedited per this repository's decision-log
convention (never hand-edit an accepted entry); this new entry narrows its
claim and records the kill-prescan design, alternatives considered, and
consequences.

Regenerated docs/decisions/README.md via
scripts/generate_decisions_index.py. Verified D-201 is the next free
decision number: origin/main tops out at D-198, and D-199/D-200 are
already claimed by this PR (#780) and PR #786 respectively.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>


Each of three D-068 review rounds against #780 found a new instance of
the same execution-order-vs-source-order unsoundness class in Optional[T]
narrowing (loop re-entry, then except-from-mid-try) because each round
fixed only the flagged construct instead of stating and auditing the
general invariant up front. This round's D-201 states the invariant
explicitly and applies it uniformly via killed_names; the retrospective
entry records the lesson for future flow-sensitive analysis work.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@rotnov

rotnov commented Aug 25, 2026

Copy link
Copy Markdown
Owner Author

D-068 re-review round 3: kill-prescan for re-enterable narrowed bodies

This round fixes a soundness defect class in flow-sensitive Optional[T] narrowing found in two new places after two prior fix rounds already landed (through b7d03402): narrowing was established via a single left-to-right source-order pass, reconciled only at control-flow joins, which is unsound whenever a body can be entered/re-entered such that a statement earlier in execution order comes from later in source order than the read it should invalidate.

Repros verified empirically (before/after)

  1. Loop re-entryif x is not None: i=0; while i<2: print(x+1); x=None; i=i+1. Before this fix: accepted (unsound — print(x+1) on iteration 2 actually runs after iteration 1's x=None). After: rejected with T0021.
  2. except-from-mid-tryif x is not None: try: x=None; raise ValueError("boom") except ValueError: return x+1. Before: accepted (unsound — the handler is reached only after the kill inside try). After: rejected with T0021.

Both confirmed as real .py files against cargo run --bin pycc -- check/run before any code change, then reconfirmed rejected after the fix.

Also fixed (warning-severity, not soundness): match case bodies and try/except/else/finally bodies were using raw per-statement loops instead of narrow::check_stmt_sequence[_in_function], spuriously rejecting a nested early-return guard that should have narrowed the rest of the same body.

Approach taken and why

Approach 1 (kill-prescan) over Approach 2 (scope-down fallback), per the task's explicit preference. Before checking/lowering a re-enterable body, recursively collect every name that body reassigns anywhere within it (new pycc_hir::killed_names) and drop those names' narrowing overlay entries for the entire body up front — a conservative, non-fixpoint, whole-body rule. Built cleanly with zero regressions on the first attempt, so the scope-down fallback was never needed.

Implemented identically in both pycc_types (checker, via narrow::apply_kill_prescan) and pycc_mir (MIR lowering) — pycc_mir cannot depend on pycc_types, so the shared killed_names primitive lives in pycc_hir, the common dependency.

MIR/checker consistency: grepped every caller of narrowed_ty in crates/pycc_mir/src/expr.rs — exactly one call site, automatically consistent with the checker's new rule since it reads the same scopes structure apply_kill_prescan mutates.

Files and functions changed

  • crates/pycc_hir/src/lib.rs — new killed_names/collect_killed_names (canonical primitive: which statement kinds route a bare-name target through assignment/binding).
  • crates/pycc_types/src/narrow.rs — new apply_kill_prescan.
  • crates/pycc_types/src/lib.rsapply_kill_prescan wired into While/ForRange/ForList (module-scope and function-scope) and enum-loop helpers; check_match case bodies routed through narrow::check_stmt_sequence[_in_function].
  • crates/pycc_types/src/exception.rscheck_try_stmt's body/handler.body/orelse/finalbody loops routed through a new check_stmt_sequence_shared helper (replacing the old per-statement check_stmt_shared, now dead and removed); apply_kill_prescan applied to the try body before checking the handler.
  • crates/pycc_mir/src/lib.rs, crates/pycc_mir/src/stmt.rs — mirrored kill-prescan application at the equivalent MIR lowering sites.

Tests added

  • crates/pycc_types/src/tests.rs: a_narrowed_read_inside_a_while_loop_body_the_same_body_later_kills_is_rejected, an_except_handler_reached_after_a_try_body_kill_is_rejected, a_while_loop_body_that_reads_but_never_kills_the_narrowed_name_stays_narrowed (completeness guard), plus 5 warning-fix regression tests (nested_early_return_guard_narrows_the_rest_of_the_same_match_case_body, ..._the_try_body, ..._an_except_handler_body, ..._the_else_body, a_plain_narrowed_read_inside_the_finally_body_still_type_checks).
  • crates/pycc_mir/src/tests/narrow.rs: a_while_body_that_reads_then_kills_the_narrowed_name_does_not_unwrap_the_read, a_while_test_reading_a_name_the_body_kills_does_not_unwrap_the_test, a_while_body_that_reads_but_never_kills_the_narrowed_name_still_unwraps_the_read (completeness guard), an_except_handler_reached_after_a_try_body_kill_does_not_unwrap_the_read.
  • crates/pycc_hir/src/tests.rs: 14 direct unit tests for killed_names/collect_killed_names covering every statement-kind match arm, added to close a coverage gap the new function introduced.

Gates

  • cargo test --workspace: 0 failures.
  • cargo llvm-cov --workspace --fail-under-lines 100 --fail-under-regions 100: 100.00% lines / 100.00% regions, exit 0.
  • cargo clippy --workspace --all-targets -- -D warnings: exit 0.
  • ruby scripts/check_roadmap_evidence.rb: pass.
  • GITHUB_PAGES=true sh scripts/check-site.sh: pass (llms.txt budget not tripped).

Decision log

New entry D-201 narrows D-199's Consequences claim ("a narrowing fact never survives a reassignment of the narrowed name" — true only for the constructs D-199 covered, not in general once loops/try-except are in scope). D-199 itself is left unedited per this repo's decision-log convention. docs/decisions/README.md regenerated.

Retrospective

Added a 2026-08-25 entry to docs/AGENT_RETROSPECTIVE.md: three consecutive D-068 review rounds against this PR found the same defect class in new constructs because each round fixed only what was flagged instead of characterizing the general invariant up front. Lesson: audit every construct where execution order can diverge from source order as part of original design work, not reactively per review round.

Still needed before merge

Per D-068, another fresh pinned-reviewer (ievo:deep-reviewer) pass is required over this round's diff before merge, same as the prior two rounds. This session does not have Agent-tool access to invoke it directly — a session that does should run it against the current head (18f303cb) before merge. Per D-024, this PR is not being merged by this session; it is left for the repository owner / a session with reviewer access.

rotnov and others added 2 commits August 25, 2026 10:49
D-068 re-review round 4 of #780 flagged the "Narrowing & flow typing"
section as stale: it still described only D-199's original if/else
scope and never mentioned that D-201's kill-prescan (round 3) extended
narrowing survival into while/for loop bodies, try/except handlers,
and match case bodies, subject to the prescan's conservative
whole-body kill rule.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
D-068 re-review round 4 of #780 traced the actual reason a try's
finally body needs no separate kill-prescan: it is checked against
`joined`, an Environment folded from body_env (the full try-body
walk, including dead code after a raise) through join_loop_body, then
intersected with each handler's and the orelse's end-state via
join_if_branches -- and it is narrow::join_narrowed's strict
intersection, not "not a narrowing-sensitive path", that actually
excludes any name killed on any of those paths. D-201 is not yet an
accepted decision at the time of this correction -- it lands in this
same pull request -- so its own justification text is corrected in
place per this repository's append-only rule, which applies only to
already-accepted entries.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@rotnov

rotnov commented Aug 25, 2026

Copy link
Copy Markdown
Owner Author

D-068 re-review round 4: doc-completion follow-up

A fourth pinned-reviewer pass against this PR's kill-prescan soundness fix (round 3, 088ec5f0..18f303cb) returned zero blockers — "The soundness claim now holds." It found two should-fix documentation warnings and one optional, explicitly non-blocking note. This round addresses all three.

Warnings fixed

  1. docs/TYPE_SYSTEM.md's "Narrowing & flow typing" section was stale — it only described D-199's original if/else narrowing scope. Added a paragraph describing the round-3 (D-201) extension: narrowing now survives into while/for loop bodies (including the loop's own re-evaluated test), try/except handler bodies, and match case bodies, via a conservative whole-body kill-prescan (pycc_hir::killed_names) rather than a fixpoint analysis — plus a one-line note on why finally needs no separate prescan (it's checked against the strict-intersection join of the try body / handlers / orelse). Linked to D-201 following this doc's existing citation convention for other decision entries. Commit 8bab55cd.

  2. tests/fixtures/conformance-breadth-manifest.json's PEP 604 row — inspected and left unchanged. The manifest's proven bullets are strictly evidenced by a registered conformance fixture (every existing evidence value across the whole manifest is a tests/fixtures/*.py path); pep_0604_union.py itself does not exercise any loop/try/except/match narrowing. The round-3 kill-prescan capability is covered by Rust unit tests in crates/pycc_types/src/tests.rs (e.g. nested_early_return_guard_narrows_inside_an_unrelated_outer_while_in_function_scope, a_narrowed_read_inside_a_while_loop_body_the_same_body_later_kills_is_rejected, nested_early_return_guard_narrows_the_rest_of_the_same_match_case_body, nested_early_return_guard_narrows_the_rest_of_the_try_body), not by a conformance fixture, so adding a proven bullet citing pep_0604_union.py as evidence would overclaim relative to this manifest's own evidentiary discipline. No change made.

Optional item: D-201's finally justification

Corrected in place (commit ee5810ea). The reviewer traced the actual mechanism precisely: finally is checked against joined, an Environment built by folding body_env (the full try-body walk in source order, including dead code after a raise) through join_loop_body, then intersecting each handler's and the orelse's end-state via join_if_branches — and it's narrow::join_narrowed's strict intersection that actually excludes any killed name, not merely "not a narrowing-sensitive path" as D-201 previously said. Verified this against check_try_stmt in crates/pycc_types/src/exception.rs (lines 102–111) and join_narrowed's doc comment in crates/pycc_types/src/narrow.rs before editing. D-201 is not yet an accepted decision — it lands in this same PR — so AGENTS.md's append-only rule (which applies only to already-accepted entries) doesn't block correcting it in place; a superseding entry is unnecessary here.

Gates — independently re-run this round

  • cargo test --workspace: all green (1312-test unit suite plus all integration suites, 0 failed).
  • cargo clippy --workspace --all-targets -- -D warnings: clean — only the 3 pre-existing, unrelated warnings in tests/slice1_codegen_depth.rs (multi-line string escape lints), not gated, untouched.
  • cargo llvm-cov --workspace --fail-under-lines 100 --fail-under-regions 100: 100.00% lines / 100.00% regions, independently re-run (previous round's report was self-reported-only).
  • GITHUB_PAGES=true sh scripts/check-site.sh: passed, independently re-run. docs/TYPE_SYSTEM.md is not referenced by site/llms-txt-context-manifest.json's non-optional documents at all, so the doc addition carries no llms.txt byte-budget risk despite the tight margin noted in the previous round.

All commits are pushed to feat/issue-769-optional-narrowing:

  • 8bab55cd — docs(types): describe kill-prescan narrowing scope in TYPE_SYSTEM.md
  • ee5810ea — docs(decisions): correct D-201's finally-needs-no-prescan mechanism

Believed merge-ready pending the repository owner's own final look. Not merging myself per D-024.

Resolves conflicts against #774 (PEP 572 walrus operator), which merged
concurrently: both PRs added new MirExpr match arms (OptionalUnwrap vs
NamedExpr) at the same sites in bigint_rc.rs and exception.rs, and both
touched the If/While lowering arms in pycc_mir/stmt.rs and pycc_types/lib.rs
(kill-prescan narrowing vs walrus pre-binding) -- merged to preserve both
features. docs/AGENT_RETROSPECTIVE.md and docs/ROADMAP.md conflicts were
concurrent doc appends, kept both entries.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
rotnov and others added 3 commits August 25, 2026 13:37
…769 overlap

collect_named_expr_bindings's match became non-exhaustive after merging
main's NamedExpr work in with OptionalUnwrap's kill-prescan work; add the
missing arm. pycc_types/src/tests.rs required corresponding fixture updates
from the same overlap.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
… walrus kills (D-068 review of #780/#774's interaction)

Two blocker findings from a D-068 pinned-reviewer round examining #780's
Optional[T] narrowing (D-199/D-201) merged against #774's PEP 572 walrus
support:

1. pycc_mir::expr::pre_bind_named_expr_targets bound a walrus target via
   bind_variable but never called kill_narrowing, so `(x := None)` inside
   a narrowed `if` branch left the stale `$narrowed:{name}` sentinel in
   place -- a read right after it kept unconditionally lowering to
   MirExpr::OptionalUnwrap for a value the walrus had just overwritten.
   Fixed by adding the same kill_narrowing call HirStmt::Assign's own arm
   already makes.

2. pycc_hir::collect_killed_names (the shared D-201 kill-prescan
   primitive) put a bare ExprStmt in a no-op arm and never inspected
   If/While's own test expression for an embedded NamedExpr, so a
   walrus-only kill inside a re-enterable while body was invisible to the
   prescan -- unsoundly leaving a pre-kill read narrowed on every
   iteration after the first. Fixed with a new
   collect_named_expr_targets_in_expr walker, wired into the ExprStmt/
   If-test/While-test arms.

Both are exercised by targeted regression tests plus a coverage-pinning
test hitting every HirExpr arm of the new walker; a full check_source
integration test confirms the checker now rejects the loop-reentry shape
with T0021, matching the existing plain-assignment kill's behavior.

D-201 is corrected in place (not yet merged into main, so the append-only
rule for accepted decisions does not yet apply) to document both fixes.
Confirmed via `cargo llvm-cov` before/after that the pre-existing coverage
gaps in pycc_mir::expr.rs (super().method(args) lowering) and
pycc_types::lib.rs (unroll_enum_loops_in_stmts recursion) already existed
at the c304ae9 base commit and are unrelated to this change; flagged
separately for tracked follow-up issues rather than fixed here.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
CI-mechanics-only fix round for this PR:

- Trim docs/ROADMAP.md prose (the new #774 walrus milestone entry and
  several verbose sentences in the Language surface/Type system/CLI/
  Diagnostics rows) without dropping any distinct fact or citation, to
  restore the site/llms-txt-context-manifest.json aggregate budget from
  263090 to a passing byte count after merging main's #774/#150 docs.
- Update site/status/index.html's "not yet" section: Optional[T]
  parsing and is/is not None comparisons already landed (D-197), and
  this PR's #769 adds top-level is/is not None narrowing of a checked
  Optional binding (D-199), so the page no longer claims Optional and
  narrowing have no grammar surface at all. Satisfies
  scripts/check_status_page_freshness.rb, which requires a
  site/status/index.html or site/index.html update whenever
  docs/ROADMAP.md gains a new feature-landing paragraph (here, #769's).
- Update tests/fixtures/pages-performance-manifest.json's
  source_artifact_sha256 pin for site/status/index.html to match its
  new content.

No compiler logic changed; crates/* untouched.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Optional[int] is None / is not None flow-sensitive narrowing (Part 2 of #747)

1 participant