Types(TY7): match exhaustiveness, unreachable arms, per-arm narrowing #32

praghunathan · 2026-02-06T05:30:00+01:00

praghunathan commented

2026-02-06 05:30:00 +01:00

Types(TY7): match exhaustiveness, unreachable arms, per-arm narrowing

Along the way:

types(TY7): match exhaustiveness, unreachable arms, per-arm narrowing
parser(TY7-frontend): value-position type-algebra operators
types(TY7): Assert::guard flow narrowing
types(TY7): dead-code-after-Nothing block-statement sweep (E0720)
style: repo-wide rustfmt reconcile under pinned 1.93
types(TY7): String/EmptyString value-algebra split narrowing
types(TY7): structural list-match exhaustiveness (E0719 list form)
types(TY7): list-arm unreachability (E0721 structural dual)
Merge branch '032-types-ty7-match--types-ty7-match-exhaustivene' into feat/032-types-ty7-match-exhaustiveness-unreachable-arm
Merge branch 'master' into feat/032-types-ty7-match-exhaustiveness-unreachable-arm

Touches 46 files: docs/impl/03-parser.md, docs/impl/08-diagnostics.md, docs/impl/resolution/N6-hir-lowering.md, docs/impl/slices.md, docs/impl/type-system/TY7-exhaustive-match-and-narrowing.md, docs/syntax.md and 40 more.

Types(TY7): match exhaustiveness, unreachable arms, per-arm narrowing Along the way: - types(TY7): match exhaustiveness, unreachable arms, per-arm narrowing - parser(TY7-frontend): value-position type-algebra operators - types(TY7): Assert::guard flow narrowing - types(TY7): dead-code-after-Nothing block-statement sweep (E0720) - style: repo-wide rustfmt reconcile under pinned 1.93 - types(TY7): String/EmptyString value-algebra split narrowing - types(TY7): structural list-match exhaustiveness (E0719 list form) - types(TY7): list-arm unreachability (E0721 structural dual) - Merge branch '032-types-ty7-match--types-ty7-match-exhaustivene' into feat/032-types-ty7-match-exhaustiveness-unreachable-arm - Merge branch 'master' into feat/032-types-ty7-match-exhaustiveness-unreachable-arm Touches 46 files: `docs/impl/03-parser.md`, `docs/impl/08-diagnostics.md`, `docs/impl/resolution/N6-hir-lowering.md`, `docs/impl/slices.md`, `docs/impl/type-system/TY7-exhaustive-match-and-narrowing.md`, `docs/syntax.md` and 40 more.

tvidal approved these changes

2026-02-07 09:30:00 +01:00

tvidal left a comment

A clear improvement. The change in src/rust/crates/ck_types/src/check_block.rs is the part I would have argued for.

A clear improvement. The change in `src/rust/crates/ck_types/src/check_block.rs` is the part I would have argued for.

src/rust/crates/ck_types/src/check_block.rs

					
				@ -76,0 +129,4 @@

				            ExprKind::List { elements } if elements.is_empty()

				        );

				        let value_ty = if is_empty_list {

				            self.record_type(value, ann.clone());

record_type is cloned on what looks like a hot path. Is the ownership forced here, or can this borrow?

`record_type` is cloned on what looks like a hot path. Is the ownership forced here, or can this borrow?

src/rust/crates/ck_types/src/diag.rs

					
				@ -482,0 +550,4 @@

				/// statement / tail. Shares the code with the [TY5](../../../../docs/impl/type-system/TY5-method-call-sugar.md)

				/// method-on-`Nothing` form (both are dead-code-after-`Nothing`).

				#[must_use]

				pub fn e0720_dead_stmt(primary: Span) -> Diagnostic {

e0720_dead_stmt is public. Does anything outside the crate call it, or is it pub because that was easier? Every public item is a promise.

`e0720_dead_stmt` is public. Does anything outside the crate call it, or is it pub because that was easier? Every public item is a promise.

praghunathan commented

2026-02-08 05:30:00 +01:00

It can borrow. The clone of record_type was left over from before the lifetime was threaded through src/rust/crates/ck_types/src/check_block.rs, and it is gone.

It can borrow. The clone of `record_type` was left over from before the lifetime was threaded through `src/rust/crates/ck_types/src/check_block.rs`, and it is gone.

praghunathan commented

2026-02-08 05:30:00 +01:00

Nothing outside calls e0720_dead_stmt. It is pub(crate) in src/rust/crates/ck_types/src/diag.rs now.

Nothing outside calls `e0720_dead_stmt`. It is pub(crate) in `src/rust/crates/ck_types/src/diag.rs` now.

hkowalski approved these changes

2026-02-09 08:00:00 +01:00

hkowalski left a comment

Read it too. No objection to src/rust/crates/ck_types/src/check_block.rs.

Read it too. No objection to `src/rust/crates/ck_types/src/check_block.rs`.

praghunathan added 10 commits

2026-02-09 09:30:00 +01:00

types(TY7): match exhaustiveness, unreachable arms, per-arm narrowing 77fa61064d

First TY7 sliver: the `match` HIR node (ExprKind::Match + Arm + Pattern)
plus CST→HIR lowering, union/single-nominal exhaustiveness (E0719),
unreachable arms (E0721, renumbered around the shipped E0720 dead-code
code), and per-arm pattern narrowing (a `c: Cat` arm binds `c` to `Cat`).

Flow narrowing, list-pattern (Maranget) exhaustiveness, variant-payload
binder typing, and the E0720 dead-code-after-`Nothing` block sweep stay
deferred — a value still flows and no false diagnostic fires.

parser(TY7-frontend): value-position type-algebra operators 8bc1f0653a

Lock and implement the value-position precedence of the type-algebra
operators `is` / `is not` / `and` / `or` / `not` (syntax.md + 03-parser.md),
retiring the E0047 "precedence undecided" bail. This is the front-end
prerequisite for TY7 flow narrowing, which needs `Assert::guard(x is T)`
to actually parse.

- Precedence (loosest tier, below `with`): `is`/`is not` (left = 8, RHS a
  single type via parse_type_expr_single — no or-union fold), `not` (prefix,
  right = 7), `and` (6,7), `or` (4,5). So `x is Cat or x is Dog` is two
  tests joined by `or`, and `not x is Int` is `not (x is Int)`.
- New CST node `TypeTestExpr`; `and`/`or` reuse `BinaryExpr`, `not` reuses
  `UnaryExpr`. AST accessor `TypeTestExpr { value, ty, is_negated }`.
- HIR: `ExprKind::TypeTest { value, negated }`, `BinOp::And`/`Or`,
  `UnOp::Not`. The asserted type is read off the CST at synth time (the
  manifest-read discipline), not carried in the node.
- Resolver lowering split into `lower/operators.rs` (binary/unary/type-test)
  to stay under the R3 cap; only the unavoidable `syntax_kind.rs` enum
  growth touches the ratchet (798 -> 802, justified).
- TypeTest synthesizes `Bool` in the checker (narrowing recognizer is the
  next sliver); ck_eval defers it to Unit like `match`.

All four gates green: build, test, clippy -D warnings, link checker.

types(TY7): Assert::guard flow narrowing 65355de49e

Land the flow-narrowing sliver: a successful `Assert::guard(p)` narrows the
locals `p` constrains for the rest of its block and the block's tail.

- `narrow.rs`: the finite recognizer over the type-algebra predicate shapes
  the front-end slice just unblocked — `x is T` (→ T), `x is not T`
  (→ residual = current minus T), `not (x is T)`, `p and q` (both deltas),
  and `x is T or x is U` on the same local (→ T or U). Unrecognized shapes
  return the empty delta (no narrowing, no error) — the same "recognizer
  either recognizes or stays silent" discipline TY3 uses. `Assert::guard` is
  detected by effect+op name off the interner (Assert is ambient, can't be
  redeclared).
- `synth_block`: layered narrowing env — each guard's delta saves the local's
  prior table entry and is unwound at block exit, so references after the
  guard read the narrowed type while the local's declared type is restored.
- `ExprKind::TypeTest` synthesizes `Bool`.

Goldens prove narrowing end-to-end through the union-Opaque silence: E0718
fires on the *narrowed* concrete type (assert_guard_narrows, the `is not`
residual in assert_guard_is_not_narrows), and a Cat-only fn accepts the
narrowed value with no E0702 (assert_guard_enables_call). Recognizer unit
tests cover residual + disjunction merge.

Deferred (documented in TY7): the `== / != EmptyString` value-level String
split, De Morgan under `not`, list-pattern exhaustiveness, payload-binder
typing, the E0720 dead-code sweep.

All four gates green: build, test, clippy -D warnings, link checker.

types(TY7): dead-code-after-Nothing block-statement sweep (E0720) a1efde49bb

The third TY7 sliver: a `terminated` flag in `synth_block` flips when a
statement's expression synthesizes to `Nothing` (a future `Panic::raise`,
an empty `match`), or when an `Assert::guard` narrows a local to `Nothing`
(its predicate is unsatisfiable, so its continuation cannot run — the
locked negative-residual rule the flow-narrowing sliver set up). Once
terminated, every later statement and the block tail fires E0720
(`diag::e0720_dead_stmt`), sharing the code with the TY5 method-on-Nothing
form. The dead node is still synthesized first (side-table stays total),
and `Nothing` stays assignable to any expectation, so no type-mismatch
competes.

Extracted `synth_let_stmt` out of `synth_block` to keep it under the R4
80-line cap.

Goldens: assert_guard_dead_continuation (guard->Nothing), empty_match_terminates
(statement->Nothing); both fully # trap-covered, so the untrapped ratchet holds.

style: repo-wide rustfmt reconcile under pinned 1.93 51cd4c7314

The toolchain pin was bumped to 1.93 without a follow-up reformat, leaving
the committed tree failing `cargo fmt --check` (11 files / 26 hunks). Run
`cargo fmt` under the pinned toolchain to bring the tree back to a clean
formatting baseline. Pure formatting; no behavior change.

types(TY7): String/EmptyString value-algebra split narrowing 08ec097787

Add the `== / != EmptyString` recognizer row (narrow.rs), the value-algebra
mirror of `is`/`is not`: an operand synthesizing to `Ty::EmptyString` (the `""`
literal) narrows a bare local — `s == ""` to `EmptyString`, `s != ""` to the
residual. Shares the `narrow_to` core with the type-test reader; fires only with
no outstanding `not` (the algebras never mix in one expression).

Fix a latent span-trivia bug the slice exposed: a `Literal` node span can carry
leading whitespace (the RHS of `s != ""` spans ` ""`), so `synth_lit_at`
misclassified a genuine `""` as `String`. Trim before the emptiness test —
whitespace outside the quote delimiters is never part of the value.

Goldens: string_empty_split_narrows.cktest (`!=` -> String),
string_empty_eq_narrows.cktest (`==` -> EmptyString); both zero-diagnostic gates.

types(TY7): structural list-match exhaustiveness (E0719 list form) f732efcc04

Fifth TY7 sliver. A match with at least one `[ … ]` arm takes a
separate Maranget-style path (synth_list_match) from the tag-set one — a
list scrutinee is a single `List<T, N>` nominal the tag-set path would
wrongly read as one exhaustive tag.

Each unguarded arm classifies as All (`_`/bare binder), Exact(n) (a `[…]`
with no `..rest`), or Open(k) (a `[…, ..rest]`, every length ≥ k); the
match is exhaustive iff a residual arm exists or every length below the
smallest open tail is covered exactly. A gap fires E0719 (new e0719_list
helper, same code, shape-named message: an empty list, a list of N
elements, a list of N or more elements). Fail-soft on an Unknown
scrutinee or a parse-recovered arm, mirroring the tag-set path's skip.

List-arm unreachability and list-element binder typing stay deferred.

Goldens: list_match_exhaustive.cktest, list_match_missing_empty.cktest;
11 coverage-logic unit tests in match_check.rs.

types(TY7): list-arm unreachability (E0721 structural dual) 93e72bcbcc

Sixth TY7 sliver — the dual of the list-exhaustiveness sliver. A list
arm whose whole length class a preceding arm already covers fires E0721
(reusing the tag-set unreachable diagnostic; its message is generic).

list_arm_unreachable judges coverage *before* the arm (the tag-set
path's is_unreachable-then-accumulate order): a residual is dead once a
prior residual ran or the structural space is already exhaustive (same
list_missing_case core as the E0719 check); a fixed-length arm is dead
once that length is covered by an equal exact arm, an open tail
at-or-below it, or a residual; an open [..rest] arm (every length ≥ k)
is dead only under a wider-or-equal open tail or a residual — finite
exact arms can never subsume its infinite tail. Guarded arms and stray
non-list patterns (ListCover::None) make no claim.

Golden: list_match_unreachable_arm.cktest ([] + [x, ..rest] + [only] →
E0721 on [only], trapped so the untrapped-diagnostic ratchet holds at
112); 9 unreachability unit tests in match_check.rs.

Merge branch '032-types-ty7-match--types-ty7-match-exhaustivene' into feat/032-types-ty7-match-exhaustiveness-unreachable-arm 7cb609638f

TY7 exhaustive match + narrowing, value-position type-algebra, rustfmt reconcile

Brings ai/ai-8178 into master: TY7 type-checker work (match exhaustiveness,
unreachable arms, per-arm + Assert::guard narrowing, structural list-match,
String/EmptyString value-algebra split, dead-code-after-Nothing sweep),
value-position type-algebra operators in the parser, and the repo-wide
rustfmt reconcile under the pinned 1.93 toolchain. New TY7 code reformatted
to keep fmt green. Gates: build + clippy -D warnings + test + fmt all clean.

Merge branch 'master' into feat/032-types-ty7-match-exhaustiveness-unreachable-arm 5affcda454

L6 stdlib unit injection + module-prose """…""" lexer token

Brings ai/ai-dabc into master: L6 loader-closure stdlib unit injection, the
module-prose triple-quote lexer token (ProseBlock + scan_prose_block), and the
stdlib corpus redone with .ckh/.ck header splits. Resolved the R3 MAX_FILE_LOC
conflict: both slices widened the cap from 798, and they compound — syntax_kind.rs
took both the TY7 TypeTestExpr kind and the ProseBlock variant, lib.rs took the
prose scanner — so the tight worst case is a 805-line tie across both files.
Gates: build + clippy -D warnings + test (43 ok) + fmt all clean.

tvidal manually merged commit dc6f64a04a into master

2026-02-09 09:30:00 +01:00

tvidal referenced this pull request from a commit

2026-02-09 09:30:00 +01:00

Merge pull request #32 from northgale/feat/032-types-ty7-match-exhaustiveness-unreachable-arm

tvidal referenced this pull request

2026-02-09 09:30:00 +01:00

fix(values): record fields carry their full word list (debt #63) + named-tuple projection lands (debt #38) — Alloc::alloc callable #77

tvidal referenced this pull request from a commit

2026-02-09 09:30:00 +01:00

feat(coherence): the key discriminates concrete tags — Money<USD> ≠ Money<EUR> (debt #32); the generic-impl stamp channel settled (debt #37)

praghunathan referenced this pull request