TY7 De Morgan narrowing + pattern-binder typing #33

Manually merged
tvidal merged 2 commits from feat/033-ty7-de-morgan-narrowing-pattern-binder-typing into master 2026-02-09 17:17:05 +01:00
Owner

TY7 De Morgan narrowing + pattern-binder typing

Along the way:

  • types(TY7): De Morgan narrowing + conjunction-by-intersection
  • types(TY7): pattern-binder typing (variant payloads + list elements)

Touches 11 files: docs/impl/type-system/TY7-exhaustive-match-and-narrowing.md, src/rust/crates/ck_cktest/src/pipeline.rs, src/rust/crates/ck_types/src/check.rs, src/rust/crates/ck_types/src/driver.rs, src/rust/crates/ck_types/src/lib.rs, src/rust/crates/ck_types/src/match_check.rs and 5 more.

TY7 De Morgan narrowing + pattern-binder typing Along the way: - types(TY7): De Morgan narrowing + conjunction-by-intersection - types(TY7): pattern-binder typing (variant payloads + list elements) Touches 11 files: `docs/impl/type-system/TY7-exhaustive-match-and-narrowing.md`, `src/rust/crates/ck_cktest/src/pipeline.rs`, `src/rust/crates/ck_types/src/check.rs`, `src/rust/crates/ck_types/src/driver.rs`, `src/rust/crates/ck_types/src/lib.rs`, `src/rust/crates/ck_types/src/match_check.rs` and 5 more.
tvidal approved these changes 2026-02-09 13:00:01 +01:00
tvidal left a comment

Good. Small enough to read in one sitting, and src/rust/crates/ck_types/src/match_check.rs is easier to follow than it was.

Good. Small enough to read in one sitting, and `src/rust/crates/ck_types/src/match_check.rs` is easier to follow than it was.
@ -473,0 +525,4 @@
} => {
cx.results.locals.insert(*local, scrutinee_ty.clone());
}
_ => {}
Owner

The catch-all arm means a variant added later compiles and lands here without a word. Can the match on _ name every variant so the compiler tells us?, at src/rust/crates/ck_types/src/match_check.rs:528.

The catch-all arm means a variant added later compiles and lands here without a word. Can the match on `_` name every variant so the compiler tells us?, at src/rust/crates/ck_types/src/match_check.rs:528.
Author
Owner

Named them all. A new variant is a compile error in src/rust/crates/ck_types/src/match_check.rs now, which is where we want to find out.

Named them all. A new variant is a compile error in `src/rust/crates/ck_types/src/match_check.rs` now, which is where we want to find out.
dferreira approved these changes 2026-02-09 15:57:59 +01:00
dferreira left a comment

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

Read it too. No objection to `src/rust/crates/ck_types/src/match_check.rs`.
Seventh TY7 sliver. The Assert::guard recognizer now distributes an
outstanding `not` through `and`/`or` (De Morgan): not (p and q) →
(not p) or (not q); not (p or q) → (not p) and (not q) — the case that
narrows, e.g. not (x is Cat or x is Dog) over Cat or Dog or Bird ⇒ Bird.

This rested on making conjunction compose by intersection
(merge_conjunction / intersect, the dual of residual): a local
constrained by both sides of an `and` narrows to the common leaves, and
disjoint constraints intersect to Nothing (unsatisfiable guard → dead
continuation, E0720). Fixes a latent imprecision in the plain `p and q`
row (last-write-wins concatenation gave the wrong type for a
doubly-constrained local). The value-algebra ==/!= rows stay un-flipped
(the two algebras never mix in one expression).

Golden: assert_guard_de_morgan_narrows.cktest (trapped, ratchet holds at
112); merge_conjunction / intersect unit tests in narrow.rs.
Eighth TY7 sliver — #1 of the "finish TY7" pair. A match arm's pattern
binders now take real types instead of Unknown.

Variant payloads (Maybe::Some(s) over Maybe<Int> ⇒ s: Int) required
building the per-variant payload-type cache N1 and expand_data_type had
deferred: a new project-global PayloadTypeTable (sibling of
build_field_types, threaded type_check_module → check_fn_body → Walker)
lifts each data variant's positional payload types with the parent's
generic params encoded POSITIONALLY as Ty::Var(TypeVarId(i)), and
PayloadTypeTable::instantiate substitutes the matched tag's args at the
pattern site — so the positional vars never escape into the general type
space (data types have no globally-canonical vars).

List elements ([x, ..xs] over List<Cat, 8> ⇒ x: Cat) read the
scrutinee's first non-value type argument; the ..xs rest binds the
scrutinee list type, an element-correct over-approximation (exact
smaller size bound deferred). Only bare Binder sub-patterns are seeded;
named-payload variants (Auth { reason }) stay Unknown (record
destructuring, deferred).

Goldens: match_variant_payload_binder.cktest, match_list_element_binder
.cktest (both trapped, ratchet holds at 112); subst / instantiate unit
tests in payload.rs. Extracted build_payload_cache in pipeline.rs to
keep typecheck_pages under the R4 LoC cap.
tvidal manually merged commit d00240cf68 into master 2026-02-09 17:17:05 +01:00
Sign in to join this conversation.
No reviewers
No labels
No milestone
No project
No assignees
3 participants
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
northgale/cklang-bootstrap!33
No description provided.