diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs index 03a18a89..993d3481 100644 --- a/src/ccl/ccl_utils.rs +++ b/src/ccl/ccl_utils.rs @@ -298,7 +298,7 @@ pub fn is_trivially_true_predicate(expr: &Expr) -> bool { /// `D ⇒ D` with no refinement wrapper: the refinement would carry no /// information, and skipping it keeps program dumps and golden tests /// free of `{D | true ▷ const}` noise. The refinement gets a freshly -/// built predicate term — safe because witnesses match by structural +/// built predicate term — safe because refinements match by structural /// predicate equality, while walkers key DAG dedup on the [`PredicateId`]. /// /// Op-conversion compiles `Apply(p, Iterate)` to an `IterateExtent` tile @@ -476,7 +476,7 @@ fn restamp_spine_result(node: &mut Expr, new_result: Type) { /// `Fun(Refinement(_, _), _)` — a refinement on a function domain. Inference /// no longer *requires* this (any `target` with `value_ty <: target` is a /// well-typed upcast), but it is the only shape lowering produces today and -/// the one [`crate::ccl::lambda_elim`]'s groupby reconstruction reads a witness +/// the one [`crate::ccl::lambda_elim`]'s groupby reconstruction reads a refinement /// off of, so this asserts the lowering contract: a non-conforming target is /// a construction-time bug, not a user error, so it panics rather than /// emitting a cast `lambda_elim` would mishandle. See [`TypedExprNode::Cast`] @@ -491,14 +491,14 @@ pub fn make_cast(value: Expr, target_ty: Type) -> Expr { Expr::cast(value, target_ty) } -/// Read the domain refinement off a cast target type — the refinement witness a +/// Read the domain refinement off a cast target type — the refinement a /// [`make_cast`] target carries on its `Fun(Refinement(_, r), _)` shape. /// /// [`crate::ccl::lambda_elim`]'s cast-wrapped-lambda arm calls this on a /// [`TypedExprNode::Cast`]'s `target` to reattach the refinement to the /// reconstructed `groupby` lambda. (Inference does not need it: it types the /// cast as the upcast `value_ty <: target` and lets the solver carry the -/// witness.) The returned `Refinement` shares the predicate's `Rc` with +/// refinement.) The returned `Refinement` shares the predicate's `Rc` with /// `target`. pub fn cast_target_refinement(target: &Type) -> Option { let Type::Fun { domain, .. } = target else { diff --git a/src/ccl/channelize.rs b/src/ccl/channelize.rs index 362492a7..3a07db03 100644 --- a/src/ccl/channelize.rs +++ b/src/ccl/channelize.rs @@ -1838,14 +1838,14 @@ fn collection_union_type(feeds: &[Expr]) -> Type { match &cod { None => cod = Some((**codomain).clone()), // The channel's element type is the **join** of its - // contributions, so a witness only survives if every one of them + // contributions, so a refinement only survives if every one of them // establishes it: `c << 1` and `c << 2` contribute // `{Int | __elem == 1}` and `{Int | __elem == 2}` and the channel // is a plain `Int`. This is the register law (`emit`'s `MutWrite` // rule) for the append-kind history: a channel is not one value // but the sequence its contributions produce. Some(c) if c != &**codomain => { - cod = Some(join_witnesses(c, codomain)); + cod = Some(join_refinements(c, codomain)); } // Every `<<` contribution to one channel is constrained into // the channel's shared `value` var at inference, so the @@ -1880,16 +1880,16 @@ fn collection_union_type(feeds: &[Expr]) -> Type { } /// The join of two types that agree modulo refinements: their shared skeleton -/// carrying only the witnesses **both** sides establish. +/// carrying only the refinements **both** sides establish. /// -/// Witnesses are compared structurally, as everywhere else (`Refinement`'s +/// Refinements are compared structurally, as everywhere else (`Refinement`'s /// `PartialEq`), and the skeletons must already agree — the caller's /// `debug_assert` states that invariant. -fn join_witnesses(a: &Type, b: &Type) -> Type { +fn join_refinements(a: &Type, b: &Type) -> Type { let mut layers: Vec = Vec::new(); let mut cur = a; while let Type::Refinement(inner, r) = cur { - if type_carries_witness(b, r) { + if type_carries_refinement(b, r) { layers.push(r.clone()); } cur = inner; @@ -1901,11 +1901,11 @@ fn join_witnesses(a: &Type, b: &Type) -> Type { .fold(cur.clone(), |acc, r| Type::Refinement(Box::new(acc), r)) } -/// Whether `ty`'s own refinement layers include `witness`. -fn type_carries_witness(ty: &Type, witness: &Refinement) -> bool { +/// Whether `ty`'s own refinement layers include `refinement`. +fn type_carries_refinement(ty: &Type, refinement: &Refinement) -> bool { let mut cur = ty; while let Type::Refinement(inner, r) = cur { - if r == witness { + if r == refinement { return true; } cur = inner; diff --git a/src/ccl/context.rs b/src/ccl/context.rs index 78787874..75375a1d 100644 --- a/src/ccl/context.rs +++ b/src/ccl/context.rs @@ -1008,7 +1008,7 @@ pub fn compile_program( // graph an adjacency that doesn't chain would otherwise hide. Planning // surfaces each iterated / join-satisfying extent on its producer's // codomain (`refine_codomain` / `set_codomain`) and the strict checker - // matches the fresh refinement witnesses it mints by structural predicate + // matches the fresh refinements it mints by structural predicate // equality, so the staging shapes now validate without re-blinding the // check or peeling cast refinements. typecheck(&join_planned).expect("type error after join planning"); diff --git a/src/ccl/design/ir.md b/src/ccl/design/ir.md index 737632fc..2cfee64d 100644 --- a/src/ccl/design/ir.md +++ b/src/ccl/design/ir.md @@ -95,7 +95,7 @@ Lambdas do not survive to the dataflow graph: [lambda elimination](optimization. Lowering ([`ccl_utils::make_cast`]) emits it for list-comprehension filters, for-loop `if`-guards, and `groupby`. The only `target` shape lowering produces today is `Fun(Refinement(_, 𝑝), _)`: a function type whose domain carries the predicate `𝑝`, so the cast attaches a refinement to a collection function's domain. `target` is the lowering-time *specification* (its domain/codomain are typically `Type::Hole`, carrying only the refinement); the resolved cast type lands on `expr.ty` after inference — the same `user_annotation`-vs-`ty` split used elsewhere. -`Cast` is an **upcast**: its whole typing rule is the single subtype obligation `value_ty <: target`. For the domain refinement lowering emits, that holds by contravariance — `(𝐷 ⇒ 𝑉) <: ({𝐷 | 𝑝} ⇒ 𝑉)` because `{𝐷 | 𝑝} <: 𝐷` — so viewing an unrefined-domain collection function at a refined-domain type is sound. A *covariant* refinement (casting `Int` to `{Int | 𝑝}`) correctly *fails* the check — acquiring a value-level refinement is a runtime/SMT-checked narrowing, not an upcast. How the solver discharges the refinement obligation — flowing the demanded witness onto the target-domain variable and stacking it so chained casts compose — is covered in [type-inference.md](type-inference.md#45-dependent-refinements-via-pi-types). +`Cast` is an **upcast**: its whole typing rule is the single subtype obligation `value_ty <: target`. For the domain refinement lowering emits, that holds by contravariance — `(𝐷 ⇒ 𝑉) <: ({𝐷 | 𝑝} ⇒ 𝑉)` because `{𝐷 | 𝑝} <: 𝐷` — so viewing an unrefined-domain collection function at a refined-domain type is sound. A *covariant* refinement (casting `Int` to `{Int | 𝑝}`) correctly *fails* the check — acquiring a value-level refinement is a runtime/SMT-checked narrowing, not an upcast. How the solver discharges the refinement obligation — flowing the demanded refinement onto the target-domain variable and stacking it so chained casts compose — is covered in [type-inference.md](type-inference.md#45-dependent-refinements-via-pi-types). `lambda_elim`, planning, and operator conversion carry the domain refinement through to a runtime `Restrict`: a `Cast` around a group-by lambda becomes a **Pi-const** form whose refinement planning's pointful group-by recognizer reads off the predicate, while a `Cast` wrapping point-free filter/guard code survives lambda elimination unchanged and is consumed as a domain refinement at planning — see [optimization.md](optimization.md). The current `Cast` only honours domain-refinement targets; the direction for a general `𝑈 ⇒ 𝑇` cast is in [type-inference.md](type-inference.md#6-future-work). diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index e544d1e9..c5e33758 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -1,6 +1,6 @@ # Cambra's Inference Algorithm -This document outlines the design, architecture, and nomenclature of Cambra's algebraic-subtyping inference engine. It details how the algorithm works, how information flows through the system, and where our implementation intentionally departs from the upstream academic reference—most notably by carrying refinement witnesses on the lattice and folding monomorphization into the coalesce walk. +This document outlines the design, architecture, and nomenclature of Cambra's algebraic-subtyping inference engine. It details how the algorithm works, how information flows through the system, and where our implementation intentionally departs from the upstream academic reference—most notably by carrying refinements on the lattice and folding monomorphization into the coalesce walk. A [glossary](#7-glossary) at the end defines every term of art used below. The conceptual walkthrough in §1 introduces each term where it is first needed; the glossary is a quick-reference to consult afterward. @@ -124,9 +124,9 @@ def identity(x): **Implemented today:** -* **Let-polymorphism (functions).** A `let` whose RHS is a *function definition* is generalized: the RHS is typed one level deeper, generalized into a `PolyScheme` at the binding site, and instantiated freshly per use. Because Cambra targets fully-monomorphized output, generalization is paired with **monomorphization**, integrated into the coalesce walk (`infer::specialize_use`): a use of a generalized binding is specialized at first visit — clone + `freshen_expr_type_slots`, a two-way pin against the use's *live* instantiation type, and a re-entrant coalesce of the clone — and the binding's `let` rebuilds itself as the chain of demanded specializations. Specialization is keyed on the *resolved* type, so same-typed uses **share** one definition. So `def f(x): x == x; f(1); f("foo")` type-checks and runs, a generator used at two element types compiles to two cached specializations (see F2), and a generalized UDF used only inside *another* generalized definition (poly-calls-poly) specializes by plain recursion — its use becomes concrete inside each wrapper clone's re-entrant walk. Levels are live (extrude fires on a genuine level mismatch). +* **Let-polymorphism (functions).** A `let` whose RHS is a *function definition* is generalized: the RHS is typed one level deeper, generalized into a `PolyScheme` at the binding site, and instantiated freshly per use. Because Cambra targets fully-monomorphized output, generalization is paired with **monomorphization**, integrated into the coalesce walk (`infer::specialize_use`): a use of a generalized binding is specialized at first visit — clone + `freshen_expr_type_slots`, a two-way pin against the use's *live* instantiation type, and a re-entrant coalesce of the clone — and the binding's `let` rebuilds itself as the chain of demanded specializations. Specialization is keyed on the use's **instantiation identity** (a `SpecKey`, not a resolved type — see [Keying a specialization](#keying-a-specialization)), so uses that instantiate the definition identically **share** one definition. So `def f(x): x == x; f(1); f("foo")` type-checks and runs, a generator used at two element types compiles to two cached specializations (see F2), and a generalized UDF used only inside *another* generalized definition (poly-calls-poly) specializes by plain recursion — its use becomes concrete inside each wrapper clone's re-entrant walk. Levels are live (extrude fires on a genuine level mismatch). * **Tagged variants.** The dual of records, natively supporting sum types and pattern-match exhaustiveness inside the structural solver (see §4). Both named (`.Tag(...)`) and positional (`++`-style) sums are handled. -* **Lattice-carried refinements.** Refinement witnesses ride the lattice natively (compared by structural predicate equality) rather than being stitched on by a post-pass; see §4 and [`crate::ccl::infer::solver`]'s `# Refinements`. +* **Lattice-carried refinements.** Refinements ride the lattice natively (compared by structural predicate equality) rather than being stitched on by a post-pass; see §4 and [`crate::ccl::infer::solver`]'s `# Refinements`. * **Dependent refinements (Pi types).** Refinement predicates may close over an outer binder; `Type::Fun` carries an optional Pi binder, the solver derives binder correspondences when constraining function types, and dependent application discharges the binder to its argument at coalesce. Group-by lookup `groupby(xs, key)(𝑘₀)` types as `{𝑖 | 𝑖 ▷ xs ▷ key == 𝑘₀} ⇒ 𝑉`. See §4.5. **Implicit polymorphism, not `Type::ForAll`.** Cambra's `ccl::Type` has no `Type::ForAll`. The choice is *pragmatic*, not a philosophical ban on representing polymorphism: level-based type variables give implicit polymorphism that is efficient and meshes with the existing solver, and monomorphizing at use sites (integrated into the coalesce walk, above) is the natural way to lower it to the concrete-typed output codegen wants. This does **not** preclude *explicit* `∀`/Π types — the `cast` and `iterate` signatures in the pi-types work (`cast : (𝑇: Type) ⇒ {𝑈: Type | 𝑈 <: 𝑇} ⇒ 𝑇`) are quantified over `Type`, i.e. `∀`/Π under another name — and the two may well coexist. Implicit level-based polymorphism is simply the most natural mechanism for the inference engine *today*. @@ -134,7 +134,7 @@ def identity(x): **Not yet implemented:** * **Explicit quantification (`∀`/Π types).** Explicit `∀`/Π types as a first-class `Type` for the cases implicit level-based polymorphism cannot express. Does not block today's coverage; a natural next step. -* **SMT-backed refinements.** Augmenting the lattice-carried refinement witnesses (today compared by structural equality only) with logical payloads (e.g. `v > 0`) reasoned about — implication, not just equality — by an external SMT solver such as Z3. +* **SMT-backed refinements.** Augmenting the lattice-carried refinements (today compared by structural equality only) with logical payloads (e.g. `v > 0`) reasoned about — implication, not just equality — by an external SMT solver such as Z3. *(There are parallel workstreams planned, such as a separate nominal-type/trait-resolution pass, but the core lattice capabilities revolve around these features.)* @@ -146,7 +146,7 @@ The inference engine drives the AST through two passes, defined in `ccl/infer/`, ### Pass 1: Constraint Emission -The algorithm walks the AST top-down. It normalizes each node's expected type into a solver-ready `ccl::Type` (via `normalize_annotation`: `Hole` → fresh `Type::Infer`; `Refinement` wrappers are *kept* — they ride the lattice as refinement witnesses, see §4), generates constraints, and writes each node's resulting `Type` directly onto `expr.ty`. +The algorithm walks the AST top-down. It normalizes each node's expected type into a solver-ready `ccl::Type` (via `normalize_annotation`: `Hole` → fresh `Type::Infer`; `Refinement` wrappers are *kept* — they ride the lattice natively, see §4), generates constraints, and writes each node's resulting `Type` directly onto `expr.ty`. Because inference variables are shared `Rc`s, constraints emitted *after* a node's type is stored continue to accumulate bounds that remain visible through the stored `Type` — so there is no separate side table; the AST node *is* the record of the node's inferred type. @@ -218,13 +218,13 @@ The solver's single-sided `Var <: Var` constrain rule leaves a few *structural* **Morphism domains (projections and lambdas) — rebuilt during the coalesce walk (`Apply` and `Compose`).** A morphism's domain appears only at a negative position, and the one-way constraints emitted around it (`fn_ty <: domain ⇒ codomain` and `arg <: domain` at an `Apply`; the adjacency `prev_cod <: next_dom` in a `Compose`) deliver the concrete value flowing in only as a *lower* bound, while the uppers carry just what the morphism's own body demands — so negative-polarity coalesce materializes the narrow body-demand shape. A `Proj`'s domain coalesces field-narrow (e.g. `.0` of a multi-accumulator loop's `step` tuple coalesces to a 1-tuple `(T)` instead of the full `(T, U)`); a lambda's record param narrows to the fields its body touches (`{label}` instead of `{id, label}`), with untouched params left `Infer`. -`coalesce_node` rebuilds it **structurally, after coalescing the children**, via the shared `specialize_projection_domain` / `specialize_lambda_domain`: the `Apply` arm replaces a projection's or directly-applied lambda's domain with the resolved argument (and an argument-position lambda's with the function's resolved inner domain), the `Compose` arm with the preceding morphism's already-resolved codomain (and the chain's own type with `Fun(first.domain, last.codomain)`), and refinement predicates recover the same way through `coalesce_type_predicates`. A lambda's body-usage refinement witnesses are preserved by re-wrapping them around the new base (deduped by structural `Refinement` equality against witnesses the input already carries), and its `param.ty` binder slot is re-derived from the rewritten domain (`refresh_lambda_param_slot`). This is **use-site specialization** — the closed-form sibling of `specialize_use`'s per-`let` specialization (the morphism's domain *equals* its input, so it is one overwrite rather than clone+pin+coalesce; see §2). Doing it post-coalesce — rather than recording a reverse bound at emit time — is what keeps it robust: an emit-time bound is recorded against a specific inference variable, and let-polymorphism's monomorphization re-mints those variables (splicing freshened definitions at use sites), so the bound would not follow to the variable the node's recorded type ends up carrying. Reading the resolved shapes directly sidesteps that entirely. +`coalesce_node` rebuilds it **structurally, after coalescing the children**, via the shared `specialize_projection_domain` / `specialize_lambda_domain`: the `Apply` arm replaces a projection's or directly-applied lambda's domain with the resolved argument (and an argument-position lambda's with the function's resolved inner domain), the `Compose` arm with the preceding morphism's already-resolved codomain (and the chain's own type with `Fun(first.domain, last.codomain)`), and refinement predicates recover the same way through `coalesce_type_predicates`. A lambda's body-usage refinements are preserved by re-wrapping them around the new base (deduped by structural `Refinement` equality against refinements the input already carries), and its `param.ty` binder slot is re-derived from the rewritten domain (`refresh_lambda_param_slot`). This is **use-site specialization** — the closed-form sibling of `specialize_use`'s per-`let` specialization (the morphism's domain *equals* its input, so it is one overwrite rather than clone+pin+coalesce; see §2). Doing it post-coalesce — rather than recording a reverse bound at emit time — is what keeps it robust: an emit-time bound is recorded against a specific inference variable, and let-polymorphism's monomorphization re-mints those variables (splicing freshened definitions at use sites), so the bound would not follow to the variable the node's recorded type ends up carrying. Reading the resolved shapes directly sidesteps that entirely. **Binder slots — filled during the coalesce walk (no lexical scope needed).** A `Var` use needs *no* scope lookup: it shares its binder's inference variable — a monomorphic `let` binds verbatim (`instantiate` freshens nothing) so every use coalesces to exactly what the binder coalesces to, and a *generalized* `let`'s uses are rewritten by the walk itself to reference per-type specializations (which does carry a scope — the walk's stack of specialization frames and shadow markers; see §3.1). What the bottom-up `expr.ty` resolution *doesn't* reach is the **binder slots**: a binder carries a type that is not any node's `expr.ty` — a `Lambda`'s `param.ty`, a `Let`'s `binding.ty`, a `Case` pattern's `binding.ty`, a `For`'s target slot. Each is resolved explicitly in `coalesce_node`, mirroring its definition (inference runs before the mutability/transaction phases, so the recurrence carriers `LetRec`/`Transact` never reach coalesce): -* **`Lambda` `param.ty`** — derived from the lambda's coalesced domain (so body-usage restriction witnesses, which are negative-polarity facts visible only in the contravariant domain, survive), and re-derived whenever a parent arm specializes the domain (`refresh_lambda_param_slot`). +* **`Lambda` `param.ty`** — derived from the lambda's coalesced domain (so body-usage restriction refinements, which are negative-polarity facts visible only in the contravariant domain, survive), and re-derived whenever a parent arm specializes the domain (`refresh_lambda_param_slot`). * **`Let` `binding.ty`** — the (already-coalesced) bound expression's type. emit never constrains the binding slot and the generic `expr.ty` resolution skips it, so without this line a `let`-bound `Var`'s **binder slot** (not its uses) stays `Type::Hole`. * **`Case` / `For` slots** — run through `resolve_var_type` like any `expr.ty`. @@ -249,9 +249,141 @@ Because the algorithm drops HM's union-find equality engine, it behaves in ways Vanilla algebraic subtyping makes a `let`-bound function polymorphic by **freshening**: every time a generalized binding is used, the solver copies its type graph, minting fresh variables for that use site. This is ordinary let-generalization/instantiation — the same idea as HM's `∀`-quantification — applied to the bound graph rather than to a syntactic type scheme. -**How Cambra applies this — and then lowers it.** A `let` binding a *function definition* (`should_generalize`) is typed one level deeper (`in_let_rhs`) and generalized into a `PolyScheme` at the binding level (`scoped_let`); each `Var` use then `instantiate`s a fresh copy, exactly the freshening above. Because every pass after inference is monomorphic, the generalized binding is lowered to concrete code **inside the coalesce walk** (integrated monomorphization): the walk carries a scope of *specialization frames* — one per in-scope generalized `let`, plus shadow markers for every other binder — and a use of a generalized binding specializes at first visit (`specialize_use`). By coalesce time the constraint graph is *complete* (emission saw the whole program), so a use's instantiation is fully determined when the bottom-up walk reaches it: the walk resolves it off the live graph, and on a memo miss clones the definition (`freshen_expr_type_slots` freshens an independent copy — uniformly over terms and types, so a refinement predicate's slots and the suspended-substitution payloads riding the copied bound edges are renamed in the same traversal as every other slot), **pins the clone two-way to the use's live instantiation type**, coalesces the clone re-entrantly *in the definition site's scope* (entries pushed between definition and use are suspended, so a same-named binder introduced in between cannot capture the clone's references), renames the use to a synthetic `Mono` name (`Name::mono`) carrying the source binding plus a globally-fresh uid, and stamps the specialization's resolved type on it. When the `let`'s body walk completes, the node rebuilds itself as the chain of demanded specializations (`coalesce_generalized_let`), running the §6.2 `let`-closing discharge per spliced layer; a binding never demanded is dropped as dead code. Same-typed uses share one clone — the memo is keyed on the resolved type (stored as the specialization's own resolved type). The definition's own subtree is never coalesced in place: its quantified variables have no use-site bounds, so coalescing it would both produce an under-determined type and overwrite the bound-bearing `InferVar`s the clones freshen from. - -Specializing *during* the walk — rather than splicing after it — is load-bearing twice over. First, every parent derives its type from concrete children on the first pass: in particular a parent `Apply`'s dependent-codomain discharge forces against the specialization's resolved predicate terms, so parent types are never re-derived from a second, graph-unreachable copy of the discharge logic. Second, chained polymorphism (a generalized UDF used only inside *another* generalized definition, poly-calls-poly) needs no special ordering: the inner use is reached only inside an outer clone's re-entrant walk, after that clone's pin has driven the use's instantiation concrete, and the inner binding's frame is still in scope below the outer's. The ordering invariant that makes in-walk specialization sound: **specialization may only add bounds to variables the walk has not yet read** — a use's pin touches its own instantiation variables (read right after, at its own stamp), the clone's fresh variables (read only inside the clone's walk), and otherwise deposits only α-copies of demands the instantiation already made at emit; `coalesce_node`'s `Apply` arm coalesces function before argument to keep even those copies behind the read front. The invariant is **checked explicitly, not just argued**: the walk logs every graph read as a `(var-laden type, resolution)` pair (the snapshot shares the live `InferVar`s), and `assert_reads_stable` re-resolves each against the *final* graph at end of pass, requiring the structural skeleton — bases, ranges, shapes, refinement-layer count, with under-determined positions wildcarded and predicate *content* deferred to `check_scope_valid` / the post-inference reconcile — to be unchanged. A pin that retroactively altered an already-read variable's resolution trips it by name (debug builds; free in release). Refinement layers count because a witness is lattice content like a record field, so a bound determines it as much as it determines the base; the **one** read that excludes them is the one producing a specialization's own memo key, where the pin that immediately follows the read is itself what moves the witnesses and two uses differing only in witnesses are meant to share a specialization (`ReadPurpose::SpecializationKey`). That read's *skeleton* is still held fixed — keying on a stale one would pick the wrong clone. The contravariant-domain coalescing of §2 — the opposite-polarity fallback plus `coalesce_node`'s per-morphism domain specialization (projections and lambdas) — is the monomorphic coalescing rule for those vars; it is sound because every variable reaching coalesce is monomorphically determined (§1). +**How Cambra applies this — and then lowers it.** A `let` binding a *function definition* (`should_generalize`) is typed one level deeper (`in_let_rhs`) and generalized into a `PolyScheme` at the binding level (`scoped_let`); each `Var` use then `instantiate`s a fresh copy, exactly the freshening above. Because every pass after inference is monomorphic, the generalized binding is lowered to concrete code **inside the coalesce walk** (integrated monomorphization): the walk carries a scope of *specialization frames* — one per in-scope generalized `let`, plus shadow markers for every other binder — and a use of a generalized binding specializes at first visit (`specialize_use`). By coalesce time the constraint graph is *complete* (emission saw the whole program), so a use's instantiation is fully determined when the bottom-up walk reaches it: the walk resolves it off the live graph, and on a memo miss clones the definition (`freshen_expr_type_slots` freshens an independent copy — uniformly over terms and types, so a refinement predicate's slots and the suspended-substitution payloads riding the copied bound edges are renamed in the same traversal as every other slot), **pins the clone two-way to the use's live instantiation type**, coalesces the clone re-entrantly *in the definition site's scope* (entries pushed between definition and use are suspended, so a same-named binder introduced in between cannot capture the clone's references), renames the use to a synthetic `Mono` name (`Name::mono`) carrying the source binding plus a globally-fresh uid, and stamps the specialization's resolved type on it. When the `let`'s body walk completes, the node rebuilds itself as the chain of demanded specializations (`coalesce_generalized_let`), running the §6.2 `let`-closing discharge per spliced layer; a binding never demanded is dropped as dead code. Uses that instantiate the definition identically share one clone — the memo is keyed on a `SpecKey`, taken from the use's live type before its pin, and an entry stores the key of the use that minted it (see [Keying a specialization](#keying-a-specialization)). The definition's own subtree is never coalesced in place: its quantified variables have no use-site bounds, so coalescing it would both produce an under-determined type and overwrite the bound-bearing `InferVar`s the clones freshen from. + +Specializing *during* the walk — rather than splicing after it — is load-bearing twice over. First, every parent derives its type from concrete children on the first pass: in particular a parent `Apply`'s dependent-codomain discharge forces against the specialization's resolved predicate terms, so parent types are never re-derived from a second, graph-unreachable copy of the discharge logic. Second, chained polymorphism (a generalized UDF used only inside *another* generalized definition, poly-calls-poly) needs no special ordering: the inner use is reached only inside an outer clone's re-entrant walk, after that clone's pin has driven the use's instantiation concrete, and the inner binding's frame is still in scope below the outer's. The ordering invariant that makes in-walk specialization sound: **specialization may only add bounds to variables the walk has not yet read** — a use's pin touches its own instantiation variables (read right after, at its own stamp), the clone's fresh variables (read only inside the clone's walk), and otherwise deposits only α-copies of demands the instantiation already made at emit; `coalesce_node`'s `Apply` arm coalesces function before argument to keep even those copies behind the read front. The invariant is **checked explicitly, not just argued**: the walk logs every graph read as a `(var-laden type, resolution)` pair (the snapshot shares the live `InferVar`s), and `assert_reads_stable` re-resolves each against the *final* graph at end of pass, requiring the structural skeleton — bases, ranges, shapes, refinement-layer count, with under-determined positions wildcarded and predicate *content* deferred to `check_scope_valid` / the post-inference reconcile — to be unchanged. A pin that retroactively altered an already-read variable's resolution trips it by name (debug builds; free in release). Refinement layers count because a refinement is lattice content like a record field, so a bound determines it as much as it determines the base; the **one** read that excludes them is a use's own instantiation resolution, where the pin that immediately follows the read is itself what moves the refinements (`ReadPurpose::Instantiation`). That is sound because the read's consumers are refinement-insensitive — it seeds the clone's channel-domain pairings and blames a resolution failure — and, in particular, *sharing does not ride on it*: that is the `SpecKey`'s job, and a key consults both bound directions precisely so it does not depend on which polarity a rendering would have picked. The read's *skeleton* is still held fixed — a stale one would pair channel domains wrong. The contravariant-domain coalescing of §2 — the opposite-polarity fallback plus `coalesce_node`'s per-morphism domain specialization (projections and lambdas) — is the monomorphic coalescing rule for those vars; it is sound because every variable reaching coalesce is monomorphically determined (§1). + +#### Keying a specialization + +The memo that decides which uses share a specialization is keyed on a `SpecKey` +(`src/ccl/infer/solver/spec_key.rs`), **not** on a resolved `Type`. The distinction +is the whole content of the design here, because the two answer different questions. + +A resolved type answers *"what should be stamped on this node"*, and is +deliberately lossy in service of that: a domain is a negative position, so it +resolves from upper bounds — from what the definition body demands — which narrows +away a position the body never touches, and leaves an argument's refinement (a *lower* +bound, from the emit-time `arg <: domain` edge) invisible except where the +opposite-polarity fallback happens to fire. A specialization key answers *"would +two uses' clones be the same code"*, and must be complete: a clone's interior reads +its parameter at a **positive** position, so it sees exactly the refinements the +domain's rendering drops. Keying on a rendering compares one polarity's view +against a clone built from the other's, which shares a clone between two uses whose +interiors differ — the clone then carries one call site's argument type at another's. + +A `SpecKey` is therefore the pair of **directed reads** of the use's instantiation +type, the root taken once at each polarity and the two *kept apart*: + +* the **positive** read is the stamping view (domain from the definition's demands); +* the **negative** read is the clone's view (domain from the argument that flowed + in, codomain from the consumer's demand). + +The negative read is the load-bearing half, and the pair is exhaustive: +use-specific information enters an instantiation through exactly two channels — an +`arg <: domain` edge and a consumer's `codomain <: demand` edge — and the negative +read follows precisely those. Merging the two views is wrong, because it forgets +which *direction* a contribution came from and the pin the key stands in for is +direction-sensitive. *Saturating* — following both bound lists at every variable — +is worse: the bound graph is connected across unrelated uses (two calls' arguments +meet at the shared variable of an operator's scheme), so an undirected closure +walks out of one use into every other and every use keys on the whole program's +literals. Within a read, merging is always **union**: a key that narrows can only +under-split, and under-splitting is a miscompile while over-splitting is a wasted +clone. An under-determined position is one canonical empty view rather than a fresh +`Infer` placeholder, so two unexercised uses can still share. + +Both sides of the comparison must be computed by **one procedure at one point in +the pin's lifecycle** — from the use's live type, before its own pin — and an entry +stores the key of the use that minted it. Keying an entry on its clone's +*coalesced* type instead is a second, incompatible coordinate system: for any +definition whose clone type gains a refinement across the pin, no candidate key could +ever equal a stored one, so the memo becomes write-only and even identical call +sites clone per site. + +**A key is not instantaneous, and it is not a function of the post-emission +graph.** "One point in the pin's lifecycle" is exact about each use's *own* pin, +but the two keys in a comparison are not taken at the same instant: an entry's was +taken before the pin of the use that minted it, a candidate's later, with every +intervening pin already in the graph. The tempting strengthening — that a pin only +*transports* use-specific information across polarity and never creates it, so no +other use's pin can move a key — is **false**. A pin does not only transport; for a +*nested* use it **deposits the consumer's demand**. In `f(f(3))`, +`coalesce_node`'s `Apply` arm takes function before argument, so the outer use of +`f` specializes first and its pin is what drives the outer clone's domain +concrete. That domain *is* the demand on the inner call's result, so it reaches +the inner use through the `codomain <: demand` edge — one of the two channels the +negative read follows *by design*. The inner use is therefore keyed against a +demand that did not exist at end of emission. + +Whether the deposit is *visible to the key* depends on how much structure the +demand carries. Where the demand resolves to a bare base the two reads agree and +nothing is observable, which is why a snapshot-and-compare check over the suite +passes here. It stops passing as soon as a demand carries structure a key records: +once an operator's effect on types is itself a type, the same `f = \x -> x * 2`, +`f(f(3))` splits, the inner use's negative read gaining exactly the layer the +outer pin deposited. The positive read does not move, and no key moves for any +other reason. + +So key equality is walk-order sensitive, and the memo can compare keys read in two +different graph states. The residue is **over-splitting** — a use keyed against a +thinner demand does not match an entry keyed against a fatter one, and the cost is +a redundant clone, the same direction as the known imprecision below. It is not +symmetric with under-splitting: a thin key and a fat key are unequal, so a use +carrying a real demand cannot be served by an entry that never saw one. + +**The key is only expressible in-walk — which is an argument *for* in-walk +specialization, not a cost of it.** A monomorphizer that ran *after* coalesce +would have no choice but to key on a resolved type, because by then a resolved +type is all there is: `expr.ty` has been overwritten in place and the bound graph +it was resolved from is gone. Specializing *inside* the coalesce walk is what +leaves a use's instantiation still var-laden with its bounds still live at the +moment the key is taken — so `SpecKey` is not merely a better key than the +rendering, it is one only this architecture can express. The discriminating +information is present the instant emission finishes; the pin transports it across +polarity rather than discovering it. + +**Why other monomorphizers key on a finished value.** rustc keys an instance on +its definition plus its generic arguments, C++ on the template-argument list, +Swift on a substitution map, MLton on the type-argument list in a single +post-inference pass. Every one of them keys on a *finished value*, and can, +because their generic bodies are already typed and instantiation is substitution. +Cambra has no `Type::ForAll` and never types a generic body at all — the +definition's own subtree is never coalesced in place — so monomorphization here +**is** the act of typing the body, not the duplication of already-typed code. That +places it in C++'s category, the one mainstream compiler where instantiation +genuinely re-runs semantic analysis, and it is the real reason the key has to be +read off a live graph. A reader arriving from rustc would otherwise take that for +an implementation choice. What is *not* the reason: poly-calls-poly on its own +does not force the in-walk arrangement — discovering the *set* of instantiations +is a reachability fixpoint in every monomorphizer, and recursing into each new +specialization handles it. (Closest prior art: Lutze, Schuster & Brachthäuser, +*The Simple Essence of Monomorphization*, OOPSLA 2025 — monomorphization as a flow +analysis over an algebraic-subtyping system, including where it stops being +possible, at the cyclic flow of polymorphic recursion.) + +**Specializing precisely is the correct rule, not a budget choice.** A refinement +layer on an iterated domain is *compiled* — `planning::iterate` emits one +`restrict(p)` filter per layer — so a refinement is code, and two clones pinned to +different refinements are genuinely different code. Since every literal carries its +own singleton ([A literal is refined by its own value](#a-literal-is-refined-by-its-own-value)), +the practical rule is one specialization per distinct argument tuple. `inline` +beta-reduces scalar UDFs, so the cost lands on collection-producing ones, which it +leaves cached. + +**Known imprecision.** The key summarizes the pin's *input*, so two uses differing +only in a position the clone never reads still key apart (`λ a, b → a` at `(1, 2)` +and `(1, 5)` mints two identical clones). Keying on the pin's *output* — the +finished clone, deduped structurally — would share exactly when the emitted code is +identical, but it cannot be a lookup, only a build-then-dedupe, and it needs +α-equivalence over the names minted fresh per clone (`Name::mono` uids, coalesce's +`Infer` placeholders, per-instantiation `ChanDom` names), a way to undo a discarded +clone's pin, and reference-liveness filtering at the splice. The two compose — this +key as the fast path, clone-equality as a precision tier on a miss — so nothing +here has to be undone to get there. Relatedly, a *hit* is not re-pinned: a miss +pins a var-laden clone (identifying variables), while a hit's specialization is +already concrete, and pinning that against a still-var-laden use type is a strictly +stronger demand that rejects uses the key correctly considers shareable. Checking a +hit wants a non-recording subsumption test, which the solver does not have. **Refinement predicates under monomorphization.** A `Refinement` has no synthetic identity: it carries an *immutable* predicate term (`Rc`), and its identity is the **type-blind structural equality** of that term (`eq_refinement_predicate`) — the predicate's embedded `Type` slots are inference metadata and never participate. A predicate occurs at many sites — its syntactic origin (a `Cast` target, a `user_annotation`) and every position `constrain`/`freshen_above` propagates the refinement onto — but those are independent occurrences, not aliases of one mutable cell. Two facts make this work without the cell-retirement machinery the mutable design needed. First, a free use of a generalized binding may live *only* inside a predicate (a list-comprehension filter calling a UDF lowers to a cast-target predicate); the coalesce walk reaches such uses because `coalesce_type_predicates` runs `coalesce_node` over every predicate it encounters with the walk's specialization scope live, and the post-inference `inline` pass substitutes inside predicates likewise. Second, because predicates are immutable, **a use-site coalesce *rebuilds* a predicate rather than mutating one shared with the definition** — so there is nothing to privatize, retire, or re-point: a specialization clone freshens its predicate as a proper substitution instance (`freshen_above`'s `Refinement` arm freshens the predicate's type slots through the same cache, and its `Infer` arm freshens the discharge-payload terms riding copied bound edges), and `compact_type` simply `force_refinement`s each refinement it materializes (a vacuous force shares the `Rc`, a substituting one rebuilds). The residual case the mutable design's whole-tree fix-up swept up — a refinement materialized from the definition's bound *before* its first specialization carries the definition's quantified vars — is harmless here: equality is type-blind, so a predicate carrying the definition's quantified vars compares equal to its specialized instance. Passes that need *occurrence* identity rather than equality (visited sets that dedup a predicate term shared by `Rc` across positions — the term graph is a DAG, since immutable `Rc` cannot form a cycle) key on the predicate `Rc`'s address (`PredicateId`). @@ -462,7 +594,7 @@ Inference does not *infer* a multi-atom sum from a primitive collision (it raise #### A literal is refined by its own value -A literal is typed by *which* literal it is: `5 : {Int | __elem == 5}`, its base refined by the singleton predicate. Not a `Literal(base, value)` constructor — an ordinary witness, so every rule above applies unchanged and none has to learn a new case. +A literal is typed by *which* literal it is: `5 : {Int | __elem == 5}`, its base refined by the singleton predicate. Not a `Literal(base, value)` constructor — an ordinary refinement, so every rule above applies unchanged and none has to learn a new case. The reason is that a literal knows more about itself than its base does, and that knowledge is what a proof obligation needs: `a[0]` can only discharge against `Array(3, 𝑇)`'s index range if `0`'s type says it *is* `0`. Typing `5` as plain `Int` throws that away at the one place it is free to keep. The predicate is built **typed** — only *node* annotations get their embedded predicates re-inferred, and this one rides a type the rule makes rather than one a user wrote. @@ -470,25 +602,25 @@ What this changed is instructive, because refinements were rare enough before th * **An operator does not propagate its operands' refinements** (`apply_binary_scheme` strips them). Arithmetic's `∀α. α → α → α` shares *one* variable across both operands and the result, so a refinement reaching α claims the operator preserved it. No binary operator does: `x + x` where `x` is `2` gives `4`. The claim is invisible while operands merely join — distinct refinements intersect to none — and wrong when they do not, since intersecting a set with itself is that set. The unary path deliberately keeps them: its operators are monomorphic, and its other user is aggregates, whose operand is a *collection* whose refinements describe its domain. * **A mutable register takes no refinement** from its initializer or from any single write. A register is not one value but the sequence its writes produce, so its value type is the join over all of them; taking one contribution's refinement would assert it never changes, which is what declaring it mutable denies. The rule holds at every place a register's value type is *built*, not just at the `:=`/`+=` rule: the `Transact` carrier's keys (where the seed is the value type's only lower bound, so an unstripped seed would resolve the register — and every read of it — to the seed's singleton), the recognition that builds that carrier, and the phase that reads the value type back off the seed binding. -* **Every merge point joins** — a list's elements, a `Case`'s arms, a register's seed and writes, a channel's contributions. This is the one rule the singleton made load-bearing, and the one place it is easy to get wrong, because a merge that simply *adopts one input's type* looks right until the inputs carry different refinements. The law: a refinement is a fact about **a value**, and a merge point is not one value — it is whichever input the runtime supplies — so a witness survives the merge only if *every* input establishes it. Two arms depositing different singletons intersect to none (`1 if 𝑐 else 2` is an `Int`); two arms depositing the same restriction keep it (identical filtered comprehensions stay filtered, `5 if 𝑐 else 5` is still the `5`). Where the merge is a fresh variable every input flows into, the solver's join *is* the rule and nothing has to strip; where a pass builds the merged type by hand (`channelize`'s channel union, the `Transact` carrier's key seeds) it must intersect the witnesses explicitly. +* **Every merge point joins** — a list's elements, a `Case`'s arms, a register's seed and writes, a channel's contributions. This is the one rule the singleton made load-bearing, and the one place it is easy to get wrong, because a merge that simply *adopts one input's type* looks right until the inputs carry different refinements. The law: a refinement is a fact about **a value**, and a merge point is not one value — it is whichever input the runtime supplies — so a refinement survives the merge only if *every* input establishes it. Two arms depositing different singletons intersect to none (`1 if 𝑐 else 2` is an `Int`); two arms depositing the same restriction keep it (identical filtered comprehensions stay filtered, `5 if 𝑐 else 5` is still the `5`). Where the merge is a fresh variable every input flows into, the solver's join *is* the rule and nothing has to strip; where a pass builds the merged type by hand (`channelize`'s channel union, the `Transact` carrier's key seeds) it must intersect the refinements explicitly. - **Stripping is not the join.** It over-approximates in the safe direction (a witness every input establishes is thrown away) and it is not variance-stable: for a *collection* input, whose extent rides the contravariant `Fun` domain, relating a refined input to a stripped sibling demands `𝐷 <: {𝐷 | 𝑝}` and rejects two arms that are literally the same expression. `𝐷 <: {𝐷 | 𝑝}` is never a real obligation in this language — acquiring a witness is an explicit `cast` — so seeing one means an erasure manufactured it. Inputs whose extents genuinely differ meet on the domain (both witnesses accumulate — the extent both admit), since that is where a function type's join puts them. + **Stripping is not the join.** It over-approximates in the safe direction (a refinement every input establishes is thrown away) and it is not variance-stable: for a *collection* input, whose extent rides the contravariant `Fun` domain, relating a refined input to a stripped sibling demands `𝐷 <: {𝐷 | 𝑝}` and rejects two arms that are literally the same expression. `𝐷 <: {𝐷 | 𝑝}` is never a real obligation in this language — acquiring a refinement is an explicit `cast` — so seeing one means an erasure manufactured it. Inputs whose extents genuinely differ meet on the domain (both refinements accumulate — the extent both admit), since that is where a function type's join puts them. * **A `Mut` input derefs into the join**, exactly as a mutable read derefs into a tuple element, so a `Case` over two registers types as their *value*. The second-class discipline's rule 1 therefore has no `Mut` on the selection to reject; what it protects — a selected register reaching a position that writes through it — is its argument clause, which reads the argument *node*. See [No aliasing: `Mut` values are second-class (downward-only)](mutability.md#no-aliasing-mut-values-are-second-class-downward-only). * **`__elem` is bound by the refinement it rides**, so it is never free *in a type* — the free-variable walk must not report it so. * **Beta reduction discharges a refined parameter** when the argument's type entails it: substituting the argument is what establishes the precondition. Singletons are *not* erased after inference. They are ordinary refinements and ride through to the runtime like any other, which also keeps them available to a future constant fold. They print as the literal they pin (`5`, not `{Int | __elem == 5}`). -#### Refinements as witness sets +#### Refinements on the lattice -A refinement `{T | p}` carries a **set** of *witnesses* (each a [`Refinement`]) — the term for a refinement in its role as a black box to the subtyping lattice: the lattice accumulates witnesses and matches them by identity, never reasoning about what they imply (the predicate's logical content is real and used by the runtime, just opaque *here*). It is a fourth structural dimension on `CompactType`, width-subtyped exactly like records: **`{b₁ | S₁} <: {b₂ | S₂}` iff `b₁ <: b₂` and `S₂ ⊆ S₁ ∪ witnesses(b₁)`** — more refinements ⇒ subtype. So `{T | p, q} <: {T | p}` and `{T | p} <: T`, but `{T | q} ⊀ {T | p}`. Witnesses match by **type-blind structural equality of their predicate terms** (`Refinement`'s `PartialEq` / `eq_refinement_predicate`) — *not* by predicate implication (`{T | x > 0} ⊀ {T | x > -1}`). Structural matching makes witness identity agnostic to *where* a predicate was constructed (join planning re-mints `{D | p}` at every marker it emits — `make_iterate` / `make_restrict` / `refine_with` — and must match the structurally-identical contract recorded elsewhere on the tree) and to in-place type resolution (copies of one predicate along a monomorphization descent line differ only in their inferred-type slots); a pointer-equal predicate `Rc` short-circuits as the fast path, since a refinement that merely flows around shares its `Rc`. The witness set merges with the *same polarity rule as `rec`* (positive ⇒ intersect, negative ⇒ union) and is carried verbatim through simplification (witnesses are positional, never folded into a variable's identity, so co-occurrence merging can't move or drop them). +A **refined type** `{T | p}` carries a *set* of [`Refinement`]s, and the lattice treats each as a black box: it accumulates them and matches them by identity, never reasoning about what they imply (the predicate's logical content is real and used by the runtime, just opaque *here*). It is a fourth structural dimension on `CompactType`, width-subtyped exactly like records: **`{b₁ | S₁} <: {b₂ | S₂}` iff `b₁ <: b₂` and `S₂ ⊆ S₁ ∪ refinements(b₁)`** — more refinements ⇒ subtype. So `{T | p, q} <: {T | p}` and `{T | p} <: T`, but `{T | q} ⊀ {T | p}`. Refinements match by **type-blind structural equality of their predicate terms** (`Refinement`'s `PartialEq` / `eq_refinement_predicate`) — *not* by predicate implication (`{T | x > 0} ⊀ {T | x > -1}`). Structural matching makes refinement identity agnostic to *where* a predicate was constructed (join planning re-mints `{D | p}` at every marker it emits — `make_iterate` / `make_restrict` / `refine_with` — and must match the structurally-identical contract recorded elsewhere on the tree) and to in-place type resolution (copies of one predicate along a monomorphization descent line differ only in their inferred-type slots); a pointer-equal predicate `Rc` short-circuits as the fast path, since a refinement that merely flows around shares its `Rc`. The refinement set merges with the *same polarity rule as `rec`* (positive ⇒ intersect, negative ⇒ union) and is carried verbatim through simplification (refinements are positional, never folded into a variable's identity, so co-occurrence merging can't move or drop them). -A refinement is **required**, so `constrain_subtype` is strict for *concrete* bases: an unrefined concrete value does **not** flow into a refined position (`T ⊀ {T | p}`), and `{T | q} ⊀ {T | p}`. The one subtlety is the `S₂ ⊆ S₁ ∪ witnesses(b₁)` clause: when the subtype side's base `b₁` is an **inference variable**, it can still acquire the deficit `S₂ \ S₁`, so the solver flows `b₁ <: {b₂ | S₂ \ S₁}` onto the variable rather than rejecting (the refinement analog of how the record/function arms thread structure through a variable base; it fails later iff the variable resolves to a concrete base lacking those witnesses). This is what lets a value that is *already* refined be cast to acquire a further witness — `{D | p} ⇒ V <: {?a | q} ⇒ V` records `?a <: {D | p}`, stacking `q` over `p` (nested list-comprehension filters). Acquiring a refinement on a *concrete* value is still an *explicit* operation, not subsumption: the explicit `Cast` node from [PR #218](https://github.com/cambra-dev/Cambra/pull/218) (an upcast — `value <: target` — written `cast({D | r} ⇒ V, value)`) makes refinement-acquisition explicit, and the interpreter compiles a refinement on a **collection domain** to a runtime `Restrict`/`Filter` at the iteration boundary (the `Iterate`/`Restrict` arms of `operator_conversion`, where `extent_of` strips the domain refinement into a `Restrict`). The predicate `Expr` of each witness is inferred/coalesced like any other sub-tree (annotation-borne predicates via `emit_annotation_predicates` / `coalesce_type_predicates`). +A refinement is **required**, so `constrain_subtype` is strict for *concrete* bases: an unrefined concrete value does **not** flow into a refined position (`T ⊀ {T | p}`), and `{T | q} ⊀ {T | p}`. The one subtlety is the `S₂ ⊆ S₁ ∪ refinements(b₁)` clause: when the subtype side's base `b₁` is an **inference variable**, it can still acquire the deficit `S₂ \ S₁`, so the solver flows `b₁ <: {b₂ | S₂ \ S₁}` onto the variable rather than rejecting (the refinement analog of how the record/function arms thread structure through a variable base; it fails later iff the variable resolves to a concrete base lacking those refinements). This is what lets a value that is *already* refined be cast to acquire a further refinement — `{D | p} ⇒ V <: {?a | q} ⇒ V` records `?a <: {D | p}`, stacking `q` over `p` (nested list-comprehension filters). Acquiring a refinement on a *concrete* value is still an *explicit* operation, not subsumption: the explicit `Cast` node from [PR #218](https://github.com/cambra-dev/Cambra/pull/218) (an upcast — `value <: target` — written `cast({D | r} ⇒ V, value)`) makes refinement-acquisition explicit, and the interpreter compiles a refinement on a **collection domain** to a runtime `Restrict`/`Filter` at the iteration boundary (the `Iterate`/`Restrict` arms of `operator_conversion`, where `extent_of` strips the domain refinement into a `Restrict`). The predicate `Expr` of each refinement is inferred/coalesced like any other sub-tree (annotation-borne predicates via `emit_annotation_predicates` / `coalesce_type_predicates`). **Refinements in the post-inference check.** The post-inference structural check (`infer::check`, reimplemented on the same structural rules as emission via the `Typing` trait — see §2, *The post-inference check*) is **strict and refinement-aware throughout** — it does not strip refinements before its width-subtyping checks. It runs `constrain_subtype` in two places, both fully refinement-aware: -* **Adjacency rules** (a `Compose` link's `prev_cod <: next_dom`, an `Apply`'s argument-vs-domain) check *refinement flow*: feeding an unrefined producer into a refinement consumer is rejected (`T ⊀ {T | p}`), exactly as the solver is. There is **no cast escape** — a producer must already carry the refinement its consumer demands. A `… ≫ (id ≫ cast({D | r} ⇒ V))` chain composes because join planning surfaces the iterated / join-satisfying domain on the *producing* morphism's codomain, so the upstream genuinely supplies `{D | r}` (see the reconstructability bullets below). The producer's witness and the cast's contract are typically re-minted as distinct predicate terms, so the adjacency relies on the structural-predicate match above. +* **Adjacency rules** (a `Compose` link's `prev_cod <: next_dom`, an `Apply`'s argument-vs-domain) check *refinement flow*: feeding an unrefined producer into a refinement consumer is rejected (`T ⊀ {T | p}`), exactly as the solver is. There is **no cast escape** — a producer must already carry the refinement its consumer demands. A `… ≫ (id ≫ cast({D | r} ⇒ V))` chain composes because join planning surfaces the iterated / join-satisfying domain on the *producing* morphism's codomain, so the upstream genuinely supplies `{D | r}` (see the reconstructability bullets below). The producer's refinement and the cast's contract are typically re-minted as distinct predicate terms, so the adjacency relies on the structural-predicate match above. * **The reconcile** (a node's rule-reconstructed type vs the type inference recorded on it) is the plain strict `rule <: recorded` subtype check, refinements included (the recorded type may be a width-wider supertype — e.g. an annotation). A rule that rebuilds a node's type from its children rebuilds its refinements too, so a recorded refinement the reconstruction lacks is a real disagreement about the node — and in practice it is one specific bug: a **merge point that took one input's refinement** instead of the join of all of them (see the merge law above). Comparing modulo refinements here — stripping both sides, or a refinement-blind relation — is the *only* thing that hides that class, and this is the check best placed to catch it. Keeping it strict is what forced each merge point to join. For the reconcile to hold, the passes that *introduce* refined types post-inference (lambda-elim, join-planning) must leave each node's recorded type **reconstructable** — consistent with what the bottom-up rules rebuild from its children. These sites were emitting internally-inconsistent or under-refined nodes and are now fixed at the source rather than papered over by relaxing the check: @@ -528,7 +660,7 @@ Freshening (`freshen_above`) is polarity-free and recurses through the payload l There is no conversion *into* a solver type — the solver consumes `ccl::Type` as-is. The only adjustment Pass 1 makes is `normalize_annotation`, which readies a user annotation / expected type for constraint solving: * **Holes (`Type::Hole`):** become fresh `Type::Infer` variables at the current level. -* **Refinements:** are **kept** (recursing to normalize the inner) — they ride the lattice as refinement witnesses (above). A `Refinement(Hole, r)` source annotation thus becomes `Refinement(?fresh, r)`. +* **Refinements:** are **kept** (recursing to normalize the inner) — they ride the lattice natively (above). A `Refinement(Hole, r)` source annotation thus becomes `Refinement(?fresh, r)`. * **Everything else** — including existing `Type::Infer` vars, `Tuple`/`Record` products, and `Type::Variant` sums — is kept verbatim and handled by the solver's structural constraint rules. Tuples and records are width-subtyped positionally/by name; variants are admissible at both polarities (the dual of records), so they need no fresh-var indirection. ### Flowing Out: coalescing @@ -537,7 +669,7 @@ Once constraints are resolved (Pass 2), `coalesce_compact` resolves each node's * **Products:** dense `Index` keys become `Type::Tuple`; `Name` keys become `Type::Record`; a sparse `Index` product (an open/under-determined position) coalesces to a fresh `Type::Infer` rather than a concrete product. * **Variants:** materialize into `Type::Variant(Vec<(FieldKey, Type)>)` with tags in `BTreeMap` order. A variant payload sits at a record-field-like position, so it inherits that position's polarity and coalesces by the same rule as a record field value. An all-`Index` variant pretty-prints as a bare `A | B | C`. -* **Refinements:** the witness set carried at a position is re-wrapped as nested `Type::Refinement` layers around the materialized inner type (in first-insertion order — deterministic and, since consumers strip at all depths, order-independent). +* **Refinements:** the refinement set carried at a position is re-wrapped as nested `Type::Refinement` layers around the materialized inner type (in first-insertion order — deterministic and, since consumers strip at all depths, order-independent). * **Incompatible bounds:** if a variable accumulates multiple distinct concrete primitives (e.g. `Int` and `String`) with no tag to discriminate them, the solver emits an `IncompatibleBounds` error. A *tagged* sum is unaffected — `[.0: Int | .1: String]` is a single `Variant`, not a primitive collision. * **Recursive types:** the algorithm has no occurs check. With one-way Apply edges a self-application like `λx. x x` produces no cyclic bound graph — it types cleanly (MLsub would give `(α ∧ (α ⇒ β)) ⇒ β`; Cambra drops the unconstrained `α` leg and infers `(?a ⇒ ?b) ⇒ ?c`, an unapplied-lambda type carrying `Infer`s), while *misusing* one (`(λy. y y)(1)`) still fails with `ExpectedFunction`. Should a residual cyclic bound graph ever form, `coalesce_compact` rejects it with a `RecursiveType` error — a defensive check; no current emission path produces one. @@ -557,7 +689,7 @@ Some refinement predicates **close over an outer binder**. The motivating case i **Coalesce forces suspended substitutions.** `compact_go` threads a substitution accumulator: descending a bound edge composes the edge's *rendering morphism* (`edge_render_subst`: `ty_subst`, transported across `self_subst` by rename-inversion, or by the identity for a discharge — exact because the content lives in the post-discharge context and cannot mention the discharged binder, debug-asserted) and the composite is applied — *forced* — at each refinement-predicate leaf. A bound reached transitively through `𝑣 → 𝑤 → …` thus arrives with every edge's morphism composed (the deferred transitive closure recovered by the walk). Identity accumulator ⇒ no-op. -**Dependent application.** `Typing::apply` types `f(arg)`. Emit constrains `fn_ty <: (𝑥: 𝑑) ⇒ result` against an expected Pi (the one-way Apply shape edge of §2) and returns `result` under a suspended discharge `[𝑥 ↦ arg]` on a fresh variable's lower edge, fired on the partition predicate at coalesce. So `groupby(xs, key)(𝑘₀)` types as `{𝑖 | 𝑖 ▷ xs ▷ key == 𝑘₀} ⇒ 𝑉`. The **post-inference check** (`CheckCtx::apply`) re-runs the discharge on the resolved codomain so its reconstruction matches; `force_refinement` rewrites the predicate to the same term in both places, so the two refinements compare equal under structural witness equality (§4). +**Dependent application.** `Typing::apply` types `f(arg)`. Emit constrains `fn_ty <: (𝑥: 𝑑) ⇒ result` against an expected Pi (the one-way Apply shape edge of §2) and returns `result` under a suspended discharge `[𝑥 ↦ arg]` on a fresh variable's lower edge, fired on the partition predicate at coalesce. So `groupby(xs, key)(𝑘₀)` types as `{𝑖 | 𝑖 ▷ xs ▷ key == 𝑘₀} ⇒ 𝑉`. The **post-inference check** (`CheckCtx::apply`) re-runs the discharge on the resolved codomain so its reconstruction matches; `force_refinement` rewrites the predicate to the same term in both places, so the two refinements compare equal under structural refinement equality (§4). The expected binder is **always globally fresh** (proposal §5.2 verbatim; the §3.6 freshness discipline). The two-sided edge storage is what makes this sound at every polarity and in every constraint order: the correspondence `[𝑘 ↦ 𝑥]` and the discharge `[𝑥 ↦ arg]` compose forward along the closure regardless of whether `fn_ty` was concrete at the apply site or resolved only later (the opaque/higher-order case — a dependent function received as a *parameter* — now discharges correctly, unblocking O3 at the graph level). A contravariant position is reached by side-*swapping*, not inversion, so the discharge arrives at a `map`/aggregate's parameter domain intact. The remaining deferral is the domain-join corner — two *distinct* discharges meeting at one coalescing position (O1/O4) — guarded loudly by the closure bridge's tripwire. @@ -569,7 +701,7 @@ The expected binder is **always globally fresh** (proposal §5.2 verbatim; the **Deferred (flagged in code).** * **O2 (polymorphic case)** — `freshen_above` copy-and-freshens a refined value's predicate type slots through the shared cache (its `Refinement` arm), so a specialization's predicate is a proper freshen instance rather than a shared `Rc`. Immutable predicate terms are acyclic, so no refinement-cycle guard is needed. -* **O4** — two *different* discharges of one refinement (`g(0)` vs `g(1)`) are distinguished once forced — `force_refinement` rewrites the predicate term and witness equality is structural (§4) — and the constraint cache is σ-aware, so the two discharges record distinct edges rather than conflating. The residual domain-join corner is two *distinct non-invertible* morphisms meeting at one variable (O1/O4), guarded loudly by `bridge_holder_gap`'s panic tripwire rather than silently dropped. +* **O4** — two *different* discharges of one refinement (`g(0)` vs `g(1)`) are distinguished once forced — `force_refinement` rewrites the predicate term and refinement equality is structural (§4) — and the constraint cache is σ-aware, so the two discharges record distinct edges rather than conflating. The residual domain-join corner is two *distinct non-invertible* morphisms meeting at one variable (O1/O4), guarded loudly by `bridge_holder_gap`'s panic tripwire rather than silently dropped. The pipeline passes downstream of inference treat function types structurally and compare modulo the Pi binder (`Type::without_pi_names`). **Refinement-predicate compilation is deferred out of lambda-elim** (proposal §6.3): predicates ride through inference and lambda-elim in their bare pointful form (a bare boolean over the implicit `REFINEMENT_BINDER`), and **planning** compiles them. Order matters: the group-by / hash-join recognizers run *first*, on the bare form — compiling first would destroy the pointful shapes they match (see the pointful-join-recognizers plan) — and `planning::compile_refinement_predicates` then runs the lambda-elim → simplify sub-pipeline on each remaining predicate (keyed by predicate `Rc` identity) before the generic `iterate`/`restrict` lowering consumes it. This is what lets a refined collection — including a group-by over a *filtered* source (`[sum(x) for x in groupby([y+10 for y in xs if y<6], key)]`) — compile to a runtime `Restrict`/`Filter` rather than reaching op-conversion as an un-compiled predicate. Single-key dependent lookups (`sum(groupby(xs, key)(k))`) and the nested filtered-source group-by both run end-to-end with correct values. @@ -659,7 +791,13 @@ in the type recording that it happened. Nor is the join undefined. It is the dependent sum `Σ (𝑤 ∈ {𝐷ᵢ}). 𝑤 ⤇ 𝑉` over the candidate domains, whose witness `𝑤` is the runtime branch discriminant and which is -eliminated by distributing the consumer over it. **That Σ is the least upper bound** +eliminated by distributing the consumer over it. (*Witness* here is the standard +sense — the inhabitant that picks which summand you are in — and is deliberately +kept. It is unrelated to the retired sense of the word, which named a refinement in +its role as a black box to the subtyping lattice; that reading is now spelled out +as a property of the lattice instead, under +[Refinements on the lattice](#refinements-on-the-lattice). A sweep for the retired +term should leave this one alone.) **That Σ is the least upper bound** — data functions over distinct domains are incomparable, and their join is a different element of the lattice rather than one of them. So the lattice is *incomplete* without Σ, and the three rules here are one model: @@ -741,7 +879,7 @@ the join like any other, so a `Case` over two registers types as their *value*, the second-class discipline still rejects a selected register reaching a write position because rule 1 reads the argument *node* rather than its type (see the merge-law bullets under -[Refinements as witness sets](#refinements-as-witness-sets)). +[Refinements on the lattice](#refinements-on-the-lattice)). > **Deferred — heterogeneous-scalar union (follow-up).** The design goal is for > heterogeneous scalar arms (`1 if c else "x"`) to coalesce to a union. @@ -1041,13 +1179,13 @@ Consult these definitions as needed; each term is introduced in context in §1 | **Level mismatch** | Algebraic subtyping | During `constrain` involving a variable `v`, the condition that the other side contains a variable whose level is numerically higher than `v`'s. Triggers extrude. | | **Extrude** | Algebraic subtyping | On a level mismatch, the process of copying a type down to a target level by replacing each too-high variable with a fresh proxy at that level (linked back via the polarity-appropriate bound), so the constraint can be recorded without leaking inner-scope variables. | | **Scheme (PolyScheme)** | Algebraic subtyping | A generalized type with a cutoff level. Variables whose level is numerically greater than the cutoff are quantified; using the scheme *instantiates* (freshens) them at the current level. | -| **CompactType** | Algebraic subtyping | A flat, per-position bag of contributions (variables, atoms, an optional record shape, an optional variant shape, an optional function shape, and a witness set) produced for simplification and co-occurrence analysis. | +| **CompactType** | Algebraic subtyping | A flat, per-position bag of contributions (variables, atoms, an optional record shape, an optional variant shape, an optional function shape, and a refinement set) produced for simplification and co-occurrence analysis. | | **`CompactGraph`** | Algebraic subtyping | A top-level `CompactType` plus a side-table of recursive-variable definitions; the intermediate produced by `compact_type` and consumed by `simplify_type` / `coalesce_compact`. | | **Coalesce** | Algebraic subtyping | Materializing a `CompactGraph` back into an immutable `ccl::Type`: positive occurrences become a union of lower bounds, negative occurrences an intersection of upper bounds. | | **`FieldKey`** | Algebraic subtyping | The shared key for record/tuple fields *and* variant tags: `Index(usize)` for positional (anonymous) keys, `Name(SmolStr)` for named ones. | | **`Variant` (tagged sum)** | Both | The single sum representation: `Type::Variant`, keyed by [`FieldKey`]. Named tags are source-level `.Tag(...)`; positional (`Index`) tags are anonymous sums (what `++` produces). Width-subtyping is the dual of records (a subtype has *fewer* tags). | -| **`ccl::Type`** | Both | The public, immutable, user-facing AST type — and, since the unification, also the solver's working representation. Inference unknowns are `Type::Infer`; `Hole` is normalized to a fresh var, while `Refinement` is kept and rides the lattice as a refinement witness. | -| **Refinement witness** | Both | A `Type::Refinement(T, r)` carries a refinement witness `r` (an immutable predicate `Rc`) — a refinement in its role as a black box to the subtyping lattice. A type holds a *set* of witnesses, width-subtyped like records (more refinements ⇒ subtype; `{T\|p,q} <: {T\|p}`). Witnesses compare by type-blind structural predicate equality (`Refinement`'s `PartialEq`; pointer-equal predicates short-circuit) — not implication. A refinement is *required* — `constrain_subtype` is strict (`T ⊀ {T\|p}`); acquiring one is an explicit runtime `Restrict` at the collection-iteration boundary, not subsumption. | +| **`ccl::Type`** | Both | The public, immutable, user-facing AST type — and, since the unification, also the solver's working representation. Inference unknowns are `Type::Infer`; `Hole` is normalized to a fresh var, while `Refinement` is kept and rides the lattice as a refinement. | +| **Refinement** | Both | A `Type::Refinement(T, r)` carries a refinement `r` (an immutable predicate `Rc`) — a refinement in its role as a black box to the subtyping lattice. A type holds a *set* of refinements, width-subtyped like records (more refinements ⇒ subtype; `{T\|p,q} <: {T\|p}`). Refinements compare by type-blind structural predicate equality (`Refinement`'s `PartialEq`; pointer-equal predicates short-circuit) — not implication. A refinement is *required* — `constrain_subtype` is strict (`T ⊀ {T\|p}`); acquiring one is an explicit runtime `Restrict` at the collection-iteration boundary, not subsumption. | | **Let Binding Resolution** | Cambra-Specific | Ensuring a `Let` binding's fully resolved type overwrites the type of any `Var` references to it within the let body. | | **`InferArena`** | Cambra-Specific | The single owner of every inference variable minted during one `infer()` run. Captures each mint through a thread-local sink and, on `Drop`, clears all variables' bounds to break the `Rc` cycles that mutual subtyping constraints form — the end-of-inference cleanup that reference counting alone cannot do. See §3.2. | | **Pi type** | Both | A `Type::Fun` with `name: Some(𝑥)` — the dependent function type `(𝑥: domain) ⇒ codomain`, with `𝑥` bound in `codomain` and referenceable by nested refinement predicates. `name: None` is the ordinary arrow. See §4.5. | diff --git a/src/ccl/expr.rs b/src/ccl/expr.rs index 57dcb1cf..cfdbab9c 100644 --- a/src/ccl/expr.rs +++ b/src/ccl/expr.rs @@ -177,8 +177,8 @@ pub enum TypedExprNode { /// because `{𝐷 | 𝑝} <: 𝐷` — so viewing an unrefined-domain collection /// function at a refined-domain type is sound. The /// refinement-aware solver ([`crate::ccl::infer::solver::constrain_subtype`]) - /// flows the witness onto the fresh target-domain variable, *stacking* it - /// onto any witnesses the value already carries, so nested casts compose + /// flows the refinement onto the fresh target-domain variable, *stacking* it + /// onto any refinements the value already carries, so nested casts compose /// (nested list comprehensions). `target`'s predicate is inferred by the /// same `emit_annotation_predicates` / `coalesce_type_predicates` path as /// any refinement-bearing type. A *covariant* refinement (e.g. casting diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index 02239f18..c30e77af 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -1223,7 +1223,7 @@ pub fn check_mut_write_targets(expr: &Expr) -> Result<(), Vec> { /// `Mut` on `user_annotation` (while the coalesced `.ty` slot is the value type /// — reads deref), and a *non-`Mut`* annotation (`y: int = x`) declares a value, /// so the binding is not a mutable variable even if a write-site demand coalesced its `.ty` -/// to `Mut`. Only when there is no annotation does `.ty` witness mutability (a +/// to `Mut`. Only when there is no annotation does `.ty` itself decide mutability (a /// coalesced alias). Reading the annotation first is what makes `y += 1` on a /// `y: int = x` deref-copy the "not a mutable variable" error the discipline /// promises, rather than a silently-accepted write. diff --git a/src/ccl/infer/check.rs b/src/ccl/infer/check.rs index 2b6ab44a..6bd84115 100644 --- a/src/ccl/infer/check.rs +++ b/src/ccl/infer/check.rs @@ -35,7 +35,7 @@ use super::{lit_base, map_constrain_err}; /// /// Refinement handling: Check is refinement-*aware* — it constrains the real /// (un-stripped) types via [`Typing::require_sub`], so the lattice's -/// restriction-witness subsetting (`unrefined ⊀ refined`) is enforced. The explicit +/// restriction-refinement subsetting (`unrefined ⊀ refined`) is enforced. The explicit /// cast operator canonicalizes restriction *acquisition*, so the long-standing /// deep strip is gone, and the check runs both after inference *and* after /// join planning (`context.rs`). @@ -49,7 +49,7 @@ use super::{lit_base, map_constrain_err}; /// `Rc` at every marker, the producer's `{D | r}` and the consumer's contract /// rarely share an `Rc`; [`crate::ccl::infer::solver`]'s subset check matches them /// by *structural predicate equality* (not just `Rc` identity) so the re-minted -/// witnesses still chain. (Previously this gap was papered over by a +/// refinements still chain. (Previously this gap was papered over by a /// `contains_cast` peel in `emit_compose` and by leaving planning output un-checked.) pub(super) struct CheckCtx { schemes: OperatorSchemes, @@ -121,7 +121,7 @@ impl Typing for CheckCtx { ) -> Result<(), LocatedInferError> { // Delegate to the solver's `constrain_subtype` — the single source of // truth for width/variance and (since refinements ride the lattice as - // restriction witnesses) witness subsetting. A failure is recorded (not + // restriction refinements) refinement subsetting. A failure is recorded (not // propagated) so the walk continues and reports every error. if let Err(e) = constrain_subtype(sub, sup, &mut ConstrainCache::new_kind_blind()) { let located = self.raise(map_constrain_err(e, &at())); @@ -191,7 +191,7 @@ impl Typing for CheckCtx { at: &dyn Fn() -> String, ) -> Result<(Type, Type), LocatedInferError> { // Destructure the resolved type directly (no inference vars). Peel any - // outer refinement witnesses the function picked up during solving, + // outer refinements the function picked up during solving, // and — pre-desugar only — read through a transparent handle to the // value it wraps: a defer's `Feed` to its channel, and a `Mut` history to // its value (a `Mut`-typed collection used as a for-loop source derefs diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs index d2c54806..47e4872f 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -37,7 +37,7 @@ pub(super) struct Binding { /// Whether a `let` bound to `def` at `level` should be **generalized** — /// typed polymorphically, with each use [`PolyScheme::instantiate`]ing a fresh -/// copy and the coalesce walk specializing per distinct resolved use type +/// copy and the coalesce walk specializing per distinct use instantiation /// ([`specialize_use`](super::solve::specialize_use)). Requires both of: /// /// - **A function definition** (`def` is a `Lambda`). Let-polymorphism @@ -145,7 +145,7 @@ impl InferCtx { /// `Type`: every `Hole` becomes a fresh inference variable at the /// current level. Everything else — including existing `Infer` vars, /// the structural variants the solver operates on, and `Refinement` - /// wrappers (refinements ride the lattice as refinement witnesses) — is + /// wrappers (refinements ride the lattice as refinements) — is /// kept, recursing to normalize nested holes. pub(super) fn normalize_annotation(&self, ty: &Type) -> Type { match ty { @@ -153,7 +153,7 @@ impl InferCtx { Type::Hole => fresh_var(self.level), // Refinements ride the lattice: keep the wrapper, normalize the // inner (so a `Refinement(Hole, r)` source annotation becomes - // `Refinement(?fresh, r)` rather than losing the witness). + // `Refinement(?fresh, r)` rather than losing the refinement). Type::Refinement(inner, r) => { Type::Refinement(Box::new(self.normalize_annotation(inner)), r.clone()) } @@ -309,7 +309,7 @@ impl Typing for InferCtx { let scheme = if generalize { // Polymorphic: generalize at the outer level. Each `Var` use // instantiates a fresh copy; the coalesce walk then specializes - // the definition per distinct resolved use type + // the definition per distinct use instantiation // (`specialize_use`). PolyScheme::poly(self.level, bound_ty.clone()) } else { diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index 96d12541..454a8427 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -472,7 +472,7 @@ pub(super) fn emit_lambda( let param_simple = ctx.normalize(¶m.ty); param.ty = param_simple.clone(); // The param is bound in scope under the *unrefined* `param_simple`, so - // `Var(param)` body references stay bare; restriction witnesses decorate only + // `Var(param)` body references stay bare; restriction refinements decorate only // the function boundary. let body_ty = ctx.scoped(¶m.name, ¶m_simple, |ctx| ctx.subexpr(body))?; @@ -511,7 +511,7 @@ pub(super) fn emit_lambda( /// rather than as a bare `value <: target` obligation, because the refinement /// lattice is strict (`unrefined ⊀ refined`) so the value cannot flow *into* /// the refined target by subtyping. Re-wrapping the domain stacks `r` over any -/// witnesses `value` already carries, so chained casts (nested list-comprehension +/// refinements `value` already carries, so chained casts (nested list-comprehension /// filters) compose. /// /// `as_function` is the mode-generic decompose: in Emit the one-way @@ -525,7 +525,7 @@ pub(super) fn emit_lambda( /// domain-refinement's bare predicate is typed by `emit_bare_predicate` (the /// element bound to `D`, the predicate checked `Bool`) exactly as [`emit_lambda`] /// handles a lambda's own refinement; `coalesce_type_predicates(&expr.ty)` -/// resolves it later (the result shares `target`'s witness `r`). +/// resolves it later (the result shares `target`'s refinement `r`). /// /// Shared by `emit_node` (Emit) and `check_node` (Check) via [`Typing`]. pub(super) fn emit_cast( @@ -864,7 +864,7 @@ pub(super) fn emit_aggregate( /// /// A genuinely-polymorphic function definition ([`Typing::is_generalizable`]) /// is generalized so each `Var` use instantiates a fresh copy; the coalesce -/// walk later specializes the definition per distinct resolved use type +/// walk later specializes the definition per distinct use instantiation /// ([`specialize_use`](super::solve::specialize_use)). Everything else is bound /// monomorphically and shared (the pre-let-poly behavior). Generalization /// carries no use-count or generator condition — see @@ -1300,7 +1300,7 @@ pub(super) fn emit_compose( for (i, t) in tys.iter().enumerate().skip(1) { let (d_i, c_i) = ctx.as_function(t, &|| "Compose[i]".to_string())?; // Strict refinement-aware adjacency: `prev_cod <: next_dom`, refinement - // witnesses and all — no cast escape. A producer must already supply the + // refinements and all — no cast escape. A producer must already supply the // refinement its consumer demands. Join planning surfaces the // join-satisfying / iterated domain on each producing morphism's // codomain (`planning`'s `refine_codomain` / iteration-source diff --git a/src/ccl/infer/mod.rs b/src/ccl/infer/mod.rs index d69261e0..8af3acf0 100644 --- a/src/ccl/infer/mod.rs +++ b/src/ccl/infer/mod.rs @@ -13,14 +13,14 @@ //! Because the vars are shared `Rc`s, later constraints //! accumulate into bounds that are already visible through the stored //! `Type` — no side table is needed. Domain refinements ride the type -//! lattice as restriction witnesses on [`Type::Refinement`] (introduced by the +//! lattice as restriction refinements on [`Type::Refinement`] (introduced by the //! `cast` Apply arm), so they flow through the solver structurally. //! 2. **Coalesce + write-back + monomorphize**: walk the tree again and, for //! each node, run //! [`coalesce_compact`](crate::ccl::infer::solver::coalesce_compact) to //! resolve the inference variables in its `expr.ty` in place. The same //! walk lowers let-polymorphism: a use of a generalized `let` is -//! specialized at first visit, memoized per distinct resolved type +//! specialized at first visit, memoized per distinct instantiation //! ([`specialize_use`](solve::specialize_use)), and the `let` rebuilds //! itself as the chain of demanded specializations //! ([`coalesce_generalized_let`](solve::coalesce_generalized_let)). @@ -38,7 +38,7 @@ //! monomorphic, generalization is paired with **monomorphization**, //! integrated into the coalesce walk: at a generalized use, the walk resolves //! the instantiation type off the live constraint graph (complete by then), -//! emits one specialized clone of the definition per distinct resolved type +//! emits one specialized clone of the definition per distinct instantiation //! (`freshen_expr_type_slots` + a constrain-against-the-live-use-type pin + a //! re-entrant coalesce), and rewrites the use to reference its //! specialization. So inference both type-checks the polymorphism and lowers diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index 66e8298b..cf284d07 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -11,9 +11,10 @@ // The coalesce walk also performs **integrated monomorphization**: let- // generalization is lowered to concrete, per-type code *inside* the walk. A // use of a generalized binding specializes at first visit (`specialize_use`, -// from `coalesce_node`'s `Var` hook), memoized per distinct resolved type so -// same-typed uses share one definition. The binding's `let` node then rebuilds -// itself as the chain of demanded specializations (`coalesce_generalized_let`). +// from `coalesce_node`'s `Var` hook), memoized per distinct instantiation +// (`SpecKey`) so uses that instantiate it identically share one definition. The +// binding's `let` node then rebuilds itself as the chain of demanded +// specializations (`coalesce_generalized_let`). // The coalesce and monomorphization arms are mutually recursive // (`coalesce_node` ↔ `specialize_use`) over one shared [`CoalesceCtx`], so they // live in a single module. @@ -21,8 +22,9 @@ use crate::ccl::ccl_utils::PredMemo; use crate::ccl::infer::InferError; use crate::ccl::infer::solver::{ - CoalesceError, ConstrainCache, FreshenCache, FreshenLevel, coalesce_compact, compact_type, - constrain_subtype, freshen_expr_type_slots, seed_chan_dom_pairings, simplify_type, + CoalesceError, ConstrainCache, FreshenCache, FreshenLevel, SpecKey, coalesce_compact, + compact_type, constrain_subtype, freshen_expr_type_slots, seed_chan_dom_pairings, + simplify_type, spec_key, }; use crate::ccl::provenance::NodeId; use crate::ccl::symbolic::symbolic; @@ -119,7 +121,7 @@ fn push_coalesce_err( /// /// Beyond resolving types, the walk performs **integrated monomorphization**: /// a use of a generalized `let` is specialized at first visit (memoized per -/// distinct resolved type), so every parent's type is derived from concrete +/// distinct instantiation), so every parent's type is derived from concrete /// children on the first pass — there is no post-coalesce splice and no /// re-derivation of dependent types. The constraint graph is *complete* by /// coalesce time (emission saw the whole program), so a use's instantiation @@ -167,16 +169,16 @@ impl CoalesceCtx { self.record_read_for(ReadPurpose::Stamp, unresolved, resolved, label); } - /// [`record_read`](Self::record_read) for a read whose result is a - /// specialization *key* rather than a type stamped on the tree — see - /// [`ReadPurpose::SpecializationKey`]. - fn record_read_spec_key( + /// [`record_read`](Self::record_read) for a use's instantiation resolution, + /// which is consumed structurally rather than stamped on the tree — see + /// [`ReadPurpose::Instantiation`]. + fn record_read_instantiation( &mut self, unresolved: &Type, resolved: &Type, label: impl Fn() -> String, ) { - self.record_read_for(ReadPurpose::SpecializationKey, unresolved, resolved, label); + self.record_read_for(ReadPurpose::Instantiation, unresolved, resolved, label); } fn record_read_for( @@ -205,35 +207,40 @@ impl CoalesceCtx { #[derive(Clone, Copy, PartialEq, Eq)] enum ReadPurpose { /// The resolution was **stamped on a node**, so every part of it is - /// load-bearing downstream: refinement witnesses are compared (by layer + /// load-bearing downstream: refinements are compared (by layer /// count — see [`types_agree_modulo_unread`]) along with the base skeleton. Stamp, - /// The resolution keyed a specialization (`specialize_use`'s memo lookup and - /// the baseline for the clone's two-way pin), and is *not* what the use node - /// ends up carrying — that is the clone's own coalesced type. + /// A use's instantiation resolution in [`specialize_use`], which is consumed + /// *structurally* — it seeds the clone's channel-domain pairings + /// (`seed_chan_dom_pairings`) and blames a resolution failure — and is **not** + /// what the use node ends up carrying (that is the specialization's own + /// coalesced type). It is also not the specialization key: keying on a resolved + /// type is exactly the bug [`SpecKey`] replaced. /// - /// Witnesses are excluded from the comparison here, and the reason is not that - /// a bound arrives late — nothing does. An argument's witness reaches the + /// Refinements are excluded from the comparison here, and the reason is not that + /// a bound arrives late — nothing does. An argument's refinement reaches the /// instantiation as a **lower** bound on the domain variable /// (`(8, 0) <: ?dom`, from the emit-time `arg <: domain` edge), and a domain is /// a *negative* position, where coalescing intersects **upper** bounds. So the - /// witness is in the graph before this read and simply not on the side the read + /// refinement is in the graph before this read and simply not on the side the read /// consults. The pin that immediately follows adds the clone's parameter /// variable as an upper bound of `?dom` and drives the same information into - /// it, which is the path that makes the witness visible — so re-resolving the + /// it, which is the path that makes the refinement visible — so re-resolving the /// snapshot at end of pass yields it (`pick = \lo, hi -> …` at `pick(8, 0)`: /// `?dom` has `lower=[(8, 0)] upper=[?52]` and resolves to `(Int)`; after the /// pin, `upper=[?52, (?89)]` and it resolves to `(8)`). /// /// That makes the drift a property of *when* the read is taken relative to the /// pin, not of any bound going stale — which is why every [`Stamp`](Self::Stamp) - /// read is stable and only this one moves. The key's only consumer is - /// [`Specialization::use_ty`]'s equality, where a witness the read could not see - /// can only cause a **miss** — a fresh private clone, at worst a wasted one, - /// never a mis-typed use. The *base skeleton* is still held fixed: a stale - /// skeleton could make the lookup **hit** the wrong clone, which is a different - /// thing entirely. - SpecializationKey, + /// read is stable and only this one moves. Excluding refinements is sound because + /// this resolution's consumers are refinement-insensitive: `seed_chan_dom_pairings` + /// matches positions constructor-wise *through* refinements to find rigid + /// `ChanDom` names, and it already tolerates a position where the two sides + /// disagree structurally. Nothing about *sharing* rides on this read — that is + /// [`SpecKey`]'s job, and it consults both bound lists precisely so it does not + /// depend on which polarity a rendering would have picked. The *base skeleton* + /// is still held fixed here: a stale skeleton would pair channel domains wrong. + Instantiation, } /// One type the walk read (debug builds): the var-laden type exactly as it @@ -277,13 +284,13 @@ fn assert_reads_stable(reads: &[ReadRecord]) { /// **bounds on inference variables**, so this checks the *structural skeleton* a /// bound determines — bases, ranges, sources, Pi binder names, /// function/product/variant shape, and, for a [`ReadPurpose::Stamp`] read, the -/// *number* of refinement layers at each position. A witness is lattice content +/// *number* of refinement layers at each position. A refinement is lattice content /// like a record field, so a bound determines it as much as it determines the /// base: one appearing on — or vanishing from — a variable an earlier read /// consumed is exactly the staleness this guards, and with every literal /// carrying a singleton, refinement-bearing types are the common case rather -/// than the exotic one. `witnesses` is `false` only for the specialization-key -/// read that documents why. +/// than the exotic one. `refinements` is `false` only for the +/// [`Instantiation`](ReadPurpose::Instantiation) read, which documents why. /// /// Two drifts are legitimate and out of scope: /// @@ -298,11 +305,11 @@ fn assert_reads_stable(reads: &[ReadRecord]) { /// — both lowering by the very machinery this guards, neither a stale /// bound. The predicate *terms* are checked elsewhere (`check_scope_valid` /// and the post-inference `check` reconcile). Layer *count* is therefore the -/// strongest witness comparison available here: it catches a witness arriving +/// strongest refinement comparison available here: it catches a refinement arriving /// or leaving without depending on term identity, which legitimately churns. #[cfg(debug_assertions)] -fn types_agree_modulo_unread(read: &Type, now: &Type, witnesses: bool) -> bool { - // Peel refinement layers, counting them. The *base* under the witnesses is +fn types_agree_modulo_unread(read: &Type, now: &Type, refinements: bool) -> bool { + // Peel refinement layers, counting them. The *base* under the refinements is // what recurses structurally; predicate content is out of scope (above). fn peel<'t>(mut t: &'t Type, layers: &mut usize) -> &'t Type { while let Type::Refinement(inner, _) = t { @@ -314,7 +321,7 @@ fn types_agree_modulo_unread(read: &Type, now: &Type, witnesses: bool) -> bool { let (mut read_layers, mut now_layers) = (0, 0); let read = peel(read, &mut read_layers); let now = peel(now, &mut now_layers); - if witnesses && read_layers != now_layers { + if refinements && read_layers != now_layers { return false; } match (read, now) { @@ -341,26 +348,26 @@ fn types_agree_modulo_unread(read: &Type, now: &Type, witnesses: bool) -> bool { }, ) => { n1 == n2 - && types_agree_modulo_unread(d1, d2, witnesses) - && types_agree_modulo_unread(c1, c2, witnesses) + && types_agree_modulo_unread(d1, d2, refinements) + && types_agree_modulo_unread(c1, c2, refinements) } (Type::Tuple(xs), Type::Tuple(ys)) => { xs.len() == ys.len() && xs .iter() .zip(ys) - .all(|(x, y)| types_agree_modulo_unread(x, y, witnesses)) + .all(|(x, y)| types_agree_modulo_unread(x, y, refinements)) } (Type::Record(xs), Type::Record(ys)) => { xs.len() == ys.len() && xs.iter().zip(ys).all(|((nx, x), (ny, y))| { - nx == ny && types_agree_modulo_unread(x, y, witnesses) + nx == ny && types_agree_modulo_unread(x, y, refinements) }) } (Type::Variant(xs), Type::Variant(ys)) => { xs.len() == ys.len() && xs.iter().zip(ys).all(|((kx, x), (ky, y))| { - kx == ky && types_agree_modulo_unread(x, y, witnesses) + kx == ky && types_agree_modulo_unread(x, y, refinements) }) } // Two histories of *different* kinds never agree — an `Overwrite` and a @@ -405,10 +412,10 @@ fn types_agree_modulo_unread(read: &Type, now: &Type, witnesses: bool) -> bool { domain: domain.clone(), codomain: value.clone(), }; - types_agree_modulo_unread(&stream, other, witnesses) + types_agree_modulo_unread(&stream, other, refinements) } crate::ccl::HistoryKind::Overwrite => { - types_agree_modulo_unread(value, other, witnesses) + types_agree_modulo_unread(value, other, refinements) } }, _ => false, @@ -438,48 +445,92 @@ struct SpecializeFrame { /// The binding's polymorphism level — the freshen cutoff: variables /// deeper than this are the quantified ones. cutoff: Level, - /// Specializations minted so far. Scanned linearly, comparing a candidate use's - /// resolved type against each entry's [`Specialization::use_ty`] by `PartialEq` - /// — structural, with refinement witnesses comparing by type-blind predicate - /// equality — so same-typed uses share one specialization. + /// Specializations minted so far, scanned linearly. + /// A candidate use's [`SpecKey`] is compared against each entry's — both + /// computed by the *same* procedure at the *same* point in the pin's lifecycle + /// (from the use's live type, before its own pin), so the comparison is + /// self-consistent. What it is *not* is instantaneous: an entry was keyed + /// before its **own** pin, a candidate after every intervening one, and a pin + /// can widen a key that is not its own. A consumer's pin is what makes the + /// demand on a nested use's result concrete, and that demand reaches the key + /// through the `codomain <: demand` channel the negative read follows by + /// design — so in `f(f(3))`, where the walk takes function before argument, + /// the inner use is keyed against a demand the outer use's pin deposited. Key + /// equality is therefore walk-order sensitive (observably so once a demand + /// carries structure a key records; where it resolves to a bare base the two + /// reads agree). The residue is over-splitting, which costs a clone rather + /// than sharing a wrong one. See `src/ccl/design/type-inference.md`, + /// "Keying a specialization". /// - /// **A refinement makes two uses distinct**, so `f(1)` and `f(2)` mint separate - /// clones now that a literal carries its own singleton. Keying modulo refinements - /// would be the better rule — a refinement changes no code — but the clone is - /// pinned to its use type, so a shared clone would carry one use's refinement and - /// reject the others. Sharing needs the clone built at the stripped type - /// throughout, which is more than a key change. + /// **What keeps the scan cheap, and what would stop.** Each comparison is a + /// deep structural [`SpecKey`] walk, so the cost is quadratic in a binding's + /// specialization count. The bound on that count is *not* "one per distinct + /// type": every literal carries its own singleton refinement, so the rule is + /// one specialization per distinct argument tuple, and a definition called + /// with a fresh literal tuple at every site grows `specs` with **call sites**. + /// What holds it down today is `inline`, which beta-reduces scalar UDFs — the + /// definitions that survive to be cloned are the collection-producing ones it + /// leaves cached. If that ever bites it is the scan that has to change, not + /// the key. /// - /// The comparison is deliberately conservative in one direction, and it matters - /// that it is *this* direction: an entry's key is the clone's **coalesced** type, - /// which carries every witness the pin delivered, while a candidate's is its - /// instantiation resolved *before* its own pin runs — where a witness sitting on - /// the domain's *lower* bounds is invisible (see - /// [`ReadPurpose::SpecializationKey`]). So a use whose witness the pre-pin - /// resolution cannot see does not match an otherwise-identical entry, and mints - /// its own clone: a wasted clone, never a use served by a clone pinned to - /// someone else's refinement. + /// **Both sides being one procedure is the load-bearing part.** Keying an entry + /// on the clone's *coalesced* type instead is what made this table write-only: + /// a clone type carries whatever the pin settled, a candidate's pre-pin + /// resolution does not, and for any definition whose clone type acquires a + /// refinement across the pin the two could never be equal — so even two *identical* + /// call sites missed each other and minted a clone apiece. (The rationale that + /// justified it — that a later same-typed use resolves through the first pin's + /// extended chains — does not hold: every use instantiates its own fresh + /// variables, which the first clone's pin never touches.) /// - /// The waste is per **call site**, not per distinct type, for any definition - /// whose clone type acquires a witness only across the pin — two calls at the - /// *same* literal miss each other too. Which definitions those are depends on - /// how the body uses the parameter: `\a, b -> a + b` applied at `(1, 2)` keys on - /// `((1, Int) ⇒ Int)` and shares one clone, while `\lo, hi -> sum([v for v in xs - /// if v >= lo])` applied at `(8, 0)` keys on `((Int) ⇒ Int)` against an entry - /// stored as `((8) ⇒ Int)` and does not. Both candidate fixes are the ones noted - /// above — key modulo refinements (needs the clone built at the stripped type), - /// or resolve the key *after* the pin. + /// **Why the key is not a resolved `Type`.** A resolved type is a + /// polarity-correct *rendering*: a domain resolves from upper bounds (what the + /// body demands), so a position the body ignores is narrowed away and an + /// argument's refinement — a *lower* bound — is invisible unless + /// `compact_type`'s opposite-polarity fallback happens to fire there. The + /// clone's interior reads its parameter at a positive position and sees exactly + /// those refinements. Keying on a rendering therefore compared one polarity's view + /// against a clone built from the other's, and two uses differing only in a + /// key-invisible position shared a clone whose interior asserted the *first* + /// use's argument (`\a, b -> a + b` at `(1, 2)` and `(1, 5)` both keyed on + /// `((1, Int) ⇒ Int)`, and the shared clone typed `.1` as `2`). A [`SpecKey`] + /// keeps *both* directed reads of the instantiation instead — including the one + /// whose domain follows lower bounds — so it sees what the pin transmits. + /// + /// **The remaining gap: this over-splits.** The key summarizes the pin's + /// *input*, so two uses that differ in a position the clone never reads still + /// key apart — `\a, b -> a` at `(1, 2)` and `(1, 5)` mints two identical clones, + /// and a definition containing a `defer` mints one per use (its channel domain is + /// named per instantiation, so those clones genuinely *are* distinct). Every + /// literal carries a singleton, so the practical rule is one clone per distinct + /// argument tuple; `inline` beta-reduces scalar UDFs, but a + /// collection-producing one stays cached, so that is where code size grows. + /// + /// Closing it means keying on the pin's *output* — the finished clone — which + /// cannot be a lookup, only a build-then-dedupe: build for every use, then + /// discard a clone that is structurally equal to an existing entry + /// (`TypedExpr`'s `PartialEq` already excludes `NodeId` and compares types with + /// type-blind refinement equality, which is the right notion). That shares + /// exactly when the emitted code is identical. It needs three things this does + /// not: α-equivalence over the names minted fresh per clone (`Name::mono` uids + /// from nested specializations, coalesce's `Infer` placeholders, and the + /// per-instantiation `ChanDom` names) — most cheaply by drawing them from a + /// clone-local counter and globalizing on retention; a way to undo the discarded + /// clone's pin, which has already deposited bounds into the live graph; and + /// reference-liveness filtering at the splice, since a discarded clone's walk can + /// leave specializations on an *enclosing* frame with no surviving use. The two + /// compose — this key as the fast path, clone-equality as a precision tier on a + /// miss — so nothing here has to be undone to get there. specs: Vec, } /// One memoized specialization of a generalized definition. struct Specialization { - /// The memo key: this specialization's **own coalesced type** — which is what - /// the use node carrying it is stamped with, and is the use's instantiation type - /// plus whatever the two-way pin settled. Not the pre-pin `resolved` snapshot the - /// lookup compares against; see [`SpecializeFrame::specs`] for why the asymmetry - /// is the safe direction. - use_ty: Type, + /// The memo key: the [`SpecKey`] of the use that minted this specialization, + /// taken from its live instantiation type *before* its pin — + /// the same procedure at the same point every candidate's key is taken, which + /// is what makes the comparison self-consistent (see [`SpecializeFrame::specs`]). + key: SpecKey, /// Its binding name — a [`Name::mono`] carrying the source binding's name /// as provenance and a globally-fresh uid for identity (so it can neither /// capture nor be captured). @@ -775,7 +826,7 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { with_shadows(ctx, [param_name], |ctx| coalesce_node(body, level, ctx)); // `param.ty` is resolved from the lambda's coalesced domain in // the end-of-function block (it can't be coalesced standalone: - // body-usage refinement witnesses are negative-polarity upper-bound + // body-usage refinements are negative-polarity upper-bound // facts that only materialize in the contravariant domain // position of `expr.ty`). Domain-refinement predicates ride // `expr.ty` and are coalesced with it. @@ -829,7 +880,7 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { // resolved — rather than via an emit-time reverse-adjacency bound // is what keeps it robust under let-polymorphism's monomorphization // (which re-mints var identities a recorded bound would not follow). - // A morphism's coalesced type may carry *outer* refinement witnesses + // A morphism's coalesced type may carry *outer* refinements // it acquired during solving (`{Fun(d, c) | r}` — the same shape // `CheckCtx::as_function` peels); the value flowing to the next // morphism is still the bare codomain, so peel before @@ -991,7 +1042,7 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { // compact → simplify → coalesce pipeline to materialize a concrete // `Type`. // - // Refinements ride the lattice as refinement witnesses, so a refined + // Refinements ride the lattice as refinements, so a refined // domain coalesces straight onto `expr.ty` here — downstream passes // (`lambda_elim` included) read it from the type. let label = symbolic(expr); @@ -1159,10 +1210,11 @@ fn coalesce_type_predicates(ty: &mut Type, level: Level, ctx: &mut CoalesceCtx) // Integrated monomorphization (the coalesce walk's specialization arms). // // A use of a generalized binding specializes at first visit (`specialize_use`, -// from `coalesce_node`'s `Var` hook), memoized per distinct resolved type so -// same-typed uses share one definition — a collection/generator UDF used at -// several element types compiles to one *cached* binding per element type -// rather than a copy per call site (cf. [`crate::ccl::inline`]). The binding's +// from `coalesce_node`'s `Var` hook), memoized per distinct instantiation +// (`SpecKey`) so uses that instantiate it identically share one definition — a +// collection/generator UDF used at several element types compiles to one +// *cached* binding per element type rather than a copy per call site (cf. +// [`crate::ccl::inline`]). The binding's // `let` node then rebuilds itself as the chain of demanded specializations // (`coalesce_generalized_let`). A binding used at K distinct types becomes K // nested `let`s; one never used at all is dropped as dead code. @@ -1190,32 +1242,12 @@ fn coalesce_type_predicates(ty: &mut Type, level: Level, ctx: &mut CoalesceCtx) // logs every graph read (`record_read`) as a `(var-laden type, resolution)` // pair — the snapshot shares the live `InferVar`s — and `assert_reads_stable` // re-resolves each against the *final* graph at end of pass, requiring the -// skeleton *and its refinement witnesses* to be unchanged +// skeleton *and its refinements* to be unchanged // (`types_agree_modulo_unread`). A pin that retroactively changed an // already-read variable's resolution trips it by name. The lone exception is -// the read that produces a specialization's own memo key, where witnesses are -// excluded and the reason is on `ReadPurpose::SpecializationKey`. Debug builds -// only; free in release. +// the use's own instantiation resolution, where refinements are excluded and the +// reason is on `ReadPurpose::Instantiation`. Debug builds only; free in release. -/// Specialize a use of a generalized binding (frame at `frame_idx` in the -/// walk's scope) to its resolved instantiation type, then rewrite the use to -/// reference the specialization and stamp the specialization's resolved type -/// on it. -/// -/// On a memo miss this clones the frame's definition, freshens it -/// independently ([`freshen_expr_type_slots`] — quantified-variable renaming -/// over every type slot, including refinement predicates and bound-edge -/// discharge payloads), **pins it two-way to the use's live instantiation -/// type** (the use type is itself -/// var-laden for a use inside another clone — the chained poly-calls-poly -/// case — and the live pin is what lets such interior uses resolve concrete), -/// and coalesces the clone re-entrantly. The re-entrant walk runs in the -/// *definition site's* scope — entries above the frame are suspended — so a -/// name the definition references resolves to what was in scope where it was -/// written, not to a same-named binder introduced between definition and use. -// `ConstrainCache` keys on `Type`, whose `Refinement` predicates carry interior -// mutability; the solver relies on identity-by-`uid`, not the mutable payload -// (matching the solver's module-level allow). /// Mint a fresh [`NodeId`](crate::ccl::provenance::NodeId) for every node in a /// monomorphization clone. /// @@ -1232,6 +1264,26 @@ fn freshen_clone_node_ids(expr: &mut Expr) { expr.freshen_node_ids_deep(); } +/// Specialize a use of a generalized binding (frame at `frame_idx` in the +/// walk's scope) to its instantiation, then rewrite the use to reference the +/// specialization and stamp the specialization's resolved type on it. +/// +/// Sharing is decided by the use's [`SpecKey`] — both directed reads of its +/// instantiation, taken off the live graph before the pin. On a miss this clones +/// the frame's definition, freshens it independently ([`freshen_expr_type_slots`] +/// — quantified-variable renaming over every type slot, including refinement +/// predicates and bound-edge discharge payloads), **pins it two-way to the use's +/// live instantiation type** (the use type is itself var-laden for a use inside +/// another clone — the chained poly-calls-poly case — and the live pin is what +/// lets such interior uses resolve concrete), and coalesces the clone +/// re-entrantly. The re-entrant walk runs in the *definition site's* scope — +/// entries above the frame are suspended — so a name the definition references +/// resolves to what was in scope where it was written, not to a same-named binder +/// introduced between definition and use. On a hit the use is simply renamed and +/// stamped — see the hit path for why it is deliberately *not* re-pinned. +// `ConstrainCache` keys on `Type`, whose `Refinement` predicates carry interior +// mutability; the solver relies on identity-by-`uid`, not the mutable payload +// (matching the solver's module-level allow). #[allow(clippy::mutable_key_type)] pub(super) fn specialize_use(use_expr: &mut Expr, frame_idx: usize, ctx: &mut CoalesceCtx) { // The use's instantiation type, resolved off the live graph. The graph is @@ -1249,23 +1301,41 @@ pub(super) fn specialize_use(use_expr: &mut Expr, frame_idx: usize, ctx: &mut Co // Log the use's instantiation read for the ordering-invariant check. The // snapshot keeps the live instantiation vars; the pin below (and any // later specialization) may only *add* bounds to them, so re-resolving at - // end-of-pass must still agree on the *skeleton* (the use node itself is - // overwritten with the specialization name, but the read is what the walk - // consumed here — as a memo key, which is why witnesses are excluded from - // the comparison; see `ReadPurpose::SpecializationKey`). - ctx.record_read_spec_key(&use_expr.ty, &resolved, || symbolic(use_expr)); - // A use type can resolve with residual `Infer` placeholders only when - // nothing concrete ever reached its instantiation (a generic definition - // the program never exercises at a concrete type). Inference deliberately - // tolerates the residue (`Type::Infer`'s invariant); the strict - // post-inference typecheck is the layer that rejects it. Placeholder - // identities are fresh per resolution, so such uses never share a memo - // entry — each gets its own (under-determined) specialization. + // end-of-pass must still agree on the *skeleton*. Refinements are excluded + // because the pin that immediately follows is itself what moves them, and + // this resolution's consumers are refinement-insensitive (see + // `ReadPurpose::Instantiation`). + ctx.record_read_instantiation(&use_expr.ty, &resolved, || symbolic(use_expr)); + // The specialization key: what decides whether this use may share an + // existing clone. Read off the live graph *before* the pin, exactly as every + // other use's is, so both sides of the comparison below are one procedure at + // one point in the pin's lifecycle. It is deliberately not `resolved` — a + // resolved type is a polarity-correct rendering, which narrows away positions + // the definition body ignores and cannot see an argument's refinement on a + // domain's lower bounds; see `SpecializeFrame::specs`. + // + // An under-determined instantiation (a generic definition the program never + // exercises at a concrete type) keys as the canonical empty `SpecKey` rather + // than on fresh `Infer` placeholder ids, so such uses *do* share one + // specialization. Inference deliberately tolerates the residue + // (`Type::Infer`'s invariant); the strict post-inference typecheck rejects it. + let key = spec_key(&use_expr.ty); let ScopeEntry::Generalized(frame) = &ctx.scope[frame_idx] else { unreachable!("lookup_generalized returns indices of Generalized entries only"); }; - if let Some(spec) = frame.specs.iter().find(|s| s.use_ty == resolved) { + if let Some(spec) = frame.specs.iter().find(|s| s.key == key) { let (name, ty) = (spec.name.clone(), spec.def.ty.clone()); + // A hit is *not* re-pinned, and the reason is worth recording because + // pinning here looks like the obvious way to make the key's faithfulness + // checked rather than argued. It is not available: a miss pins a + // *var-laden* clone, so its pin identifies variables, while a hit's + // specialization is already coalesced and concrete — pinning that against + // a still-var-laden use type is a strictly stronger demand, and it + // rejects uses the key correctly considers shareable (an unrefined lower + // bound on the use's domain variable that the clone's own coalesce would + // have intersected away instead fails `T ⊀ {T | p}` outright). Checking a + // hit needs a non-recording *subsumption* test rather than a constrain, + // which the solver has no notion of today. use_expr.node = TypedExprNode::Var(name); use_expr.ty = ty; return; @@ -1346,13 +1416,19 @@ pub(super) fn specialize_use(use_expr: &mut Expr, frame_idx: usize, ctx: &mut Co let ScopeEntry::Generalized(frame) = &mut ctx.scope[frame_idx] else { unreachable!("suspended entries were restored above the frame"); }; - // The memo key is the *specialization's* resolved type, not this use's - // pre-pin resolution: the two differ exactly by the canonical-chain - // extension above, and every later same-typed use resolves its witnesses - // through the now-extended chains — i.e. to the predicate terms `clone.ty` - // carries. + // The entry is keyed on the pre-pin key computed above — *not* on + // `clone.ty`. A clone type is the pin's output and a candidate's key is its + // input; keying an entry on one and the lookup on the other is what made this + // table write-only (see `SpecializeFrame::specs`). + debug_assert!( + frame.specs.iter().all(|s| s.key != key), + "specialization memo invariant (one entry per distinct key) violated: \ + minting a second specialization of `{}` for key {key} — the lookup and \ + the insert disagree about what identifies a specialization", + frame.name, + ); frame.specs.push(Specialization { - use_ty: clone.ty.clone(), + key, name: spec_name, def: clone, }); @@ -1473,11 +1549,11 @@ pub(super) fn specialize_projection_domain(morphism: &mut Expr, input: &Type) { /// Overwriting (rather than merging) the base is sound: `arg <: domain` was /// constrained at emit, so the input satisfies every body demand. /// -/// The lambda's coalesced domain may carry refinement witnesses (body-usage facts +/// The lambda's coalesced domain may carry refinements (body-usage facts /// that exist only in this negative-polarity position); they are preserved by -/// re-wrapping them around `input`, deduping against witnesses `input` already +/// re-wrapping them around `input`, deduping against refinements `input` already /// carries (structural [`Refinement`](crate::ccl::Refinement) equality). Outer -/// refinement witnesses on the function type itself are likewise preserved. +/// refinements on the function type itself are likewise preserved. /// /// `input` is supplied by the use site: the argument at a direct-redex /// `Apply`, the enclosing function's parameter domain when the lambda is @@ -1518,18 +1594,18 @@ pub(super) fn specialize_lambda_domain(lambda: &mut Expr, input: &Type) { dom_layers.push(r); base = *inner; } - // Re-wrap the collected witnesses around `input`, skipping witnesses it - // already carries (the argument edge may have deposited the same witness on both). - let mut input_witnesses = Vec::new(); + // Re-wrap the collected refinements around `input`, skipping refinements it + // already carries (the argument edge may have deposited the same refinement on both). + let mut input_refinements = Vec::new(); let mut t = input; while let Type::Refinement(inner, r) = t { - input_witnesses.push(r); + input_refinements.push(r); t = inner; } let new_dom = dom_layers .into_iter() .rev() - .filter(|r| !input_witnesses.contains(&r)) + .filter(|r| !input_refinements.contains(&r)) .fold(input.clone(), |acc, r| Type::Refinement(Box::new(acc), r)); lambda.ty = fn_layers.into_iter().rev().fold( // Preserve the Pi binder: specialization rewrites only the domain @@ -1550,7 +1626,7 @@ pub(super) fn specialize_lambda_domain(lambda: &mut Expr, input: &Type) { /// Fill a lambda's `param.ty` binder slot from its coalesced function type's /// domain. Deriving the slot from the resolved domain — rather than /// coalescing the slot var standalone — is what preserves body-usage -/// refinement witnesses, which are negative-polarity facts visible only in the +/// refinements, which are negative-polarity facts visible only in the /// contravariant domain. No-op for non-lambdas and unresolved function types. fn refresh_lambda_param_slot(expr: &mut Expr) { if let TypedExprNode::Lambda { param, .. } = &mut expr.node @@ -1568,30 +1644,31 @@ mod tests { // ----- ordering-invariant comparison (`types_agree_modulo_unread`) ----- - // A witness that appears (or vanishes) between a read and the final graph is + // A refinement that appears (or vanishes) between a read and the final graph is // a bound that arrived after the read consumed the variable — the staleness - // the ordering invariant forbids — so a `Stamp` read rejects it. The - // specialization-*key* read is the one place witnesses are excluded, because - // the pin that follows the read is itself what moves them and two uses - // differing only in witnesses share a specialization by design. + // the ordering invariant forbids — so a `Stamp` read rejects it. A use's + // `Instantiation` read is the one place refinements are excluded, because the + // pin that follows the read is itself what moves them and that read's + // consumers (channel-domain pairing, error blame) do not look at refinements. + // Sharing does *not* ride on it — that is `SpecKey`'s job. #[cfg(debug_assertions)] #[test] - fn witness_drift_fails_a_stamp_read_and_passes_a_key_read() { + fn refinement_drift_fails_a_stamp_read_and_passes_an_instantiation_read() { use super::types_agree_modulo_unread; let plain = Type::Base(BaseType::Int); let refined = refined_int(TypedExpr::lit(crate::ccl::Lit::Int(8))); for (read, now) in [(&plain, &refined), (&refined, &plain)] { assert!( !types_agree_modulo_unread(read, now, true), - "a stamp read must not tolerate witness drift ({read} vs {now})" + "a stamp read must not tolerate refinement drift ({read} vs {now})" ); assert!( types_agree_modulo_unread(read, now, false), - "a specialization-key read compares skeletons only ({read} vs {now})" + "an instantiation read compares skeletons only ({read} vs {now})" ); } - // The skeleton *under* the witnesses is held fixed either way — keying on - // a stale one is what would pick the wrong specialization. + // The skeleton *under* the refinements is held fixed either way — a stale + // one would pair the clone's channel domains against the wrong positions. assert!(!types_agree_modulo_unread( &plain, &Type::Base(BaseType::String), @@ -1684,13 +1761,15 @@ mod tests { } #[test] - fn monomorphize_shares_one_specialization_per_type() { + fn monomorphize_specializes_per_distinct_instantiation() { // let f = λx. x in (f 1, f 2, f "a") // - // Three uses at two *distinct* types (Int twice, String once). The lead - // F1 concern: specialization is keyed on the resolved type, not the use - // site, so the two `Int` uses share *one* definition — exactly two - // specializations, not three. + // Three uses, three distinct instantiations. Every literal carries its own + // singleton, so the two `Int` uses instantiate `f` at *different* refined + // types and get a specialization each — and that is the intended rule, not + // a shortfall: a refinement layer on an iterated domain is compiled (one + // `restrict` filter per layer), so refinements are code and two clones + // pinned to different ones are genuinely different code. let f = TypedExpr::lambda("x", Type::Hole, TypedExpr::var("x")); let body = TypedExpr::new(TypedExprNode::Tuple(vec![ TypedExpr::apply(lit_int(1), TypedExpr::var("f")), @@ -1703,19 +1782,40 @@ mod tests { ty, Type::Tuple(vec![int_lit_ty(1), int_lit_ty(2), str_lit_ty("a"),]) ); - // A refinement makes two uses distinct, so a literal argument mints its own - // specialization — see the `specs` field doc. Sharing modulo refinements is - // the better rule and needs the clone built at the stripped type. let (specializations, used_names) = specialization_stats(&e); assert_eq!( specializations, 3, - "one specialization per distinct use type" + "one specialization per distinct instantiation" ); + assert_eq!(used_names.len(), 3); + } + + /// The complement, and the guard on the memo actually memoizing: uses that + /// instantiate the definition *identically* must share one specialization. + /// + /// This is the half that regressed when an entry was keyed on its clone's + /// coalesced type while a candidate was keyed on its own pre-pin resolution. + /// For any definition whose clone type gains a refinement across the pin, those + /// two could never be equal, so the table was write-only — even these + /// character-identical call sites missed each other and cloned per site, and + /// the table accumulated several entries under one key. + #[test] + fn identical_instantiations_share_one_specialization() { + // let f = λx. x in (f 1, f 1, f "a") + let f = TypedExpr::lambda("x", Type::Hole, TypedExpr::var("x")); + let body = TypedExpr::new(TypedExprNode::Tuple(vec![ + TypedExpr::apply(lit_int(1), TypedExpr::var("f")), + TypedExpr::apply(lit_int(1), TypedExpr::var("f")), + TypedExpr::apply(lit_string("a"), TypedExpr::var("f")), + ])); + let mut e = TypedExpr::let_bind("f", f, body); + run_inference(&mut e).expect("type-checks"); + let (specializations, used_names) = specialization_stats(&e); assert_eq!( - used_names.len(), - 3, - "a literal argument mints its own specialization, so none collapse" + specializations, 2, + "the two identical `Int` uses share one specialization" ); + assert_eq!(used_names.len(), 2); } #[test] @@ -1877,11 +1977,15 @@ mod tests { let mut e = TypedExpr::let_bind("f", f, TypedExpr::let_bind("g", g, uses)); run_inference(&mut e).expect("mixed direct + chained uses type-check"); let (specializations, used_names) = specialization_stats(&e); - // The direct `Int` use no longer shares the chained `Int` clone: the two - // literals give the two uses distinct types, so each mints its own - // specialization (see the `specs` field doc). - assert_eq!(specializations, 5, "per-use g + f specializations"); - assert_eq!(used_names.len(), 5); + // Two `g` specializations (Int, String) and two `f` ones — *not* three: + // the direct `f(1)` and the `f(y)` reached inside `g`'s Int clone + // instantiate `f` identically, so they key the same and group onto one + // specialization. This is the "memo is per frame, not per demanding + // region" property, and it is what keying on a `SpecKey` restores — + // keying an entry on its clone's coalesced type instead made these two + // miss each other (see `SpecializeFrame::specs`). + assert_eq!(specializations, 4, "one g + one f specialization per type"); + assert_eq!(used_names.len(), 4); } #[test] diff --git a/src/ccl/infer/solver/coalesce.rs b/src/ccl/infer/solver/coalesce.rs index 1efafd79..05d544a1 100644 --- a/src/ccl/infer/solver/coalesce.rs +++ b/src/ccl/infer/solver/coalesce.rs @@ -277,7 +277,7 @@ fn coalesce_compact_go(ct: &CompactType, polarity: bool) -> Result Option { + /// The atom `ty` contributes, or `None` for a non-atomic type. Shared with + /// the sibling specialization-key walk, which classifies leaves the same way + /// (see `src/ccl/infer/solver/spec_key.rs`). + pub(super) fn from_type(ty: &Type) -> Option { match ty { Type::Base(b) => Some(AtomKey::Prim(b.clone())), Type::UIntRange(n) => Some(AtomKey::UIntRange(*n)), @@ -87,7 +90,7 @@ impl AtomKey { /// data function's domain alternatives becomes `Conflict` and is reported loudly at coalesce /// ([`super::coalesce::CoalesceError::DomainJoinConflict`]), never a mid-merge /// panic. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] pub enum KindMerge { /// domain — the ordinary contravariant meet. Compute, @@ -111,7 +114,7 @@ impl KindMerge { /// supplied where a collection is demanded (e.g. `sum(λ x → x + 1)`) is a concrete /// `Compute` value against a `Data` demand, rejected up front in /// [`constrain_kind`](super::constrain) — it never reaches a var here. - fn of(kind: &crate::ccl::ty::FunKind) -> Self { + pub(super) fn of(kind: &crate::ccl::ty::FunKind) -> Self { use crate::ccl::ty::FunKind; match kind { FunKind::Compute => KindMerge::Compute, @@ -272,7 +275,7 @@ pub struct CompactType { /// `Data ⊔ Data` join accumulated alternatives via [`union_domains`]), and the /// codomain. Recursively merged with polarity flip on the domain. pub fun: Option, - /// Witness contributions at this position. A set with `==` + /// Refinement contributions at this position. A set with `==` /// membership (deduplicated by [`Refinement`]'s structural `PartialEq`), /// stored as a `Vec` in first-insertion order. A refinement-set is /// width-subtyped exactly like `rec`: more refinements ⇒ subtype @@ -355,19 +358,19 @@ impl CompactType { } } - /// Merge two witness sets. The set-op tracks + /// Merge two refinement sets. The set-op tracks /// polarity the same way `rec` does — positive ⇒ *intersect*, /// negative ⇒ *union* — because refinement-sets width-subtype like /// record fields (more refinements ⇒ subtype). At a positive - /// position the value reliably carries only the witnesses *both* + /// position the value reliably carries only the refinements *both* /// sides guarantee; at a negative position a consumer that may /// impose either set imposes their union. fn merge_refinements(pol: bool, lhs: Vec, rhs: Vec) -> Vec { if pol { - // The types are being unioned, so the refinement witnesses should be intersected. + // The types are being unioned, so the refinements should be intersected. lhs.into_iter().filter(|r| rhs.contains(r)).collect() } else { - // The types are being intersected, so the refinement witnesses should be unioned. + // The types are being intersected, so the refinements should be unioned. let mut out = lhs; for r in rhs { if !out.contains(&r) { @@ -534,6 +537,20 @@ struct CompactState { /// bound edge composes its own `subst` in (`then(edge_subst, subst_acc)`), and /// the composite is applied where a refinement predicate is reached — the /// coalesce-time forcing of suspended substitutions (design §3.6). +/// +/// **Sibling walk — change the two together.** `key_go` +/// (`src/ccl/infer/solver/spec_key.rs`) traverses `Type` in lockstep with this +/// function: the same polarity flip on a `Fun` domain, the same no-flip on +/// `History` children, the same `then(edge_subst, subst_acc)` composition at a +/// bound edge, the same binder shadowing for a Pi codomain, the same +/// `(uid, pol)` cycle guard. That agreement *is* the soundness argument for a +/// specialization key: a bound the key cannot see is one the clone's own +/// resolution cannot see either, because the clone resolves through this walk +/// over the same edges from the same side. Nothing enforces it, so a new `Type` +/// variant — or a change to how an edge substitution composes, or to where +/// polarity flips — has to be mirrored there in the same change. A divergence is +/// silent, and what it produces is a shared clone whose interior was resolved +/// against a different use's argument. fn compact_go( ty: &Type, pol: bool, @@ -549,13 +566,13 @@ fn compact_go( | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn => CompactType::from_atom(AtomKey::from_type(ty).unwrap()), - // Refinements ride the lattice as a witness set: compact the underlying - // type, then attach this layer's witness. Walking a variable's bound + // Refinements ride the lattice as a refinement set: compact the underlying + // type, then attach this layer's refinement. Walking a variable's bound // that is `Refinement(D, r)` therefore unions `r` into that variable's // compacted position — the propagation path. The accumulated - // substitution is *forced* on the witness: it rebuilds the predicate + // substitution is *forced* on the refinement: it rebuilds the predicate // with its free binders rewritten (e.g. discharging a dependent - // application's argument) before the witness lands in the position. + // application's argument) before the refinement lands in the position. // The predicate is an immutable term, so a non-vacuous force builds a // fresh predicate from the (freshened) bound's content directly. Type::Refinement(inner, r) => { @@ -740,7 +757,7 @@ fn compact_go( // end. Seeding with `from_var` would mix the variable's *empty* // refinement set into the merge, and at positive polarity `merge` // *intersects* refinement sets (`merge_refinements`) — so the empty - // seed would intersect away every bound's witnesses (∅ is absorbing under + // seed would intersect away every bound's refinements (∅ is absorbing under // intersection). The variable identity must be refinement-*neutral*; // `rec`/`var`/`fun` get this for free from their `None` merge // identity, but refinement sets have no such sentinel, so we keep diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index e3c7b329..4952ef9b 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -4,7 +4,7 @@ //! variables' bound lists, propagating transitively (`constrain_go`), //! bridging two-sided edge substitutions (`bridge_holder_gap`), and recovering //! from level mismatches by `extrude`. Refinement layers are peeled/wrapped -//! (`peel_refinements` / `wrap_refinements`) so a witness deficit can flow onto +//! (`peel_refinements` / `wrap_refinements`) so a refinement deficit can flow onto //! a variable base. // The `constrain` cycle cache (`ConstrainCache`) keys on `(Type, Type)`. `Type` @@ -809,12 +809,12 @@ fn constrain_go( ) => Ok(()), // Refinement subtyping: - // {b₁ | S₁} <: {b₂ | S₂} iff b₁ <: b₂ and σ(S₂) ⊆ σ(S₁) ∪ witnesses(b₁) + // {b₁ | S₁} <: {b₂ | S₂} iff b₁ <: b₂ and σ(S₂) ⊆ σ(S₁) ∪ refinements(b₁) // (more refinements ⇒ subtype). Refinements match by [`Refinement`]'s - // `PartialEq` — structural predicate equality — so a witness join planning + // `PartialEq` — structural predicate equality — so a refinement join planning // rebuilt as a fresh term still matches; never by predicate // implication. The two sides live in different binder contexts, so an - // lhs witness is transported through the correspondence (`σ(S₁)`, via + // lhs refinement is transported through the correspondence (`σ(S₁)`, via // [`Subst::force_refinement`]) before comparing: a predicate mentioning // a Pi binder matches its renamed — or, when a discharge edge composed // into σ on the way through a variable, *discharged* — copy on the @@ -830,8 +830,8 @@ fn constrain_go( // rather than rejecting — the refinement analog of how the // record/function arms thread structure through variables. The // requirement then fails later iff the variable resolves to a concrete - // base lacking those witnesses. Without this, a value that is *already* - // refined could never be cast to add a further witness (nested + // base lacking those refinements. Without this, a value that is *already* + // refined could never be cast to add a further refinement (nested // list-comprehension filters: `{D|p} ⇒ V <: {?a|q} ⇒ V`), even though // the assignment `?a := {D|p}` exists. // @@ -846,9 +846,9 @@ fn constrain_go( let (rbase, rrefs) = peel_refinements(rhs); // The refinements rhs requires that no transported lhs layer // matches (by `Refinement`'s structural `PartialEq`). Each side's - // witnesses are forced through its own morphism into the ambient frame + // refinements are forced through its own morphism into the ambient frame // before comparing (`sl(S₁)` vs `sr(S₂)`); the deficit keeps the - // *untransported* rhs witnesses, since the recursive constraint below + // *untransported* rhs refinements, since the recursive constraint below // carries `sr` for them. let lrefs_in_ambient: Vec = lrefs.iter().map(|l| sl.force_refinement(l)).collect(); @@ -863,7 +863,7 @@ fn constrain_go( } else if matches!(lbase, Type::Infer(_)) { // Variable base: flow the deficit onto it (`b₁ <: {b₂ | deficit}`) // rather than rejecting; it fails later iff the variable - // resolves to a concrete base lacking those witnesses. + // resolves to a concrete base lacking those refinements. let demanded = wrap_refinements(rbase, &deficit); constrain_go(lbase, &demanded, sl, sr, cache) } else { @@ -882,7 +882,7 @@ fn constrain_go( } /// Peel all outer [`Type::Refinement`] layers, returning the bare base type -/// and the refinement witnesses carried by the peeled layers (outermost first). +/// and the refinements carried by the peeled layers (outermost first). fn peel_refinements(ty: &Type) -> (&Type, Vec<&Refinement>) { let mut refs = Vec::new(); let mut cur = ty; @@ -897,7 +897,7 @@ fn peel_refinements(ty: &Type) -> (&Type, Vec<&Refinement>) { /// outermost-first), preserving their order. /// /// Used by [`constrain_subtype`]'s refinement arm to rebuild the deficit -/// refinement `{rbase | S₂ \ S₁}` from the rhs's own layers, so the kept witnesses +/// refinement `{rbase | S₂ \ S₁}` from the rhs's own layers, so the kept refinements /// retain their real [`crate::ccl::Refinement`] payloads (predicate `Rc`s). fn wrap_refinements(base: &Type, refs: &[&Refinement]) -> Type { refs.iter().rev().fold(base.clone(), |acc, r| { @@ -1172,10 +1172,10 @@ mod tests { } #[test] - fn refined_missing_witness_is_not_subtype() { + fn refined_missing_refinement_is_not_subtype() { // {Int | q} 0 with x<10" hazard applies /// only to representations that fold the predicate into the variable's /// identity; ours keeps them positional.) diff --git a/src/ccl/infer/solver/spec_key.rs b/src/ccl/infer/solver/spec_key.rs new file mode 100644 index 00000000..11a1c5b2 --- /dev/null +++ b/src/ccl/infer/solver/spec_key.rs @@ -0,0 +1,790 @@ +//! The **specialization key**: a canonical, polarity-complete fingerprint of a +//! monomorphization use's instantiation type. +//! +//! # Why this is not a `Type` +//! +//! A resolved [`Type`] answers "what should be stamped on this node". That answer +//! is *deliberately* lossy: a domain is a negative position, so it resolves from +//! upper bounds — from what the definition body demands — and a position the body +//! never touches is narrowed away entirely, while a refinement sitting on the +//! argument's *lower* bounds is invisible unless +//! [`compact_type`](super::compact_type)'s opposite-polarity fallback happens to +//! fire at that exact position. +//! +//! A specialization key answers a different question: "would two uses' clones be +//! the same code?" That answer must be **complete**, because it decides whether +//! one use is served by a clone whose interior was resolved against a *different* +//! use's argument. The clone's interior reads its parameter at a *positive* +//! position, so it sees exactly the lower-bound refinements a polarity-correct +//! rendering of the domain drops. Keying on a rendering therefore compares one +//! polarity's view against a clone built from the other's. +//! +//! # Both directed views, not an undirected closure +//! +//! The temptation is to "saturate": follow *both* bound lists at every variable. +//! That is wrong, and instructively so — the bound graph is connected across +//! unrelated uses (two calls' arguments meet at the shared variable of an +//! operator's scheme), so an undirected closure walks out of one use and into +//! every other. Every use of a definition then keys on the union of the whole +//! program's literals, and they all compare equal: the exact defect this key +//! exists to remove, arrived at from the other side. +//! +//! Polarity has to direct the *traversal*. What the key needs is **both directed +//! reads** of the use's instantiation type — the root taken once at each polarity: +//! +//! - The [`positive`](SpecKey::positive) read is the stamping view: a domain is +//! negative, so it follows upper bounds — what the definition body demands — +//! while the codomain follows lower bounds, what the definition supplies. +//! - The [`negative`](SpecKey::negative) read is the **clone's** view: the domain +//! flips to positive and follows *lower* bounds — the argument that flowed in — +//! while the codomain follows upper bounds, the consumer's demand on the result. +//! +//! The negative read is the load-bearing half, because it is the polarity the +//! clone's interior reads its parameter at. And the pair covers the channels +//! through which a use's own information enters: the emit-time `arg <: domain` +//! edge (a *lower* bound of a negative position) and a consumer's +//! `codomain <: demand` edge (an *upper* bound of a positive position). Both +//! reads stay directed, so neither leaves the use's own cone. +//! +//! **What "covers" does and does not mean.** The two reads flip in lockstep, so +//! at the *root's* immediate positions they are exact opposites and every bound +//! list is consulted by one of them. Deeper in, they diverge: a variable `?e` +//! reached only through `?d`'s lower bounds is visited only by the negative read, +//! at whatever polarity the traversal arrived with — so `?e`'s other bound list is +//! read by neither. That is not a hole, because it is precisely the direction the +//! *clone* reads that position at too: the clone's own resolution walks the same +//! edges from the same side, so a bound the key cannot see is one the clone cannot +//! see either, and the two stay in agreement. The guarantee is agreement with the +//! pin, not omniscience about the graph. +//! +//! **The two are kept apart, not merged.** Merging them into one view per position +//! loses which *direction* a contribution arrived from, and the pin the key is +//! standing in for is direction-sensitive: a use whose domain must accept a plain +//! `Int` cannot be served by a specialization whose parameter is refined, even +//! though the union of both reads is `{Int | …}` on both sides. (This is not +//! hypothetical — it is what a merged key got wrong for a definition used both +//! directly and through a generalized wrapper.) Comparing the views separately is +//! also strictly more discriminating, and over-splitting is a wasted clone while +//! under-splitting is a miscompile. +//! +//! # The remaining rules +//! +//! - **Union, never narrow.** Polarity picks which bounds to follow; merging is +//! always union. A polarity-correct merge *intersects* record fields and refinement +//! sets at one of the two polarities, which is what makes a rendering forget an +//! argument's unused fields. A key that narrows can only under-split, and +//! under-splitting is a miscompile while over-splitting is a wasted clone. +//! - **Canonical when under-determined.** A position nothing concrete reached is +//! the [`Default`] key, not a freshly-minted `Infer` placeholder. Placeholder +//! ids are fresh per resolution, so a key carrying them could never match a +//! second time. +//! - **Conflict-tolerant.** Two atoms, or two history kinds, at one position are +//! both recorded. A key is a fingerprint, not a type that has to typecheck — +//! the real resolution is what reports the conflict, and a key that raised an +//! error would have to pick a specialization anyway. +//! +//! The property this buys: *if two uses' keys are equal then the clone coalesced +//! under either use's pin is the same code*, because every edge the clone's own +//! resolution can follow is followed, from the same side, by one of the two reads. + +use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet, btree_map::Entry}; +use std::fmt; + +use smol_str::SmolStr; + +use crate::ccl::subst::Subst; +use crate::ccl::{FieldKey, HistoryKind, InferVarId, Refinement, Type}; + +use super::compact::{AtomKey, KindMerge}; + +/// The identity of a use's instantiation, for deciding which uses may share one +/// monomorphization specialization: its two directed reads, kept apart (see the +/// module docs for why merging them is wrong). +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct SpecKey { + /// The stamping view — a domain resolved from the definition's demands. + positive: KeyView, + /// The clone's view — a domain resolved from the argument that flowed in. + /// This is the half that sees a use's refinements. + negative: KeyView, +} + +/// A canonical fingerprint of one position, under one directed read. +/// +/// Every field accumulates by **union** ([`KeyView::union`]); the all-empty value +/// ([`Default`]) is both the "nothing concrete here" view and the merge identity. +/// Equality is structural, with refinement sets compared as *sets* (they accumulate +/// in first-insertion order, which is not canonical) — see the [`PartialEq`] impl. +#[derive(Debug, Clone, Default)] +struct KeyView { + /// Leaf contributions (bases, ranges, sources, `Txn`, channel domains). + atoms: BTreeSet, + /// Refinements at this position, deduplicated by [`Refinement`]'s + /// type-blind structural equality. Order is insertion order, so equality + /// compares these as a set. + refinements: Vec, + /// Function contributions, **keyed by kind** so a compute arrow and a data + /// collection at one position stay distinguishable rather than one shadowing + /// the other — exactly as [`history`](Self::history) is keyed by + /// [`HistoryKind`]. Each maps to `(domain, codomain)`. + /// + /// The kind belongs in the key because it is what a clone *compiles to*: a + /// specialization pinned at `⤇` iterates a domain that a `⇒` use does not + /// supply. It is read through [`KindMerge::of`], the same resolved-from-bounds + /// view compaction uses, rather than off the [`FunKind`](crate::ccl::ty::FunKind) + /// itself — an inferred kind is a variable here, and keying on its *identity* + /// (fresh per instantiation) would split every use into its own key while + /// telling us nothing. + /// + /// Like every other field this reads the live graph mid-solve, so a kind may + /// still be accumulating; that is the same bargain the `Infer` bounds make, and + /// the same guarantee holds — agreement with the pin, not omniscience. + /// + /// The Pi binder name is deliberately **not** part of the key. It is either + /// cosmetic (stripped at materialization when no predicate references it) or + /// it is referenced by a refinement predicate — and the predicate itself is in + /// `refinements`, compared structurally. Keeping the name would also make the + /// key sensitive to the solver's per-site fresh dependent-application binders + /// (`Name::solver_arg`), which would split every use into its own key. + fun: BTreeMap, Box)>, + /// Record/tuple fields, unioned. Tuples and records share this representation + /// keyed by `Index` / `Name`, exactly as `compact_type` normalizes them. + rec: BTreeMap, + /// Variant tags, unioned. + var: BTreeMap, + /// History contributions, keyed by kind so an `Overwrite` and an `Append` + /// handle at one position stay distinguishable rather than one shadowing the + /// other. Each maps to `(value, domain)`. + history: BTreeMap, Box)>, +} + +/// Structural equality, with `refinements` compared as a set. +/// +/// Refinements accumulate in first-insertion order, which depends on the order the +/// walk happened to reach a variable's bounds — not on the position's meaning. A +/// positional comparison would therefore split two identical instantiations whose +/// bound lists were built in different orders. Both sides are deduplicated on +/// insertion, so equal lengths plus containment is set equality. +impl PartialEq for KeyView { + fn eq(&self, other: &Self) -> bool { + fn same_refinements(a: &[Refinement], b: &[Refinement]) -> bool { + a.len() == b.len() && a.iter().all(|w| b.contains(w)) + } + self.atoms == other.atoms + && same_refinements(&self.refinements, &other.refinements) + && self.fun == other.fun + && self.rec == other.rec + && self.var == other.var + && self.history == other.history + } +} + +impl Eq for KeyView {} + +impl KeyView { + /// Fold `other` into `self` positionwise. Union everywhere: sets union, maps + /// union by key with matching entries merged recursively, and a shape present + /// on one side only passes through. + fn union(&mut self, other: KeyView) { + self.atoms.extend(other.atoms); + for w in other.refinements { + if !self.refinements.contains(&w) { + self.refinements.push(w); + } + } + for (kind, (domain, codomain)) in other.fun { + match self.fun.entry(kind) { + Entry::Vacant(e) => { + e.insert((domain, codomain)); + } + Entry::Occupied(mut e) => { + let (d0, c0) = e.get_mut(); + d0.union(*domain); + c0.union(*codomain); + } + } + } + union_map(&mut self.rec, other.rec); + union_map(&mut self.var, other.var); + for (kind, (value, domain)) in other.history { + match self.history.entry(kind) { + Entry::Vacant(e) => { + e.insert((value, domain)); + } + Entry::Occupied(mut e) => { + let (v0, d0) = e.get_mut(); + v0.union(*value); + d0.union(*domain); + } + } + } + } + + fn from_atom(a: AtomKey) -> KeyView { + KeyView { + atoms: BTreeSet::from([a]), + ..Default::default() + } + } +} + +fn union_map(into: &mut BTreeMap, from: BTreeMap) { + for (k, v) in from { + match into.entry(k) { + Entry::Vacant(e) => { + e.insert(v); + } + Entry::Occupied(mut e) => e.get_mut().union(v), + } + } +} + +/// A terse, type-like rendering, for assertion messages and traces. An empty view +/// is `_`; a position with several contributions joins them with `&`. +impl fmt::Display for KeyView { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + let mut parts: Vec = self.atoms.iter().map(|a| a.to_type().to_string()).collect(); + for (kind, (d, c)) in &self.fun { + let arrow = match kind { + KindMerge::Data => "⤇", + KindMerge::Compute => "⇒", + KindMerge::Conflict => "⇒!", + }; + parts.push(format!("({d} {arrow} {c})")); + } + if !self.rec.is_empty() { + let fields: Vec = self.rec.iter().map(|(k, v)| format!("{k}: {v}")).collect(); + parts.push(format!("({})", fields.join(", "))); + } + if !self.var.is_empty() { + let tags: Vec = self.var.iter().map(|(k, v)| format!(".{k}: {v}")).collect(); + parts.push(format!("[{}]", tags.join(" | "))); + } + for (kind, (value, domain)) in &self.history { + let name = match kind { + HistoryKind::Overwrite => "Mut", + HistoryKind::Append => "Feed", + }; + parts.push(format!("{name}({value}, {domain})")); + } + let base = if parts.is_empty() { + "_".to_string() + } else { + parts.join(" & ") + }; + if self.refinements.is_empty() { + write!(f, "{base}") + } else { + let preds: Vec = self + .refinements + .iter() + .map(|w| crate::ccl::symbolic::symbolic(&w.predicate)) + .collect(); + write!(f, "{{{base} | {}}}", preds.join(", ")) + } + } +} + +/// Renders the two views, or just one when they agree (the common case for a +/// fully-determined instantiation). +impl fmt::Display for SpecKey { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + if self.positive == self.negative { + write!(f, "{}", self.positive) + } else { + write!(f, "{} ⊣ {}", self.positive, self.negative) + } + } +} + +/// Walk-wide state: the cycle guard, the per-variable memo, and the truncation +/// counter that decides what may be memoized. +struct KeyCtx { + /// Variables whose bounds are currently being walked, per polarity — the same + /// key `compact_type`'s cycle guard uses, and for the same reason: a variable + /// legitimately appears at both polarities in one type. + visiting: HashSet<(InferVarId, bool)>, + /// Completed keys per `(variable, polarity)`, for variables reached under the + /// identity substitution. + /// + /// Sound because a variable's directed key depends only on the variable and + /// the direction — not on the position it was reached from. A variable reached + /// under a *non-identity* substitution bypasses the memo: the substitution + /// rewrites the predicates the walk materializes, so that result *is* + /// position-dependent. + memo: HashMap<(InferVarId, bool), KeyView>, + /// How many cycle back-edges the walk has dropped. A key computed while a + /// truncation occurred inside it is *incomplete* — it is missing whatever the + /// back-edge would have contributed — so it must not be memoized. Comparing + /// the counter before and after a variable's expansion is what detects that. + truncations: usize, +} + +/// The specialization key of `ty`: its two directed reads (see the module docs). +/// +/// Reads the live bound graph, so it must be called with the graph in the state +/// the use's pin will see — i.e. *before* the pin, matching every other use's +/// key, so that both sides of a memo comparison are computed by one procedure at +/// one point in the pin's lifecycle. +pub fn spec_key(ty: &Type) -> SpecKey { + let mut ctx = KeyCtx { + visiting: HashSet::new(), + memo: HashMap::new(), + truncations: 0, + }; + // One walk-wide `ctx` for both reads: its memo is keyed by polarity, so the + // two reads share it without contaminating each other. + SpecKey { + positive: key_go(ty, true, &Subst::id(), &mut ctx), + negative: key_go(ty, false, &Subst::id(), &mut ctx), + } +} + +fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView { + match ty { + Type::Base(_) + | Type::UIntRange(_) + | Type::DataSource(_) + | Type::ChanDom(..) + | Type::Txn => KeyView::from_atom( + AtomKey::from_type(ty).expect("every atomic type classifies as an AtomKey"), + ), + // A `Hole` contributes nothing — the same "no information here" the + // default key denotes, so a `Hole` keys identically to an + // under-determined `Infer`. That collision cannot merge two uses that + // actually differ, because emission normalizes every annotation + // (`normalize_annotation` turns a `Hole` into a fresh `Type::Infer`), so + // no `Hole` reaches a use's instantiation type in the first place. The + // arm is for exhaustiveness, and "no information here" is the honest + // reading if one ever did. + Type::Hole => KeyView::default(), + // A refinement rides the position it refines. The accumulated substitution + // is forced on it exactly as `compact_go` does, so a suspended + // dependent-application discharge lands in the key as the predicate the + // clone will actually carry — that is use-specific information, and two + // uses discharging different arguments *should* key apart. + Type::Refinement(inner, r) => { + let mut k = key_go(inner, pol, subst_acc, ctx); + let r = subst_acc.force_refinement(r); + if !k.refinements.contains(&r) { + k.refinements.push(r); + } + k + } + Type::Fun { + name, + domain, + codomain, + kind, + } => { + // The domain is contravariant — the flip that makes the dual read + // follow an argument's *lower* bounds. + let dom = key_go(domain, !pol, subst_acc, ctx); + // A Pi binder shadows the accumulated substitution inside the + // codomain, as in `compact_go`. The binder *name* itself is not part + // of the key — see `SpecKey::fun`. + let cod_acc = match name { + Some(b) => subst_acc.shadow(b), + None => subst_acc.clone(), + }; + let cod = key_go(codomain, pol, &cod_acc, ctx); + // Resolved through `KindMerge::of`, not off the `FunKind` itself: an + // inferred kind is a variable whose identity is fresh per instantiation, + // so keying on it would split every use; its *bounds* are the answer, and + // reading them here is what compaction does at the same point in the solve. + KeyView { + fun: BTreeMap::from([(KindMerge::of(kind), (Box::new(dom), Box::new(cod)))]), + ..Default::default() + } + } + Type::Tuple(ts) => KeyView { + rec: ts + .iter() + .enumerate() + .map(|(i, t)| (FieldKey::Index(i), key_go(t, pol, subst_acc, ctx))) + .collect(), + ..Default::default() + }, + Type::Record(fs) => KeyView { + rec: fs + .iter() + .map(|(n, t)| { + ( + FieldKey::Name(SmolStr::from(n.as_str())), + key_go(t, pol, subst_acc, ctx), + ) + }) + .collect(), + ..Default::default() + }, + Type::Variant(tags) => KeyView { + var: tags + .iter() + .map(|(k, t)| (k.clone(), key_go(t, pol, subst_acc, ctx))) + .collect(), + ..Default::default() + }, + // A history's children are invariant, so they recurse at the reference's + // own polarity — no flip, matching `compact_go`. + Type::History { + value, + domain, + kind, + } => { + let value = key_go(value, pol, subst_acc, ctx); + let domain = key_go(domain, pol, subst_acc, ctx); + KeyView { + history: BTreeMap::from([(*kind, (Box::new(value), Box::new(domain)))]), + ..Default::default() + } + } + // A variable contributes its **polarity-correct** bounds only. Following + // both here instead is what leaks out of this use's cone and into every + // other use's arguments; the two root reads are what cover both + // directions without ever mixing them at one variable. There is no + // opposite-polarity fallback either — the dual read subsumes it. + Type::Infer(state) => { + let memo_key = (state.uid, pol); + let memoizable = subst_acc.is_id(); + if memoizable && let Some(k) = ctx.memo.get(&memo_key) { + return k.clone(); + } + if !ctx.visiting.insert(memo_key) { + // A cycle in the bound graph (`?a <: ?b` and `?b <: ?a` is + // ordinary). Drop the back-edge: whatever it would contribute is + // already on the path that reached it. Recorded so the partial + // result this produces is never cached. + ctx.truncations += 1; + return KeyView::default(); + } + let bounds = { + let b = state.bounds.borrow(); + if pol { + b.lower.clone() + } else { + b.upper.clone() + } + }; + let truncations_before = ctx.truncations; + let mut acc = KeyView::default(); + for b in &bounds { + // Compose the edge's morphism before descending, as `compact_go` + // does: a bound reached transitively arrives with every edge's + // substitution composed. + let inner_acc = Subst::then(&b.render_subst(), subst_acc); + acc.union(key_go(&b.ty, pol, &inner_acc, ctx)); + } + ctx.visiting.remove(&memo_key); + if memoizable && ctx.truncations == truncations_before { + ctx.memo.insert(memo_key, acc.clone()); + } + acc + } + } +} + +#[cfg(test)] +mod tests { + // `ConstrainCache` keys on `(Type, Type)`; its interior mutability is + // identity-by-`uid` and never inspected by `Hash`/`Eq`, so the lint's hazard + // does not apply (see `constrain`'s module-level note). + #![allow(clippy::mutable_key_type)] + + use std::rc::Rc; + + use super::*; + use crate::ccl::infer::solver::{ConstrainCache, constrain_subtype, fresh_var}; + use crate::ccl::infer_var::Bound; + use crate::ccl::{BaseType, Lit, TypedExpr}; + + fn int() -> Type { + Type::Base(BaseType::Int) + } + + /// `{Int | __elem == n}` — a literal's singleton, the refinement every literal + /// carries and therefore the one this key exists to see. + fn singleton(n: i64) -> Type { + crate::ccl::infer::lit_singleton(&Lit::Int(n)) + } + + fn refined(marker: i64) -> Refinement { + Refinement::born(Rc::new(TypedExpr::lit(Lit::Int(marker)))) + } + + #[test] + fn atoms_and_shapes_are_structural() { + assert_eq!(spec_key(&int()), spec_key(&int())); + assert_ne!(spec_key(&int()), spec_key(&Type::Base(BaseType::String))); + assert_eq!( + spec_key(&Type::Tuple(vec![int(), int()])), + spec_key(&Type::Tuple(vec![int(), int()])) + ); + // Width matters: a key must not equate a 1-tuple with a 2-tuple, or a + // narrowed domain would share a clone with an unnarrowed one. + assert_ne!( + spec_key(&Type::Tuple(vec![int()])), + spec_key(&Type::Tuple(vec![int(), int()])) + ); + } + + #[test] + fn refinements_participate_and_distinguish() { + assert_ne!(spec_key(&int()), spec_key(&singleton(1))); + assert_ne!(spec_key(&singleton(1)), spec_key(&singleton(2))); + assert_eq!(spec_key(&singleton(1)), spec_key(&singleton(1))); + } + + #[test] + fn refinement_sets_compare_order_insensitively() { + let a = Type::Refinement( + Box::new(Type::Refinement(Box::new(int()), refined(1))), + refined(2), + ); + let b = Type::Refinement( + Box::new(Type::Refinement(Box::new(int()), refined(2))), + refined(1), + ); + assert_eq!(spec_key(&a), spec_key(&b)); + } + + /// An under-determined position is one canonical value, not a fresh + /// placeholder — two such uses must be able to share. + #[test] + fn under_determined_positions_are_canonical() { + assert_eq!(spec_key(&fresh_var(0)), spec_key(&fresh_var(0))); + assert_eq!(spec_key(&fresh_var(0)), SpecKey::default()); + } + + /// The defect the key exists to fix: an argument's refinement reaches a domain + /// variable as a **lower** bound, where a negative-position materialization + /// cannot see it. The saturated key sees it, so two calls differing only + /// there key apart. + #[test] + fn lower_bound_refinement_is_visible_where_a_materialization_narrows() { + let mut keys = Vec::new(); + for n in [2, 5] { + let dom = fresh_var(0); + let mut cache = ConstrainCache::new(); + // The emit-time `arg <: domain` edge, for an argument carrying its + // literal's singleton. + constrain_subtype(&singleton(n), &dom, &mut cache).expect("arg flows into domain"); + // And the definition's demand, which is all a negative resolution of + // `dom` would consult. + constrain_subtype(&dom, &int(), &mut cache).expect("domain meets the body's demand"); + keys.push(spec_key(&Type::fun(dom, int()))); + } + assert_ne!( + keys[0], keys[1], + "two calls whose only difference is an argument refinement on the \ + domain's lower bounds must not share a specialization" + ); + } + + /// A cycle between two variables terminates, and the walk still collects what + /// is reachable on the way rather than bailing out to the empty key. (`?a <: + /// ?b` with `?b <: ?a` is the ordinary spurious cycle, not a recursive type.) + #[test] + fn mutually_constrained_vars_terminate() { + let a = fresh_var(0); + let b = fresh_var(0); + let mut cache = ConstrainCache::new(); + constrain_subtype(&a, &b, &mut cache).expect("a <: b"); + constrain_subtype(&b, &a, &mut cache).expect("b <: a"); + constrain_subtype(&singleton(7), &a, &mut cache).expect("7 <: a"); + let k = spec_key(&a); + assert_ne!(k, SpecKey::default(), "the lower bound must be collected"); + assert_eq!(k, spec_key(&a), "and the walk must be deterministic"); + // The refinement is on `a`'s lower bounds, so it is the *positive* read that + // carries it — the same asymmetry a domain position exploits in reverse. + assert_eq!(k.positive, spec_key(&singleton(7)).positive); + } + + /// A key computed while a cycle back-edge was dropped is **incomplete**, so it + /// must not enter the memo — otherwise a later position that reaches the same + /// variable from outside the cycle is served the truncated view. + /// + /// The shape: `?a` and `?b` are mutually constrained and each carries a + /// refinement of its own, so each one's *complete* view is both refinements. + /// Reached from position 0, `?b` expands with `?a` already on the stack — the + /// back-edge is dropped and `?b` sees only its own `2`. Position 1 then asks for + /// `?b` directly, where nothing is on the stack and the answer is `{1, 2}`. + /// Without [`KeyCtx::truncations`] guarding the insert, the truncated `{2}` is + /// cached at position 0 and returned at position 1, and one type has two + /// different keys depending on where the walk met it. + /// + /// The cycle is built by **writing the bound lists directly** rather than + /// through [`constrain_subtype`], and that is the point: `constrain_go` keeps + /// the bound graph transitively closed, so a back-edge it recorded really does + /// contribute nothing new and the guard never fires. This walk must not depend + /// on that invariant — bounds also arrive carrying an edge substitution + /// (`Bound::render_subst`), where the transitive copy and the direct one are not + /// the same contribution. + #[test] + fn a_truncated_expansion_is_not_memoized() { + fn push_lower(var: &Type, ty: Type) { + let Type::Infer(v) = var else { + unreachable!("fresh_var yields Type::Infer"); + }; + v.bounds.borrow_mut().lower.push(Bound::conc(ty)); + } + let a = fresh_var(0); + let b = fresh_var(0); + push_lower(&a, singleton(1)); + push_lower(&a, b.clone()); + push_lower(&b, singleton(2)); + push_lower(&b, a.clone()); + + // Both variables reach both refinements, so both positions see both — no + // matter which one the walk expands first. + let both = spec_key(&Type::Tuple(vec![a.clone(), b.clone()])); + let (pos0, pos1) = ( + &both.positive.rec[&FieldKey::Index(0)], + &both.positive.rec[&FieldKey::Index(1)], + ); + assert_eq!( + pos0, pos1, + "the second position was served a view truncated while computing the \ + first: {pos0} vs {pos1}" + ); + assert_eq!( + pos0.refinements.len(), + 2, + "both refinements, at both positions: {pos0}" + ); + + // And the whole key is independent of the order the walk meets them. + assert_eq!(both, spec_key(&Type::Tuple(vec![b, a]))); + } + + /// [`KeyView::union`]'s structural merges: two bounds contributing *different* + /// shapes at one position must merge positionwise rather than one winning. + /// + /// Only the variable arm ever calls `union` with two non-empty views, so these + /// merges are unreachable except through a variable carrying several bounds — + /// which is exactly the ordinary case for a use whose argument and whose + /// definition-side demand both say something. + #[test] + fn several_bounds_at_one_position_merge_positionwise() { + // `?v` bounded below by two function types that differ only in their + // codomain: the merged view must carry both codomain atoms, not the first. + let v = fresh_var(0); + let mut cache = ConstrainCache::new(); + for cod in [int(), Type::Base(BaseType::String)] { + let f = Type::fun(singleton(1), cod); + constrain_subtype(&f, &v, &mut cache).expect("bound flows into v"); + } + let k = spec_key(&v); + let (dom, cod) = k + .positive + .fun + .values() + .next() + .expect("both bounds are functions, so the merged view has a function shape"); + assert_eq!( + cod.atoms.len(), + 2, + "a conflict at one position is recorded, not resolved: {cod}" + ); + assert_eq!( + dom.refinements.len(), + 1, + "the shared domain refinement is deduplicated, not doubled: {dom}" + ); + } + + /// A function's **kind** is part of its identity for the same reason a history's + /// flavour is: `𝐷 ⇒ 𝑉` and `𝐷 ⤇ 𝑉` are one shape and compile to different code — + /// a specialization pinned at `⤇` iterates a domain a `⇒` use does not supply — so + /// a clone keyed on one must not serve a use of the other. + /// + /// The kind reaches the key through `KindMerge::of`, so a concrete arrow keys by + /// what it *is*. An unresolved `FunKind::Var` resolves from its bounds like any + /// other position, which is what keeps two uses of one generic binding sharing a + /// clone instead of splitting on a per-instantiation variable identity. + #[test] + fn fun_kind_is_part_of_the_key() { + assert_ne!( + spec_key(&Type::fun(int(), int())), + spec_key(&Type::data_fun(int(), int())), + "a capability and a collection of the same shape must not share a clone" + ); + // An *unresolved* kind does not split: both uses read the same unbounded var + // through `KindMerge::of`, which answers `Compute` (the capability default). + let unresolved = || Type::Fun { + name: None, + kind: crate::ccl::ty::FunKind::fresh_var(), + domain: Box::new(int()), + codomain: Box::new(int()), + }; + assert_eq!( + spec_key(&unresolved()), + spec_key(&unresolved()), + "two fresh kind vars are the same unresolved answer, not two identities" + ); + // And the merge keeps two concrete kinds apart rather than one shadowing the + // other — what keying `fun` by `KindMerge` buys, and why it needs `Ord`. + let mut merged = key_go( + &Type::fun(int(), int()), + true, + &Subst::id(), + &mut fresh_ctx(), + ); + merged.union(key_go( + &Type::data_fun(int(), int()), + true, + &Subst::id(), + &mut fresh_ctx(), + )); + assert_eq!( + merged.fun.len(), + 2, + "a compute and a data arrow at one position are distinct contributions: {merged}" + ); + } + + /// A history's flavour is part of its identity: a `Mut(Int, Txn)` register and + /// a `Feed(Int, Txn)` channel are the same `domain ⇒ value` shape and must not + /// key alike, or a clone pinned to one would serve a use of the other. + #[test] + fn history_kind_is_part_of_the_key() { + let history = |kind| Type::History { + value: Box::new(int()), + domain: Box::new(Type::Txn), + kind, + }; + assert_ne!( + spec_key(&history(HistoryKind::Overwrite)), + spec_key(&history(HistoryKind::Append)) + ); + // And the merge keeps them apart rather than one shadowing the other — + // which is what the `history` map being keyed by kind buys, and why + // `HistoryKind` needs `Ord`. Driven through `union` directly: `constrain` + // reads an `Overwrite` handle *through* to its value type, so the two kinds + // never reach one variable's bound list by way of a subtyping edge. + let mut merged = key_go( + &history(HistoryKind::Overwrite), + true, + &Subst::id(), + &mut fresh_ctx(), + ); + merged.union(key_go( + &history(HistoryKind::Append), + true, + &Subst::id(), + &mut fresh_ctx(), + )); + assert_eq!( + merged.history.len(), + 2, + "an Overwrite and an Append at one position are distinct contributions: {merged}" + ); + } + + fn fresh_ctx() -> KeyCtx { + KeyCtx { + visiting: HashSet::new(), + memo: HashMap::new(), + truncations: 0, + } + } +} diff --git a/src/ccl/infer/typing.rs b/src/ccl/infer/typing.rs index db3d448e..eb7d10e1 100644 --- a/src/ccl/infer/typing.rs +++ b/src/ccl/infer/typing.rs @@ -230,7 +230,7 @@ pub(super) trait Typing { } /// Peel every outer [`Type::Refinement`] layer off `t`, returning the bare -/// structural type underneath. Non-allocating — only unwraps the outer witnesses a +/// structural type underneath. Non-allocating — only unwraps the outer refinements a /// node acquired during solving; nested refinements are left in place. pub(super) fn peel_refinements_outer(t: &Type) -> &Type { let mut cur = t; diff --git a/src/ccl/inline.rs b/src/ccl/inline.rs index 3bfa7997..dfea065f 100644 --- a/src/ccl/inline.rs +++ b/src/ccl/inline.rs @@ -1229,8 +1229,10 @@ mod tests { /// precondition beta-reduction would silently drop, so the assert fires /// rather than substituting. Pins the guard that keeps /// [`refinement_discharged_by`] from being weakened to "any refined param is - /// fine" — e.g. if specialization were ever keyed modulo refinements, one - /// literal's singleton could reach the param slot of a call made at another. + /// fine" — the shape this arrives in is a monomorphization key that cannot tell + /// two call sites' refinements apart, which lets one literal's singleton reach + /// the param slot of a call made at another (see `src/ccl/design/type-inference.md`, + /// "Keying a specialization"). #[test] #[should_panic(expected = "does not entail")] fn refined_outer_param_not_entailed_by_argument_asserts() { diff --git a/src/ccl/lower/comprehension.rs b/src/ccl/lower/comprehension.rs index 2323c53c..c8d61e12 100644 --- a/src/ccl/lower/comprehension.rs +++ b/src/ccl/lower/comprehension.rs @@ -73,7 +73,7 @@ pub(super) fn lower_list_comp( // into both the body chain and the loop-join predicate: copies of a // minted tree stay structurally equal (uids are preserved by // cloning), which is what lets inference dedup the predicate-side - // refinement witnesses against the body-side ones. See the "mint before + // refinements against the body-side ones. See the "mint before // copy" contract in `crate::ccl::uniquify`. let source = uniquify::run(lower_expr(iter, ctx)?); let var_name = extract_name_target(target, "comprehension target")?; diff --git a/src/ccl/mut_elim.rs b/src/ccl/mut_elim.rs index a87f393e..88968aa1 100644 --- a/src/ccl/mut_elim.rs +++ b/src/ccl/mut_elim.rs @@ -1036,8 +1036,8 @@ pub(crate) fn register_value_tys<'a>( /// tree records reads at the deref'd value directly, as the phase's own /// hand-built test trees do. The written type then stands in, **stripped** — a /// register takes no refinement from any single contribution, and an unstripped -/// one would be a witness acquired by erasure rather than by `cast` -/// (`src/ccl/design/type-inference.md`, "Refinements as witness sets"). +/// one would be a refinement acquired by erasure rather than by `cast` +/// (`src/ccl/design/type-inference.md`, "Refinements on the lattice"). fn collect_writes(expr: &Expr, reg_vtys: &HashMap, out: &mut Vec<(Name, Type)>) { if let TypedExprNode::MutWrite { name, value } = &expr.node && !out.iter().any(|(n, _)| n == name) diff --git a/src/ccl/simplify.rs b/src/ccl/simplify.rs index 2d959a3b..c54e460b 100644 --- a/src/ccl/simplify.rs +++ b/src/ccl/simplify.rs @@ -88,7 +88,7 @@ use crate::ccl::{ /// [`TypedExprNode::Cast`] carries a domain refinement (a filter) on its type, /// so it is tempting to protect it the same way — dropping a cast looks like a /// "filter silently dropped" hazard. It is not, and adding the guard -/// regresses real reductions (witness: `test_new_compile::case_27` in +/// regresses real reductions (refinement: `test_new_compile::case_27` in /// `tests/compilation_pipeline.rs`). No rule matches a `Cast` node (the /// simplify rules operate on `Apply`/`Compose`), so none collapses `cast(v)` /// to `v` directly; a rule only *drops a sub-tree containing a cast* when that diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index e28820c6..96f2e80b 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -432,7 +432,12 @@ pub enum Type { /// Which flavour of [`Type::History`] a handle is — a mutable variable (`:=`) or a /// feed channel (`defer` / `<<`). The two are the same object (a `domain ⇒ /// value` history) but read and materialize differently; see [`Type::History`]. -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +/// +/// `Ord` carries no semantics — the two kinds are unordered alternatives. It +/// exists so a kind can key a `BTreeMap`, which is how the monomorphization +/// specialization key holds a position's history contributions without having to +/// pick a winner between two kinds (see `src/ccl/infer/solver/spec_key.rs`). +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum HistoryKind { /// A mutable variable introduced by `:=` — deref-on-read to the scalar `value`, /// a `get_prev_seq` / `get_prev_txn` recurrence, a `final_or_default` trailing @@ -944,7 +949,7 @@ impl PartialEq for Refinement { /// predicate was constructed, so a `{D | p}` that join planning /// re-minted at a marker (`make_iterate` / `make_restrict` / /// `refine_with`) compares equal to its structural twin — which is what - /// lets the post-planning `typecheck` chain the re-minted witnesses. This + /// lets the post-planning `typecheck` chain the re-minted refinements. This /// is *equality*, not implication — `{T | p}` and `{T | q}` with /// structurally-distinct predicates remain unequal. /// @@ -996,7 +1001,7 @@ impl Eq for Refinement {} /// ([`ccl_utils::cast_target_refinement`]) — a semantic filter, not inference /// metadata. Two predicates that each contain a cast and differ only in the /// nested filter (e.g. embedded comprehensions filtering `> 0` vs `< 0`) -/// denote different refinements; conflating them would let witness-deficit +/// denote different refinements; conflating them would let refinement-deficit /// matching accept an unsatisfied demand and refinement dedup drop a runtime /// `Restrict`. The target's *base* types are still skipped. The recursion /// terminates on tree shape alone: a predicate is an immutable `Rc`, diff --git a/src/ccl/uniquify.rs b/src/ccl/uniquify.rs index 827cae63..6adfb6f4 100644 --- a/src/ccl/uniquify.rs +++ b/src/ccl/uniquify.rs @@ -60,7 +60,7 @@ //! predicate; chained comparisons clone the shared middle operand). A copy //! made of *raw* trees would mint distinct uids per copy here, making //! α-equivalent copies structurally unequal — and the loop-join shape relies -//! on the copies comparing equal (witness dedup collapses the +//! on the copies comparing equal (refinement dedup collapses the //! predicate's source against the body's). So lowering runs this pass on a //! subtree *before* cloning it (see `lower_list_comp` Phase 1), and the //! whole-program run treats minted names as settled: minted binding sites diff --git a/tests/compilation_pipeline/generators_udf_poly.rs b/tests/compilation_pipeline/generators_udf_poly.rs index cd3cb7bb..cbd5518f 100644 --- a/tests/compilation_pipeline/generators_udf_poly.rs +++ b/tests/compilation_pipeline/generators_udf_poly.rs @@ -40,6 +40,46 @@ fn test_function_def_polymorphic_used_at_two_types() { check_scalar(code, Value::Bool(true)); } +// Two calls at the same *base* types but different argument literals. Every +// literal carries its own singleton, so the two uses instantiate the UDF at +// genuinely different refined types and must not share a specialization — the +// clone's interior is resolved against the argument that pinned it, so a shared +// clone would carry one call's argument type at the other's call site. +// +// These are regression guards for a specialization memo keyed on a *resolved +// type*: because a domain resolves from its upper bounds, an argument's refinement +// (a lower bound) was invisible in the key exactly where the definition body +// supplied something concrete, so a difference confined to such a position keyed +// equal. `\a, b -> a + b` at `(1, 2)` and `(1, 5)` both keyed on +// `((1, Int) ⇒ Int)`, shared a clone typing `.1` as `2`, and the post-inline +// consistency wall then panicked ("Type mismatch for Apply: expected 5, found +// 2"). `SpecKey` reads both bound directions, so the two key apart. +// +// The controls matter as much as the cases: a difference in the *first* argument +// always keyed apart (its refinement reached the key), and two identical calls must +// still **share** — the fix must not degrade into cloning per call site. +#[rstest] +#[timeout(Duration::from_secs(10))] +// Differs only in the second argument — the position the old key could not see. +#[case("h = \\a, b -> a + b\nh(1, 2) + h(1, 5)", Value::Int(9))] +// Differs in the first argument: keyed apart even before the fix. +#[case("h = \\a, b -> a + b\nh(2, 1) + h(5, 1)", Value::Int(9))] +// Three call sites, two of them differing only in an invisible position. +#[case("h = \\a, b -> a + b\nh(1, 2) + h(1, 5) + h(1, 9)", Value::Int(19))] +// Identical calls: one specialization, shared. +#[case("h = \\a, b -> a + b\nh(1, 2) + h(1, 2)", Value::Int(6))] +// A single-argument UDF, where the shared clone's body carried the first call's +// singleton on its parameter reference (`λ x : Int → x:<1> + 1`). That happened +// to compile to the right answer, so this case pins the *result* while the +// unit-level `SpecKey` tests pin the keying. +#[case("f = \\x -> x + 1\nf(1) + f(2)", Value::Int(5))] +fn test_polymorphic_udf_calls_differing_only_in_a_literal( + #[case] code: &str, + #[case] expected: Value, +) { + check_scalar(code, expected); +} + // --------------------------------------------------------------------------- // Generator functions — def f(xs): for x in xs: yield expr // ---------------------------------------------------------------------------