From 834417649b5efd421eac482a83dc9db189529bf7 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Mon, 10 Aug 2026 14:25:26 -0700 Subject: [PATCH 1/6] Traits: state what an operator requires of its operands, not that they are the same MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A polymorphic operator's requirement cannot be stated as a signature. The only relation a signature can put between two operands is that they *share a variable*, which also forces every other lattice dimension to agree — so one operand's refinement became a requirement on the other, and a refinement both operands carried survived onto a value the operator computed rather than selected. Arithmetic, comparison and negation now state a **trait** instead: unrelated inference variables per operand, plus an obligation recorded beside the graph. Because an operator's result is an ordinary variable rather than a marker standing for a computation, information still flows backwards through it — so a function typechecks without its call sites, and `(1 + 2) and True` is an ordinary bound conflict. The refinement strip in `apply_binary_scheme` goes away rather than being fixed: a syntactic peel does nothing for an operand still holding a `Type::Infer`. `src/ccl/infer/solver/traits.rs` opens with the vocabulary; [type-inference.md](src/ccl/design/type-inference.md#traits) carries the design. One term to fix here, because it reads two ways: an **obligation** is a single claim with two halves, and neither alone is "the obligation" — *the operands are types some implementation accepts*, **and** *each associated position is what that implementation associates*. A trait names **associated types** (Rust's term) rather than having *an* output, and a type is associated only when it **depends** on the types satisfying the trait. Three shapes result — unary with an `Output` (`Negatable`), binary with one (`Addable`), binary with **none** (`Equatable`/`Orderable`) — each exercised by ordinary programs (`each_trait_shape_types_a_real_program`). The third is the correction worth reviewing. A comparison's `Bool` is the same for every pair the trait accepts, so it says nothing about them: it is the *operator's* signature, not the trait's — `PartialEq` has no associated type either. Modelling it as one made "a comparison settles its output at birth" look like a property when it was a constant mis-recorded as a computed type. `Neg` moves off its monomorphic scheme for the same reason, giving the unary arity a real user. A candidate set shrinks as base types arrive, and an associated type is deposited once every survivor agrees on it — onto **associated positions only**, since the obligation is their sole source of information while an operand always has the program's own `left <: A` edge. How much is determined is therefore a property of the table, and shrinks as it grows *including for an associated type*: `\x -> x + 1` has result `Int` only because `Int` in the second position leaves one row, and `Addable(Float, Int) ⇝ Float` would open the result just as the parameter already is. Hence agreement, not uniqueness, as the deposit condition. Each variant's doc states its shape — how many types it is over, and what it associates — and `Trait::arity`/`assocs` read that shape off the table so the prose cannot drift from the rows (`every_trait_has_a_consistent_shape`). One invariant carries the mechanism — a concrete type reaching an operand variable must reach the obligation watching it — and the bound closure does *not* provide it. A variable's lower bounds are written in four places, delivery is wired into each, and all four are load-bearing: deleting one fails exactly its own case in `a_concrete_operand_reaches_its_obligation`. [The design doc](src/ccl/design/type-inference.md#delivery-the-watch-follows-the-edge) argues it; `verify_narrowing_is_complete` checks it on every program rather than trusting it. `test_lambda_unapplied` asserts an open parameter with the codomain per case; `test_collect_multi_conflict` and `test_unary_neg_wrong_type` see `NoTraitImpl` naming the trait instead of a mismatch against a hardcoded domain. `a_register_that_reads_itself_still_gets_a_type` ports #51's recurrence cases, which pin something stronger here: narrowing consumes bounds as they are recorded rather than resolved types, so an obligation never enters the recurrence — the base it needs sits on the register's seed. **`max`'s comparability tripwire flips**, closing `type-checker-traits-comparability`. `Comparable(γ)` on its codomain is the fourth shape — unary, associating nothing, since the scheme already returns an element of what it consumes. That needed a fix worth reviewing on its own: a contribution is now classified three ways rather than two — it offers a base, is *not determined yet* (a variable, a hole, a `Feed` handle), or is *determined and not a base* (a tuple, record, variant, function). Only the middle one is "nothing to say"; the third is rejected. Collapsing the two let composites through, so `(1, 2) == (3, 4)` type-checked as `Bool` — a tuple narrowed nothing, and a comparison has no associated position to leave unresolved, so no later wall saw it either. Composites now satisfy no trait (`a_composite_satisfies_no_trait`), which is what the closed tables were always meant to mean. --- src/ccl/design/type-inference.md | 75 ++- src/ccl/infer/api.rs | 94 ++- src/ccl/infer/check.rs | 80 ++- src/ccl/infer/context.rs | 36 ++ src/ccl/infer/emit.rs | 95 ++- src/ccl/infer/mod.rs | 26 +- src/ccl/infer/schemes.rs | 180 ++++-- src/ccl/infer/solver/constrain.rs | 72 ++- src/ccl/infer/solver/mod.rs | 1 + src/ccl/infer/solver/scheme.rs | 53 +- src/ccl/infer/solver/traits.rs | 959 ++++++++++++++++++++++++++++++ src/ccl/infer/typing.rs | 30 + src/ccl/infer_var.rs | 14 + tests/type_check.rs | 305 +++++++++- 14 files changed, 1895 insertions(+), 125 deletions(-) create mode 100644 src/ccl/infer/solver/traits.rs diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index ebf13ff4..5c0d34ed 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -684,7 +684,9 @@ The reason is that a literal knows more about itself than its base does, and tha What this changed is instructive, because refinements were rare enough before that several rules assumed their absence. Each was already wrong for a user-written refinement; literals are merely the first thing that makes them reachable. -* **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. +* **An operator does not *inherit* its operands' refinements**, and does not have to be *made* not to. A refinement is a fact about a value, so an operator that computes a new value cannot carry one over: `𝑥 + 𝑥` where `𝑥` is `2` produces `4`. Arithmetic, comparison and negation state their requirement as a [trait](#traits), over a variable per operand and per associated type — all unrelated — which leaves no path for an operand's refinement to reach the result by sharing. The remaining monomorphic operators (`and`, `++`, `not`) keep an ordinary scheme and pass their operands verbatim — nothing is shared with the result, so a refined operand simply flows into a concrete domain. Aggregates likewise keep theirs, since their operand is a *collection* whose refinements describe its domain and the rule must see them. + + Inheriting is not the same as **computing**, and only the first is ruled out. `{Int | __elem == 2} + {Int | __elem == 3}` genuinely *is* `{Int | __elem == 5}`, and a trait implementation is where such a rule would live, since it determines the output type rather than forcing it to be a position the operands already occupy. Today every implementation computes a base and stops — a property of the table, not of the mechanism. Two things would have to change to lift it: an implementation would need the operands' *types* rather than their bases, and the deposit would have to move to a point where those types are final. Eager deposit is sound for a base because a base never weakens, while a refinement set only shrinks as further lower bounds arrive — so a refinement computed from a partial view is too strong. A rule computing from resolved operands then meets recurrences (`x := x + 1` resolves its operand through its own output), where it must already be sound at the cut; and anything beyond constant folding and interval arithmetic needs predicate *implication*, which the lattice deliberately does not have (refinements match structurally — see this file's module-level note in `src/ccl/infer/solver/mod.rs`). * **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 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. @@ -1130,6 +1132,67 @@ Recorded so a reader can tell a deliberate boundary from an oversight. --- +## Traits + +The constraint lattice can state that two positions are **equal** or **related by subtyping**. That is everything an operator needs when its result *is* one of its operands — `max(xs)` returns an element, `x.f` returns the field — because "is one of" is a shared lattice position. It is not enough for an operator whose result is **computed from** its operands, and `+` is the smallest example: the sum of two values is neither of them. (Sharing one variable across operands and result — the signature this replaced — states the requirement in the one place it is wrong in both polarities at once; `an_operator_result_carries_no_operand_refinement` pins the consequence.) + +### Vocabulary + +* A **trait** is a named requirement a type may satisfy — `Addable`, `Orderable`, `Comparable`. **A trait is not a type**: no `Type` variant, no lattice point, no subtyping edge, and the type grammar and `constrain_go`'s rules are untouched. Types *satisfy* traits. +* An **implementation** is one row of a trait's table: the types it accepts, and the types it associates with them. +* An **associated type** is a type a trait *names* — `Output`, the type an arithmetic operator's result takes. A trait is a requirement rather than a function, so it associates any number, **including none**. A type is associated only when it *depends* on the types satisfying the trait: a comparison's `Bool` is the same for every pair `Equatable` accepts, so it belongs to the operator's signature and `Equatable` associates nothing — recording it as an association would claim the trait determines something it does not. +* An **obligation** is one recorded instance of a trait at specific type positions: one **operand position** per argument the trait takes, and one **associated position** per type it names. It is a single claim with two halves, and neither alone is the obligation: *the operand positions are types some implementation accepts*, **and** *each associated position is what that implementation associates*. Every position is an ordinary inference variable, unrelated to the others. + +An operator's signature is therefore `𝐴₁ → … → 𝐴ₙ → 𝑅` plus the obligation, for the trait's arity `𝑛`, where `𝑅` is either one of the associated positions or a type the operator fixes. The three shapes the operators take: + +| operator | signature | obligation | +|---|---|---| +| `+` | `∀ 𝐴 𝐵 𝑂. 𝐴 → 𝐵 → 𝑂` | `Addable(𝐴, 𝐵)`, `Output` at `𝑂` | +| `==` | `∀ 𝐴 𝐵. 𝐴 → 𝐵 → Bool` | `Equatable(𝐴, 𝐵)`, nothing associated | +| unary `-` | `∀ 𝐴 𝑂. 𝐴 → 𝑂` | `Negatable(𝐴)`, `Output` at `𝑂` | + +Mechanism: `src/ccl/infer/solver/traits.rs`. + +Because an associated position like `𝑂` is an ordinary variable rather than a marker standing for a computation, information flows *backwards* through an operator's result and misusing that result is an ordinary diagnostic — `(1 + 2) and True` fails as a bound conflict. A computed-type marker cannot have this property: the solver cannot compare an unreduced computation against anything, so a function could not be typechecked without seeing its call sites. + +### Refinements are transparent + +`{𝑇 | 𝑝}` satisfies a trait exactly when `𝑇` does. This holds *by construction*: satisfaction is judged on each bound contribution as it arrives, with refinements peeled at that moment — when the base actually exists. An operand is usually still an inference variable at emission, so a peel performed *there* would have nothing to work on. + +### Discharge is incremental + +An obligation is a monotone fact discharged as the graph fills in, the shape [`FunKindVar`](#46-data-vs-compute-functions) already uses for kinds — not a sweep at the end of solving. Each operand position carries a **candidate set** of implementations that only ever shrinks; each associated type is deposited on its position as an ordinary lower bound as soon as every surviving candidate agrees on it. Order therefore does not matter. + +What arrives at a position is classified three ways, and the third is easy to miss: a contribution either offers a **base**, is **not determined yet** (an inference variable, a hole, a transient `Feed` handle whose payload arrives separately), or is **determined and not a base** (a tuple, record, variant or function). The first narrows; the third is rejected outright, because no implementation can ever accept it; only the second is genuinely "nothing to say". + +Collapsing the last two is a live hazard rather than a hypothetical. While "no base here" meant "no information", `(1, 2) == (3, 4)` type-checked as `Bool`: a tuple narrowed nothing, and a comparison has no associated position to leave unresolved, so no later wall saw it either. The same hole let `max` accept a tuple codomain. + +What narrowing cannot reject is a position the program never determines — which is the honest outcome, reported as an unresolved variable rather than as a missing implementation. + +### What an obligation determines, and what it leaves alone + +The deposit rule is *whatever every surviving implementation agrees on*, applied to the **associated positions only**. Nothing is ever deposited onto an operand. + +The asymmetry is not soundness — with one candidate left, its operand types are implied exactly as its associated types are. It is that the obligation is an associated position's **only** source of information and never an operand's: an associated position is a fresh variable nothing else constrains from below, while an operand always has the program's own `operandᵢ <: 𝐴ᵢ` edge. Determining an operand from the table would be recovering information the program was supposed to supply, which hides an under-connected lowering instead of fixing it. + +How much gets determined is therefore a property of the table, and shrinks as the table grows — **for the output too**. Today `λ 𝑥 → 𝑥 + 1` is `∀𝐴 𝑂. (𝐴 : Addable(𝐴, Int)) ⇒ 𝐴 → 𝑂` with `𝑂` resolving to `Int`, because `Int` in the second position leaves only `(Int, Int) ⇝ Int`. Adding `Addable(Float, Int) ⇝ Float` would leave two candidates whose outputs disagree, and the result would become as open as the parameter already is. That is the type honestly tracking a language that has become more permissive, and it is why the deposit waits for *agreement* rather than firing on a unique candidate. + +### Delivery: the watch follows the edge + +An obligation is attached to each operand variable as a *watch* (`InferVar::watches`), and everything the invariant rests on is **delivery** — a concrete type reaching an operand variable has to reach the obligation watching it. + +The bound closure does not deliver on its own. When two variables sit at different polymorphism levels — which is what a `let` RHS produces, being emitted one level deeper — their edge is recorded by the arm whose closure runs against the *other* side's bounds, so a type already sitting on the lower variable is never re-offered. The graph is still correct, but only *transitively* readable, which is something coalesce does and emission does not. + +A variable's lower bounds are written in exactly four places, and delivery is wired into every one: `constrain_go`'s two variable arms (a concrete contribution is delivered directly; a var-var edge propagates the watch *downward*, toward the variables feeding the watched one, and delivers what they already know), `extrude`'s proxy seeding, and `freshen_above`'s clone — the latter two because both seed bounds by direct writes rather than through `constrain_go`. + +That the list is closed is an argument about today's code, not something the compiler enforces, and a missed delivery is quiet: the obligation simply never narrows, so a type is left undetermined and surfaces phases later on an interior node. `verify_narrowing_is_complete` therefore checks the argument rather than trusting it — after emission, every watched operand is resolved against the completed graph, and a resolved base must already have narrowed its obligation. `a_concrete_operand_reaches_its_obligation` covers the four writers with a case per mechanism. + +### Requirements are generalized + +Obligations ride variables through `freshen_above`, so a generalized function carries its operators' requirements into its scheme. Each use instantiates and discharges its **own** copy — sharing one would let a `String` use empty an `Int` use's candidate set. + +--- + ## 5. CCL-specific inference rules §1–§4 describe the engine generically; the general two-pass structure (emit → coalesce) is §2. This section covers the per-node wiring specific to CCL's AST — the structural rule each `TypedExprNode` variant emits. `ccl::infer` runs on a `TypedExpr` whose nodes all carry `Type::Hole`, calls the emit rules below per node, and coalesces the resulting constraint graph back onto each `expr.ty` (§2). A residual `Type::Infer(id)` after inference means the coalesce pass left a variable genuinely unconstrained (e.g. the parameter of an unapplied identity lambda). @@ -1142,18 +1205,20 @@ Recorded so a reader can tell a deliberate boundary from an oversight. | Op kind | Operand constraint | Result type | |---|---|---| -| `Arithmetic` | both operands constrained `<: α` (joined into a shared variable) | operand type | +| `Arithmetic` | a trait obligation over two *unrelated* variables — `Addable`, `Subtractable`, `Multipliable`, `Divisible` | the trait's `Output` | +| `Compare` | a trait obligation — `Equatable` (`==`, `!=`) or `Orderable` (`<`, `<=`, `>`, `>=`), which associate nothing | `Bool`, fixed by the operator | | `Concat` | both operands constrained to `String` | `String` | -| `Compare` | both operands constrained `<: α` (joined into a shared variable) | `Bool` | | `BoolLogic` | both operands constrained to `Bool` | `Bool` | -**Note**: String + String → `Concat` rewriting is performed at **compile time** (in `lambda_elim.rs`), not at inference time. The inference pass only constrains both operands to `String` and returns `String` as the result type. +The bottom two rows are ordinary schemes, because their operand types are fixed. The top two are not, and could not be: see [Traits](#traits). + +**Note**: String + String → `Concat` rewriting is performed at **compile time** (in `simplify.rs`), not at inference time. Inference accepts `(String, String) ⇝ String` as an `Addable` implementation and returns `String`. ### UnaryOp type rules | Op kind | Operand constraint | Result type | |---|---|---| -| `Neg` | operand constrained to `Int` | `Int` | +| `Neg` | a **unary** trait obligation — `Negatable` | the trait's `Output` | | `Not` | operand constrained to `Bool` | `Bool` | ### `Case` inference diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index 47e7793d..86314ce5 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -105,6 +105,11 @@ impl InferArena { /// [`crate::ccl::arena_enter`]). pub fn new() -> Self { crate::ccl::arena_enter(); + // The trait-narrowing audit trail is per-run, exactly as the variable + // capture is: checking one run's obligations against another's graph would + // resolve variables that no longer have bounds. + #[cfg(debug_assertions)] + crate::ccl::infer::solver::traits::clear_watch_log(); InferArena { _not_send_sync: std::marker::PhantomData, } @@ -123,6 +128,10 @@ impl Drop for InferArena { // edges, so the (otherwise cyclic) refcounts can all reach zero. for var in crate::ccl::arena_exit() { var.bounds.borrow_mut().clear(); + // A trait obligation holds its output `Type`, which holds a variable, + // which watches the obligation — a cycle of exactly the kind the bound + // lists make, and severed the same way. + var.watches.borrow_mut().clear(); } } } @@ -335,6 +344,29 @@ pub enum InferError { /// Display label for the message (see the type docs — not the location). at: String, }, + /// An operator was used at operand types no implementation of its trait + /// accepts — `1 > "a"`, `"a" - "b"`, or a polymorphic function applied at a type + /// its body's operators cannot handle. + /// + /// Distinct from [`InferError::TypeMismatch`] on purpose: the two operands did + /// not fail to *relate*, and neither is wrong on its own. What failed is the + /// operator's requirement about the pair, so the message names the trait and + /// what the position could have accepted rather than showing two types that + /// "don't match". + NoTraitImpl { + /// The trait with no implementation left, e.g. `Addable`. + trait_: String, + /// The operand position (0-based) whose type ruled the last one out. + position: u8, + /// The base type found there. Boxed for the same reason + /// [`InferError::TypeMismatch`]'s types are — to keep `Result` small. + found: Box, + /// What that position could still have accepted, given what was already + /// known about the other operand. + accepted: Vec, + /// Display label for the message (see the type docs — not the location). + at: String, + }, /// A partial tuple or partial record was not resolved to a concrete type. UnresolvedPartial { /// Display string of the partial type. @@ -520,6 +552,25 @@ impl std::fmt::Debug for InferError { } Ok(()) } + InferError::NoTraitImpl { + trait_, + position, + found, + accepted, + at, + } => { + let accepted = accepted + .iter() + .map(|t| t.to_string()) + .collect::>() + .join(" or "); + write!( + f, + "No {trait_} implementation for {at}: operand {} is {found}, but \ + the only type accepted there is {accepted}", + position + 1, + ) + } InferError::MissingField { key, found, at } => match (key, found) { // A tuple's positions are its width, so that is the fact to state: the // projection asked for a position past the end. @@ -1979,23 +2030,28 @@ mod tests { #[test] fn test_collect_multi_conflict() { // λ x → Apply(λ a:Int → a, Var(x)) + Apply(λ b:String → b, Var(x)) - // `x` is the argument to both an Int-domain and a String-domain function. - // The sound one-way `arg <: domain` rule records `x <: Int` and - // `x <: String` — two upper bounds, with no eager cross-constraint — so - // the conflict surfaces structurally at coalesce when the bounds collide - // (`IncompatibleBounds`, an untagged-sum rejection) rather than as an - // eager `TypeMismatch` from the (retired) reverse `domain <: arg`. Both - // correctly reject the program. + // `x` is the argument to both an Int-domain and a String-domain function, + // whose results are then added. + // + // The rejection comes from the `+`, and names the actual problem: no + // `Addable` implementation takes an `Int` and a `String`. It arrives during + // emission, as soon as both operand types are known — the operator states a + // requirement about the *pair*, so it need not wait for the two to collide on + // a shared variable at coalesce. + // + // The one-way `arg <: domain` rule that puts them there is what the + // `IncompatibleBounds` tests in `tests/type_check.rs` cover, joining two types + // without an operator in the way. let mut expr = double_apply_lambda(Type::Base(BaseType::Int), Type::Base(BaseType::String)); let mut ctx = TypeInferenceContext::new(); let errs = infer_bare(&mut expr, &mut ctx).expect_err("expected an Int/String conflict"); assert!( errs.iter().any(|e| matches!( e, - InferError::IncompatibleBounds { conflicting, .. } - if conflicting.contains("Int") && conflicting.contains("String") + InferError::NoTraitImpl { trait_, found, .. } + if trait_ == "Addable" && **found == Type::Base(BaseType::String) )), - "expected IncompatibleBounds Int/String, got {errs:?}" + "expected NoTraitImpl for Addable at a String operand, got {errs:?}" ); } @@ -2555,20 +2611,20 @@ mod tests { fn test_unary_neg_wrong_type() { let mut ctx = TypeInferenceContext::new(); use crate::ccl::UnaryOpKind; - // -true → TypeMismatch(Bool, Int). + // `-true`: negation states `Negatable`, so the rejection names the trait and + // the type it will not accept rather than reporting a mismatch against a + // hardcoded `Int` domain. let mut expr = Expr::unary(UnaryOpKind::Neg, Expr::lit(Lit::Bool(true))); - let errs = infer_bare(&mut expr, &mut ctx) - .expect_err("expected TypeMismatch Bool/Int under inference"); + let errs = infer_bare(&mut expr, &mut ctx).expect_err("Bool is not negatable"); assert!( errs.iter().any(|e| matches!( e, - InferError::TypeMismatch { type_a, type_b, .. } - if matches!( - (type_a.as_ref(), type_b.as_ref()), - (Type::Base(BaseType::Bool), Type::Base(BaseType::Int)) - ) + InferError::NoTraitImpl { trait_, position, found, .. } + if trait_ == "Negatable" + && *position == 0 + && **found == Type::Base(BaseType::Bool) )), - "expected TypeMismatch Bool/Int, got {errs:?}" + "expected NoTraitImpl for Negatable at a Bool operand, got {errs:?}" ); } diff --git a/src/ccl/infer/check.rs b/src/ccl/infer/check.rs index 74d863f5..c295cf6a 100644 --- a/src/ccl/infer/check.rs +++ b/src/ccl/infer/check.rs @@ -18,6 +18,7 @@ use super::emit::{ use super::schemes::OperatorSchemes; use super::typing::{Typing, peel_refinements_outer}; use super::{lit_base, map_constrain_err}; +use crate::ccl::infer::solver::traits::{Assoc, Trait, offered_base}; /// Post-inference structural type-check state. /// @@ -113,6 +114,75 @@ impl Typing for CheckCtx { ann.clone() } + fn require_trait( + &mut self, + trait_: Trait, + operands: &[&Type], + assoc: Option, + at: &dyn Fn() -> String, + ) -> Result, LocatedInferError> { + // No obligation is created here, for two independent reasons. Types are + // already concrete, so there is nothing to discharge incrementally; and Check + // runs outside any `InferArena`, so an obligation's variable⇄obligation cycle + // would never be broken. + // + // What this rule is *for* is supplying the node's type so the reconcile below + // has something to compare against — the common path, taken 3,812 times across + // the pipeline suite. + // + // The rejection branch is not a user-error backstop. Catching user type errors + // is entirely inference's job; Check exists to catch **compiler bugs that + // corrupt types**, which is why a Check error that is not `UnresolvedInfer` + // panics at the wall rather than being reported. So this firing means + // inference has a hole or a later pass rewrote the tree into something + // ill-typed — and it reuses `NoTraitImpl` for the same reason + // [`Typing::require_sub`] reuses `TypeMismatch` here: the error vocabulary + // describes the inconsistency, the wall supplies the interpretation. Measured + // across the suite: it never fires. + let bases: Option> = operands.iter().map(|t| offered_base(t)).collect(); + let Some(bases) = bases else { + // Pre-desugar residue (a `Feed` handle, an un-eliminated `Mut`, a + // still-`Infer` position under `Strictness::PreDesugar`) is not something + // this rule can judge — the strictness wall decides whether a residual + // type is tolerable at this point in the pipeline. + return Ok(assoc.map(|_| self.fresh())); + }; + let matched = trait_ + .impls() + .iter() + .find(|i| i.args.len() == bases.len() && i.args.iter().eq(bases.iter().copied())); + match matched { + Some(matched) => Ok(assoc.map(|name| { + matched + .assoc_ty(name) + .map(|b| Type::Base(b.clone())) + .unwrap_or_else(|| fresh_var(self.level)) + })), + None => { + // Blame the last position: with the earlier ones fixed, it is the one + // whose type ruled the implementation out. + let position = bases.len().saturating_sub(1); + let prefix: Vec = + bases[..position].iter().map(|b| (*b).clone()).collect(); + let accepted: Vec = trait_ + .impls() + .iter() + .filter(|i| i.args.len() == bases.len() && i.args[..position] == prefix[..]) + .filter_map(|i| i.args.get(position).cloned().map(Type::Base)) + .collect(); + let located = self.raise(InferError::NoTraitImpl { + trait_: trait_.to_string(), + position: position as u8, + found: Box::new(Type::Base(bases[position].clone())), + accepted, + at: at(), + }); + self.errors.push(located); + Ok(assoc.map(|_| fresh_var(self.level))) + } + } + } + fn require_sub( &mut self, sub: &Type, @@ -345,18 +415,18 @@ fn check_node_rule(expr: &mut Expr, ctx: &mut CheckCtx) -> Result emit_apply(function, argument, ctx)?, TypedExprNode::BinOp { left, op, right } => { - let scheme = ctx.schemes.binop(*op).clone(); - emit_binop(left, right, &scheme, ctx)? + let sig = ctx.schemes.binop(*op); + emit_binop(left, right, &sig, ctx)? } TypedExprNode::UnaryOp(op, inner) => { - let scheme = ctx.schemes.unary(*op).clone(); - emit_unary(inner, &scheme, ctx)? + let sig = ctx.schemes.unary(*op); + emit_unary(inner, &sig, ctx)? } TypedExprNode::Aggregate { input, kind } => { let scheme = ctx.schemes.aggregate(*kind).clone(); - emit_aggregate(input, &scheme, ctx)? + emit_aggregate(input, &scheme, *kind, ctx)? } // Check never generalizes (`is_generalizable` is `false`), so every diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs index ceda023f..bb6f9c7c 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -20,6 +20,7 @@ use super::emit::emit_node; use super::schemes::OperatorSchemes; use super::typing::Typing; use super::{coalesce_for_error, map_constrain_err}; +use crate::ccl::infer::solver::traits::{Assoc, Trait, TraitObligation}; /// A lexical-scope entry: the binder's polymorphic scheme. /// @@ -275,6 +276,41 @@ impl Typing for InferCtx { self.normalize_annotation(ann) } + fn require_trait( + &mut self, + trait_: Trait, + operands: &[&Type], + assoc: Option, + at: &dyn Fn() -> String, + ) -> Result, LocatedInferError> { + debug_assert_eq!( + operands.len(), + trait_.arity(), + "{trait_} is over {} type(s); an operator wired to it must supply that many", + trait_.arity(), + ); + let positions: Vec = operands.iter().map(|_| self.fresh()).collect(); + // Only a requested association gets a variable for the obligation to settle; + // a pure requirement determines nothing and mints none. + let wanted = assoc.map(|name| (name, self.fresh())); + let obligation = TraitObligation::new(trait_, wanted.clone().into_iter().collect()); + for (i, position) in positions.iter().enumerate() { + obligation.watch(position, i as u8); + } + // A trait whose implementations already agree settles here, before any + // operand is known — the ordinary "all candidates agree" rule reaching its + // condition immediately, not a special case. + obligation + .try_deposit(&mut self.cache) + .map_err(|e| self.raise(map_constrain_err(e, &at())))?; + // Operands flow in as ordinary lower bounds, refinements and all. The + // narrowing hook peels them where the base actually arrives. + for (operand, position) in operands.iter().zip(&positions) { + self.require_sub(operand, position, at)?; + } + Ok(wanted.map(|(_, ty)| ty)) + } + fn require_sub( &mut self, sub: &Type, diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index 71ce52c7..70ff709b 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -12,13 +12,15 @@ use crate::ccl::infer::solver::{PolyScheme, fun, prim}; use crate::ccl::infer::{InferError, LocatedInferError}; use crate::ccl::symbolic::symbolic; use crate::ccl::{ - BaseType, Branch, Expr, Name, ProjKey, Refinement, TransactKey, Type, TypedBinding, - TypedExprNode, V_ABORT, V_COMMIT, WriterSite, + AggregateKind, BaseType, Branch, Expr, Name, ProjKey, Refinement, TransactKey, Type, + TypedBinding, TypedExprNode, V_ABORT, V_COMMIT, WriterSite, }; use super::context::InferCtx; +use super::schemes::{OpSignature, OperatorResult}; use super::typing::{Typing, peel_refinements_outer}; use super::{product, variant_type}; +use crate::ccl::infer::solver::traits::Trait; /// Walk one expression node, emit constraints for it, write its inferred /// `Type` onto `expr.ty`, and return that `Type`. Sub-expressions recurse; @@ -101,18 +103,18 @@ fn emit_node_inner(expr: &mut Expr, ctx: &mut InferCtx) -> Result { - let scheme = ctx.schemes.binop(*op).clone(); - emit_binop(left, right, &scheme, ctx)? + let sig = ctx.schemes.binop(*op); + emit_binop(left, right, &sig, ctx)? } TypedExprNode::UnaryOp(op, inner) => { - let scheme = ctx.schemes.unary(*op).clone(); - emit_unary(inner, &scheme, ctx)? + let sig = ctx.schemes.unary(*op); + emit_unary(inner, &sig, ctx)? } TypedExprNode::Aggregate { input, kind } => { let scheme = ctx.schemes.aggregate(*kind).clone(); - emit_aggregate(input, &scheme, ctx)? + emit_aggregate(input, &scheme, *kind, ctx)? } TypedExprNode::Let { @@ -409,19 +411,14 @@ fn emit_bare_predicate( /// Apply a binary scheme: instantiate, build the expected call shape, /// constrain_subtype. Returns the fresh result variable. /// -/// Operand types enter **stripped of refinements**, and that is load-bearing rather -/// than tidying. An operator scheme relates *base* types — arithmetic is -/// `∀α. α → α → α`, one variable shared across both operands and the result — so any -/// refinement reaching α propagates to the result, claiming the operator preserved -/// it. No binary operator does: `+` on two values that are each `2` produces `4`, not -/// a `2`. The claim is invisible while both operands merely *join* (distinct -/// refinements intersect to none), and wrong the moment they do not — `x + x` keeps -/// `x`'s refinement, because intersecting a set with itself is that set. +/// Only the **monomorphic** binary operators come here — `and`/`or`/… and `++`, +/// whose signatures are fixed (`Bool → Bool → Bool`, `String → String → String`). +/// Nothing is shared between an operand and the result, so a refined operand simply +/// flows into a concrete domain and the refinement stops there; the operands +/// therefore enter verbatim. /// -/// A refinement is a fact about a *value*; carrying it across an operator that -/// computes a new value is exactly the mistake this prevents. (An operator that -/// genuinely refines its result — a future constant fold — states that itself, -/// rather than inheriting it by variable sharing.) +/// The polymorphic operators — arithmetic and comparison — have no scheme at all: +/// their requirement is a trait ([`Typing::require_trait`]). fn apply_binary_scheme( ctx: &mut C, scheme: &PolyScheme, @@ -431,10 +428,7 @@ fn apply_binary_scheme( ) -> Result { let body = ctx.instantiate(scheme); let result = ctx.fresh(); - let expected = fun( - strip_refinements(left), - fun(strip_refinements(right), result.clone()), - ); + let expected = fun(left.clone(), fun(right.clone(), result.clone())); ctx.require_sub(&body, &expected, at)?; Ok(result) } @@ -602,24 +596,59 @@ pub(super) fn emit_apply( ctx.apply(&fn_ty, &arg_ty, argument, &|| "Apply".to_string()) } +/// Record an operator's single obligation and give back its result type. +/// +/// The translation between the two halves of the contract: [`OperatorResult`] is what +/// the *operator* declares, [`Typing::require_trait`] speaks only of associations. +fn require_single_obligation( + ctx: &mut C, + trait_: Trait, + operands: &[&Type], + result: &OperatorResult, + at: &dyn Fn() -> String, +) -> Result { + match result { + OperatorResult::Associated(name) => { + let ty = ctx.require_trait(trait_, operands, Some(*name), at)?; + Ok(ty.expect("an operator asking for an association gets its position back")) + } + OperatorResult::Fixed(base) => { + ctx.require_trait(trait_, operands, None, at)?; + Ok(Type::Base(base.clone())) + } + } +} + pub(super) fn emit_binop( left: &mut Expr, right: &mut Expr, - scheme: &PolyScheme, + sig: &OpSignature, ctx: &mut C, ) -> Result { let left_ty = ctx.subexpr(left)?; let right_ty = ctx.subexpr(right)?; - apply_binary_scheme(ctx, scheme, &left_ty, &right_ty, &|| "BinOp".to_string()) + let at = || "BinOp".to_string(); + match sig { + OpSignature::Scheme(scheme) => apply_binary_scheme(ctx, scheme, &left_ty, &right_ty, &at), + OpSignature::SingleObligation { trait_, result } => { + require_single_obligation(ctx, *trait_, &[&left_ty, &right_ty], result, &at) + } + } } pub(super) fn emit_unary( inner: &mut Expr, - scheme: &PolyScheme, + sig: &OpSignature, ctx: &mut C, ) -> Result { let inner_ty = ctx.subexpr(inner)?; - apply_unary_scheme(ctx, scheme, &inner_ty, &|| "UnaryOp".to_string()) + let at = || "UnaryOp".to_string(); + match sig { + OpSignature::Scheme(scheme) => apply_unary_scheme(ctx, scheme, &inner_ty, &at), + OpSignature::SingleObligation { trait_, result } => { + require_single_obligation(ctx, *trait_, &[&inner_ty], result, &at) + } + } } /// Tuple literal: each element type becomes a positional product field. @@ -857,10 +886,20 @@ pub(super) fn emit_collection_union( pub(super) fn emit_aggregate( input: &mut Expr, scheme: &PolyScheme, + kind: AggregateKind, ctx: &mut C, ) -> Result { let input_ty = ctx.subexpr(input)?; - apply_unary_scheme(ctx, scheme, &input_ty, &|| "Aggregate".to_string()) + let at = || "Aggregate".to_string(); + let result = apply_unary_scheme(ctx, scheme, &input_ty, &at)?; + // `max` returns an element of what it consumes, so the scheme already gives it a + // type; what the scheme cannot say is that the element must be *orderable*. That + // is a pure requirement — `Comparable` associates nothing, and the result type + // stays the scheme's. + if kind == AggregateKind::Max { + ctx.require_trait(Trait::Comparable, &[&result], None, &at)?; + } + Ok(result) } /// Emit/check a `let`, returning the body type. diff --git a/src/ccl/infer/mod.rs b/src/ccl/infer/mod.rs index dae7ff65..ce839593 100644 --- a/src/ccl/infer/mod.rs +++ b/src/ccl/infer/mod.rs @@ -59,8 +59,12 @@ //! //! The [`OperatorSchemes`] registry additionally contains [`PolyScheme`](crate::ccl::infer::solver::PolyScheme)s for //! the handful of operator/projection cases that are inherently polymorphic -//! (`Compare : ∀α. α → α → Bool`, `Max : ∀α γ. (α → γ) → γ`, etc.). Each scheme -//! is `instantiate`d at every use site, minting fresh vars per use. +//! (`Max : ∀α γ. (α → γ) → γ`, etc.). Each scheme is `instantiate`d at every use +//! site, minting fresh vars per use. +//! +//! Arithmetic and comparison have **no** scheme: their requirement is a trait +//! rather than a signature, because a signature could only relate their operands +//! by sharing a variable — see `src/ccl/design/type-inference.md`, "Traits". //! //! Most `Builtin` nodes are introduced post-inference by //! `lambda_elim`/`planning` with their type pre-stamped on the node, and @@ -195,6 +199,18 @@ pub(super) fn map_constrain_err(err: ConstrainError, ctx_label: &str) -> InferEr type_a: Box::new(coalesce_for_error(&lhs)), type_b: Box::new(coalesce_for_error(&rhs)), }, + ConstrainError::NoTraitImpl { + trait_, + position, + found, + accepted, + } => InferError::NoTraitImpl { + trait_: trait_.to_string(), + position, + found: Box::new(found), + accepted: accepted.into_iter().map(Type::Base).collect(), + at: ctx_label.to_string(), + }, ConstrainError::DataDomainMismatch { lhs, rhs } => InferError::TypeMismatch { ctx: format!( "collection domain conflict at {ctx_label} (a collection's domain is \ @@ -352,6 +368,12 @@ pub(crate) fn run( // the node whose rule raised it (`Typing::raise`). emit_node(expr, &mut sub_ctx).map_err(|e| vec![e])?; + // The graph is complete here and nothing has been materialized yet — the one + // point at which eager trait narrowing can be checked against the ground truth + // it was approximating incrementally. Debug-only, and a pure read of the graph. + #[cfg(debug_assertions)] + solver::traits::verify_narrowing_is_complete(|ty| resolve_var_type(ty).ok()); + // Pass 2: resolve each node's inference variables in place into expr.ty, // fill the binder slots that aren't any node's expr.ty (the `Let` binding // slot in particular — this subsumed the former `saturate` pass), and diff --git a/src/ccl/infer/schemes.rs b/src/ccl/infer/schemes.rs index cb387fd5..7ee598be 100644 --- a/src/ccl/infer/schemes.rs +++ b/src/ccl/infer/schemes.rs @@ -5,11 +5,62 @@ use std::collections::BTreeMap; use crate::ccl::FieldKey; +use crate::ccl::infer::solver::traits::{Assoc, Trait}; use crate::ccl::infer::solver::{PolyScheme, fresh_var, fun, prim}; -use crate::ccl::{AggregateKind, BaseType, BinOpKind, Builtin, Level, Type, UnaryOpKind}; +use crate::ccl::{ + AggregateKind, ArithmeticKind, BaseType, BinOpKind, Builtin, CompareKind, Level, Type, + UnaryOpKind, +}; use super::product; +/// Where a trait-typed operator's result type comes from. +/// +/// This is the operator's half of the contract, which is why it lives here beside the +/// signatures rather than with the traits: a trait *associates* a type when that type +/// depends on the types satisfying it, and an operator whose result is the same +/// whatever it accepts states that itself. Keeping the two apart is what stops a +/// constant from being mis-recorded as an associated type. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum OperatorResult { + /// An associated type of the required trait — `+`'s result is `Addable`'s + /// `Output`. + Associated(Assoc), + /// Fixed by the operator regardless of the operand types — `==` yields `Bool` for + /// every pair `Equatable` accepts, which is why `Equatable` associates nothing. + Fixed(BaseType), +} + +/// How an operator states what it requires of its operands. +/// +/// Two shapes, because there are two genuinely different situations: an operator +/// whose operand types are *fixed* is fully described by a signature, and one that is +/// polymorphic in them is not — the only relation a signature can state between two +/// operands is that they share a variable, which also forces every other lattice +/// dimension to agree. +pub(super) enum OpSignature { + /// A fixed signature: `and`, `or`, …, `++`, and `not`. + Scheme(PolyScheme), + /// The operands — **all of them, in order** — are the arguments of exactly one + /// obligation `trait_(𝐴₁, …, 𝐴ₙ)`, and the operator's result is either fixed or + /// one of *that* obligation's associated types. + /// + /// Deliberately narrower than "this operator is trait-typed", and named for the + /// shape rather than the mechanism because it cannot express: more than one + /// obligation; an obligation over a subset of the operands; a separate obligation + /// per operand; or a result drawn from some obligation other than the one + /// constraining the operands. Every operator has this shape today. One that did + /// not would want its own rule in `emit_node` rather than a wider variant here, + /// since a wider variant would have to be interpreted somewhere and that + /// interpretation is what a rule *is*. + SingleObligation { + /// The trait the operands jointly satisfy. + trait_: Trait, + /// Where the operator's own result type comes from. + result: OperatorResult, + }, +} + /// Schemes for operators that lift cleanly to fixed signatures. /// /// Each scheme is built once per [`InferCtx`](super::context::InferCtx); @@ -18,20 +69,16 @@ use super::product; /// whose typing rules require AST-level reasoning (`Apply`, `Lambda`, /// `Let`, `Case`, `List`, …) are handled by per-case rules in /// `emit_node` rather than via this registry. +/// +/// Arithmetic, comparison and negation are absent for a different reason: they are +/// polymorphic in their operands, which no signature can state without also forcing +/// every other lattice dimension to agree. They state a [`Trait`] instead — see +/// [`OpSignature`], which is what a lookup here returns. pub struct OperatorSchemes { - /// `∀α. α → α → α` — both operands agree, result is the same type. - /// Matches today's `infer_binop` Arithmetic rule which only enforces - /// operand agreement, not numeric-ness (operator conversion catches - /// non-numeric arithmetic later). - arithmetic: PolyScheme, - /// `∀α. α → α → Bool`. - compare: PolyScheme, /// `Bool → Bool → Bool`. bool_logic: PolyScheme, /// `String → String → String`. concat: PolyScheme, - /// `Int → Int`. - neg: PolyScheme, /// `Bool → Bool`. not_op: PolyScheme, /// `∀α. (α → Int) → Int` — the full Sum operator type, applied @@ -73,18 +120,6 @@ impl OperatorSchemes { const SCHEME_LEVEL: Level = 0; const BODY_LEVEL: Level = 1; - // Arithmetic: ∀α. α → α → α - let alpha = fresh_var(BODY_LEVEL); - let arithmetic = - PolyScheme::poly(SCHEME_LEVEL, fun(alpha.clone(), fun(alpha.clone(), alpha))); - - // Compare: ∀α. α → α → Bool - let alpha = fresh_var(BODY_LEVEL); - let compare = PolyScheme::poly( - SCHEME_LEVEL, - fun(alpha.clone(), fun(alpha, prim(BaseType::Bool))), - ); - // BoolLogic: Bool → Bool → Bool let bool_logic = PolyScheme::mono(fun( prim(BaseType::Bool), @@ -97,9 +132,6 @@ impl OperatorSchemes { fun(prim(BaseType::String), prim(BaseType::String)), )); - // Neg: Int → Int - let neg = PolyScheme::mono(fun(prim(BaseType::Int), prim(BaseType::Int))); - // Not: Bool → Bool let not_op = PolyScheme::mono(fun(prim(BaseType::Bool), prim(BaseType::Bool))); @@ -173,11 +205,8 @@ impl OperatorSchemes { let get_prev_txn = PolyScheme::poly(SCHEME_LEVEL, fun(product(tup), nu)); Self { - arithmetic, - compare, bool_logic, concat, - neg, not_op, aggregate_sum, aggregate_max, @@ -187,19 +216,57 @@ impl OperatorSchemes { } } - pub(super) fn binop(&self, op: BinOpKind) -> &PolyScheme { + /// How `op`'s signature is stated — a fixed scheme, or a trait requirement. + /// + /// The split is total and exclusive: an operator whose operand types are fixed + /// has a scheme, and one that is polymorphic in them has a trait. There is no + /// operator with both, because a scheme that quantified over its operands could + /// only relate them by *sharing a variable*, which is precisely the claim that + /// is wrong in both polarities (see [`OpSignature::SingleObligation`]). + /// Which typing rule `op` states. + /// + /// The arithmetic and comparison operators are polymorphic in their operands, so + /// they state a trait; `and`/`or`/… and `++` have fixed operand types, so an + /// ordinary scheme says everything there is to say and an obligation would add a + /// mechanism with no choice to make. + /// + /// A scheme is cloned rather than borrowed so the caller's `ctx` borrow is + /// released before the rule takes `ctx` mutably; a [`PolyScheme`] is `Rc`-shaped, + /// so this is cheap. + pub(super) fn binop(&self, op: BinOpKind) -> OpSignature { + let arithmetic = |trait_| OpSignature::SingleObligation { + trait_, + result: OperatorResult::Associated(Assoc::Output), + }; + // Every comparison yields `Bool` whatever operands it accepts, so the result + // is the operator's to state and `Equatable`/`Orderable` associate nothing. + let comparison = |trait_| OpSignature::SingleObligation { + trait_, + result: OperatorResult::Fixed(BaseType::Bool), + }; match op { - BinOpKind::Arithmetic(_) => &self.arithmetic, - BinOpKind::Compare(_) => &self.compare, - BinOpKind::BoolLogic(_) => &self.bool_logic, - BinOpKind::Concat => &self.concat, + BinOpKind::Arithmetic(ArithmeticKind::Add) => arithmetic(Trait::Addable), + BinOpKind::Arithmetic(ArithmeticKind::Sub) => arithmetic(Trait::Subtractable), + BinOpKind::Arithmetic(ArithmeticKind::Mul) => arithmetic(Trait::Multipliable), + BinOpKind::Arithmetic(ArithmeticKind::FloorDiv) => arithmetic(Trait::Divisible), + BinOpKind::Compare(CompareKind::Equals | CompareKind::NotEquals) => { + comparison(Trait::Equatable) + } + BinOpKind::Compare(_) => comparison(Trait::Orderable), + BinOpKind::BoolLogic(_) => OpSignature::Scheme(self.bool_logic.clone()), + BinOpKind::Concat => OpSignature::Scheme(self.concat.clone()), } } - pub(super) fn unary(&self, op: UnaryOpKind) -> &PolyScheme { + /// See [`Self::binop`] — the same split. `not` is genuinely monomorphic + /// (`Bool → Bool`), so it keeps a scheme. + pub(super) fn unary(&self, op: UnaryOpKind) -> OpSignature { match op { - UnaryOpKind::Neg => &self.neg, - UnaryOpKind::Not => &self.not_op, + UnaryOpKind::Neg => OpSignature::SingleObligation { + trait_: Trait::Negatable, + result: OperatorResult::Associated(Assoc::Output), + }, + UnaryOpKind::Not => OpSignature::Scheme(self.not_op.clone()), } } @@ -235,7 +302,6 @@ impl Default for OperatorSchemes { mod tests { use super::super::test_helpers::*; use super::OperatorSchemes; - use crate::ccl::infer::int_lit_ty; use crate::ccl::{AggregateKind, Builtin, Type, TypedBinding, TypedExpr, TypedExprNode}; /// `GetPrevTxn`'s scheme instantiates to @@ -300,29 +366,25 @@ mod tests { ); } - /// TRIPWIRE — documents a known soundness gap, NOT desired behavior. + /// `max` is defined at eval only for orderable bases (`Int`/`UInt`/`String` — + /// see merge/identity in `ccl/mod.rs`), and its scheme `∀α γ. (α ⤇ γ) ⇒ γ` + /// cannot say so: `γ` is the codomain it *returns*, so nothing about it is + /// constrained. /// - /// `Max` has scheme `∀α γ. (α ⇒ γ) ⇒ γ` (see `aggregate_max`), so its - /// codomain `γ` is wholly unconstrained and it type-checks over *any* - /// codomain. But `Max` is only *defined* at eval for orderable base types - /// (`Int`/`UInt`/`String` — see merge/identity in `ccl/mod.rs`). So `max` - /// over a function with a tuple codomain type-checks and infers - /// `Tuple([Int, Int])`, even though it has no defined runtime behavior. + /// `Comparable(γ)` says it — a **pure requirement**, associating nothing, since + /// the scheme already supplies the result type. A codomain the program never + /// determines is still accepted here, as an unresolved variable rather than a + /// missing implementation; that is the ordinary limit of narrowing, not a gap + /// specific to `max`. /// - /// `Max` *should* require an orderable codomain. The correct long-term fix - /// is a first-class comparability bound, which arrives with traits — there - /// is no value in a stopgap validation now. When that lands, inference will - /// start rejecting this program and this test will fail loudly; whoever - /// lands traits should flip it to assert rejection. - /// - /// Tracked by `type-checker-traits-comparability` (P3) in the project vault. + /// Closes `type-checker-traits-comparability` (P3) in the project vault. #[test] - fn max_over_non_orderable_codomain_is_unsoundly_accepted() { + fn max_over_a_non_orderable_codomain_is_rejected() { // Aggregate { input: λx → (1, 2), kind: Max }. The input stands in for a // data collection of tuples (what `max` really consumes), so it carries // the `data_fun` provenance stamp lowering puts on a collection — without // it, the bare lambda is a `Compute` capability and `max`'s `Data` demand - // rejects it on *kind* before the codomain-orderability gap under test. + // rejects it on *kind* before the codomain orderability under test. let lam = TypedExpr::new(TypedExprNode::Lambda { param: TypedBinding { name: "x".into(), @@ -336,8 +398,14 @@ mod tests { }) .with_user_annotation(Type::data_fun(Type::Hole, Type::Hole)); let mut e = TypedExpr::aggregate(lam, AggregateKind::Max); - let ty = run_inference(&mut e).expect("inference succeeds (the bug under test)"); - // Buggy current behavior: the non-orderable tuple codomain is accepted. - assert_eq!(ty, Type::Tuple(vec![int_lit_ty(1), int_lit_ty(2)])); + let errs = run_inference(&mut e).expect_err("a tuple codomain is not orderable"); + assert!( + errs.iter().any(|e| matches!( + e, + crate::ccl::infer::InferError::NoTraitImpl { trait_, .. } + if trait_ == "Comparable" + )), + "expected NoTraitImpl for Comparable, got {errs:?}" + ); } } diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index 1494de1e..7a93e8bb 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -21,8 +21,9 @@ use smol_str::SmolStr; use crate::ccl::subst::Subst; use crate::ccl::ty::{FunKind, FunKindVar}; -use crate::ccl::{Bound, HistoryKind, InferVar, InferVarId, Level, Refinement, Type}; +use crate::ccl::{BaseType, Bound, HistoryKind, InferVar, InferVarId, Level, Refinement, Type}; +use super::traits::{Trait, link_watches, notify_lower}; use super::type_level; use crate::ccl::FieldKey; use crate::ccl::ccl_utils::strip_refinements; @@ -108,6 +109,24 @@ pub enum ConstrainError { /// The domain demanded at the position. rhs: Type, }, + /// An operand's type ruled out the last implementation of a trait an operator + /// requires — `1 > "a"`, or `\x -> x + 1` applied to a string. + /// + /// Raised from the bound-recording arm that delivered the offending type, so it + /// fires the moment the program states the conflict rather than at a later phase + /// that goes looking for it. + NoTraitImpl { + /// The trait with no implementation left. + trait_: Trait, + /// The operand position whose type ruled the last one out. + position: u8, + /// The type that arrived there — a base no implementation accepts, or a + /// shape that is not a base at all. + found: Type, + /// What that position could still have accepted, given everything already + /// known about the other operand. + accepted: Vec, + }, } /// Cache of in-progress subtyping checks. Breaks cycles introduced through @@ -623,10 +642,12 @@ fn constrain_go_impl( } // Implicit deref (read): a `Mut` handle meeting any non-`Mut` demand — // concrete OR an inference variable — reads its value. This MUST precede - // the `Infer` arms below: `+`/`<` etc. are polymorphic (`∀α. α → α → α`), - // so `cnt + 1` emits `Mut(Int, D) <: ?α`; dereffing here flows `Int` onto - // `?α`, whereas the `(_, Infer)` arm would record the handle itself as a - // lower bound and coalesce `?α` to a `Mut`. + // the `Infer` arms below: an operator constrains its operand against a fresh + // variable (`cnt + 1` emits `Mut(Int, D) <: ?α` for `Addable`'s first operand + // position), and dereffing here flows `Int` onto `?α` — where the narrowing + // hook can read a base off it. The `(_, Infer)` arm would instead record the + // handle itself as a lower bound, offering the obligation nothing and + // coalescing `?α` to a `Mut`. ( Type::History { value, @@ -648,6 +669,12 @@ fn constrain_go_impl( .push(Bound::edge(sl.clone(), rhs.clone(), sr.clone())); Rc::clone(s.lower()) }; + // A var-var edge carries the watch downward (see `link_watches`); the + // closure below only re-offers `lv`'s lowers to `rhs` when the levels let + // this arm run, which is precisely what a `let` RHS breaks. + if let Type::Infer(rv) = rhs { + link_watches(lv, rv, cache)?; + } for low in lows.iter() { let (tau_l, tau_u) = bridge_holder_gap(&low.self_subst, sl); constrain_go( @@ -676,6 +703,19 @@ fn constrain_go_impl( .push(Bound::edge(sr.clone(), lhs.clone(), sl.clone())); Rc::clone(s.upper()) }; + // Deliver the contribution to any trait obligation this variable is an + // operand of. This arm is the *only* hook site needed: an operand type + // reaches an obligation as a lower bound, and the closure below plus its + // dual in the upper arm mean a bound reaching a variable that flows into + // a watched one is re-constrained *directly against* the watched + // variable — so both arrival orders (edge-then-bound, bound-then-edge) + // land the concrete type here. The one path that bypasses the closure is + // `extrude`, which seeds a proxy's bounds by direct writes; it copies the + // watch list instead. + notify_lower(rv, lhs, cache)?; + if let Type::Infer(lv) = lhs { + link_watches(lv, rv, cache)?; + } for up in ups.iter() { let (tau_l, tau_u) = bridge_holder_gap(sr, &up.self_subst); constrain_go( @@ -927,6 +967,26 @@ fn wrap_refinements(base: &Type, refs: &[&Refinement]) -> Type { }) } +/// Give an extrusion proxy the same trait obligations as the variable it +/// approximates. +/// +/// Extrusion seeds a proxy's bounds by **direct writes** rather than through +/// `constrain_go`, so it is the one path where a concrete type can reach a watched +/// variable's stand-in without passing the narrowing hook. A bound recorded on the +/// proxy afterwards would otherwise never reach the obligation, and the operand's +/// type would silently fail to narrow it. +/// +/// Copied unconditionally, at both polarities. The proxy and the original stay +/// linked, so a fact can legitimately arrive at both — but narrowing is an +/// idempotent set intersection, which makes the duplicate delivery a no-op rather +/// than something to reason about per polarity. +fn copy_watches(from: &Rc, to: &Rc) { + let watches = from.watches.borrow().clone(); + if !watches.is_empty() { + to.watches.borrow_mut().extend(watches); + } +} + /// Lift `ty` so that all its variables live at level ≤ `target_level`. /// /// When a constraint crosses level boundaries (e.g. an outer-scope variable @@ -1003,6 +1063,7 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac // level, linked to the original by the appropriate bound. let nvs = InferVar::fresh(target_level); cache.insert((tv.uid, pol), Rc::clone(&nvs)); + copy_watches(tv, &nvs); // Each branch snapshots only the list it does *not* push to — the // positive one seeds from `lower` and writes `upper`, the negative @@ -1105,6 +1166,7 @@ fn extrude_invariant(ty: &Type, target_level: Level, cache: &mut ExtrudeCache) - let has_neg_link = cached_neg.as_ref().is_some_and(|n| Rc::ptr_eq(n, &nvs)); cache.insert((tv.uid, true), Rc::clone(&nvs)); cache.insert((tv.uid, false), Rc::clone(&nvs)); + copy_watches(tv, &nvs); // Snapshot the original's bounds, excluding any edge that already // points at this proxy (a polar extrusion pushed one such link into diff --git a/src/ccl/infer/solver/mod.rs b/src/ccl/infer/solver/mod.rs index 21824f0b..a6533f4c 100644 --- a/src/ccl/infer/solver/mod.rs +++ b/src/ccl/infer/solver/mod.rs @@ -46,6 +46,7 @@ pub mod constrain; pub mod scheme; pub mod simplify_type; pub mod spec_key; +pub mod traits; // Re-export every symbol that external modules reach through the // `crate::ccl::infer::solver::…` path (chiefly the inference engine), so the diff --git a/src/ccl/infer/solver/scheme.rs b/src/ccl/infer/solver/scheme.rs index e8fbc1fe..f0ca3057 100644 --- a/src/ccl/infer/solver/scheme.rs +++ b/src/ccl/infer/solver/scheme.rs @@ -9,6 +9,7 @@ use std::collections::HashMap; use std::rc::Rc; +use super::traits::{TraitObligation, TraitObligationId}; use crate::ccl::subst::Subst; use crate::ccl::ty::{FunKind, FunKindVar, FunKindVarId}; use crate::ccl::{Bound, InferVar, InferVarId, Level, Refinement, Type, TypedExpr}; @@ -27,7 +28,7 @@ use crate::ccl::{Bound, InferVar, InferVarId, Level, Refinement, Type, TypedExpr /// # Usage /// /// Two sources of schemes: (1) operator/projection signatures that are -/// inherently polymorphic (`Compare : ∀α. α → α → Bool`, +/// inherently polymorphic (`Max : ∀α γ. (α ⤇ γ) ⇒ γ`, /// `Proj(Index n) : ∀α. {n: α, …} → α`, etc.), built once in /// `OperatorSchemes`; and (2) let-generalization — a multi-use function /// binding is generalized into a `PolyScheme` at its binding level @@ -90,6 +91,13 @@ pub struct FreshenCache { /// `DomainJoinConflict`. Freshening mints one `κ'` per original `κ` (bounds /// copied so def-intrinsic forcing survives), consistently within a copy. pub kind_vars: HashMap>, + /// Original trait obligation → its per-instantiation copy, for the same reason + /// as [`kind_vars`](Self::kind_vars): a generalized function's operator + /// requirements are quantified along with the variables they constrain, so each + /// use discharges *its own* copy. `λ 𝑥 → 𝑥 + 1` generalizes to + /// `∀A O. (A : Addable(A, Int)) ⇒ A → O`; sharing one obligation across uses + /// would let a `String` use narrow the `Int` use's candidate set to nothing. + pub obligations: HashMap>, } impl FreshenCache { @@ -352,11 +360,54 @@ pub fn freshen_above( s.set_lower(new_lows); s.set_upper(new_ups); } + freshen_watches(lim, tv, &v, target, cache); Type::Infer(v) } } } +/// Copy `tv`'s trait obligations onto its freshened counterpart `v`. +/// +/// Runs *after* the bounds write-back, so an obligation reached through a bound has +/// already had its variables freshened into the cache and the copy's watches line up +/// with the copy's variables. +/// +/// The clone is inserted into the cache **before** its associated positions are +/// freshened. +/// The obligation graph is cyclic — an obligation holds its output type, which holds +/// a variable, which watches the obligation — so freshening the output re-enters +/// here, and a clone that is not yet reachable would be minted twice: once per +/// operand, each watching a different copy, and neither ever narrowed by both +/// operands. +fn freshen_watches( + lim: Level, + tv: &Rc, + v: &Rc, + target: FreshenLevel, + cache: &mut FreshenCache, +) { + let watches = tv.watches.borrow().clone(); + for (obligation, pos) in watches { + if let Some(existing) = cache.obligations.get(&obligation.uid) { + existing.watch(&Type::Infer(Rc::clone(v)), pos); + continue; + } + // Phase 1: a copy carrying the original's candidate set, with the output + // position still pointing at the definition's — enough to be reachable. + let copy = TraitObligation::new_from(&obligation); + cache.obligations.insert(obligation.uid, Rc::clone(©)); + copy.watch(&Type::Infer(Rc::clone(v)), pos); + // Phase 2: now that re-entry finds the copy, freshen the output. + copy.set_assoc_types( + obligation + .assoc_types() + .iter() + .map(|ty| freshen_above(lim, ty, target, cache)) + .collect(), + ); + } +} + /// Freshen a refinement's predicate: clone the (immutable) predicate term, /// freshen its type slots through `cache`, and install a fresh `Rc`. See /// [`freshen_above`]'s `Refinement` arm. diff --git a/src/ccl/infer/solver/traits.rs b/src/ccl/infer/solver/traits.rs new file mode 100644 index 00000000..ccce4eb6 --- /dev/null +++ b/src/ccl/infer/solver/traits.rs @@ -0,0 +1,959 @@ +//! Traits: what a polymorphic operator requires of its operands, and what that +//! determines about its result. +//! +//! # Vocabulary +//! +//! - A **trait** is a named requirement a type may satisfy — `Addable`, `Orderable`. +//! It is **not a type**: nothing here adds a [`Type`] variant, a lattice point or a +//! subtyping edge, and the type grammar and `constrain_go`'s rules are untouched. +//! - An **implementation** ([`TraitImpl`]) is one row of a trait's table: the types it +//! accepts, and the types it associates with them. +//! - An **associated type** ([`Assoc`]) is a type a trait *names* — `Output`, the type +//! an arithmetic operator's result takes. A trait is a requirement rather than a +//! function, so it associates any number, **including none**. A type is associated +//! only when it *depends* on the types satisfying the trait: a comparison's `Bool` is +//! the same for every pair `Equatable` accepts, so it belongs to the operator's +//! signature (`OperatorResult::Fixed`, in `src/ccl/infer/schemes.rs`) and +//! `Equatable` associates nothing. +//! - An **obligation** ([`TraitObligation`]) is one recorded instance of a trait at +//! specific type positions: one **operand position** per argument the trait takes, +//! and one **associated position** per type it names. It is a single claim with two +//! halves, and neither alone is "the obligation": *the operand positions are types +//! some implementation accepts*, **and** *each associated position is what that +//! implementation associates*. Every position is an ordinary inference variable, +//! unrelated to the others. (`Addable(𝐴, 𝐵)` with `Output` at `𝑂` is the shape to +//! picture, but the arity and the association count are both the trait's.) +//! - A **watch** is an obligation's attachment to an operand variable, which is how a +//! bound landing anywhere in the program reaches it. +//! +//! An operator's signature is therefore `𝐴₁ → … → 𝐴ₙ → 𝑅` plus the obligation, for the +//! trait's arity `𝑛`, where `𝑅` is either one of the associated positions or a type +//! the operator fixes — which operator states which is `schemes.rs`'s business, not +//! this module's. Because an associated position is an +//! ordinary variable rather than a marker standing for a computation, information +//! flows *backwards* through an operator's result like any other type — which is what +//! lets a function be typechecked without consulting its call sites. +//! +//! # Refinements are transparent +//! +//! `{𝑇 | 𝑝}` satisfies a trait exactly when `𝑇` does, by construction rather than by +//! a stripping step: satisfaction is judged on each bound contribution as it arrives, +//! with refinements peeled at that moment — when the base actually exists. +//! +//! # Discharge is incremental +//! +//! An obligation is a monotone fact discharged as the graph fills in, the shape +//! [`FunKindVar`](crate::ccl::ty::FunKindVar) already uses for kinds; no phase runs +//! "once everything is known". Each operand position carries a **candidate set** of +//! implementations that only ever shrinks ([`TraitObligation::narrow`]), and each +//! associated type is deposited on its position as an ordinary lower bound as soon as +//! every surviving candidate agrees on it ([`TraitObligation::try_deposit`]). +//! +//! # What an obligation determines, and what it leaves alone +//! +//! The deposit rule is *whatever every surviving implementation agrees on*, and it is +//! applied to the **associated positions only**. Nothing is ever deposited onto an +//! operand. +//! +//! The asymmetry is not soundness — with one candidate left, its operand types are +//! implied exactly as its associated types are. It is that the obligation is an +//! associated position's **only** source of information and never an operand's: an +//! associated position is a fresh variable nothing else constrains from below, while +//! an operand always has the program's own `operandᵢ <: 𝐴ᵢ` edge. Determining an operand from the table would be recovering +//! information the program was supposed to supply, which hides an under-connected +//! lowering instead of fixing it. +//! +//! How much gets determined is therefore a property of the table, and shrinks as the +//! table grows — **for an associated type too**. Today `λ 𝑥 → 𝑥 + 1` has result `Int`, +//! because `Int` in the second position leaves only `(Int, Int) ⇝ Int`. Adding +//! `Addable(Float, Int) ⇝ Float` would leave two candidates whose outputs disagree, +//! and the result would become as open as the parameter already is. That is the type +//! honestly tracking a language that has become more permissive, and it is why the +//! deposit waits for *agreement* rather than firing on a unique candidate. + +use std::cell::{Cell, RefCell}; +use std::fmt; +use std::rc::Rc; +use std::sync::atomic::{AtomicU32, Ordering}; + +use crate::ccl::{BaseType, InferVar, Type}; + +use super::constrain::{ConstrainCache, ConstrainError, constrain_subtype}; + +/// A trait: a named requirement on types, together with any types it associates +/// with them. +/// +/// Closed and built-in. The set is the operators the language has, not a user +/// vocabulary — but the implementations are already *data* ([`Trait::impls`]), so a +/// user-declared trait is a table extension rather than a new mechanism. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum Trait { + /// `+` over `(𝐴, 𝐵)`, associating `Output`. The `(String, String) ⇝ String` row is + /// why surface `+` on strings types through arithmetic; `simplify` rewrites it to + /// `Concat` later. + Addable, + /// `-` over `(𝐴, 𝐵)`, associating `Output`. + Subtractable, + /// `*` over `(𝐴, 𝐵)`, associating `Output`. + Multipliable, + /// `//` over `(𝐴, 𝐵)`, associating `Output`. + Divisible, + /// `==` and `!=` over `(𝐴, 𝐵)`, associating **nothing** — the `Bool` is the + /// operator's, identical for every pair the trait accepts. + Equatable, + /// `<`, `<=`, `>`, `>=` over `(𝐴, 𝐵)`, associating **nothing**, as [`Equatable`]. + /// + /// [`Equatable`]: Trait::Equatable + Orderable, + /// Unary `-` over `(𝐴)`, associating `Output`. + Negatable, + /// `max`'s codomain, over `(𝐴)`, associating **nothing** — a pure requirement, + /// since the aggregate's scheme already returns an element of what it consumes. + Comparable, +} + +/// A type a trait associates with the types satisfying it — Rust's *associated +/// type*. +/// +/// A trait is a requirement, not a function, so an associated type is something it +/// happens to name rather than something it must produce. A trait may associate any +/// number, **including none**: a bare requirement (`Orderable(γ)` on an aggregate's +/// codomain) associates nothing, and saying so is better than manufacturing an +/// output no one reads. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)] +pub enum Assoc { + /// The type an operator's result takes. + Output, +} + +/// One implementation: the types it accepts, and what it associates with them. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct TraitImpl { + /// The accepted types, positionally. A slice rather than a fixed array because + /// arity is the trait's business — every operator trait is binary today, and an + /// `Orderable` over one type is the obvious next one. + pub args: &'static [BaseType], + /// The types this implementation associates, by name. Empty for a trait that is + /// a pure requirement. + pub assoc: &'static [(Assoc, BaseType)], +} + +impl TraitImpl { + /// The type this implementation associates with `name`, if any. + pub fn assoc_ty(&self, name: Assoc) -> Option<&BaseType> { + self.assoc.iter().find(|(n, _)| *n == name).map(|(_, t)| t) + } +} + +/// `(Int, Int) ⇝ Int` and `(UInt, UInt) ⇝ UInt` — the numeric arithmetic rows every +/// arithmetic trait shares. +const NUMERIC: &[TraitImpl] = &[ + TraitImpl { + args: &[BaseType::Int, BaseType::Int], + assoc: &[(Assoc::Output, BaseType::Int)], + }, + TraitImpl { + args: &[BaseType::UInt, BaseType::UInt], + assoc: &[(Assoc::Output, BaseType::UInt)], + }, +]; + +/// The numeric rows plus `(String, String) ⇝ String`. +const NUMERIC_OR_STRING: &[TraitImpl] = &[ + TraitImpl { + args: &[BaseType::Int, BaseType::Int], + assoc: &[(Assoc::Output, BaseType::Int)], + }, + TraitImpl { + args: &[BaseType::UInt, BaseType::UInt], + assoc: &[(Assoc::Output, BaseType::UInt)], + }, + TraitImpl { + args: &[BaseType::String, BaseType::String], + assoc: &[(Assoc::Output, BaseType::String)], + }, +]; + +/// Homogeneous comparison over every base the interpreter can compare. +/// +/// **Associates nothing.** A comparison's `Bool` is fixed by the *operator's* +/// signature, not computed by the trait: it is the same `Bool` for every pair of +/// types the trait accepts, so it carries no information about them. Recording it as +/// an associated type would state that the trait determines something it does not — +/// the same mistake as an operator inheriting an operand's refinement, one level up. +const COMPARABLE: &[TraitImpl] = &[ + TraitImpl { + args: &[BaseType::Int, BaseType::Int], + assoc: &[], + }, + TraitImpl { + args: &[BaseType::UInt, BaseType::UInt], + assoc: &[], + }, + TraitImpl { + args: &[BaseType::String, BaseType::String], + assoc: &[], + }, + TraitImpl { + args: &[BaseType::Bool, BaseType::Bool], + assoc: &[], + }, +]; + +/// Unary negation. One operand, and an `Output` that genuinely depends on it — the +/// arity and association shape `Addable` and `Equatable` between them do not have. +const NEGATABLE: &[TraitImpl] = &[TraitImpl { + args: &[BaseType::Int], + assoc: &[(Assoc::Output, BaseType::Int)], +}]; + +/// The bases an aggregate can order, matching `max`'s merge in `ccl/mod.rs`. Unary +/// and associating nothing — the fourth shape, and a pure requirement. +const ORDERED: &[TraitImpl] = &[ + TraitImpl { + args: &[BaseType::Int], + assoc: &[], + }, + TraitImpl { + args: &[BaseType::UInt], + assoc: &[], + }, + TraitImpl { + args: &[BaseType::String], + assoc: &[], + }, +]; + +impl Trait { + /// This trait's implementations. + /// + /// Every table is **homogeneous** — both operand positions accept the same base + /// — which is a fact about today's rows, not about the mechanism: nothing in + /// narrowing or deposit assumes it. The tables mirror + /// `interpreter::binop::apply_binop_column`, so a program this accepts is one + /// the interpreter can actually run. In particular there is no `Unit` row (the + /// interpreter cannot compare units) and no cross-base row, since `Int` and + /// `UInt` are unrelated leaves in the lattice and never join. + pub fn impls(self) -> &'static [TraitImpl] { + match self { + Trait::Addable => NUMERIC_OR_STRING, + Trait::Subtractable | Trait::Multipliable | Trait::Divisible => NUMERIC, + Trait::Equatable | Trait::Orderable => COMPARABLE, + Trait::Negatable => NEGATABLE, + Trait::Comparable => ORDERED, + } + } + + /// How many types this trait is over. + /// + /// Derived from the table rather than declared beside it, so the shape each + /// variant's doc states cannot drift from the rows that implement it — + /// `every_trait_has_a_consistent_shape` pins that every row agrees. + pub fn arity(self) -> usize { + self.rows_agree_on().0 + } + + /// The types this trait associates, by name. Empty for a pure requirement. + pub fn assocs(self) -> Vec { + self.rows_agree_on().1 + } + + /// The `(arity, associated names)` its first row declares. + fn rows_agree_on(self) -> (usize, Vec) { + let first = self + .impls() + .first() + .expect("every trait has at least one implementation"); + ( + first.args.len(), + first.assoc.iter().map(|(n, _)| *n).collect(), + ) + } + + /// The trait's name, for diagnostics. + pub fn name(self) -> &'static str { + match self { + Trait::Addable => "Addable", + Trait::Subtractable => "Subtractable", + Trait::Multipliable => "Multipliable", + Trait::Divisible => "Divisible", + Trait::Equatable => "Equatable", + Trait::Orderable => "Orderable", + Trait::Negatable => "Negatable", + Trait::Comparable => "Comparable", + } + } +} + +impl fmt::Display for Trait { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str(self.name()) + } +} + +/// Stable identity of a [`TraitObligation`]. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)] +pub struct TraitObligationId(pub(crate) u32); + +static OBLIGATION_COUNTER: AtomicU32 = AtomicU32::new(0); + +/// One recorded instance of a trait at specific type positions, carrying both halves +/// of the claim: that the operand positions are types some implementation accepts, and +/// that each associated position is what that implementation associates. Arity and +/// association count are the trait's — `Addable(𝐴, 𝐵)` with `Output` at `𝑂` is one +/// shape, `Negatable(𝐴)` with `Output` and `Equatable(𝐴, 𝐵)` with none are the others. +/// See this module's *Vocabulary*. +/// +/// Held by [`Rc`] and *watched* by each operand variable ([`TraitObligation::watch`]), +/// so a bound arriving anywhere in the program reaches it without any pass having to +/// go looking for obligations. +/// +/// The operand *types* are deliberately not stored: narrowing is push-based — the +/// contribution arrives at the watch — so holding them would buy nothing and only +/// add `Rc` edges for the arena to sever. +pub struct TraitObligation { + /// Stable, globally-unique identity. Freshening clones an obligation once per + /// instantiation and keys the copy on this. + pub uid: TraitObligationId, + /// The trait being required. + pub trait_: Trait, + /// The implementations still consistent with everything seen so far. + /// Monotonically shrinking; empty is unrepresentable (it is the error). + candidates: RefCell>, + /// The type positions this obligation associates, one per name the trait + /// declares. Empty for a trait that is a pure requirement — the mechanism then + /// still narrows and still rejects, it simply determines nothing. + assoc: Vec, +} + +/// One associated position of an obligation: the name, the type standing in for it, +/// and whether that type has been settled yet. +struct AssocPosition { + name: Assoc, + /// A `RefCell` because freshening rewrites it to the instantiation's own variable + /// after the clone exists — the obligation graph is cyclic (obligation → position + /// → variable → watches → obligation), so the clone has to be reachable before + /// its positions can be built. + ty: RefCell, + /// Set before constraining, so a re-entrant narrow cannot deposit twice. + deposited: Cell, +} + +impl TraitObligation { + /// Record an instance of `trait_` whose associated names stand at the given type + /// positions, with every implementation still a candidate. + pub fn new(trait_: Trait, assoc: Vec<(Assoc, Type)>) -> Rc { + Rc::new(TraitObligation { + uid: TraitObligationId(OBLIGATION_COUNTER.fetch_add(1, Ordering::Relaxed)), + trait_, + candidates: RefCell::new(trait_.impls().to_vec()), + assoc: assoc + .into_iter() + .map(|(name, ty)| AssocPosition { + name, + ty: RefCell::new(ty), + deposited: Cell::new(false), + }) + .collect(), + }) + } + + /// A per-instantiation copy of `original`, for freshening. + /// + /// The candidate set is copied **as narrowed**, not reset to the full table: it + /// records what the *definition* already determined (`λ 𝑥 → 𝑥 + 1` has ruled out + /// every row whose second operand is not `Int`), which every instantiation + /// inherits. Narrowing past that point is what differs per use, and that is + /// exactly what the copy makes independent. + /// + /// The associated positions are deliberately left pointing at the original's; the + /// caller rewrites them once the copy is reachable (see + /// [`set_assoc_types`](Self::set_assoc_types)). Their deposited flags copy too — a + /// deposit already made rides the freshened bound onto the copy, so redoing it + /// would record the same fact twice. + pub(super) fn new_from(original: &Rc) -> Rc { + Rc::new(TraitObligation { + uid: TraitObligationId(OBLIGATION_COUNTER.fetch_add(1, Ordering::Relaxed)), + trait_: original.trait_, + candidates: RefCell::new(original.candidates()), + assoc: original + .assoc + .iter() + .map(|p| AssocPosition { + name: p.name, + ty: RefCell::new(p.ty.borrow().clone()), + deposited: Cell::new(p.deposited.get()), + }) + .collect(), + }) + } + + /// Watch `ty` at operand position `pos`, so every lower bound landing there + /// narrows this obligation. + /// + /// `ty` must be an inference variable: an operator's rule mints one per operand + /// precisely so the operand's *own* type flows in as a bound rather than being + /// read at emission, when it is not yet known. + pub fn watch(self: &Rc, ty: &Type, pos: u8) { + let Type::Infer(v) = ty else { + debug_assert!( + false, + "a trait obligation watches an inference variable, not {ty:?} — an \ + operator's rule mints a fresh variable per operand", + ); + return; + }; + v.watches.borrow_mut().push((Rc::clone(self), pos)); + #[cfg(debug_assertions)] + register_watch(self, pos, ty); + } + + /// The candidates still live, for diagnostics and tests. + pub fn candidates(&self) -> Vec { + self.candidates.borrow().clone() + } + + /// The type standing at each associated position, in declaration order. + /// Freshening reads these, rewrites them, and writes them back with + /// [`set_assoc_types`](Self::set_assoc_types). + pub(super) fn assoc_types(&self) -> Vec { + self.assoc.iter().map(|p| p.ty.borrow().clone()).collect() + } + + /// Rewrite the associated positions. Freshening's second phase; see + /// [`AssocPosition::ty`]. + pub(super) fn set_assoc_types(&self, tys: Vec) { + debug_assert_eq!( + tys.len(), + self.assoc.len(), + "an obligation's associated positions are fixed at construction", + ); + for (position, ty) in self.assoc.iter().zip(tys) { + *position.ty.borrow_mut() = ty; + } + } + + /// Reject a shape no implementation can accept at position `pos`. + /// + /// Distinct from [`narrow`](Self::narrow) failing: nothing is *ruled out* here, + /// because there was never a candidate to rule out. The contribution is simply + /// outside the vocabulary the trait is defined over. + fn reject(self: &Rc, pos: u8, found: &Type) -> Result<(), ConstrainError> { + Err(ConstrainError::NoTraitImpl { + trait_: self.trait_, + position: pos, + found: found.clone(), + accepted: self + .candidates + .borrow() + .iter() + .filter_map(|i| i.args.get(pos as usize).cloned()) + .collect(), + }) + } + + /// Restrict position `pos` to implementations accepting `base`, then deposit the + /// output if that settles it. + /// + /// Monotone and idempotent: narrowing by a base already consistent with every + /// candidate is a no-op, which is what makes double delivery (the same fact + /// reaching a variable and its extrusion proxy) harmless. + fn narrow( + self: &Rc, + pos: u8, + base: &BaseType, + cache: &mut ConstrainCache, + ) -> Result<(), ConstrainError> { + { + let mut candidates = self.candidates.borrow_mut(); + let accepted: Vec = candidates + .iter() + .filter_map(|i| i.args.get(pos as usize).cloned()) + .collect(); + // A candidate with no such position is one this trait's arity does not + // reach; it cannot accept the contribution, so it drops out too. + candidates.retain(|i| i.args.get(pos as usize) == Some(base)); + if candidates.is_empty() { + return Err(ConstrainError::NoTraitImpl { + trait_: self.trait_, + position: pos, + found: Type::Base(base.clone()), + accepted, + }); + } + } + self.try_deposit(cache) + } + + /// Deposit the output type on `𝑂` if every surviving candidate agrees on it. + /// + /// An ordinary `constrain_subtype`, run **inline**: narrowing *reads nothing* off + /// the bound graph — it consumes exactly the contribution being recorded — so + /// there is no stale-read hazard and no reason to defer the write to a later + /// phase. The [`Cell`] is set before constraining, so a re-entrant narrow reached + /// through this very edge cannot deposit twice. + pub fn try_deposit(self: &Rc, cache: &mut ConstrainCache) -> Result<(), ConstrainError> { + for position in &self.assoc { + if position.deposited.get() { + continue; + } + let Some(settled) = self.agreed_assoc(position.name) else { + continue; + }; + position.deposited.set(true); + let target = position.ty.borrow().clone(); + constrain_subtype(&Type::Base(settled), &target, cache)?; + } + Ok(()) + } + + /// The type every surviving implementation associates with `name`, or `None` if + /// they disagree — the condition a deposit waits on. + fn agreed_assoc(&self, name: Assoc) -> Option { + let candidates = self.candidates.borrow(); + let (first, rest) = candidates + .split_first() + .expect("a candidate set is never empty: emptying it is the error"); + let settled = first.assoc_ty(name)?; + rest.iter() + .all(|i| i.assoc_ty(name) == Some(settled)) + .then(|| settled.clone()) + } +} + +// Identity-based, mirroring `InferVar`/`FunKindVar`: borrow-free, so it never +// inspects the (mutable, potentially borrowed) candidate set. +impl PartialEq for TraitObligation { + fn eq(&self, other: &Self) -> bool { + self.uid == other.uid + } +} +impl Eq for TraitObligation {} +impl std::hash::Hash for TraitObligation { + fn hash(&self, state: &mut H) { + self.uid.hash(state); + } +} +impl fmt::Debug for TraitObligation { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}#{}", self.trait_, self.uid.0) + } +} + +#[cfg(debug_assertions)] +thread_local! { + /// Every watch established during this inference run, as `(obligation, position, + /// operand type)` — the audit trail [`verify_narrowing_is_complete`] checks. + /// + /// Debug-only, and deliberately *not* a field on [`TraitObligation`]: narrowing + /// is push-based, so production code never needs an operand's type, and keeping + /// it out of the obligation means the release build carries neither the `Rc` + /// edges nor the temptation to read a type where a bound should have been + /// delivered. + static WATCH_LOG: RefCell, u8, Type)>> = + const { RefCell::new(Vec::new()) }; +} + +#[cfg(debug_assertions)] +fn register_watch(obligation: &Rc, pos: u8, ty: &Type) { + WATCH_LOG.with(|log| { + log.borrow_mut() + .push((Rc::clone(obligation), pos, ty.clone())) + }); +} + +/// Discard the audit trail. Called when an inference run begins, so one run's +/// obligations are never checked against another's graph. +#[cfg(debug_assertions)] +pub fn clear_watch_log() { + WATCH_LOG.with(|log| log.borrow_mut().clear()); +} + +/// Check that eager narrowing saw everything the finished graph knows — the +/// invariant the whole mechanism rests on: **every concrete type reaching an operand +/// variable reaches its obligation**. +/// +/// A variable's lower bounds are written in exactly four places, and delivery is +/// wired into every one: `constrain_go`'s two variable arms (`notify_lower` for a +/// concrete contribution, `link_watches` for a var-var edge), `extrude`'s proxy +/// seeding (`copy_watches`), and `freshen_above`'s clone (`freshen_watches`). Each is +/// load-bearing — `a_concrete_operand_reaches_its_obligation` has a case per +/// mechanism, confirmed by deleting the mechanism and watching only its case fail. +/// +/// That the list is closed is an argument about today's code, not a property the +/// compiler enforces, and a missed delivery is quiet: an obligation that never +/// narrows leaves its output unresolved, which reads as an ordinary under-determined +/// program and can surface phases later, on an interior node, as a wall complaining +/// about a variable with no obvious connection to an operator. +/// +/// So the argument is checked rather than trusted. After emission, every watched +/// operand is resolved against the completed graph, and a resolved base must already +/// have narrowed its obligation. A fifth writer added later surfaces here, on +/// whichever program exercises it, naming the operand and the stale candidate set. +/// +/// `resolve` is passed in because resolution lives above this module; it must be a +/// *read* of the graph (`compact` → `simplify` → `coalesce`), never something that +/// records a bound, or the check would perturb what it is checking. +#[cfg(debug_assertions)] +pub fn verify_narrowing_is_complete(resolve: impl Fn(&Type) -> Option) { + WATCH_LOG.with(|log| { + for (obligation, pos, operand) in log.borrow().iter() { + let Some(resolved) = resolve(operand) else { + // A position the program left conflicting: coalesce reports it, and + // there is no single base narrowing could have been offered. + continue; + }; + let Some(base) = offered_base(&resolved) else { + // Not a base leaf, so nothing was owed to the obligation. + continue; + }; + let candidates = obligation.candidates(); + debug_assert!( + candidates.iter().all(|i| i.args[*pos as usize] == *base), + "trait narrowing missed a bound: operand {pos} of {obligation:?} \ + resolves to {base:?}, but its candidate set still holds {candidates:?} \ + — some path wrote this variable's lower bounds without delivering to \ + its watches (see `verify_narrowing_is_complete`)", + ); + } + }); +} + +/// What a bound contribution tells a trait about the position it landed on. +/// +/// The distinction between the last two variants is the whole point. Both narrow +/// nothing, but for opposite reasons: one is a position the program has not +/// determined *yet*, and one is a shape no implementation can *ever* accept. +/// Treating them alike is what let `(1, 2) == (3, 4)` type-check — a tuple narrows +/// nothing, and a trait with no associated type has nothing left unresolved for a +/// later wall to catch, so the program passed. +pub enum Offered<'a> { + /// A base leaf, with refinements peeled — the fact narrowing consumes. + Base(&'a BaseType), + /// Nothing known here yet: an inference variable, a hole, or a transient handle + /// whose payload arrives separately (a `Feed`; a `Mut` is dereferenced before the + /// variable arms, so it never reaches a watch). + Unknown, + /// A concrete shape that is not a base and never will be. No implementation + /// accepts it, so the requirement fails here rather than silently going + /// undischarged. + NotABase, +} + +/// What `ty` offers a trait. +/// +/// Refinements are peeled here and nowhere else, which is the whole of "a refinement +/// does not affect a trait": the fact is read off the base, at the moment the base +/// arrives. +pub fn offered(ty: &Type) -> Offered<'_> { + let mut cur = ty; + while let Type::Refinement(inner, _) = cur { + cur = inner; + } + match cur { + Type::Base(b) => Offered::Base(b), + // Products, sums and functions are fully determined and are not bases. A + // collection compared or added is the same mistake as a tuple. + Type::Tuple(_) | Type::Record(_) | Type::Variant(_) | Type::Fun { .. } => Offered::NotABase, + // Everything else is either a variable, a placeholder, or a carrier whose + // payload reaches the watch by another route. + _ => Offered::Unknown, + } +} + +/// The base `ty` offers, if any — for callers that only need the narrowing fact. +pub fn offered_base(ty: &Type) -> Option<&BaseType> { + match offered(ty) { + Offered::Base(b) => Some(b), + _ => None, + } +} + +/// Propagate `upper`'s obligations down to `lower` when the edge `lower <: upper` is +/// recorded, and deliver what `lower` already knows. +/// +/// A concrete type does **not** reliably reach a watched variable through the bound +/// closure alone, and the exception is the common case rather than a corner. When +/// `lower` and `upper` sit at different polymorphism levels — which is exactly what a +/// `let` RHS produces, since it is emitted one level deeper — the edge is recorded by +/// the arm whose closure runs against the *other* side's bounds, so a concrete type +/// already sitting on `lower` is never re-offered to `upper`, and one arriving later +/// closes against uppers that do not include it. The graph is still correct; it is +/// only *transitively* readable, which is a thing coalesce does and constraint +/// emission does not. +/// +/// So the watch follows the edge, in the direction information flows: down, to the +/// variables feeding the watched one. This is [`FunKindVar::link`]'s move +/// (`crate::ccl::ty`) — a kind force propagates along stored links for the same +/// reason, and for kinds it is the only mechanism because a force is a flag rather +/// than a bound. +/// +/// Recursion is bounded by the watch set only ever growing: a variable that gains +/// nothing new stops the walk, which is what makes this safe on the cyclic bound +/// graph a recurrence produces. +pub(super) fn link_watches( + lower: &Rc, + upper: &Rc, + cache: &mut ConstrainCache, +) -> Result<(), ConstrainError> { + let incoming = { + let watches = upper.watches.borrow(); + if watches.is_empty() { + return Ok(()); + } + watches.clone() + }; + let added: Vec<(Rc, u8)> = { + let mut watches = lower.watches.borrow_mut(); + incoming + .into_iter() + .filter(|(ob, pos)| { + let fresh = !watches.iter().any(|(o, p)| o.uid == ob.uid && p == pos); + if fresh { + watches.push((Rc::clone(ob), *pos)); + } + fresh + }) + .collect() + }; + if added.is_empty() { + return Ok(()); + } + + // Whatever `lower` already carries is information the obligation has not been + // offered — it arrived before the edge existed. + let (known, below) = { + let bounds = lower.bounds.borrow(); + let known: Vec = bounds + .lower() + .iter() + .filter_map(|b| offered_base(&b.ty).cloned()) + .collect(); + let below: Vec> = bounds + .lower() + .iter() + .filter_map(|b| match &b.ty { + Type::Infer(v) => Some(Rc::clone(v)), + _ => None, + }) + .collect(); + (known, below) + }; + for (obligation, pos) in &added { + for base in &known { + obligation.narrow(*pos, base, cache)?; + } + } + // Transitivity: anything flowing into `lower` flows into `upper` too. + for v in below { + link_watches(&v, lower, cache)?; + } + Ok(()) +} + +/// Deliver a lower bound to every obligation watching `var`. +/// +/// Called from `constrain_go`'s lower-bound arm, with the contribution exactly as it +/// was recorded. The two side substitutions are deliberately **not** applied: a +/// substitution rewrites refinement-predicate interiors and Pi binder names, never +/// the structural skeleton, so the base leaf this reads is invariant under every +/// morphism the solver can compose. Materializing the bound into the holder's frame +/// would cost a walk and change nothing. +pub(super) fn notify_lower( + var: &Rc, + contribution: &Type, + cache: &mut ConstrainCache, +) -> Result<(), ConstrainError> { + // Snapshot: a deposit re-enters `constrain_go`, which can append watches. + let watches = { + let watches = var.watches.borrow(); + if watches.is_empty() { + return Ok(()); + } + watches.clone() + }; + match offered(contribution) { + Offered::Base(base) => { + for (obligation, pos) in watches { + obligation.narrow(pos, base, cache)?; + } + } + Offered::NotABase => { + for (obligation, pos) in watches { + obligation.reject(pos, contribution)?; + } + } + Offered::Unknown => {} + } + Ok(()) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::ccl::infer::solver::fresh_var; + + /// Both narrowing orders reach the same answer — the property that lets the + /// obligation be discharged incrementally instead of by a final sweep. + #[rstest::rstest] + #[case(&[(0, BaseType::Int), (1, BaseType::Int)])] + #[case(&[(1, BaseType::Int), (0, BaseType::Int)])] + fn narrowing_is_order_independent(#[case] steps: &[(u8, BaseType)]) { + let out = fresh_var(0); + let ob = TraitObligation::new(Trait::Addable, vec![(Assoc::Output, out.clone())]); + let mut cache = ConstrainCache::new(); + + for (pos, base) in steps { + ob.narrow(*pos, base, &mut cache) + .expect("Int + Int is addable"); + } + + assert_eq!(ob.candidates().len(), 1); + let Type::Infer(v) = &out else { unreachable!() }; + assert!( + v.bounds + .borrow() + .lower() + .iter() + .any(|b| b.ty == Type::Base(BaseType::Int)), + "the settled output type is deposited as a lower bound on O", + ); + } + + /// One known operand is enough to settle the output when every remaining + /// implementation agrees on it — without concluding anything about the *other* + /// operand, which stays open for a future heterogeneous implementation. + #[test] + fn one_known_operand_settles_an_agreed_output() { + let out = fresh_var(0); + let ob = TraitObligation::new(Trait::Addable, vec![(Assoc::Output, out.clone())]); + let mut cache = ConstrainCache::new(); + + ob.narrow(1, &BaseType::Int, &mut cache) + .expect("Int is addable"); + + assert_eq!( + ob.agreed_assoc(Assoc::Output), + Some(BaseType::Int), + "(Int, Int) ⇝ Int is the only row left, so its Output is settled", + ); + assert_eq!( + ob.candidates(), + vec![TraitImpl { + args: &[BaseType::Int, BaseType::Int], + assoc: &[(Assoc::Output, BaseType::Int)], + }] + ); + } + + /// A comparison associates **nothing**: its `Bool` is the operator's, not the + /// trait's, so there is no position for the obligation to settle and the whole + /// claim is the requirement on its operands. + /// + /// This is the shape that made associated types a *set* rather than one + /// distinguished output — and it is exercised by every comparison in the suite, + /// not just here. + #[test] + fn a_comparison_associates_nothing() { + let ob = TraitObligation::new(Trait::Equatable, Vec::new()); + let mut cache = ConstrainCache::new(); + + ob.try_deposit(&mut cache).expect("nothing to deposit"); + assert_eq!(ob.agreed_assoc(Assoc::Output), None); + + // The requirement half is untouched. + ob.narrow(0, &BaseType::Int, &mut cache) + .expect("Int is equatable"); + assert!( + ob.narrow(1, &BaseType::String, &mut cache).is_err(), + "nothing equates an Int to a String", + ); + } + + /// Operands that no implementation accepts together are rejected, and the error + /// says what the position could still have taken. + #[test] + fn incompatible_operands_have_no_implementation() { + let out = fresh_var(0); + let ob = TraitObligation::new(Trait::Orderable, vec![(Assoc::Output, out)]); + let mut cache = ConstrainCache::new(); + + ob.narrow(0, &BaseType::Int, &mut cache) + .expect("Int is orderable"); + let err = ob + .narrow(1, &BaseType::String, &mut cache) + .expect_err("nothing compares an Int to a String"); + + let ConstrainError::NoTraitImpl { + trait_, + position, + found, + accepted, + } = err + else { + panic!("expected NoTraitImpl, got {err:?}"); + }; + assert_eq!(trait_, Trait::Orderable); + assert_eq!(position, 1); + assert_eq!(found, Type::Base(BaseType::String)); + assert_eq!(accepted, vec![BaseType::Int]); + } + + /// Every implementation of a trait agrees on its **shape** — how many types it is + /// over, and which types it associates. + /// + /// [`Trait::arity`] and [`Trait::assocs`] read that shape off the first row, and + /// each variant's doc states it in prose. This is what keeps the three from + /// drifting apart: a row added with the wrong arity, or associating a name its + /// siblings do not, fails here rather than silently making `arity()` a lie. + #[test] + fn every_trait_has_a_consistent_shape() { + for trait_ in [ + Trait::Addable, + Trait::Subtractable, + Trait::Multipliable, + Trait::Divisible, + Trait::Equatable, + Trait::Orderable, + Trait::Negatable, + Trait::Comparable, + ] { + let (arity, assocs) = (trait_.arity(), trait_.assocs()); + for row in trait_.impls() { + assert_eq!( + row.args.len(), + arity, + "{trait_} has rows of differing arity: {row:?}", + ); + let names: Vec = row.assoc.iter().map(|(n, _)| *n).collect(); + assert_eq!( + names, assocs, + "{trait_} has rows associating different names: {row:?}", + ); + } + } + } + + /// A refinement is transparent: `{Int | __elem == 1}` narrows exactly as `Int` + /// does. This is the property the emit-time strip could not deliver, because at + /// emission an operand is usually still a variable with nothing to strip. + #[test] + fn a_refinement_narrows_as_its_base() { + let refined = Type::Refinement( + Box::new(Type::Base(BaseType::String)), + crate::ccl::Refinement::born(Rc::new(crate::ccl::TypedExpr::lit( + crate::ccl::Lit::Bool(true), + ))), + ); + assert_eq!(offered_base(&refined), Some(&BaseType::String)); + } + + /// A shape the table has no row for offers nothing rather than failing — see + /// [`offered_base`]. + #[test] + fn a_non_base_shape_offers_nothing() { + assert_eq!(offered_base(&Type::UIntRange(3)), None); + assert_eq!(offered_base(&Type::Txn), None); + assert_eq!(offered_base(&fresh_var(0)), None); + } +} diff --git a/src/ccl/infer/typing.rs b/src/ccl/infer/typing.rs index eb7d10e1..595b557a 100644 --- a/src/ccl/infer/typing.rs +++ b/src/ccl/infer/typing.rs @@ -4,6 +4,7 @@ use crate::ccl::ccl_utils::TermMemo; use crate::ccl::infer::solver::PolyScheme; +use crate::ccl::infer::solver::traits::{Assoc, Trait}; use crate::ccl::infer::{InferError, LocatedInferError}; use crate::ccl::provenance::NodeId; use crate::ccl::{Expr, Name, Type}; @@ -59,6 +60,35 @@ pub(super) trait Typing { /// Instantiate a polymorphic operator scheme at the current level. fn instantiate(&mut self, scheme: &PolyScheme) -> Type; + /// Type an operator whose signature is a **trait** rather than a fixed scheme — + /// arithmetic, comparison, and negation. Returns the operator's result type. + /// + /// Arity is whatever `operands` says, so this serves the unary and binary + /// operators alike. The operand types enter *verbatim*, refinements included: + /// the rule mints one unrelated variable per operand, records `operandᵢ <: 𝐴ᵢ`, + /// and states the obligation. Refinements therefore cannot leak onto the result + /// the way they do through a shared variable — not because they are stripped, but + /// because nothing the result depends on is shared with an operand. + /// + /// `assoc` is the association the caller wants back, if any. `None` records a + /// pure requirement and yields nothing — which is what an operator whose result + /// is fixed (`==`) or supplied by its own scheme (`max`) needs. + /// + /// The two modes differ in *when* the requirement can be decided, which is the + /// whole reason this is a `Typing` method rather than a shared rule body. Emit's + /// operands are usually still unresolved variables, so it records an obligation + /// that discharges as bounds arrive. Check runs after inference on concrete + /// types, so it decides immediately — and must, because there is no + /// [`InferArena`](super::api::InferArena) there to break an obligation's + /// reference cycle. + fn require_trait( + &mut self, + trait_: Trait, + operands: &[&Type], + assoc: Option, + at: &dyn Fn() -> String, + ) -> Result, LocatedInferError>; + /// Normalize a user annotation / binder type into a solver-ready `Type` /// (holes → fresh vars; refinements kept). See /// [`InferCtx::normalize_annotation`](super::context::InferCtx::normalize_annotation). diff --git a/src/ccl/infer_var.rs b/src/ccl/infer_var.rs index 57cda846..47b17e10 100644 --- a/src/ccl/infer_var.rs +++ b/src/ccl/infer_var.rs @@ -304,6 +304,19 @@ pub struct InferVar { pub level: Level, /// Mutable lower/upper bound lists. pub bounds: RefCell, + /// Trait obligations this variable is an operand of, with the position it + /// occupies in each. Every lower bound recorded here is delivered to them by + /// `notify_lower` (`src/ccl/infer/solver/traits.rs`), which is how an operator's + /// requirement is discharged incrementally rather than by a pass that goes + /// looking for obligations once solving has stopped. + /// + /// The list lives on the variable rather than in a side map on the inference + /// context because the three places that must reach it — the bound-recording + /// arms, `extrude`, and `freshen_above` — are free functions with no context in + /// hand. Like [`bounds`](Self::bounds) it is severed at arena teardown: an + /// obligation holds its output `Type`, which holds a variable, which holds the + /// obligation. + pub watches: RefCell, u8)>>, } thread_local! { @@ -359,6 +372,7 @@ impl InferVar { uid: fresh_infer_var_id(), level, bounds: RefCell::new(InferBounds::default()), + watches: RefCell::new(Vec::new()), }); ACTIVE_ARENA.with(|slot| { if let Some(vars) = slot.borrow_mut().as_mut() { diff --git a/tests/type_check.rs b/tests/type_check.rs index 13021b32..ed1f7b53 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -172,6 +172,275 @@ fn test_binary_op(#[case] code: &str, #[case] expected: BaseType) { assert_eq!(infer_program(code), Type::Base(expected)); } +/// An operator **computes** a new value, so it carries no refinement from its +/// operands — not even when both operands carry the *same* one. +/// +/// The `same_variable_twice` case is the one that regresses under a shared-variable +/// signature (`∀α. α → α → α`): the result position is positive, where refinement +/// sets *intersect*, and intersecting a set with itself returns it, so `x + x` where +/// `x` is `2` claimed the sum was `2`. Distinct singletons intersect to nothing, +/// which is why the other two cases pass either way. +#[rstest] +#[case::same_variable_twice("x = 2\nx + x")] +#[case::distinct_singletons("x = 2\ny = 3\nx + y")] +#[case::literals("2 + 2")] +fn an_operator_result_carries_no_operand_refinement(#[case] code: &str) { + assert_eq!(infer_program(code), int()); +} + +/// The three shapes a trait can take are each exercised by a real program, which is +/// what keeps the machinery from being fitted to one of them. +/// +/// | | arity | associates | +/// |---|---|---| +/// | `Negatable` | unary | `Output` | +/// | `Addable` | binary | `Output` | +/// | `Equatable` / `Orderable` | binary | nothing | +/// +/// The last row is the one worth stating: a comparison's `Bool` comes from the +/// *operator*, not the trait — it is the same `Bool` for every pair the trait accepts, +/// so it says nothing about them. Recording it as an associated type would claim the +/// trait determines something it does not. +#[rstest] +#[case::unary_with_an_output("-(2 + 3)", int())] +#[case::binary_with_an_output("2 + 3", int())] +#[case::binary_associating_nothing("2 < 3", bool_ty())] +#[case::composed("-(2 + 3) < 4", bool_ty())] +fn each_trait_shape_types_a_real_program(#[case] code: &str, #[case] expected: Type) { + assert_eq!(infer_program(code), expected); +} + +/// Negation is a trait, so an operand it has no implementation for is rejected as a +/// missing implementation rather than as a mismatch against a hardcoded domain. +#[test] +fn negation_rejects_an_operand_with_no_implementation() { + let errs = infer_program_err(r#"-"a""#); + assert!( + errs.iter() + .any(|e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Negatable")), + "expected NoTraitImpl for Negatable, got {errs:?}" + ); +} + +/// Composites are **not** comparable, and not addable either. +/// +/// The tables have no row for a tuple, record or collection — but an absent row is +/// not by itself a rejection, and for a while it was not one: a composite offers no +/// base to narrow with, and a comparison has no associated type to leave unresolved, +/// so `(1, 2) == (3, 4)` type-checked as `Bool` and failed in the interpreter. What +/// rejects it is the distinction between *not determined yet* and *determined, and +/// not a base* (`Offered` in `src/ccl/infer/solver/traits.rs`). +#[rstest] +#[case::tuple_equality("(1, 2) == (3, 4)", "Equatable")] +#[case::tuple_ordering("(1, 2) < (3, 4)", "Orderable")] +#[case::tuple_arithmetic("(1, 2) + (3, 4)", "Addable")] +#[case::record_equality("(a=1) == (a=2)", "Equatable")] +#[case::collection_equality("[1, 2] == [3, 4]", "Equatable")] +fn a_composite_satisfies_no_trait(#[case] code: &str, #[case] expected: &str) { + let errs = infer_program_err(code); + assert!( + errs.iter() + .any(|e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == expected)), + "expected NoTraitImpl for {expected}, got {errs:?}" + ); +} + +/// `unit` is comparable to nothing, because the interpreter cannot compare units — +/// an out-of-table *base*, rejected by ordinary narrowing rather than by the +/// composite rule above. +#[test] +fn a_base_outside_the_table_is_rejected() { + let errs = infer_program_err("() == ()"); + assert!( + errs.iter() + .any(|e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Equatable")), + "expected NoTraitImpl for Equatable, got {errs:?}" + ); +} + +/// A refinement is transparent to a trait: `{Int | …}` satisfies `Addable` exactly +/// when `Int` does, in both directions. +/// +/// The positive half is `2 + 2` above (singletons are addable). This is the negative +/// half — a refined `String` is no more subtractable than a bare one, and the +/// rejection names the trait rather than reporting two types that "don't match". +#[test] +fn a_refinement_does_not_make_a_type_satisfy_a_trait() { + let errs = infer_program_err(r#""a" - "b""#); + assert!( + errs.iter().any( + |e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Subtractable") + ), + "expected NoTraitImpl for Subtractable, got {errs:?}" + ); +} + +/// Operands no implementation accepts together are rejected — including for a +/// **comparison**, whose result type is `Bool` whatever the operands are. +/// +/// That last part is the whole reason the requirement is recorded as an obligation +/// rather than derived from the result. A comparison's result mentions neither +/// operand, so any scheme that reads the requirement off the result type would never +/// look at them: `1 > "a"` would type cleanly as `Bool` and fail in the interpreter. +#[rstest] +#[case::compare_int_string(r#"1 > "a""#)] +#[case::equate_int_bool("1 == True")] +#[case::add_int_bool("1 + True")] +fn operands_no_implementation_accepts_are_rejected(#[case] code: &str) { + let errs = infer_program_err(code); + assert!( + errs.iter() + .any(|e| matches!(e, InferError::NoTraitImpl { .. })), + "expected NoTraitImpl, got {errs:?}" + ); +} + +/// An operator's result flows onward as an ordinary type, so misusing it is an +/// ordinary diagnostic rather than a wall the compiler cannot explain. +/// +/// This is what an *unreduced computed type* in the result position costs: the +/// solver cannot compare one against anything, so the obligation has to be deferred +/// and retried, and a conflict that nothing re-derives escapes inference entirely. +/// Here the result is a plain inference variable that the trait deposits `Int` on, so +/// `and` rejects it exactly as it would reject any other `Int`. +#[rstest] +#[case::arithmetic_into_bool_logic("(1 + 2) and True")] +#[case::string_arithmetic_into_sum(r#"sum(["a" + "b"])"#)] +fn misusing_an_operator_result_is_an_ordinary_diagnostic(#[case] code: &str) { + assert!( + !infer_program_err(code).is_empty(), + "expected the misuse of an operator's result to be rejected" + ); +} + +/// A generalized function carries its operators' requirements into its scheme, so it +/// typechecks on its own and each use discharges its **own** copy. +/// +/// `f = \a -> \b -> a + b` is `∀A B O. (Addable(A, B) ⇝ O) ⇒ A → B → O`. Two uses at +/// different types both succeed, which is the property that fails if instantiations +/// share one obligation: whichever use narrowed first would empty the other's +/// candidate set. +#[test] +fn a_generalized_function_instantiates_its_operator_requirements() { + assert_eq!(infer_program("f = \\a, b -> a + b\nf(1, 2)"), int()); + assert_eq!( + infer_program("f = \\a, b -> a + b\nf(\"x\", \"y\")"), + string() + ); + assert_eq!( + infer_program("f = \\a, b -> a + b\n(f(1, 2), f(\"x\", \"y\"))"), + Type::Tuple(vec![int(), string()]) + ); +} + +// An obligation is discharged by *delivery*: a concrete type reaching an operand +// variable has to reach the obligation watching it. Production code writes a +// variable's lower bounds in exactly four places — `constrain_go`'s two variable +// arms, `extrude`'s proxy seeding, and `freshen_above`'s clone — and there is a case +// per mechanism below, each confirmed to discriminate by deleting the mechanism it +// names and watching only its own case fail. +// +// A missed delivery leaves a type *undetermined* rather than wrong, so it reads as an +// ordinary under-determined program rather than an error — which is why these assert +// through the consistency wall. +#[rstest] +// The variable arms, across a *level boundary*: `s + i` sits in a `let` RHS, emitted +// one level deeper than the loop binder, so `⟨binder⟩ <: A` is recorded by the arm +// that closes against `A`'s uppers and never re-offers the `Int` already sitting on +// the binder. Delivery has to follow the var-var edge downward instead. +#[case::across_a_level_boundary("s := 0\nfor i in [1, 2, 3]:\n y = s + i\n s := y\ns")] +// `extrude`: a generalized multi-argument function is emitted a level deeper than its +// use, so constraining its tuple parameter down to the use's level mints proxies +// whose bounds are seeded by *direct writes* rather than through `constrain_go`. The +// nesting matters — the outer operator's operand is the inner operator's output, and +// that is the variable that gets approximated. +#[case::through_an_extrusion_proxy("m = \\a, b -> a * b + 1\nm(3, 4)")] +// `freshen_above`: each use of a generalized function instantiates its own copy of +// the obligation, which has to be reachable from the freshened operand variables. +#[case::through_a_freshened_instantiation("k = \\a, b -> a + b\nk(k(1, 2), 3)")] +fn a_concrete_operand_reaches_its_obligation(#[case] code: &str) { + // The wall, not the root type: a missed delivery can leave an *interior* node + // undetermined while the program's own type resolves fine — which is exactly how + // the extrusion case presents. + infer_and_check(code); +} + +// The value type of a register, ignoring the sequencing domain — an `Infer` until the +// mutability-elimination phases resolve it, so it cannot be asserted on here. +fn register_value_type(code: &str) -> Type { + match infer_program(code) { + Type::History { value, .. } => *value, + other => panic!("expected a register type for `{code}`, got {other}"), + } +} + +// A register that reads itself in its own write is a **cycle**: `value(x)` is defined +// by an equation mentioning `value(x)`. These pin that an operator inside one still +// gets a type — and, more precisely, *why* it needs no cycle machinery to do so. +// +// Narrowing consumes a bound at the moment it is recorded, not a resolved type, so an +// obligation never enters the recurrence at all. The base it needs is on the +// register's **seed**, which is an ordinary lower bound of the value variable and +// reaches the operand positions like any other. That holds even when *both* operands +// are the cycle (`x := x * x`), where a rule that resolved its operands would have +// nothing to work from. +// +// The loop-carried accumulator is covered end-to-end in +// `compilation_pipeline::mutability`; these are the harder shapes no test reached — +// both operands cyclic, a cycle crossing a call boundary, mutual recursion between +// registers, and a non-`Int` base. +#[rstest] +// One cyclic operand, the shape every accumulator has. +#[case::self_add("x := 0\nx := x + 1\nx", "Int")] +// **Both** operands cyclic: only the seed offers a base. +#[case::self_multiply("x := 2\nx := x * x\nx", "Int")] +#[case::self_subtract("x := 10\nx := x - x\nx", "Int")] +// Nested, so an inner operator's output is itself an operand of an outer one. +#[case::nested("x := 0\nx := (x + 1) * (x + 2)\nx", "Int")] +#[case::deeply_nested("x := 1\nx := ((x + x) * (x + x)) + ((x * x) + (x + x))\nx", "Int")] +// Routed through user functions, so the cycle crosses a call boundary — and the +// obligations are the *freshened* copies of the callee's. +#[case::through_functions( + "def f(a):\n a + 1\ndef g(a):\n a * 2\nx := 0\nx := f(x) + g(x)\nx", + "Int" +)] +#[case::through_nested_calls("def f(a):\n a + 1\nx := 0\nx := f(f(x))\nx", "Int")] +// Two registers each defined in terms of the other: the cycle spans two equations. +#[case::mutual("x := 0\ny := 0\nx := y + 1\ny := x + 1\nx", "Int")] +#[case::three_way("x := 0\ny := 0\nz := 0\nx := z + 1\ny := x + 1\nz := y + 1\nz", "Int")] +// A non-`Int` base, so the answer comes from the operands rather than a hardcoded row. +#[case::string_accumulator("s := \"a\"\ns := s + \"b\"\ns", "String")] +// A comparison cycle: its output is `Bool` for every implementation, so it is settled +// at birth and the cycle costs it nothing. Nothing else in the suite writes one. +#[case::self_comparison("b := True\nb := (b == True)\nb", "Bool")] +#[case::conditional("x := 0\nx := x + 1 if x == 0 else x - 1\nx", "Int")] +fn a_register_that_reads_itself_still_gets_a_type(#[case] code: &str, #[case] base: &str) { + assert_eq!(register_value_type(code).to_string(), base); +} + +/// A cycle must not hide a conflict: the seed and the write have to agree, and the +/// obligation sees both as ordinary bounds. +#[test] +fn a_cycle_does_not_hide_an_operand_conflict() { + assert!( + !infer_program_err("x := 0\nx := x + \"a\"\nx").is_empty(), + "a conflict reachable only through a cyclic operand must still be a diagnostic" + ); +} + +/// The requirement travels with the function, so applying it at a type no +/// implementation accepts is rejected at the call site. +#[test] +fn a_generalized_function_rejects_a_use_its_trait_forbids() { + let errs = infer_program_err("f = \\a, b -> a - b\nf(\"x\", \"y\")"); + assert!( + errs.iter().any( + |e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Subtractable") + ), + "expected NoTraitImpl for Subtractable, got {errs:?}" + ); +} + // --------------------------------------------------------------------------- // Let binding / scoping tests // --------------------------------------------------------------------------- @@ -1141,23 +1410,51 @@ fn test_self_application_types() { ); } +/// An unapplied lambda whose parameter is used only as an operator's operand keeps an +/// **open parameter** and, today, a determined result. +/// +/// `\x -> x + 1` carries the obligation `Addable(A, Int) ⇝ O`. Nothing is ever +/// deposited onto an operand position, so `A` stays an inference variable exactly as +/// it does for `\x -> x` — the program states "`x` is addable to `Int`", and `A`'s +/// information is the program's to supply. +/// +/// `O` is a different matter: the obligation is its only source, and every +/// implementation whose second operand is `Int` returns `Int`, so it resolves. That +/// is a fact about today's table rather than a stable property — adding +/// `Addable(Float, Int) ⇝ Float` would leave two candidates whose outputs disagree +/// and open the result too, which is why this asserts the codomain per case rather +/// than as a rule. #[rstest] #[case::comparison( r" f = \x -> x > 1 f ", - Type::Fun { name: None, kind: cambra::ccl::FunKind::Compute, domain: Box::new(int()), codomain: Box::new(bool_ty()) } + bool_ty() )] #[case::arithmetic( r" f = \x -> x + 1 f ", - Type::Fun { name: None, kind: cambra::ccl::FunKind::Compute, domain: Box::new(int()), codomain: Box::new(int()) } + int() )] -fn test_lambda_unapplied(#[case] code: &str, #[case] expected: Type) { - assert_eq!(infer_program(code), expected); +fn test_lambda_unapplied(#[case] code: &str, #[case] expected_codomain: Type) { + let ty = infer_program(code); + let Type::Fun { + domain, codomain, .. + } = &ty + else { + panic!("expected a function type, got {ty}"); + }; + assert_eq!( + **codomain, expected_codomain, + "the operator's trait determines the result even with an open operand", + ); + assert!( + matches!(**domain, Type::Infer(_)), + "an operand a trait does not determine stays open, got {domain}", + ); } #[test] From 364667acd43d94e72638a398a05ff5326138796f Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 12 Aug 2026 10:37:50 -0700 Subject: [PATCH 2/6] Review: a trait is a relation over types *and functions*, and F = 0 today MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Traits section described a trait as an association between types, which reads as the whole story rather than the corner that is implemented. Say what the general shape is and where this sits inside it. - **A new subsection, "A trait is a relation, and today it relates only types."** A trait over `𝑁` operand positions, `𝐴` associated types and `𝐹` associated *functions* is an `(𝑁 + 𝐴 + 𝐹)`-ary relation whose `𝑁` operand types functionally determine the rest; an implementation is a hyper-edge and discharge is the search for a consistent one. Cambra implements `𝑁 ∈ {1, 2}`, `𝐴 ∈ {0, 1}`, `𝐹 = 0`, built into the compiler rather than declared in CHL. `𝐹 = 0` is named as a gap: `Addable`'s `String` and `Int` rows denote different functions, and because the obligation carries neither, the function is recovered outside the trait — `simplify.rs`'s `Concat` rewrite, then `apply_binop_column`'s dispatch on the operand column's runtime representation. - **Associated types move inside the trait name** — `Addable(𝐴, 𝐵 ⇝ 𝑂)`, `Negatable(𝐴 ⇝ 𝑂)`, `Equatable(𝐴, 𝐵)` — so the notation shows the relation's structure instead of listing the associations beside it. Implementation rows take the same form (`Addable(Int, Int ⇝ Int)`), which retires the split between a trait written `Addable(𝐴, 𝐵)` and a row written `(𝐴, 𝐵) ⇝ 𝑂`. - **"Refinements are transparent" answers whether it is permanent.** It is, and not by fiat: a candidate set only ever shrinks and a refinement is something a bound can deliver late, so a refined type satisfying a requirement its base does not would force a dropped candidate to be re-admitted and discharge would stop being order-independent. Growing `𝐹` does not change that — selecting a function by a predicate is dispatch on a fact about a value. - A **trait** is a requirement on a *list* of types, not on a type. Also drops the parenthetical about the signature this replaced, and re-homes its `an_operator_result_carries_no_operand_refinement` citation to §3's "operator does not inherit its operands' refinements" bullet, where the fact it pins is actually stated. ## `traits.rs`'s module doc stops mirroring the design section It had reproduced the section's five headings in the same order — 96 lines against the design doc's, with the two most mechanism-specific parts (*Delivery: the watch follows the edge*, *Requirements are generalized*) present only in the doc. That inverts the split: the module comment carried the theory and omitted the wiring, and each of the changes above had to be written twice with nothing checking that the copies agreed. It now follows `channelize.rs`'s shape — what the code *is*, plus a "Where to read more" pointer naming `type-inference.md`, "Traits" as the design of record. `Vocabulary` stays, because its terms are this module's types (`Trait`, `TraitImpl`, `Assoc`, `TraitObligation`) and the intra-doc links navigate the API. The rationale leaves: the `(𝑁 + 𝐴 + 𝐹)` framing, the one-way-deposit argument, and the `λ 𝑥 → 𝑥 + 1` worked example. *Refinements are transparent* and *Discharge is incremental* collapse into one section stating what `narrow` and `try_deposit` do, keeping their links. 96 lines to 58. --- src/ccl/design/type-inference.md | 43 ++++++++++++--- src/ccl/infer/solver/traits.rs | 94 ++++++++++++++------------------ 2 files changed, 75 insertions(+), 62 deletions(-) diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index 5c0d34ed..b09fe18f 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -684,7 +684,7 @@ The reason is that a literal knows more about itself than its base does, and tha What this changed is instructive, because refinements were rare enough before that several rules assumed their absence. Each was already wrong for a user-written refinement; literals are merely the first thing that makes them reachable. -* **An operator does not *inherit* its operands' refinements**, and does not have to be *made* not to. A refinement is a fact about a value, so an operator that computes a new value cannot carry one over: `𝑥 + 𝑥` where `𝑥` is `2` produces `4`. Arithmetic, comparison and negation state their requirement as a [trait](#traits), over a variable per operand and per associated type — all unrelated — which leaves no path for an operand's refinement to reach the result by sharing. The remaining monomorphic operators (`and`, `++`, `not`) keep an ordinary scheme and pass their operands verbatim — nothing is shared with the result, so a refined operand simply flows into a concrete domain. Aggregates likewise keep theirs, since their operand is a *collection* whose refinements describe its domain and the rule must see them. +* **An operator does not *inherit* its operands' refinements**, and does not have to be *made* not to. A refinement is a fact about a value, so an operator that computes a new value cannot carry one over: `𝑥 + 𝑥` where `𝑥` is `2` produces `4`. Arithmetic, comparison and negation state their requirement as a [trait](#traits), over a variable per operand and per associated type — all unrelated — which leaves no path for an operand's refinement to reach the result by sharing (`an_operator_result_carries_no_operand_refinement`). The remaining monomorphic operators (`and`, `++`, `not`) keep an ordinary scheme and pass their operands verbatim — nothing is shared with the result, so a refined operand simply flows into a concrete domain. Aggregates likewise keep theirs, since their operand is a *collection* whose refinements describe its domain and the rule must see them. Inheriting is not the same as **computing**, and only the first is ruled out. `{Int | __elem == 2} + {Int | __elem == 3}` genuinely *is* `{Int | __elem == 5}`, and a trait implementation is where such a rule would live, since it determines the output type rather than forcing it to be a position the operands already occupy. Today every implementation computes a base and stops — a property of the table, not of the mechanism. Two things would have to change to lift it: an implementation would need the operands' *types* rather than their bases, and the deposit would have to move to a point where those types are final. Eager deposit is sound for a base because a base never weakens, while a refinement set only shrinks as further lower bounds arrive — so a refinement computed from a partial view is too strong. A rule computing from resolved operands then meets recurrences (`x := x + 1` resolves its operand through its own output), where it must already be sound at the cut; and anything beyond constant folding and interval arithmetic needs predicate *implication*, which the lattice deliberately does not have (refinements match structurally — see this file's module-level note in `src/ccl/infer/solver/mod.rs`). * **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. @@ -1134,12 +1134,12 @@ Recorded so a reader can tell a deliberate boundary from an oversight. ## Traits -The constraint lattice can state that two positions are **equal** or **related by subtyping**. That is everything an operator needs when its result *is* one of its operands — `max(xs)` returns an element, `x.f` returns the field — because "is one of" is a shared lattice position. It is not enough for an operator whose result is **computed from** its operands, and `+` is the smallest example: the sum of two values is neither of them. (Sharing one variable across operands and result — the signature this replaced — states the requirement in the one place it is wrong in both polarities at once; `an_operator_result_carries_no_operand_refinement` pins the consequence.) +The constraint lattice can state that two positions are **equal** or **related by subtyping**. That is everything an operator needs when its result *is* one of its operands — `max(xs)` returns an element, `x.f` returns the field — because "is one of" is a shared lattice position. It is not enough for an operator whose result is **computed from** its operands, and `+` is the smallest example: the sum of two values is neither of them. ### Vocabulary -* A **trait** is a named requirement a type may satisfy — `Addable`, `Orderable`, `Comparable`. **A trait is not a type**: no `Type` variant, no lattice point, no subtyping edge, and the type grammar and `constrain_go`'s rules are untouched. Types *satisfy* traits. -* An **implementation** is one row of a trait's table: the types it accepts, and the types it associates with them. +* A **trait** is a named requirement a list of types may satisfy — `Addable`, `Orderable`, `Comparable`. **A trait is not a type**: no `Type` variant, no lattice point, no subtyping edge, and the type grammar and `constrain_go`'s rules are untouched. Types *satisfy* traits. +* An **implementation** is one row of a trait's table: the types it accepts, and the types it associates with them. Written `Addable(Int, Int ⇝ Int)` — accepted types, then `⇝`, then the associated ones. * An **associated type** is a type a trait *names* — `Output`, the type an arithmetic operator's result takes. A trait is a requirement rather than a function, so it associates any number, **including none**. A type is associated only when it *depends* on the types satisfying the trait: a comparison's `Bool` is the same for every pair `Equatable` accepts, so it belongs to the operator's signature and `Equatable` associates nothing — recording it as an association would claim the trait determines something it does not. * An **obligation** is one recorded instance of a trait at specific type positions: one **operand position** per argument the trait takes, and one **associated position** per type it names. It is a single claim with two halves, and neither alone is the obligation: *the operand positions are types some implementation accepts*, **and** *each associated position is what that implementation associates*. Every position is an ordinary inference variable, unrelated to the others. @@ -1147,18 +1147,45 @@ An operator's signature is therefore `𝐴₁ → … → 𝐴ₙ → 𝑅` plus | operator | signature | obligation | |---|---|---| -| `+` | `∀ 𝐴 𝐵 𝑂. 𝐴 → 𝐵 → 𝑂` | `Addable(𝐴, 𝐵)`, `Output` at `𝑂` | -| `==` | `∀ 𝐴 𝐵. 𝐴 → 𝐵 → Bool` | `Equatable(𝐴, 𝐵)`, nothing associated | -| unary `-` | `∀ 𝐴 𝑂. 𝐴 → 𝑂` | `Negatable(𝐴)`, `Output` at `𝑂` | +| `+` | `∀ 𝐴 𝐵 𝑂. 𝐴 → 𝐵 → 𝑂` | `Addable(𝐴, 𝐵 ⇝ 𝑂)` | +| `==` | `∀ 𝐴 𝐵. 𝐴 → 𝐵 → Bool` | `Equatable(𝐴, 𝐵)` | +| unary `-` | `∀ 𝐴 𝑂. 𝐴 → 𝑂` | `Negatable(𝐴 ⇝ 𝑂)` | Mechanism: `src/ccl/infer/solver/traits.rs`. Because an associated position like `𝑂` is an ordinary variable rather than a marker standing for a computation, information flows *backwards* through an operator's result and misusing that result is an ordinary diagnostic — `(1 + 2) and True` fails as a bound conflict. A computed-type marker cannot have this property: the solver cannot compare an unreduced computation against anything, so a function could not be typechecked without seeing its call sites. +### A trait is a relation, and today it relates only types + +The notation is a relation because a trait *is* one. A trait over `𝑁` operand +positions, `𝐴` associated types and `𝐹` associated **functions** is an +`(𝑁 + 𝐴 + 𝐹)`-ary relation in which the `𝑁` operand types functionally determine the +`𝐴` types and the `𝐹` functions — which is what the `⇝` separates. An implementation +is one hyper-edge of that relation, and discharge is the search for a hyper-edge +consistent with what inference has determined about the operand positions. + +Cambra implements `𝑁 ∈ {1, 2}`, `𝐴 ∈ {0, 1}` (`Output`, or nothing) and **`𝐹 = 0`**, +with the relation built into the compiler rather than declared in CHL. Read `𝐹 = 0` as +a gap and not as the design: an implementation's rows *have* distinct functions, and a +trait that cannot associate one cannot say which. `Addable` is the example — the row +`Addable(String, String ⇝ String)` denotes string concatenation and +`Addable(Int, Int ⇝ Int)` denotes integer addition, and because the obligation carries +neither, the function is recovered twice over outside the trait: `simplify.rs` rewrites +the `String` case to `Concat` (see [BinOp type rules](#binop-type-rules)), and the +interpreter then picks the machine operation from the operand column's runtime +representation (`apply_binop_column`, in `src/interpreter/binop.rs`). The type system +narrows to a row of types and then declines to name the code. + +Associating functions, and a CHL surface for declaring the relation, are the two +extensions this shape exists to take: the implementations are already *data* +(`Trait::impls`), so both are table extensions rather than new mechanisms. + ### Refinements are transparent `{𝑇 | 𝑝}` satisfies a trait exactly when `𝑇` does. This holds *by construction*: satisfaction is judged on each bound contribution as it arrives, with refinements peeled at that moment — when the base actually exists. An operand is usually still an inference variable at emission, so a peel performed *there* would have nothing to work on. +Transparency is permanent, and it is a consequence of incremental discharge rather than a simplification on top of it. A candidate set only ever shrinks (see [Discharge is incremental](#discharge-is-incremental)), and a refinement is one of the things a bound can deliver *late*. If `{𝑇 | 𝑝}` could satisfy a requirement `𝑇` does not, a refinement arriving after the base would have to re-admit a candidate already dropped, and discharge would stop being monotone — order would start to matter. Growing `𝐹` above zero does not change this: choosing between two functions by `𝑝` is dispatch on a fact about a *value*, which a table keyed on types cannot express and which no refinement survives anyway (`𝑥 + 𝑥` where `𝑥` is `2` produces `4`). + ### Discharge is incremental An obligation is a monotone fact discharged as the graph fills in, the shape [`FunKindVar`](#46-data-vs-compute-functions) already uses for kinds — not a sweep at the end of solving. Each operand position carries a **candidate set** of implementations that only ever shrinks; each associated type is deposited on its position as an ordinary lower bound as soon as every surviving candidate agrees on it. Order therefore does not matter. @@ -1175,7 +1202,7 @@ The deposit rule is *whatever every surviving implementation agrees on*, applied The asymmetry is not soundness — with one candidate left, its operand types are implied exactly as its associated types are. It is that the obligation is an associated position's **only** source of information and never an operand's: an associated position is a fresh variable nothing else constrains from below, while an operand always has the program's own `operandᵢ <: 𝐴ᵢ` edge. Determining an operand from the table would be recovering information the program was supposed to supply, which hides an under-connected lowering instead of fixing it. -How much gets determined is therefore a property of the table, and shrinks as the table grows — **for the output too**. Today `λ 𝑥 → 𝑥 + 1` is `∀𝐴 𝑂. (𝐴 : Addable(𝐴, Int)) ⇒ 𝐴 → 𝑂` with `𝑂` resolving to `Int`, because `Int` in the second position leaves only `(Int, Int) ⇝ Int`. Adding `Addable(Float, Int) ⇝ Float` would leave two candidates whose outputs disagree, and the result would become as open as the parameter already is. That is the type honestly tracking a language that has become more permissive, and it is why the deposit waits for *agreement* rather than firing on a unique candidate. +How much gets determined is therefore a property of the table, and shrinks as the table grows — **for the output too**. Today `λ 𝑥 → 𝑥 + 1` is `∀𝐴 𝑂. (𝐴 : Addable(𝐴, Int ⇝ 𝑂)) ⇒ 𝐴 → 𝑂` with `𝑂` resolving to `Int`, because `Int` in the second position leaves only `Addable(Int, Int ⇝ Int)`. Adding `Addable(Float, Int ⇝ Float)` would leave two candidates whose outputs disagree, and the result would become as open as the parameter already is. That is the type honestly tracking a language that has become more permissive, and it is why the deposit waits for *agreement* rather than firing on a unique candidate. ### Delivery: the watch follows the edge diff --git a/src/ccl/infer/solver/traits.rs b/src/ccl/infer/solver/traits.rs index ccce4eb6..c7cdb906 100644 --- a/src/ccl/infer/solver/traits.rs +++ b/src/ccl/infer/solver/traits.rs @@ -3,42 +3,34 @@ //! //! # Vocabulary //! -//! - A **trait** is a named requirement a type may satisfy — `Addable`, `Orderable`. -//! It is **not a type**: nothing here adds a [`Type`] variant, a lattice point or a -//! subtyping edge, and the type grammar and `constrain_go`'s rules are untouched. +//! - A **trait** ([`Trait`]) is a named requirement a *list* of types may satisfy — +//! `Addable`, `Orderable`. It is **not a type**: nothing here adds a [`Type`] +//! variant, a lattice point or a subtyping edge, and the type grammar and +//! `constrain_go`'s rules are untouched. //! - An **implementation** ([`TraitImpl`]) is one row of a trait's table: the types it -//! accepts, and the types it associates with them. +//! accepts, and the types it associates with them — written +//! `Addable(Int, Int ⇝ Int)`, accepted types then `⇝` then associated ones. //! - An **associated type** ([`Assoc`]) is a type a trait *names* — `Output`, the type -//! an arithmetic operator's result takes. A trait is a requirement rather than a -//! function, so it associates any number, **including none**. A type is associated -//! only when it *depends* on the types satisfying the trait: a comparison's `Bool` is -//! the same for every pair `Equatable` accepts, so it belongs to the operator's -//! signature (`OperatorResult::Fixed`, in `src/ccl/infer/schemes.rs`) and -//! `Equatable` associates nothing. +//! an arithmetic operator's result takes. A trait associates any number, **including +//! none**: only a type that *depends* on the types satisfying the trait belongs here, +//! so `Equatable` associates nothing and its `Bool` rides the operator's signature +//! instead (`OperatorResult::Fixed`, in `src/ccl/infer/schemes.rs`). //! - An **obligation** ([`TraitObligation`]) is one recorded instance of a trait at //! specific type positions: one **operand position** per argument the trait takes, -//! and one **associated position** per type it names. It is a single claim with two -//! halves, and neither alone is "the obligation": *the operand positions are types -//! some implementation accepts*, **and** *each associated position is what that -//! implementation associates*. Every position is an ordinary inference variable, -//! unrelated to the others. (`Addable(𝐴, 𝐵)` with `Output` at `𝑂` is the shape to -//! picture, but the arity and the association count are both the trait's.) -//! - A **watch** is an obligation's attachment to an operand variable, which is how a -//! bound landing anywhere in the program reaches it. +//! and one **associated position** per type it names — `Addable(𝐴, 𝐵 ⇝ 𝑂)` is the +//! shape to picture, though the arity and the association count are both the trait's. +//! It is a single claim with two halves, and neither alone is "the obligation": *the +//! operand positions are types some implementation accepts*, **and** *each associated +//! position is what that implementation associates*. Every position is an ordinary +//! inference variable, unrelated to the others. +//! - A **watch** is an obligation's attachment to an operand variable +//! ([`TraitObligation::watch`]), which is how a bound landing anywhere in the program +//! reaches it. //! -//! An operator's signature is therefore `𝐴₁ → … → 𝐴ₙ → 𝑅` plus the obligation, for the -//! trait's arity `𝑛`, where `𝑅` is either one of the associated positions or a type -//! the operator fixes — which operator states which is `schemes.rs`'s business, not -//! this module's. Because an associated position is an -//! ordinary variable rather than a marker standing for a computation, information -//! flows *backwards* through an operator's result like any other type — which is what -//! lets a function be typechecked without consulting its call sites. -//! -//! # Refinements are transparent -//! -//! `{𝑇 | 𝑝}` satisfies a trait exactly when `𝑇` does, by construction rather than by -//! a stripping step: satisfaction is judged on each bound contribution as it arrives, -//! with refinements peeled at that moment — when the base actually exists. +//! Every position being an ordinary inference variable — not a marker standing for an +//! unreduced computation — is what lets information flow *backwards* out of an +//! operator's result, and so what lets a function be typechecked without consulting its +//! call sites. //! //! # Discharge is incremental //! @@ -46,30 +38,24 @@ //! [`FunKindVar`](crate::ccl::ty::FunKindVar) already uses for kinds; no phase runs //! "once everything is known". Each operand position carries a **candidate set** of //! implementations that only ever shrinks ([`TraitObligation::narrow`]), and each -//! associated type is deposited on its position as an ordinary lower bound as soon as -//! every surviving candidate agrees on it ([`TraitObligation::try_deposit`]). -//! -//! # What an obligation determines, and what it leaves alone +//! associated type is deposited on its position as an ordinary lower bound once every +//! surviving candidate *agrees* on it ([`TraitObligation::try_deposit`]) — agreement, +//! not a lone survivor. A deposit reaches **associated positions only**; nothing is +//! ever written back onto an operand. //! -//! The deposit rule is *whatever every surviving implementation agrees on*, and it is -//! applied to the **associated positions only**. Nothing is ever deposited onto an -//! operand. +//! A refinement narrows exactly as its base does: `{𝑇 | 𝑝}` satisfies a trait when `𝑇` +//! does, because satisfaction is judged on each bound contribution as it arrives and +//! peels refinements at that moment — when the base actually exists. //! -//! The asymmetry is not soundness — with one candidate left, its operand types are -//! implied exactly as its associated types are. It is that the obligation is an -//! associated position's **only** source of information and never an operand's: an -//! associated position is a fresh variable nothing else constrains from below, while -//! an operand always has the program's own `operandᵢ <: 𝐴ᵢ` edge. Determining an operand from the table would be recovering -//! information the program was supposed to supply, which hides an under-connected -//! lowering instead of fixing it. +//! # Where to read more //! -//! How much gets determined is therefore a property of the table, and shrinks as the -//! table grows — **for an associated type too**. Today `λ 𝑥 → 𝑥 + 1` has result `Int`, -//! because `Int` in the second position leaves only `(Int, Int) ⇝ Int`. Adding -//! `Addable(Float, Int) ⇝ Float` would leave two candidates whose outputs disagree, -//! and the result would become as open as the parameter already is. That is the type -//! honestly tracking a language that has become more permissive, and it is why the -//! deposit waits for *agreement* rather than firing on a unique candidate. +//! `src/ccl/design/type-inference.md`, "Traits" is the design of record, and carries +//! the arguments this module only acts on: why the constraint lattice cannot state an +//! operator's requirement on its own, why a deposit is one-way and waits for agreement, +//! why refinement transparency is permanent rather than a convenience, and what a trait +//! would relate beyond types — associated *functions*, which the shape here allows and +//! does not yet have. Which operators state which requirement, and which take a fixed +//! result rather than an associated one, is `schemes.rs`'s business, not this module's. use std::cell::{Cell, RefCell}; use std::fmt; @@ -300,8 +286,8 @@ static OBLIGATION_COUNTER: AtomicU32 = AtomicU32::new(0); /// One recorded instance of a trait at specific type positions, carrying both halves /// of the claim: that the operand positions are types some implementation accepts, and /// that each associated position is what that implementation associates. Arity and -/// association count are the trait's — `Addable(𝐴, 𝐵)` with `Output` at `𝑂` is one -/// shape, `Negatable(𝐴)` with `Output` and `Equatable(𝐴, 𝐵)` with none are the others. +/// association count are the trait's — `Addable(𝐴, 𝐵 ⇝ 𝑂)` is one shape, +/// `Negatable(𝐴 ⇝ 𝑂)` and `Equatable(𝐴, 𝐵)` are the others. /// See this module's *Vocabulary*. /// /// Held by [`Rc`] and *watched* by each operand variable ([`TraitObligation::watch`]), From 34b0d63c522fd7820e36af3a8653f71056a313ae Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 12 Aug 2026 21:47:07 -0700 Subject: [PATCH 3/6] Rebase fallout: two consequences of meeting #89's never-called typechecking MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #89 resolves a definition nobody calls, which puts two of its results in contact with this branch. **A gap becomes observable.** Narrowing is delivery-driven, so a conflict that is only a trait conflict is not reached in a definition that delivers nothing: `f = \a -> (a + 1, a + "s")` places two requirements on `a`, each satisfiable alone and jointly not. Under the equality rule the two `+`s collided structurally, so resolution found it. This is the residual gap #89 already names; the two cases keep their coverage, as a test asserting they are *accepted*, so the gap has a name rather than being an absence. Called, both are still rejected, and name the trait, the operand position, and what that position accepts. **A performance guard's calibration moves.** Stating what an operator requires of each operand makes a concrete specialization far cheaper — over the doubling chain the live case drops ~437x against the dead one's ~109x — so the factor picked against the old numbers no longer holds. The bound is now the module's own claim, that dead must not cost *more* than live, rather than a factor calibrated to one measurement; `DEPTH` is 6 because that is where sharing (0.81x) and a lost memo (1.54x) are furthest apart. --- src/ccl/design/type-inference.md | 6 ++++++ tests/dead_code_specialization_cost.rs | 17 +++++++++------ tests/type_check.rs | 30 +++++++++++++++++++++----- 3 files changed, 41 insertions(+), 12 deletions(-) diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index b09fe18f..73d132b9 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -1218,6 +1218,12 @@ That the list is closed is an argument about today's code, not something the com Obligations ride variables through `freshen_above`, so a generalized function carries its operators' requirements into its scheme. Each use instantiates and discharges its **own** copy — sharing one would let a `String` use empty an `Int` use's candidate set. +### A definition nobody calls delivers nothing + +Narrowing is driven by delivery, so an obligation whose operands never receive a base narrows nothing and rejects nothing. That is exactly the residual gap named in [Typechecking a never-called definition](#typechecking-a-never-called-definition), and stating operator requirements rather than operand equality is what makes it observable: `f = λ𝑎 → (𝑎 + 1, 𝑎 + "s")` places two requirements on `𝑎`, each satisfiable alone and jointly not, and no delivery reaches either while `f` is uncalled. Under an equality rule the two `+`s collided structurally instead, so the conflict was a bound conflict and resolution found it. + +The requirements are still *recorded*, and jointly reading them is what would reject it — an unsatisfiable **intersection** of the requirements on one variable is visible with no delivery at all. That belongs to the obligation machinery rather than to the discard walk, and is not part of this change; `a_never_called_function_whose_conflict_is_only_a_trait_conflict_is_not_reached` holds the two cases so the gap has a name and a test rather than being an absence. Called, both are rejected, and with a better message than the equality rule gave: the trait, the operand position, and what that position accepts. + --- ## 5. CCL-specific inference rules diff --git a/tests/dead_code_specialization_cost.rs b/tests/dead_code_specialization_cost.rs index 32654394..795e4239 100644 --- a/tests/dead_code_specialization_cost.rs +++ b/tests/dead_code_specialization_cost.rs @@ -55,16 +55,19 @@ fn inference_allocations(code: &str) -> usize { #[test] fn a_dead_call_chain_does_not_cost_more_than_a_live_one() { - const DEPTH: usize = 4; + const DEPTH: usize = 6; let live = inference_allocations(&chain(DEPTH, true)); let dead = inference_allocations(&chain(DEPTH, false)); - // Dead does the same specialization work as live and then splices none of it, so - // it should come in *well* under. The factor is a calibrated guard rather than a - // law — measured at this depth, sharing gives `dead ≈ 0.28 × live`, and a lost - // memo gives `≈ 0.94 ×` (and exceeds `live` outright one level deeper). Halfway - // between leaves room for ordinary drift while still catching the regression. + // The bound is the module's claim itself — dead must not cost *more* than live — + // rather than a factor picked to sit under one measurement. Both sides are + // exponential in `DEPTH` (the chain's own term doubles per level), so the memo + // buys a factor, not an order; measured here, sharing gives `dead ≈ 0.81 × live` + // and declining to register a discarded use gives `≈ 1.54 ×`. `DEPTH` is 6 + // because that is where the two are furthest apart: below it the fixed cost of + // inference dilutes both, and above it the shared curve creeps toward `live` as + // the concrete specialization the live case adds stops dominating. assert!( - dead * 2 <= live, + dead <= live, "typechecking a never-called chain allocated {dead}, against {live} for the \ same code live: the specialization memo is not being shared across uses \ inside the discarded subtree" diff --git a/tests/type_check.rs b/tests/type_check.rs index ed1f7b53..d2a9362d 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -491,7 +491,6 @@ fn dead_code(defs: &str) -> String { #[case::conflicting_projections_nested("f = \\r -> (r.x.0, r.x.foo)")] #[case::conflicting_projections_curried("f = \\a -> \\b -> a.0 + a.foo")] #[case::monomorphic_param_at_two_types("f = \\g -> g(1) + g(\"s\")")] -#[case::conflicting_operand_types("f = \\a -> (a + 1, a + \"s\")")] #[case::through_a_call_in_dead_code(indoc! {r#" g = \x -> x + 1 f = \a -> g("s") @@ -538,10 +537,6 @@ fn dead_code(defs: &str) -> String { f = \a -> a.0 + a.foo f = 3 "#})] -#[case::annotated_param(indoc! {r#" - def f(x: Int): - x + "s" -"#})] fn a_never_called_function_is_still_typechecked(#[case] defs: &str) { assert!( !infer_program_err(&dead_code(defs)).is_empty(), @@ -549,6 +544,31 @@ fn a_never_called_function_is_still_typechecked(#[case] defs: &str) { ); } +/// The gap the previous test stops at, and the reason it is a gap: an obligation +/// narrows as bases are *delivered* to it, and a never-called definition delivers +/// nothing, so a conflict that is only a trait conflict is not reached — see +/// `src/ccl/design/type-inference.md`, "Typechecking a never-called definition". +/// +/// Both bodies are rejected the moment they are called (`f(1)` on either names the +/// operand, its type, and what the position accepts), so this is about *when* the +/// conflict is found, not whether. What makes them unreachable here is that neither +/// asks any one delivery to be impossible: the first places two requirements on `a` +/// — `a + 1` fixes it at `Int`, `a + "s"` at `String` — each satisfiable alone and +/// jointly not, and the second sets a requirement against an annotation. Reading a +/// value's requirements together is what closes both, and that is a property of the +/// obligation machinery rather than of the discard walk. +#[rstest] +#[case::conflicting_operand_types("f = \\a -> (a + 1, a + \"s\")")] +#[case::annotated_param(indoc! {r#" + def f(x: Int): + x + "s" +"#})] +fn a_never_called_function_whose_conflict_is_only_a_trait_conflict_is_not_reached( + #[case] defs: &str, +) { + assert_eq!(infer_program(&dead_code(defs)), int_lit(1)); +} + /// The complement, and the guard against the walk over-rejecting: typechecking a /// never-called definition is not the same as demanding it be *monomorphic*. Its /// quantified variables have no use-site bounds, so it resolves under-determined — From e9cf7798c151dccd145c227325419a533b378e0b Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Thu, 13 Aug 2026 11:49:20 -0700 Subject: [PATCH 4/6] Docs: state the trait design rather than narrate arriving at it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Traits section read as an argument for the design instead of a description of it. Three habits, removed throughout: **A fixed defect used as the rationale.** `Discharge is incremental` justified its three-way classification by recounting that `(1, 2) == (3, 4)` once type-checked. The distinction is now stated forward, as a table of contribution kinds and outcomes, with that program as an illustration of why "determined and not a base" is a rejection rather than silence. **Counterfactual as the main clause.** "The asymmetry is not soundness —", "Read `F = 0` as a gap and not as the design", "The notation is a relation because a trait *is* one". Each states the rule first now, with the alternative it rules out following where it earns the space. **Editorial voice.** "That is the type honestly tracking a language that has become more permissive", "worth reading twice". Cut. Two prose blocks that were carrying tabular content — the contribution classification and the four lower-bound writers — become a table and a list. No claim changes. --- src/ccl/design/type-inference.md | 75 +++++++++++++++++++------------- 1 file changed, 44 insertions(+), 31 deletions(-) diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index 73d132b9..2732e522 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -1153,28 +1153,29 @@ An operator's signature is therefore `𝐴₁ → … → 𝐴ₙ → 𝑅` plus Mechanism: `src/ccl/infer/solver/traits.rs`. -Because an associated position like `𝑂` is an ordinary variable rather than a marker standing for a computation, information flows *backwards* through an operator's result and misusing that result is an ordinary diagnostic — `(1 + 2) and True` fails as a bound conflict. A computed-type marker cannot have this property: the solver cannot compare an unreduced computation against anything, so a function could not be typechecked without seeing its call sites. +An associated position like `𝑂` is an ordinary inference variable, not a marker standing for a computation. So information flows *backwards* through an operator's result, and misusing that result is an ordinary diagnostic: `(1 + 2) and True` fails as a bound conflict. A marker could not do this — the solver cannot compare an unreduced computation against anything — and a function could then not be typechecked without seeing its call sites. ### A trait is a relation, and today it relates only types -The notation is a relation because a trait *is* one. A trait over `𝑁` operand -positions, `𝐴` associated types and `𝐹` associated **functions** is an -`(𝑁 + 𝐴 + 𝐹)`-ary relation in which the `𝑁` operand types functionally determine the -`𝐴` types and the `𝐹` functions — which is what the `⇝` separates. An implementation -is one hyper-edge of that relation, and discharge is the search for a hyper-edge -consistent with what inference has determined about the operand positions. +A trait over `𝑁` operand positions, `𝐴` associated types and `𝐹` associated +**functions** is an `(𝑁 + 𝐴 + 𝐹)`-ary relation in which the `𝑁` operand types +functionally determine the `𝐴` types and the `𝐹` functions; `⇝` separates the +determining side from the determined one. An implementation is one hyper-edge, and +discharge is the search for a hyper-edge consistent with what inference has determined +about the operand positions. Cambra implements `𝑁 ∈ {1, 2}`, `𝐴 ∈ {0, 1}` (`Output`, or nothing) and **`𝐹 = 0`**, -with the relation built into the compiler rather than declared in CHL. Read `𝐹 = 0` as -a gap and not as the design: an implementation's rows *have* distinct functions, and a -trait that cannot associate one cannot say which. `Addable` is the example — the row -`Addable(String, String ⇝ String)` denotes string concatenation and -`Addable(Int, Int ⇝ Int)` denotes integer addition, and because the obligation carries -neither, the function is recovered twice over outside the trait: `simplify.rs` rewrites -the `String` case to `Concat` (see [BinOp type rules](#binop-type-rules)), and the -interpreter then picks the machine operation from the operand column's runtime -representation (`apply_binop_column`, in `src/interpreter/binop.rs`). The type system -narrows to a row of types and then declines to name the code. +with the relation built into the compiler rather than declared in CHL. + +`𝐹 = 0` is a gap rather than a decision. An implementation's rows *do* denote distinct +functions — `Addable(String, String ⇝ String)` is concatenation and +`Addable(Int, Int ⇝ Int)` is integer addition — and a trait that cannot associate a +function cannot say which. The function is therefore recovered twice outside the trait: +`simplify.rs` rewrites the `String` case to `Concat` (see +[BinOp type rules](#binop-type-rules)), and the interpreter picks the machine operation +from the operand column's runtime representation (`apply_binop_column`, in +`src/interpreter/binop.rs`). The type system narrows to a row of types and then declines +to name the code. Associating functions, and a CHL surface for declaring the relation, are the two extensions this shape exists to take: the implementations are already *data* @@ -1182,37 +1183,49 @@ extensions this shape exists to take: the implementations are already *data* ### Refinements are transparent -`{𝑇 | 𝑝}` satisfies a trait exactly when `𝑇` does. This holds *by construction*: satisfaction is judged on each bound contribution as it arrives, with refinements peeled at that moment — when the base actually exists. An operand is usually still an inference variable at emission, so a peel performed *there* would have nothing to work on. +`{𝑇 | 𝑝}` satisfies a trait exactly when `𝑇` does. This holds by construction: satisfaction is judged on each bound contribution as it arrives, and refinements are peeled at that moment, when the base exists. Peeling at emission instead would have nothing to work on, an operand usually being still a variable there. -Transparency is permanent, and it is a consequence of incremental discharge rather than a simplification on top of it. A candidate set only ever shrinks (see [Discharge is incremental](#discharge-is-incremental)), and a refinement is one of the things a bound can deliver *late*. If `{𝑇 | 𝑝}` could satisfy a requirement `𝑇` does not, a refinement arriving after the base would have to re-admit a candidate already dropped, and discharge would stop being monotone — order would start to matter. Growing `𝐹` above zero does not change this: choosing between two functions by `𝑝` is dispatch on a fact about a *value*, which a table keyed on types cannot express and which no refinement survives anyway (`𝑥 + 𝑥` where `𝑥` is `2` produces `4`). +Transparency follows from incremental discharge and is permanent. A candidate set only ever shrinks ([Discharge is incremental](#discharge-is-incremental)), and a refinement is one of the things a bound can deliver late; if `{𝑇 | 𝑝}` could satisfy a requirement `𝑇` does not, a refinement arriving after the base would have to re-admit a dropped candidate, and order would start to matter. + +Growing `𝐹` above zero would not change this. Choosing between two functions by `𝑝` is dispatch on a fact about a *value*, which a table keyed on types cannot express — and which no refinement survives in any case: `𝑥 + 𝑥` where `𝑥` is `2` produces `4`. ### Discharge is incremental -An obligation is a monotone fact discharged as the graph fills in, the shape [`FunKindVar`](#46-data-vs-compute-functions) already uses for kinds — not a sweep at the end of solving. Each operand position carries a **candidate set** of implementations that only ever shrinks; each associated type is deposited on its position as an ordinary lower bound as soon as every surviving candidate agrees on it. Order therefore does not matter. +An obligation is a monotone fact, discharged as the graph fills in rather than by a sweep at the end of solving — the shape [`FunKindVar`](#46-data-vs-compute-functions) already uses for kinds. Each operand position carries a **candidate set** of implementations that only ever shrinks; each associated type is deposited on its position as an ordinary lower bound once every surviving candidate agrees on it. Order therefore does not matter. + +A contribution arriving at a position is one of three things, and each has its own outcome: -What arrives at a position is classified three ways, and the third is easy to miss: a contribution either offers a **base**, is **not determined yet** (an inference variable, a hole, a transient `Feed` handle whose payload arrives separately), or is **determined and not a base** (a tuple, record, variant or function). The first narrows; the third is rejected outright, because no implementation can ever accept it; only the second is genuinely "nothing to say". +| contribution | example | outcome | +|---|---|---| +| a **base** | `Int` | narrows the candidate set | +| **not determined yet** | a variable, a hole, a `Feed` handle whose payload arrives separately | nothing to say | +| **determined and not a base** | a tuple, record, variant, function | rejected — no implementation can accept it | -Collapsing the last two is a live hazard rather than a hypothetical. While "no base here" meant "no information", `(1, 2) == (3, 4)` type-checked as `Bool`: a tuple narrowed nothing, and a comparison has no associated position to leave unresolved, so no later wall saw it either. The same hole let `max` accept a tuple codomain. +The third is a rejection and not silence, because "no base here" is true of both it and the second. A tuple that merely failed to narrow would leave `(1, 2) == (3, 4)` well-typed: a comparison has no associated position to strand, so nothing downstream would object either. -What narrowing cannot reject is a position the program never determines — which is the honest outcome, reported as an unresolved variable rather than as a missing implementation. +A position the program never determines is not a rejection: it is reported as an unresolved variable rather than as a missing implementation. -### What an obligation determines, and what it leaves alone +### What an obligation determines -The deposit rule is *whatever every surviving implementation agrees on*, applied to the **associated positions only**. Nothing is ever deposited onto an operand. +A deposit records what every surviving implementation agrees on, and reaches the **associated positions only**. Nothing is written back onto an operand. -The asymmetry is not soundness — with one candidate left, its operand types are implied exactly as its associated types are. It is that the obligation is an associated position's **only** source of information and never an operand's: an associated position is a fresh variable nothing else constrains from below, while an operand always has the program's own `operandᵢ <: 𝐴ᵢ` edge. Determining an operand from the table would be recovering information the program was supposed to supply, which hides an under-connected lowering instead of fixing it. +The asymmetry is about where information comes from, not about soundness — with one candidate left, its operand types are implied exactly as its associated types are. An associated position is a fresh variable nothing else constrains from below, so the obligation is its only source. An operand always has the program's own `operandᵢ <: 𝐴ᵢ` edge. Determining an operand from the table would supply information the program was meant to supply, which hides an under-connected lowering rather than exposing it. -How much gets determined is therefore a property of the table, and shrinks as the table grows — **for the output too**. Today `λ 𝑥 → 𝑥 + 1` is `∀𝐴 𝑂. (𝐴 : Addable(𝐴, Int ⇝ 𝑂)) ⇒ 𝐴 → 𝑂` with `𝑂` resolving to `Int`, because `Int` in the second position leaves only `Addable(Int, Int ⇝ Int)`. Adding `Addable(Float, Int ⇝ Float)` would leave two candidates whose outputs disagree, and the result would become as open as the parameter already is. That is the type honestly tracking a language that has become more permissive, and it is why the deposit waits for *agreement* rather than firing on a unique candidate. +How much is determined follows from the table, associated positions included. `λ 𝑥 → 𝑥 + 1` is `∀𝐴 𝑂. (𝐴 : Addable(𝐴, Int ⇝ 𝑂)) ⇒ 𝐴 → 𝑂` with `𝑂` resolving to `Int`, because `Int` at the second position leaves only `Addable(Int, Int ⇝ Int)`. Adding `Addable(Float, Int ⇝ Float)` would leave two rows whose outputs disagree, and `𝑂` would be as open as `𝐴` already is — which is why a deposit waits for agreement rather than firing on a unique candidate. ### Delivery: the watch follows the edge -An obligation is attached to each operand variable as a *watch* (`InferVar::watches`), and everything the invariant rests on is **delivery** — a concrete type reaching an operand variable has to reach the obligation watching it. +An obligation is attached to each operand variable as a *watch* (`InferVar::watches`). The invariant is **delivery**: a concrete type reaching an operand variable must reach the obligation watching it. + +The bound closure does not deliver on its own. Where two variables sit at different polymorphism levels — as a `let` RHS produces, being emitted one level deeper — their edge is recorded by the arm whose closure runs against the *other* side's bounds, so a type already on the lower variable is never re-offered. The graph stays correct but is only *transitively* readable, which coalesce does and emission does not. -The bound closure does not deliver on its own. When two variables sit at different polymorphism levels — which is what a `let` RHS produces, being emitted one level deeper — their edge is recorded by the arm whose closure runs against the *other* side's bounds, so a type already sitting on the lower variable is never re-offered. The graph is still correct, but only *transitively* readable, which is something coalesce does and emission does not. +A variable's lower bounds are written in exactly four places, and delivery is wired into each: -A variable's lower bounds are written in exactly four places, and delivery is wired into every one: `constrain_go`'s two variable arms (a concrete contribution is delivered directly; a var-var edge propagates the watch *downward*, toward the variables feeding the watched one, and delivers what they already know), `extrude`'s proxy seeding, and `freshen_above`'s clone — the latter two because both seed bounds by direct writes rather than through `constrain_go`. +* `constrain_go`'s concrete arm — delivers the contribution directly. +* `constrain_go`'s var-var arm — propagates the watch *downward*, toward the variables feeding the watched one, and delivers what they already know. +* `extrude`'s proxy seeding, and `freshen_above`'s clone — both seed bounds by direct writes rather than through `constrain_go`. -That the list is closed is an argument about today's code, not something the compiler enforces, and a missed delivery is quiet: the obligation simply never narrows, so a type is left undetermined and surfaces phases later on an interior node. `verify_narrowing_is_complete` therefore checks the argument rather than trusting it — after emission, every watched operand is resolved against the completed graph, and a resolved base must already have narrowed its obligation. `a_concrete_operand_reaches_its_obligation` covers the four writers with a case per mechanism. +That the list is closed is an argument about today's code, not something the compiler enforces, and a missed delivery is quiet: the obligation never narrows, so a type is left undetermined and surfaces phases later on an interior node. `verify_narrowing_is_complete` checks the argument instead of trusting it — after emission, every watched operand is resolved against the completed graph, and a resolved base must already have narrowed its obligation. `a_concrete_operand_reaches_its_obligation` covers the four writers, a case per mechanism. ### Requirements are generalized From 24edf65a44dc037df60e80fa005eafb999c68b5d Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Thu, 13 Aug 2026 11:49:31 -0700 Subject: [PATCH 5/6] Tests: embedded programs read as programs, not as escaped newlines MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The convention `CLAUDE.md` records — `indoc!` for a multi-line program, never a single string with `\n` — with its corollary applied rather than the rule alone: a fixed line every case shares belongs in the test body, so a case carries only its own content and a genuine one-liner stays a plain string. `a_generalized_function_instantiates_its_operator_requirements` is the case where that matters most: three programs shared a definition and differed only in the uses, so the definition is hoisted and each program is one visible line of source. The register-cycle cases are the reverse — every one is a seed, a self-referential write and a read, which is a shape you cannot see in `"x := 0\nx := x + 1\nx"`. --- tests/type_check.rs | 140 +++++++++++++++++++++++++++++++++++--------- 1 file changed, 112 insertions(+), 28 deletions(-) diff --git a/tests/type_check.rs b/tests/type_check.rs index d2a9362d..d4280587 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -181,8 +181,15 @@ fn test_binary_op(#[case] code: &str, #[case] expected: BaseType) { /// `x` is `2` claimed the sum was `2`. Distinct singletons intersect to nothing, /// which is why the other two cases pass either way. #[rstest] -#[case::same_variable_twice("x = 2\nx + x")] -#[case::distinct_singletons("x = 2\ny = 3\nx + y")] +#[case::same_variable_twice(indoc! {r#" + x = 2 + x + x +"#})] +#[case::distinct_singletons(indoc! {r#" + x = 2 + y = 3 + x + y +"#})] #[case::literals("2 + 2")] fn an_operator_result_carries_no_operand_refinement(#[case] code: &str) { assert_eq!(infer_program(code), int()); @@ -322,13 +329,13 @@ fn misusing_an_operator_result_is_an_ordinary_diagnostic(#[case] code: &str) { /// candidate set. #[test] fn a_generalized_function_instantiates_its_operator_requirements() { - assert_eq!(infer_program("f = \\a, b -> a + b\nf(1, 2)"), int()); - assert_eq!( - infer_program("f = \\a, b -> a + b\nf(\"x\", \"y\")"), - string() - ); + // One definition, three programs: only the uses differ, so only the uses are + // written out. + let using = |uses: &str| format!("f = \\a, b -> a + b\n{uses}"); + assert_eq!(infer_program(&using("f(1, 2)")), int()); + assert_eq!(infer_program(&using(r#"f("x", "y")"#)), string()); assert_eq!( - infer_program("f = \\a, b -> a + b\n(f(1, 2), f(\"x\", \"y\"))"), + infer_program(&using(r#"(f(1, 2), f("x", "y"))"#)), Type::Tuple(vec![int(), string()]) ); } @@ -348,16 +355,28 @@ fn a_generalized_function_instantiates_its_operator_requirements() { // one level deeper than the loop binder, so `⟨binder⟩ <: A` is recorded by the arm // that closes against `A`'s uppers and never re-offers the `Int` already sitting on // the binder. Delivery has to follow the var-var edge downward instead. -#[case::across_a_level_boundary("s := 0\nfor i in [1, 2, 3]:\n y = s + i\n s := y\ns")] +#[case::across_a_level_boundary(indoc! {r#" + s := 0 + for i in [1, 2, 3]: + y = s + i + s := y + s +"#})] // `extrude`: a generalized multi-argument function is emitted a level deeper than its // use, so constraining its tuple parameter down to the use's level mints proxies // whose bounds are seeded by *direct writes* rather than through `constrain_go`. The // nesting matters — the outer operator's operand is the inner operator's output, and // that is the variable that gets approximated. -#[case::through_an_extrusion_proxy("m = \\a, b -> a * b + 1\nm(3, 4)")] +#[case::through_an_extrusion_proxy(indoc! {r#" + m = \a, b -> a * b + 1 + m(3, 4) +"#})] // `freshen_above`: each use of a generalized function instantiates its own copy of // the obligation, which has to be reachable from the freshened operand variables. -#[case::through_a_freshened_instantiation("k = \\a, b -> a + b\nk(k(1, 2), 3)")] +#[case::through_a_freshened_instantiation(indoc! {r#" + k = \a, b -> a + b + k(k(1, 2), 3) +"#})] fn a_concrete_operand_reaches_its_obligation(#[case] code: &str) { // The wall, not the root type: a missed delivery can leave an *interior* node // undetermined while the program's own type resolves fine — which is exactly how @@ -391,29 +410,86 @@ fn register_value_type(code: &str) -> Type { // registers, and a non-`Int` base. #[rstest] // One cyclic operand, the shape every accumulator has. -#[case::self_add("x := 0\nx := x + 1\nx", "Int")] +#[case::self_add(indoc! {r#" + x := 0 + x := x + 1 + x +"#}, "Int")] // **Both** operands cyclic: only the seed offers a base. -#[case::self_multiply("x := 2\nx := x * x\nx", "Int")] -#[case::self_subtract("x := 10\nx := x - x\nx", "Int")] +#[case::self_multiply(indoc! {r#" + x := 2 + x := x * x + x +"#}, "Int")] +#[case::self_subtract(indoc! {r#" + x := 10 + x := x - x + x +"#}, "Int")] // Nested, so an inner operator's output is itself an operand of an outer one. -#[case::nested("x := 0\nx := (x + 1) * (x + 2)\nx", "Int")] -#[case::deeply_nested("x := 1\nx := ((x + x) * (x + x)) + ((x * x) + (x + x))\nx", "Int")] +#[case::nested(indoc! {r#" + x := 0 + x := (x + 1) * (x + 2) + x +"#}, "Int")] +#[case::deeply_nested(indoc! {r#" + x := 1 + x := ((x + x) * (x + x)) + ((x * x) + (x + x)) + x +"#}, "Int")] // Routed through user functions, so the cycle crosses a call boundary — and the // obligations are the *freshened* copies of the callee's. -#[case::through_functions( - "def f(a):\n a + 1\ndef g(a):\n a * 2\nx := 0\nx := f(x) + g(x)\nx", - "Int" -)] -#[case::through_nested_calls("def f(a):\n a + 1\nx := 0\nx := f(f(x))\nx", "Int")] +#[case::through_functions(indoc! {r#" + def f(a): + a + 1 + def g(a): + a * 2 + x := 0 + x := f(x) + g(x) + x +"#}, "Int")] +#[case::through_nested_calls(indoc! {r#" + def f(a): + a + 1 + x := 0 + x := f(f(x)) + x +"#}, "Int")] // Two registers each defined in terms of the other: the cycle spans two equations. -#[case::mutual("x := 0\ny := 0\nx := y + 1\ny := x + 1\nx", "Int")] -#[case::three_way("x := 0\ny := 0\nz := 0\nx := z + 1\ny := x + 1\nz := y + 1\nz", "Int")] +#[case::mutual(indoc! {r#" + x := 0 + y := 0 + x := y + 1 + y := x + 1 + x +"#}, "Int")] +#[case::three_way(indoc! {r#" + x := 0 + y := 0 + z := 0 + x := z + 1 + y := x + 1 + z := y + 1 + z +"#}, "Int")] // A non-`Int` base, so the answer comes from the operands rather than a hardcoded row. -#[case::string_accumulator("s := \"a\"\ns := s + \"b\"\ns", "String")] +#[case::string_accumulator(indoc! {r#" + s := "a" + s := s + "b" + s +"#}, "String")] // A comparison cycle: its output is `Bool` for every implementation, so it is settled // at birth and the cycle costs it nothing. Nothing else in the suite writes one. -#[case::self_comparison("b := True\nb := (b == True)\nb", "Bool")] -#[case::conditional("x := 0\nx := x + 1 if x == 0 else x - 1\nx", "Int")] +#[case::self_comparison(indoc! {r#" + b := True + b := (b == True) + b +"#}, "Bool")] +#[case::conditional(indoc! {r#" + x := 0 + x := x + 1 if x == 0 else x - 1 + x +"#}, "Int")] fn a_register_that_reads_itself_still_gets_a_type(#[case] code: &str, #[case] base: &str) { assert_eq!(register_value_type(code).to_string(), base); } @@ -423,7 +499,12 @@ fn a_register_that_reads_itself_still_gets_a_type(#[case] code: &str, #[case] ba #[test] fn a_cycle_does_not_hide_an_operand_conflict() { assert!( - !infer_program_err("x := 0\nx := x + \"a\"\nx").is_empty(), + !infer_program_err(indoc! {r#" + x := 0 + x := x + "a" + x + "#}) + .is_empty(), "a conflict reachable only through a cyclic operand must still be a diagnostic" ); } @@ -432,7 +513,10 @@ fn a_cycle_does_not_hide_an_operand_conflict() { /// implementation accepts is rejected at the call site. #[test] fn a_generalized_function_rejects_a_use_its_trait_forbids() { - let errs = infer_program_err("f = \\a, b -> a - b\nf(\"x\", \"y\")"); + let errs = infer_program_err(indoc! {r#" + f = \a, b -> a - b + f("x", "y") + "#}); assert!( errs.iter().any( |e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Subtractable") From 65853a77b3e1eabd8b2f35786952b5cdf4c66ac3 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Fri, 14 Aug 2026 11:28:15 -0700 Subject: [PATCH 6/6] Review: a trait's rows are instances, and finding one is resolution MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two renames from review, both against terms this repo had already spent elsewhere. "Discharge" means eliminating a proof obligation throughout — `Subst::discharge` for Pi binders, refinement and assert discharge, the mutability phases — so a trait sense of it was a third meaning rather than a reuse; finding a table row is *resolution*, which is also what the literature calls it. "Implementation" is what a compiler calls its own code, and the CHL spec already says "instance" for the same thing. `TraitImpl` becomes `TraitInstance`, `Trait::impls` becomes `Trait::instances`, and `InferError::NoTraitImpl` becomes `NoTraitInstance` (its message now reads "No Addable instance for ..."). Three clarifications on top, all in the design doc's Traits section: - An obligation is what one *use* of a trait records, not "one recorded instance" — a phrase that both misdescribed it and collided with the row sense of instance. - A signature carrying an obligation is stated in general, `f : A ⇒ B requires MyTrait(A ⇝ B)`, with the operator table as the shapes that form takes today. Obligations already ride into schemes, so a user-written function carries its operators' requirements; only the surface for *writing* `requires` is missing. - What the tables hold — base types only, homogeneous rows — is now its own subsection, separate from how resolution works. `Equatable` rejecting a variant is what those rows happen to be rather than a claim that variants are incomparable, and the contribution table no longer says a non-base is a shape no instance can *ever* accept. Also fixes the section's function arrows, which were the term-level `→` where the type-level `⇒` belongs. --- src/ccl/design/type-inference.md | 50 +++++---- src/ccl/infer/api.rs | 20 ++-- src/ccl/infer/check.rs | 10 +- src/ccl/infer/context.rs | 2 +- src/ccl/infer/mod.rs | 4 +- src/ccl/infer/schemes.rs | 6 +- src/ccl/infer/solver/constrain.rs | 8 +- src/ccl/infer/solver/scheme.rs | 4 +- src/ccl/infer/solver/traits.rs | 163 ++++++++++++++++-------------- src/ccl/infer_var.rs | 2 +- tests/type_check.rs | 50 ++++----- 11 files changed, 170 insertions(+), 149 deletions(-) diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index 2732e522..def377f1 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -686,7 +686,7 @@ What this changed is instructive, because refinements were rare enough before th * **An operator does not *inherit* its operands' refinements**, and does not have to be *made* not to. A refinement is a fact about a value, so an operator that computes a new value cannot carry one over: `𝑥 + 𝑥` where `𝑥` is `2` produces `4`. Arithmetic, comparison and negation state their requirement as a [trait](#traits), over a variable per operand and per associated type — all unrelated — which leaves no path for an operand's refinement to reach the result by sharing (`an_operator_result_carries_no_operand_refinement`). The remaining monomorphic operators (`and`, `++`, `not`) keep an ordinary scheme and pass their operands verbatim — nothing is shared with the result, so a refined operand simply flows into a concrete domain. Aggregates likewise keep theirs, since their operand is a *collection* whose refinements describe its domain and the rule must see them. - Inheriting is not the same as **computing**, and only the first is ruled out. `{Int | __elem == 2} + {Int | __elem == 3}` genuinely *is* `{Int | __elem == 5}`, and a trait implementation is where such a rule would live, since it determines the output type rather than forcing it to be a position the operands already occupy. Today every implementation computes a base and stops — a property of the table, not of the mechanism. Two things would have to change to lift it: an implementation would need the operands' *types* rather than their bases, and the deposit would have to move to a point where those types are final. Eager deposit is sound for a base because a base never weakens, while a refinement set only shrinks as further lower bounds arrive — so a refinement computed from a partial view is too strong. A rule computing from resolved operands then meets recurrences (`x := x + 1` resolves its operand through its own output), where it must already be sound at the cut; and anything beyond constant folding and interval arithmetic needs predicate *implication*, which the lattice deliberately does not have (refinements match structurally — see this file's module-level note in `src/ccl/infer/solver/mod.rs`). + Inheriting is not the same as **computing**, and only the first is ruled out. `{Int | __elem == 2} + {Int | __elem == 3}` genuinely *is* `{Int | __elem == 5}`, and a trait instance is where such a rule would live, since it determines the output type rather than forcing it to be a position the operands already occupy. Today every instance computes a base and stops — a property of the table, not of the mechanism. Two things would have to change to lift it: an instance would need the operands' *types* rather than their bases, and the deposit would have to move to a point where those types are final. Eager deposit is sound for a base because a base never weakens, while a refinement set only shrinks as further lower bounds arrive — so a refinement computed from a partial view is too strong. A rule computing from resolved operands then meets recurrences (`x := x + 1` resolves its operand through its own output), where it must already be sound at the cut; and anything beyond constant folding and interval arithmetic needs predicate *implication*, which the lattice deliberately does not have (refinements match structurally — see this file's module-level note in `src/ccl/infer/solver/mod.rs`). * **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 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. @@ -1139,17 +1139,19 @@ The constraint lattice can state that two positions are **equal** or **related b ### Vocabulary * A **trait** is a named requirement a list of types may satisfy — `Addable`, `Orderable`, `Comparable`. **A trait is not a type**: no `Type` variant, no lattice point, no subtyping edge, and the type grammar and `constrain_go`'s rules are untouched. Types *satisfy* traits. -* An **implementation** is one row of a trait's table: the types it accepts, and the types it associates with them. Written `Addable(Int, Int ⇝ Int)` — accepted types, then `⇝`, then the associated ones. +* An **instance** is one row of a trait's table: the types it accepts, and the types it associates with them. Written `Addable(Int, Int ⇝ Int)` — accepted types, then `⇝`, then the associated ones. * An **associated type** is a type a trait *names* — `Output`, the type an arithmetic operator's result takes. A trait is a requirement rather than a function, so it associates any number, **including none**. A type is associated only when it *depends* on the types satisfying the trait: a comparison's `Bool` is the same for every pair `Equatable` accepts, so it belongs to the operator's signature and `Equatable` associates nothing — recording it as an association would claim the trait determines something it does not. -* An **obligation** is one recorded instance of a trait at specific type positions: one **operand position** per argument the trait takes, and one **associated position** per type it names. It is a single claim with two halves, and neither alone is the obligation: *the operand positions are types some implementation accepts*, **and** *each associated position is what that implementation associates*. Every position is an ordinary inference variable, unrelated to the others. +* An **obligation** is what one *use* of a trait records: the demand that some instance fit the type positions at that use — one **operand position** per argument the trait takes, and one **associated position** per type it names. It is a single claim with two halves, and neither alone is the obligation: *the operand positions are types some instance accepts*, **and** *each associated position is what that same instance associates*. Every position is an ordinary inference variable, unrelated to the others. -An operator's signature is therefore `𝐴₁ → … → 𝐴ₙ → 𝑅` plus the obligation, for the trait's arity `𝑛`, where `𝑅` is either one of the associated positions or a type the operator fixes. The three shapes the operators take: +A signature carries an obligation beside its type — `𝑓 : 𝐴 ⇒ 𝐵 requires MyTrait(𝐴 ⇝ 𝐵)` — and inference must find an instance satisfying it. Nothing about that is operator-specific: obligations ride variables into schemes ([Requirements are generalized](#requirements-are-generalized)), so a function inherits the requirements of the operators in its body, and `λ 𝑎 𝑏 → 𝑎 + 𝑏` is `∀ 𝐴 𝐵 𝑂. 𝐴 ⇒ 𝐵 ⇒ 𝑂 requires Addable(𝐴, 𝐵 ⇝ 𝑂)`. What is missing is only the *surface* — no CHL syntax writes `requires` yet, so every obligation is minted by an operator. (`requires` is the keyword the spec reserves for it, in [transactions as contextual parameters](../../../docs/chl-spec.md#87-direction-decided-transactions-as-contextual-parameters).) + +An operator's own signature is `𝐴₁ ⇒ … ⇒ 𝐴ₙ ⇒ 𝑅` plus its obligation, for the trait's arity `𝑛`, where `𝑅` is either one of the associated positions or a type the operator fixes. The three shapes the current operators take: | operator | signature | obligation | |---|---|---| -| `+` | `∀ 𝐴 𝐵 𝑂. 𝐴 → 𝐵 → 𝑂` | `Addable(𝐴, 𝐵 ⇝ 𝑂)` | -| `==` | `∀ 𝐴 𝐵. 𝐴 → 𝐵 → Bool` | `Equatable(𝐴, 𝐵)` | -| unary `-` | `∀ 𝐴 𝑂. 𝐴 → 𝑂` | `Negatable(𝐴 ⇝ 𝑂)` | +| `+` | `∀ 𝐴 𝐵 𝑂. 𝐴 ⇒ 𝐵 ⇒ 𝑂` | `Addable(𝐴, 𝐵 ⇝ 𝑂)` | +| `==` | `∀ 𝐴 𝐵. 𝐴 ⇒ 𝐵 ⇒ Bool` | `Equatable(𝐴, 𝐵)` | +| unary `-` | `∀ 𝐴 𝑂. 𝐴 ⇒ 𝑂` | `Negatable(𝐴 ⇝ 𝑂)` | Mechanism: `src/ccl/infer/solver/traits.rs`. @@ -1160,14 +1162,14 @@ An associated position like `𝑂` is an ordinary inference variable, not a mark A trait over `𝑁` operand positions, `𝐴` associated types and `𝐹` associated **functions** is an `(𝑁 + 𝐴 + 𝐹)`-ary relation in which the `𝑁` operand types functionally determine the `𝐴` types and the `𝐹` functions; `⇝` separates the -determining side from the determined one. An implementation is one hyper-edge, and -discharge is the search for a hyper-edge consistent with what inference has determined +determining side from the determined one. An instance is one hyper-edge, and +resolution is the search for a hyper-edge consistent with what inference has determined about the operand positions. Cambra implements `𝑁 ∈ {1, 2}`, `𝐴 ∈ {0, 1}` (`Output`, or nothing) and **`𝐹 = 0`**, with the relation built into the compiler rather than declared in CHL. -`𝐹 = 0` is a gap rather than a decision. An implementation's rows *do* denote distinct +`𝐹 = 0` is a gap rather than a decision. A trait's rows *do* denote distinct functions — `Addable(String, String ⇝ String)` is concatenation and `Addable(Int, Int ⇝ Int)` is integer addition — and a trait that cannot associate a function cannot say which. The function is therefore recovered twice outside the trait: @@ -1178,20 +1180,28 @@ from the operand column's runtime representation (`apply_binop_column`, in to name the code. Associating functions, and a CHL surface for declaring the relation, are the two -extensions this shape exists to take: the implementations are already *data* -(`Trait::impls`), so both are table extensions rather than new mechanisms. +extensions this shape exists to take: the instances are already *data* +(`Trait::instances`), so both are table extensions rather than new mechanisms. + +#### What the tables hold + +Every instance in every table accepts **base types only**, and every one is +homogeneous — `Addable(Int, Int ⇝ Int)`, never `Addable(Int, String ⇝ …)`. Both +facts are the tables' content, not properties of resolution: nothing in narrowing or +deposit assumes either. So `Equatable` rejecting a tuple, a record or a variant is +what these rows happen to be, and not a judgement that such types are incomparable. ### Refinements are transparent `{𝑇 | 𝑝}` satisfies a trait exactly when `𝑇` does. This holds by construction: satisfaction is judged on each bound contribution as it arrives, and refinements are peeled at that moment, when the base exists. Peeling at emission instead would have nothing to work on, an operand usually being still a variable there. -Transparency follows from incremental discharge and is permanent. A candidate set only ever shrinks ([Discharge is incremental](#discharge-is-incremental)), and a refinement is one of the things a bound can deliver late; if `{𝑇 | 𝑝}` could satisfy a requirement `𝑇` does not, a refinement arriving after the base would have to re-admit a dropped candidate, and order would start to matter. +Transparency follows from incremental resolution and is permanent. A candidate set only ever shrinks ([Resolution is incremental](#resolution-is-incremental)), and a refinement is one of the things a bound can deliver late; if `{𝑇 | 𝑝}` could satisfy a requirement `𝑇` does not, a refinement arriving after the base would have to re-admit a dropped candidate, and order would start to matter. Growing `𝐹` above zero would not change this. Choosing between two functions by `𝑝` is dispatch on a fact about a *value*, which a table keyed on types cannot express — and which no refinement survives in any case: `𝑥 + 𝑥` where `𝑥` is `2` produces `4`. -### Discharge is incremental +### Resolution is incremental -An obligation is a monotone fact, discharged as the graph fills in rather than by a sweep at the end of solving — the shape [`FunKindVar`](#46-data-vs-compute-functions) already uses for kinds. Each operand position carries a **candidate set** of implementations that only ever shrinks; each associated type is deposited on its position as an ordinary lower bound once every surviving candidate agrees on it. Order therefore does not matter. +An obligation is a monotone fact, resolved as the graph fills in rather than by a sweep at the end of solving — the shape [`FunKindVar`](#46-data-vs-compute-functions) already uses for kinds. Each operand position carries a **candidate set** of instances that only ever shrinks; each associated type is deposited on its position as an ordinary lower bound once every surviving candidate agrees on it. Order therefore does not matter. A contribution arriving at a position is one of three things, and each has its own outcome: @@ -1199,15 +1209,15 @@ A contribution arriving at a position is one of three things, and each has its o |---|---|---| | a **base** | `Int` | narrows the candidate set | | **not determined yet** | a variable, a hole, a `Feed` handle whose payload arrives separately | nothing to say | -| **determined and not a base** | a tuple, record, variant, function | rejected — no implementation can accept it | +| **determined, and not a base** | a tuple, record, variant, function | rejected — no instance accepts it ([What the tables hold](#what-the-tables-hold)) | The third is a rejection and not silence, because "no base here" is true of both it and the second. A tuple that merely failed to narrow would leave `(1, 2) == (3, 4)` well-typed: a comparison has no associated position to strand, so nothing downstream would object either. -A position the program never determines is not a rejection: it is reported as an unresolved variable rather than as a missing implementation. +A position that stays in the second row for the whole program — nothing ever determines it — is not a rejection either. Its obligation simply never narrows, and the variable is reported as unresolved rather than as a missing instance. ### What an obligation determines -A deposit records what every surviving implementation agrees on, and reaches the **associated positions only**. Nothing is written back onto an operand. +A deposit records what every surviving instance agrees on, and reaches the **associated positions only**. Nothing is written back onto an operand. The asymmetry is about where information comes from, not about soundness — with one candidate left, its operand types are implied exactly as its associated types are. An associated position is a fresh variable nothing else constrains from below, so the obligation is its only source. An operand always has the program's own `operandᵢ <: 𝐴ᵢ` edge. Determining an operand from the table would supply information the program was meant to supply, which hides an under-connected lowering rather than exposing it. @@ -1229,7 +1239,7 @@ That the list is closed is an argument about today's code, not something the com ### Requirements are generalized -Obligations ride variables through `freshen_above`, so a generalized function carries its operators' requirements into its scheme. Each use instantiates and discharges its **own** copy — sharing one would let a `String` use empty an `Int` use's candidate set. +Obligations ride variables through `freshen_above`, so a generalized function carries its operators' requirements into its scheme. Each use instantiates and resolves its **own** copy — sharing one would let a `String` use empty an `Int` use's candidate set. ### A definition nobody calls delivers nothing @@ -1258,7 +1268,7 @@ The requirements are still *recorded*, and jointly reading them is what would re The bottom two rows are ordinary schemes, because their operand types are fixed. The top two are not, and could not be: see [Traits](#traits). -**Note**: String + String → `Concat` rewriting is performed at **compile time** (in `simplify.rs`), not at inference time. Inference accepts `(String, String) ⇝ String` as an `Addable` implementation and returns `String`. +**Note**: String + String → `Concat` rewriting is performed at **compile time** (in `simplify.rs`), not at inference time. Inference accepts `(String, String) ⇝ String` as an `Addable` instance and returns `String`. ### UnaryOp type rules diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index 86314ce5..30ba7c73 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -344,7 +344,7 @@ pub enum InferError { /// Display label for the message (see the type docs — not the location). at: String, }, - /// An operator was used at operand types no implementation of its trait + /// An operator was used at operand types no instance of its trait /// accepts — `1 > "a"`, `"a" - "b"`, or a polymorphic function applied at a type /// its body's operators cannot handle. /// @@ -353,8 +353,8 @@ pub enum InferError { /// operator's requirement about the pair, so the message names the trait and /// what the position could have accepted rather than showing two types that /// "don't match". - NoTraitImpl { - /// The trait with no implementation left, e.g. `Addable`. + NoTraitInstance { + /// The trait with no instance left, e.g. `Addable`. trait_: String, /// The operand position (0-based) whose type ruled the last one out. position: u8, @@ -552,7 +552,7 @@ impl std::fmt::Debug for InferError { } Ok(()) } - InferError::NoTraitImpl { + InferError::NoTraitInstance { trait_, position, found, @@ -566,7 +566,7 @@ impl std::fmt::Debug for InferError { .join(" or "); write!( f, - "No {trait_} implementation for {at}: operand {} is {found}, but \ + "No {trait_} instance for {at}: operand {} is {found}, but \ the only type accepted there is {accepted}", position + 1, ) @@ -2034,7 +2034,7 @@ mod tests { // whose results are then added. // // The rejection comes from the `+`, and names the actual problem: no - // `Addable` implementation takes an `Int` and a `String`. It arrives during + // `Addable` instance takes an `Int` and a `String`. It arrives during // emission, as soon as both operand types are known — the operator states a // requirement about the *pair*, so it need not wait for the two to collide on // a shared variable at coalesce. @@ -2048,10 +2048,10 @@ mod tests { assert!( errs.iter().any(|e| matches!( e, - InferError::NoTraitImpl { trait_, found, .. } + InferError::NoTraitInstance { trait_, found, .. } if trait_ == "Addable" && **found == Type::Base(BaseType::String) )), - "expected NoTraitImpl for Addable at a String operand, got {errs:?}" + "expected NoTraitInstance for Addable at a String operand, got {errs:?}" ); } @@ -2619,12 +2619,12 @@ mod tests { assert!( errs.iter().any(|e| matches!( e, - InferError::NoTraitImpl { trait_, position, found, .. } + InferError::NoTraitInstance { trait_, position, found, .. } if trait_ == "Negatable" && *position == 0 && **found == Type::Base(BaseType::Bool) )), - "expected NoTraitImpl for Negatable at a Bool operand, got {errs:?}" + "expected NoTraitInstance for Negatable at a Bool operand, got {errs:?}" ); } diff --git a/src/ccl/infer/check.rs b/src/ccl/infer/check.rs index c295cf6a..b4a29468 100644 --- a/src/ccl/infer/check.rs +++ b/src/ccl/infer/check.rs @@ -135,7 +135,7 @@ impl Typing for CheckCtx { // corrupt types**, which is why a Check error that is not `UnresolvedInfer` // panics at the wall rather than being reported. So this firing means // inference has a hole or a later pass rewrote the tree into something - // ill-typed — and it reuses `NoTraitImpl` for the same reason + // ill-typed — and it reuses `NoTraitInstance` for the same reason // [`Typing::require_sub`] reuses `TypeMismatch` here: the error vocabulary // describes the inconsistency, the wall supplies the interpretation. Measured // across the suite: it never fires. @@ -148,7 +148,7 @@ impl Typing for CheckCtx { return Ok(assoc.map(|_| self.fresh())); }; let matched = trait_ - .impls() + .instances() .iter() .find(|i| i.args.len() == bases.len() && i.args.iter().eq(bases.iter().copied())); match matched { @@ -160,17 +160,17 @@ impl Typing for CheckCtx { })), None => { // Blame the last position: with the earlier ones fixed, it is the one - // whose type ruled the implementation out. + // whose type ruled the instance out. let position = bases.len().saturating_sub(1); let prefix: Vec = bases[..position].iter().map(|b| (*b).clone()).collect(); let accepted: Vec = trait_ - .impls() + .instances() .iter() .filter(|i| i.args.len() == bases.len() && i.args[..position] == prefix[..]) .filter_map(|i| i.args.get(position).cloned().map(Type::Base)) .collect(); - let located = self.raise(InferError::NoTraitImpl { + let located = self.raise(InferError::NoTraitInstance { trait_: trait_.to_string(), position: position as u8, found: Box::new(Type::Base(bases[position].clone())), diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs index bb6f9c7c..fa451b50 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -297,7 +297,7 @@ impl Typing for InferCtx { for (i, position) in positions.iter().enumerate() { obligation.watch(position, i as u8); } - // A trait whose implementations already agree settles here, before any + // A trait whose instances already agree settles here, before any // operand is known — the ordinary "all candidates agree" rule reaching its // condition immediately, not a special case. obligation diff --git a/src/ccl/infer/mod.rs b/src/ccl/infer/mod.rs index ce839593..9e72bf88 100644 --- a/src/ccl/infer/mod.rs +++ b/src/ccl/infer/mod.rs @@ -199,12 +199,12 @@ pub(super) fn map_constrain_err(err: ConstrainError, ctx_label: &str) -> InferEr type_a: Box::new(coalesce_for_error(&lhs)), type_b: Box::new(coalesce_for_error(&rhs)), }, - ConstrainError::NoTraitImpl { + ConstrainError::NoTraitInstance { trait_, position, found, accepted, - } => InferError::NoTraitImpl { + } => InferError::NoTraitInstance { trait_: trait_.to_string(), position, found: Box::new(found), diff --git a/src/ccl/infer/schemes.rs b/src/ccl/infer/schemes.rs index 7ee598be..47f7cab7 100644 --- a/src/ccl/infer/schemes.rs +++ b/src/ccl/infer/schemes.rs @@ -374,7 +374,7 @@ mod tests { /// `Comparable(γ)` says it — a **pure requirement**, associating nothing, since /// the scheme already supplies the result type. A codomain the program never /// determines is still accepted here, as an unresolved variable rather than a - /// missing implementation; that is the ordinary limit of narrowing, not a gap + /// missing instance; that is the ordinary limit of narrowing, not a gap /// specific to `max`. /// /// Closes `type-checker-traits-comparability` (P3) in the project vault. @@ -402,10 +402,10 @@ mod tests { assert!( errs.iter().any(|e| matches!( e, - crate::ccl::infer::InferError::NoTraitImpl { trait_, .. } + crate::ccl::infer::InferError::NoTraitInstance { trait_, .. } if trait_ == "Comparable" )), - "expected NoTraitImpl for Comparable, got {errs:?}" + "expected NoTraitInstance for Comparable, got {errs:?}" ); } } diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index 7a93e8bb..3711fb77 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -109,18 +109,18 @@ pub enum ConstrainError { /// The domain demanded at the position. rhs: Type, }, - /// An operand's type ruled out the last implementation of a trait an operator + /// An operand's type ruled out the last instance of a trait an operator /// requires — `1 > "a"`, or `\x -> x + 1` applied to a string. /// /// Raised from the bound-recording arm that delivered the offending type, so it /// fires the moment the program states the conflict rather than at a later phase /// that goes looking for it. - NoTraitImpl { - /// The trait with no implementation left. + NoTraitInstance { + /// The trait with no instance left. trait_: Trait, /// The operand position whose type ruled the last one out. position: u8, - /// The type that arrived there — a base no implementation accepts, or a + /// The type that arrived there — a base no instance accepts, or a /// shape that is not a base at all. found: Type, /// What that position could still have accepted, given everything already diff --git a/src/ccl/infer/solver/scheme.rs b/src/ccl/infer/solver/scheme.rs index f0ca3057..0a1a8298 100644 --- a/src/ccl/infer/solver/scheme.rs +++ b/src/ccl/infer/solver/scheme.rs @@ -94,8 +94,8 @@ pub struct FreshenCache { /// Original trait obligation → its per-instantiation copy, for the same reason /// as [`kind_vars`](Self::kind_vars): a generalized function's operator /// requirements are quantified along with the variables they constrain, so each - /// use discharges *its own* copy. `λ 𝑥 → 𝑥 + 1` generalizes to - /// `∀A O. (A : Addable(A, Int)) ⇒ A → O`; sharing one obligation across uses + /// use resolves *its own* copy. `λ 𝑥 → 𝑥 + 1` generalizes to + /// `∀A O. A ⇒ O requires Addable(A, Int ⇝ O)`; sharing one obligation across uses /// would let a `String` use narrow the `Int` use's candidate set to nothing. pub obligations: HashMap>, } diff --git a/src/ccl/infer/solver/traits.rs b/src/ccl/infer/solver/traits.rs index c7cdb906..5542865e 100644 --- a/src/ccl/infer/solver/traits.rs +++ b/src/ccl/infer/solver/traits.rs @@ -7,7 +7,7 @@ //! `Addable`, `Orderable`. It is **not a type**: nothing here adds a [`Type`] //! variant, a lattice point or a subtyping edge, and the type grammar and //! `constrain_go`'s rules are untouched. -//! - An **implementation** ([`TraitImpl`]) is one row of a trait's table: the types it +//! - An **instance** ([`TraitInstance`]) is one row of a trait's table: the types it //! accepts, and the types it associates with them — written //! `Addable(Int, Int ⇝ Int)`, accepted types then `⇝` then associated ones. //! - An **associated type** ([`Assoc`]) is a type a trait *names* — `Output`, the type @@ -15,14 +15,14 @@ //! none**: only a type that *depends* on the types satisfying the trait belongs here, //! so `Equatable` associates nothing and its `Bool` rides the operator's signature //! instead (`OperatorResult::Fixed`, in `src/ccl/infer/schemes.rs`). -//! - An **obligation** ([`TraitObligation`]) is one recorded instance of a trait at -//! specific type positions: one **operand position** per argument the trait takes, -//! and one **associated position** per type it names — `Addable(𝐴, 𝐵 ⇝ 𝑂)` is the -//! shape to picture, though the arity and the association count are both the trait's. -//! It is a single claim with two halves, and neither alone is "the obligation": *the -//! operand positions are types some implementation accepts*, **and** *each associated -//! position is what that implementation associates*. Every position is an ordinary -//! inference variable, unrelated to the others. +//! - An **obligation** ([`TraitObligation`]) is what one *use* of a trait records: the +//! demand that some instance fit the type positions at that use — one **operand +//! position** per argument the trait takes, and one **associated position** per type +//! it names. `Addable(𝐴, 𝐵 ⇝ 𝑂)` is the shape to picture, though the arity and the +//! association count are both the trait's. It is a single claim with two halves, and +//! neither alone is "the obligation": *the operand positions are types some instance +//! accepts*, **and** *each associated position is what that instance associates*. +//! Every position is an ordinary inference variable, unrelated to the others. //! - A **watch** is an obligation's attachment to an operand variable //! ([`TraitObligation::watch`]), which is how a bound landing anywhere in the program //! reaches it. @@ -32,12 +32,12 @@ //! operator's result, and so what lets a function be typechecked without consulting its //! call sites. //! -//! # Discharge is incremental +//! # Resolution is incremental //! -//! An obligation is a monotone fact discharged as the graph fills in, the shape +//! An obligation is a monotone fact resolved as the graph fills in, the shape //! [`FunKindVar`](crate::ccl::ty::FunKindVar) already uses for kinds; no phase runs //! "once everything is known". Each operand position carries a **candidate set** of -//! implementations that only ever shrinks ([`TraitObligation::narrow`]), and each +//! instances that only ever shrinks ([`TraitObligation::narrow`]), and each //! associated type is deposited on its position as an ordinary lower bound once every //! surviving candidate *agrees* on it ([`TraitObligation::try_deposit`]) — agreement, //! not a lone survivor. A deposit reaches **associated positions only**; nothing is @@ -52,10 +52,11 @@ //! `src/ccl/design/type-inference.md`, "Traits" is the design of record, and carries //! the arguments this module only acts on: why the constraint lattice cannot state an //! operator's requirement on its own, why a deposit is one-way and waits for agreement, -//! why refinement transparency is permanent rather than a convenience, and what a trait -//! would relate beyond types — associated *functions*, which the shape here allows and -//! does not yet have. Which operators state which requirement, and which take a fixed -//! result rather than an associated one, is `schemes.rs`'s business, not this module's. +//! why refinement transparency is permanent rather than a convenience, what the tables +//! hold and what that does *not* say about resolution, and what a trait would relate +//! beyond types — associated *functions*, which the shape here allows and does not yet +//! have. Which operators state which requirement, and which take a fixed result rather +//! than an associated one, is `schemes.rs`'s business, not this module's. use std::cell::{Cell, RefCell}; use std::fmt; @@ -70,7 +71,7 @@ use super::constrain::{ConstrainCache, ConstrainError, constrain_subtype}; /// with them. /// /// Closed and built-in. The set is the operators the language has, not a user -/// vocabulary — but the implementations are already *data* ([`Trait::impls`]), so a +/// vocabulary — but the instances are already *data* ([`Trait::instances`]), so a /// user-declared trait is a table extension rather than a new mechanism. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum Trait { @@ -112,20 +113,20 @@ pub enum Assoc { Output, } -/// One implementation: the types it accepts, and what it associates with them. +/// One instance: the types it accepts, and what it associates with them. #[derive(Debug, Clone, PartialEq, Eq)] -pub struct TraitImpl { +pub struct TraitInstance { /// The accepted types, positionally. A slice rather than a fixed array because /// arity is the trait's business — every operator trait is binary today, and an /// `Orderable` over one type is the obvious next one. pub args: &'static [BaseType], - /// The types this implementation associates, by name. Empty for a trait that is + /// The types this instance associates, by name. Empty for a trait that is /// a pure requirement. pub assoc: &'static [(Assoc, BaseType)], } -impl TraitImpl { - /// The type this implementation associates with `name`, if any. +impl TraitInstance { + /// The type this instance associates with `name`, if any. pub fn assoc_ty(&self, name: Assoc) -> Option<&BaseType> { self.assoc.iter().find(|(n, _)| *n == name).map(|(_, t)| t) } @@ -133,28 +134,28 @@ impl TraitImpl { /// `(Int, Int) ⇝ Int` and `(UInt, UInt) ⇝ UInt` — the numeric arithmetic rows every /// arithmetic trait shares. -const NUMERIC: &[TraitImpl] = &[ - TraitImpl { +const NUMERIC: &[TraitInstance] = &[ + TraitInstance { args: &[BaseType::Int, BaseType::Int], assoc: &[(Assoc::Output, BaseType::Int)], }, - TraitImpl { + TraitInstance { args: &[BaseType::UInt, BaseType::UInt], assoc: &[(Assoc::Output, BaseType::UInt)], }, ]; /// The numeric rows plus `(String, String) ⇝ String`. -const NUMERIC_OR_STRING: &[TraitImpl] = &[ - TraitImpl { +const NUMERIC_OR_STRING: &[TraitInstance] = &[ + TraitInstance { args: &[BaseType::Int, BaseType::Int], assoc: &[(Assoc::Output, BaseType::Int)], }, - TraitImpl { + TraitInstance { args: &[BaseType::UInt, BaseType::UInt], assoc: &[(Assoc::Output, BaseType::UInt)], }, - TraitImpl { + TraitInstance { args: &[BaseType::String, BaseType::String], assoc: &[(Assoc::Output, BaseType::String)], }, @@ -167,20 +168,20 @@ const NUMERIC_OR_STRING: &[TraitImpl] = &[ /// types the trait accepts, so it carries no information about them. Recording it as /// an associated type would state that the trait determines something it does not — /// the same mistake as an operator inheriting an operand's refinement, one level up. -const COMPARABLE: &[TraitImpl] = &[ - TraitImpl { +const COMPARABLE: &[TraitInstance] = &[ + TraitInstance { args: &[BaseType::Int, BaseType::Int], assoc: &[], }, - TraitImpl { + TraitInstance { args: &[BaseType::UInt, BaseType::UInt], assoc: &[], }, - TraitImpl { + TraitInstance { args: &[BaseType::String, BaseType::String], assoc: &[], }, - TraitImpl { + TraitInstance { args: &[BaseType::Bool, BaseType::Bool], assoc: &[], }, @@ -188,39 +189,40 @@ const COMPARABLE: &[TraitImpl] = &[ /// Unary negation. One operand, and an `Output` that genuinely depends on it — the /// arity and association shape `Addable` and `Equatable` between them do not have. -const NEGATABLE: &[TraitImpl] = &[TraitImpl { +const NEGATABLE: &[TraitInstance] = &[TraitInstance { args: &[BaseType::Int], assoc: &[(Assoc::Output, BaseType::Int)], }]; /// The bases an aggregate can order, matching `max`'s merge in `ccl/mod.rs`. Unary /// and associating nothing — the fourth shape, and a pure requirement. -const ORDERED: &[TraitImpl] = &[ - TraitImpl { +const ORDERED: &[TraitInstance] = &[ + TraitInstance { args: &[BaseType::Int], assoc: &[], }, - TraitImpl { + TraitInstance { args: &[BaseType::UInt], assoc: &[], }, - TraitImpl { + TraitInstance { args: &[BaseType::String], assoc: &[], }, ]; impl Trait { - /// This trait's implementations. + /// This trait's instances. /// - /// Every table is **homogeneous** — both operand positions accept the same base - /// — which is a fact about today's rows, not about the mechanism: nothing in - /// narrowing or deposit assumes it. The tables mirror - /// `interpreter::binop::apply_binop_column`, so a program this accepts is one - /// the interpreter can actually run. In particular there is no `Unit` row (the - /// interpreter cannot compare units) and no cross-base row, since `Int` and - /// `UInt` are unrelated leaves in the lattice and never join. - pub fn impls(self) -> &'static [TraitImpl] { + /// Every table holds base types only, and every row is **homogeneous** — both + /// operand positions accept the same base. Nothing in narrowing or deposit + /// assumes either, and both are answerable to + /// `interpreter::binop::apply_binop_column`, which these tables mirror so that a + /// program inference accepts is one the interpreter can run: hence no `Unit` row + /// (it cannot compare units) and no cross-base row (`Int` and `UInt` are + /// unrelated leaves that never join). What that does and does not say about the + /// mechanism is `src/ccl/design/type-inference.md`, "What the tables hold". + pub fn instances(self) -> &'static [TraitInstance] { match self { Trait::Addable => NUMERIC_OR_STRING, Trait::Subtractable | Trait::Multipliable | Trait::Divisible => NUMERIC, @@ -247,9 +249,9 @@ impl Trait { /// The `(arity, associated names)` its first row declares. fn rows_agree_on(self) -> (usize, Vec) { let first = self - .impls() + .instances() .first() - .expect("every trait has at least one implementation"); + .expect("every trait has at least one instance"); ( first.args.len(), first.assoc.iter().map(|(n, _)| *n).collect(), @@ -283,9 +285,10 @@ pub struct TraitObligationId(pub(crate) u32); static OBLIGATION_COUNTER: AtomicU32 = AtomicU32::new(0); -/// One recorded instance of a trait at specific type positions, carrying both halves -/// of the claim: that the operand positions are types some implementation accepts, and -/// that each associated position is what that implementation associates. Arity and +/// What one use of a trait records: the demand that some instance fit the type +/// positions at that use. It carries both halves of the claim — that the operand +/// positions are types some instance accepts, and that each associated position is +/// what that same instance associates. Arity and /// association count are the trait's — `Addable(𝐴, 𝐵 ⇝ 𝑂)` is one shape, /// `Negatable(𝐴 ⇝ 𝑂)` and `Equatable(𝐴, 𝐵)` are the others. /// See this module's *Vocabulary*. @@ -303,9 +306,9 @@ pub struct TraitObligation { pub uid: TraitObligationId, /// The trait being required. pub trait_: Trait, - /// The implementations still consistent with everything seen so far. + /// The instances still consistent with everything seen so far. /// Monotonically shrinking; empty is unrepresentable (it is the error). - candidates: RefCell>, + candidates: RefCell>, /// The type positions this obligation associates, one per name the trait /// declares. Empty for a trait that is a pure requirement — the mechanism then /// still narrows and still rejects, it simply determines nothing. @@ -327,12 +330,12 @@ struct AssocPosition { impl TraitObligation { /// Record an instance of `trait_` whose associated names stand at the given type - /// positions, with every implementation still a candidate. + /// positions, with every instance still a candidate. pub fn new(trait_: Trait, assoc: Vec<(Assoc, Type)>) -> Rc { Rc::new(TraitObligation { uid: TraitObligationId(OBLIGATION_COUNTER.fetch_add(1, Ordering::Relaxed)), trait_, - candidates: RefCell::new(trait_.impls().to_vec()), + candidates: RefCell::new(trait_.instances().to_vec()), assoc: assoc .into_iter() .map(|(name, ty)| AssocPosition { @@ -395,7 +398,7 @@ impl TraitObligation { } /// The candidates still live, for diagnostics and tests. - pub fn candidates(&self) -> Vec { + pub fn candidates(&self) -> Vec { self.candidates.borrow().clone() } @@ -419,13 +422,13 @@ impl TraitObligation { } } - /// Reject a shape no implementation can accept at position `pos`. + /// Reject a shape no instance can accept at position `pos`. /// /// Distinct from [`narrow`](Self::narrow) failing: nothing is *ruled out* here, /// because there was never a candidate to rule out. The contribution is simply /// outside the vocabulary the trait is defined over. fn reject(self: &Rc, pos: u8, found: &Type) -> Result<(), ConstrainError> { - Err(ConstrainError::NoTraitImpl { + Err(ConstrainError::NoTraitInstance { trait_: self.trait_, position: pos, found: found.clone(), @@ -438,7 +441,7 @@ impl TraitObligation { }) } - /// Restrict position `pos` to implementations accepting `base`, then deposit the + /// Restrict position `pos` to instances accepting `base`, then deposit the /// output if that settles it. /// /// Monotone and idempotent: narrowing by a base already consistent with every @@ -460,7 +463,7 @@ impl TraitObligation { // reach; it cannot accept the contribution, so it drops out too. candidates.retain(|i| i.args.get(pos as usize) == Some(base)); if candidates.is_empty() { - return Err(ConstrainError::NoTraitImpl { + return Err(ConstrainError::NoTraitInstance { trait_: self.trait_, position: pos, found: Type::Base(base.clone()), @@ -493,7 +496,7 @@ impl TraitObligation { Ok(()) } - /// The type every surviving implementation associates with `name`, or `None` if + /// The type every surviving instance associates with `name`, or `None` if /// they disagree — the condition a deposit waits on. fn agreed_assoc(&self, name: Assoc) -> Option { let candidates = self.candidates.borrow(); @@ -609,7 +612,7 @@ pub fn verify_narrowing_is_complete(resolve: impl Fn(&Type) -> Option) { /// /// The distinction between the last two variants is the whole point. Both narrow /// nothing, but for opposite reasons: one is a position the program has not -/// determined *yet*, and one is a shape no implementation can *ever* accept. +/// determined *yet*, and one is determined, at a type no instance accepts. /// Treating them alike is what let `(1, 2) == (3, 4)` type-check — a tuple narrows /// nothing, and a trait with no associated type has nothing left unresolved for a /// later wall to catch, so the program passed. @@ -620,9 +623,15 @@ pub enum Offered<'a> { /// whose payload arrives separately (a `Feed`; a `Mut` is dereferenced before the /// variable arms, so it never reaches a watch). Unknown, - /// A concrete shape that is not a base and never will be. No implementation - /// accepts it, so the requirement fails here rather than silently going - /// undischarged. + /// A determined type that is not a base leaf — a tuple, record, variant or + /// function. + /// + /// Every instance is keyed on a base ([`TraitInstance::args`]), so nothing in + /// any table accepts it and the requirement fails here rather than silently + /// going unresolved. That the tables hold only bases is their *content*, not a + /// property of resolution: giving `Equatable` a variant would add rows, and + /// would split this variant into the shapes a row can key on — it would not + /// change how narrowing works. NotABase, } @@ -780,7 +789,7 @@ mod tests { use crate::ccl::infer::solver::fresh_var; /// Both narrowing orders reach the same answer — the property that lets the - /// obligation be discharged incrementally instead of by a final sweep. + /// obligation be resolved incrementally instead of by a final sweep. #[rstest::rstest] #[case(&[(0, BaseType::Int), (1, BaseType::Int)])] #[case(&[(1, BaseType::Int), (0, BaseType::Int)])] @@ -807,8 +816,8 @@ mod tests { } /// One known operand is enough to settle the output when every remaining - /// implementation agrees on it — without concluding anything about the *other* - /// operand, which stays open for a future heterogeneous implementation. + /// instance agrees on it — without concluding anything about the *other* + /// operand, which stays open for a future heterogeneous instance. #[test] fn one_known_operand_settles_an_agreed_output() { let out = fresh_var(0); @@ -825,7 +834,7 @@ mod tests { ); assert_eq!( ob.candidates(), - vec![TraitImpl { + vec![TraitInstance { args: &[BaseType::Int, BaseType::Int], assoc: &[(Assoc::Output, BaseType::Int)], }] @@ -856,10 +865,10 @@ mod tests { ); } - /// Operands that no implementation accepts together are rejected, and the error + /// Operands that no instance accepts together are rejected, and the error /// says what the position could still have taken. #[test] - fn incompatible_operands_have_no_implementation() { + fn incompatible_operands_have_no_instance() { let out = fresh_var(0); let ob = TraitObligation::new(Trait::Orderable, vec![(Assoc::Output, out)]); let mut cache = ConstrainCache::new(); @@ -870,14 +879,14 @@ mod tests { .narrow(1, &BaseType::String, &mut cache) .expect_err("nothing compares an Int to a String"); - let ConstrainError::NoTraitImpl { + let ConstrainError::NoTraitInstance { trait_, position, found, accepted, } = err else { - panic!("expected NoTraitImpl, got {err:?}"); + panic!("expected NoTraitInstance, got {err:?}"); }; assert_eq!(trait_, Trait::Orderable); assert_eq!(position, 1); @@ -885,7 +894,7 @@ mod tests { assert_eq!(accepted, vec![BaseType::Int]); } - /// Every implementation of a trait agrees on its **shape** — how many types it is + /// Every instance of a trait agrees on its **shape** — how many types it is /// over, and which types it associates. /// /// [`Trait::arity`] and [`Trait::assocs`] read that shape off the first row, and @@ -905,7 +914,7 @@ mod tests { Trait::Comparable, ] { let (arity, assocs) = (trait_.arity(), trait_.assocs()); - for row in trait_.impls() { + for row in trait_.instances() { assert_eq!( row.args.len(), arity, diff --git a/src/ccl/infer_var.rs b/src/ccl/infer_var.rs index 47b17e10..70ea0058 100644 --- a/src/ccl/infer_var.rs +++ b/src/ccl/infer_var.rs @@ -307,7 +307,7 @@ pub struct InferVar { /// Trait obligations this variable is an operand of, with the position it /// occupies in each. Every lower bound recorded here is delivered to them by /// `notify_lower` (`src/ccl/infer/solver/traits.rs`), which is how an operator's - /// requirement is discharged incrementally rather than by a pass that goes + /// requirement is resolved incrementally rather than by a pass that goes /// looking for obligations once solving has stopped. /// /// The list lives on the variable rather than in a side map on the inference diff --git a/tests/type_check.rs b/tests/type_check.rs index d4280587..78d26d51 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -217,15 +217,16 @@ fn each_trait_shape_types_a_real_program(#[case] code: &str, #[case] expected: T assert_eq!(infer_program(code), expected); } -/// Negation is a trait, so an operand it has no implementation for is rejected as a -/// missing implementation rather than as a mismatch against a hardcoded domain. +/// Negation is a trait, so an operand it has no instance for is rejected as a +/// missing instance rather than as a mismatch against a hardcoded domain. #[test] -fn negation_rejects_an_operand_with_no_implementation() { +fn negation_rejects_an_operand_with_no_instance() { let errs = infer_program_err(r#"-"a""#); assert!( - errs.iter() - .any(|e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Negatable")), - "expected NoTraitImpl for Negatable, got {errs:?}" + errs.iter().any( + |e| matches!(e, InferError::NoTraitInstance { trait_, .. } if trait_ == "Negatable") + ), + "expected NoTraitInstance for Negatable, got {errs:?}" ); } @@ -247,8 +248,8 @@ fn a_composite_satisfies_no_trait(#[case] code: &str, #[case] expected: &str) { let errs = infer_program_err(code); assert!( errs.iter() - .any(|e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == expected)), - "expected NoTraitImpl for {expected}, got {errs:?}" + .any(|e| matches!(e, InferError::NoTraitInstance { trait_, .. } if trait_ == expected)), + "expected NoTraitInstance for {expected}, got {errs:?}" ); } @@ -259,9 +260,10 @@ fn a_composite_satisfies_no_trait(#[case] code: &str, #[case] expected: &str) { fn a_base_outside_the_table_is_rejected() { let errs = infer_program_err("() == ()"); assert!( - errs.iter() - .any(|e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Equatable")), - "expected NoTraitImpl for Equatable, got {errs:?}" + errs.iter().any( + |e| matches!(e, InferError::NoTraitInstance { trait_, .. } if trait_ == "Equatable") + ), + "expected NoTraitInstance for Equatable, got {errs:?}" ); } @@ -276,13 +278,13 @@ fn a_refinement_does_not_make_a_type_satisfy_a_trait() { let errs = infer_program_err(r#""a" - "b""#); assert!( errs.iter().any( - |e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Subtractable") + |e| matches!(e, InferError::NoTraitInstance { trait_, .. } if trait_ == "Subtractable") ), - "expected NoTraitImpl for Subtractable, got {errs:?}" + "expected NoTraitInstance for Subtractable, got {errs:?}" ); } -/// Operands no implementation accepts together are rejected — including for a +/// Operands no instance accepts together are rejected — including for a /// **comparison**, whose result type is `Bool` whatever the operands are. /// /// That last part is the whole reason the requirement is recorded as an obligation @@ -293,12 +295,12 @@ fn a_refinement_does_not_make_a_type_satisfy_a_trait() { #[case::compare_int_string(r#"1 > "a""#)] #[case::equate_int_bool("1 == True")] #[case::add_int_bool("1 + True")] -fn operands_no_implementation_accepts_are_rejected(#[case] code: &str) { +fn operands_no_instance_accepts_are_rejected(#[case] code: &str) { let errs = infer_program_err(code); assert!( errs.iter() - .any(|e| matches!(e, InferError::NoTraitImpl { .. })), - "expected NoTraitImpl, got {errs:?}" + .any(|e| matches!(e, InferError::NoTraitInstance { .. })), + "expected NoTraitInstance, got {errs:?}" ); } @@ -321,7 +323,7 @@ fn misusing_an_operator_result_is_an_ordinary_diagnostic(#[case] code: &str) { } /// A generalized function carries its operators' requirements into its scheme, so it -/// typechecks on its own and each use discharges its **own** copy. +/// typechecks on its own and each use resolves its **own** copy. /// /// `f = \a -> \b -> a + b` is `∀A B O. (Addable(A, B) ⇝ O) ⇒ A → B → O`. Two uses at /// different types both succeed, which is the property that fails if instantiations @@ -340,7 +342,7 @@ fn a_generalized_function_instantiates_its_operator_requirements() { ); } -// An obligation is discharged by *delivery*: a concrete type reaching an operand +// An obligation is resolved by *delivery*: a concrete type reaching an operand // variable has to reach the obligation watching it. Production code writes a // variable's lower bounds in exactly four places — `constrain_go`'s two variable // arms, `extrude`'s proxy seeding, and `freshen_above`'s clone — and there is a case @@ -478,7 +480,7 @@ fn register_value_type(code: &str) -> Type { s := s + "b" s "#}, "String")] -// A comparison cycle: its output is `Bool` for every implementation, so it is settled +// A comparison cycle: its output is `Bool` for every instance, so it is settled // at birth and the cycle costs it nothing. Nothing else in the suite writes one. #[case::self_comparison(indoc! {r#" b := True @@ -510,7 +512,7 @@ fn a_cycle_does_not_hide_an_operand_conflict() { } /// The requirement travels with the function, so applying it at a type no -/// implementation accepts is rejected at the call site. +/// instance accepts is rejected at the call site. #[test] fn a_generalized_function_rejects_a_use_its_trait_forbids() { let errs = infer_program_err(indoc! {r#" @@ -519,9 +521,9 @@ fn a_generalized_function_rejects_a_use_its_trait_forbids() { "#}); assert!( errs.iter().any( - |e| matches!(e, InferError::NoTraitImpl { trait_, .. } if trait_ == "Subtractable") + |e| matches!(e, InferError::NoTraitInstance { trait_, .. } if trait_ == "Subtractable") ), - "expected NoTraitImpl for Subtractable, got {errs:?}" + "expected NoTraitInstance for Subtractable, got {errs:?}" ); } @@ -1523,7 +1525,7 @@ fn test_self_application_types() { /// information is the program's to supply. /// /// `O` is a different matter: the obligation is its only source, and every -/// implementation whose second operand is `Int` returns `Int`, so it resolves. That +/// instance whose second operand is `Int` returns `Int`, so it resolves. That /// is a fact about today's table rather than a stable property — adding /// `Addable(Float, Int) ⇝ Float` would leave two candidates whose outputs disagree /// and open the result too, which is why this asserts the codomain per case rather