diff --git a/src/ccl/context.rs b/src/ccl/context.rs index 320c0ba6..eca6502d 100644 --- a/src/ccl/context.rs +++ b/src/ccl/context.rs @@ -1112,6 +1112,7 @@ pub fn compile_program( #[cfg(test)] mod tests { use super::*; + use rstest::rstest; /// Driver that runs `compile_program` for an error-only test, returning /// the collected error list. Discards the program — these tests only @@ -1252,6 +1253,52 @@ Error: lowering error ); } + /// The requirement sweep is a *third* blame path, beside emission's and + /// coalesce's, and it resolves to a span like both of them. + /// + /// It needs its own because it raises before coalesce and about a **place**, which + /// is not always some node's type: where a value's occurrences are split across + /// variables, the conflict sits at an interior place that only a *bound* reaches. + /// Blame is structural and does not follow bounds, so no node's type names a + /// variable standing there — which is why the failure offers the variable the walk + /// started from as well, and why both spellings below can name the lambda. + /// + /// Both are pinned because they are the same program: whether the parameters are + /// curried decides whether the place is interior, and the diagnostic must not + /// notice. Each case also puts a binding *before* the offending one, so the tree + /// root's own span is not the expected answer — without that, a blame path that had + /// silently collapsed to the root would still look correct here. + #[rstest] + #[case::curried( + "g = 2\nf = \\a -> (a + 1, a + \"s\")\ng\n", + "\\a -> (a + 1, a + \"s\")" + )] + #[case::uncurried( + "g = 2\nf = \\a, b -> (a + 1, a + \"s\")\ng\n", + "\\a, b -> (a + 1, a + \"s\")" + )] + fn unsatisfiable_operand_carries_resolved_span(#[case] code: &str, #[case] expected: &str) { + let errs = compile_err(code); + let (error, span) = errs + .iter() + .find_map(|e| match e { + CompileError::Infer { error, span } => Some((error, *span)), + _ => None, + }) + .unwrap_or_else(|| panic!("expected an Infer error, got: {errs:?}")); + assert!( + matches!(error, InferError::UnsatisfiableOperand { .. }), + "expected the sweep's own error, got {error:?}" + ); + let span = span.expect("an unsatisfiable operand resolves to a source span"); + assert_eq!( + &code[span.start..span.end], + expected, + "blame must land on a node enclosing the conflict, never the whole program \ + and never nothing", + ); + } + /// Terminal rendering: a span-carrying inference error renders /// as an ariadne report with the source line and an underline, NOT the /// bare `error: type inference: …` plain-text fallback. diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index ced14d52..21558ad9 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -320,13 +320,14 @@ repeats is dropped, so one defect stays one diagnostic however many specializati enclose it. **What this does not reach.** Resolution reads the bounds a body *recorded*, so a -requirement that only takes effect when a concrete type is **delivered** is not -evaluated here and cannot fail here. Trait obligations are the case: an obligation -narrows its candidate set as bases arrive, and one whose operand never receives a base -narrows nothing and so rejects nothing, however few implementations could ever satisfy -it. Closing that is a property of the obligation machinery — an unsatisfiable -*intersection* of the requirements on one variable is visible without any delivery — not -of this walk, which only decides whether the definition's copies are resolved at all. +requirement that takes effect only when a concrete type is **delivered** is not +evaluated here. Trait obligations are the case: an obligation narrows as bases arrive, +and one whose operand never receives a base rejects nothing, however few +instances could satisfy it. Reading a value's requirements *together* covers it, +which needs no delivery and is a separate pass +([Requirements are read together, once](#requirements-are-read-together-once)). The two +are complementary: that pass runs on every program, and this walk is what makes a dead +definition's bounds resolved in the first place. **A shape that looks like an escape and is not.** `if 𝑝: [x for x in xs if 𝑞] else: xs` is accepted with no call site, and rejected at one. That is not laxity: both arms' @@ -777,9 +778,9 @@ The two coincide only where the value's type already *is* the annotation, leavin * **Width.** `x : {a: Int} = (a=1, b=2)` binds `x` at `{a: Int}`, so `x.b` is an error. `x <: {a: Int} = (a=1, b=2)` binds `x` at the record's own type, which still has both fields, so `x.b` is `2`. * **Refinements.** A literal is typed by its own value ([A literal is refined by its own value](#a-literal-is-refined-by-its-own-value)), so `x : Int = 5` binds `x` at `Int` — the annotation is precisely what discards the singleton — while `x <: Int = 5` leaves it at `5`. Only the second still discharges `arr[x]`'s index-range obligation. -* **Delivery.** Trait narrowing consumes bases that *arrive* at an operand ([Delivery: the watch follows the edge](#delivery-the-watch-follows-the-edge)), and only the exact form puts one there — it binds at `Int`, while the bounded form binds at a variable that `Int` sits above. So `def f(x: Int): x + "s"` is rejected with no call site and `def f(x <: Int): x + "s"` is not, though both are ill-typed and both fail at the first call. +* **Delivery.** Trait narrowing consumes bases that *arrive* at an operand ([Delivery: the watch follows the edge](#delivery-the-watch-follows-the-edge)), and only the exact form puts one there — it binds at `Int`, while the bounded form binds at a variable that `Int` sits above. Both `def f(x: Int): x + "s"` and `def f(x <: Int): x + "s"` are ill-typed and both are rejected with no call site, but not by the same machinery: the exact form delivers `Int`, which narrows the obligation until `"s"` empties it, while the bounded form delivers nothing and is caught instead by [Requirements are read together, once](#requirements-are-read-together-once), reading the requirement against the bound already recorded on the value. - This last one is a difference in *reach*, not in meaning, and it is the only bullet here that is: reading the requirements on a value together with its bounds — rather than one delivery at a time — catches the bounded program too, which is the residual gap [Typechecking a never-called definition](#typechecking-a-never-called-definition) already names and locates in the obligation machinery. Do not read it as the split saying that `x <: Int` promises less; what it promises is stated above, and this row is about which mechanism happens to notice. + This last one is a difference in *reach*, not in meaning, and it is the only bullet here that is. Do not read it as the split saying that `x <: Int` promises less; what it promises is stated above, and this row is about which mechanism happens to notice. The refinement case is worth reading twice: the annotation is a bare `Int` and the forms still differ, because `5` is a strict subtype of `Int`. A "simple" annotation is no guarantee that the two agree — only a value that knows nothing beyond the annotation is. @@ -1338,11 +1339,48 @@ A position that stays in the second row for the whole program — nothing ever d ### What an obligation determines -A deposit records what every surviving instance agrees on, and reaches the **associated positions only**. Nothing is written back onto an operand. +A deposit records what every surviving instance agrees on. It reaches both kinds of position, at opposite polarities: -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. +| position | bound | because | +|---|---|---| +| associated | **lower** | the obligation is its only source — nothing else constrains it from below | +| operand | **upper** | the table states what *may* reach the operand, not what does | + +A lower bound on an operand would invent a value the program never supplied, and would let an under-connected lowering pass by supplying the type its missing edge should have carried. An upper bound cannot: it gives coalesce nothing to resolve *to*. + +How much is determined follows from the table. `λ 𝑥 → 𝑥 + 1` is `Int ⇒ Int`, because `Int` at the second position leaves only `Addable(Int, Int ⇝ Int)` and one surviving row fixes every position of it. `λ 𝑎 𝑏 → 𝑎 + 𝑏` determines nothing, and both parameters stay open. Adding `Addable(Float, Int ⇝ Float)` would reopen the first case, two rows disagreeing — which is why a deposit waits for agreement rather than firing on a unique candidate. + +### Requirements are read together, once + +Narrowing consumes one contribution at a time, so an obligation learns only what is *delivered* to it. Requirements that are individually satisfiable and jointly not therefore pass: in `λ 𝑎 → (𝑎 + 1, 𝑎 + "s")` each obligation narrows through its **other** operand, to `{Int}` and `{String}`; neither set is empty, and nothing compares them. + +A pass between emission and coalesce closes this. For each value it intersects what every requirement on that value accepts, with three outcomes: + +* **Empty** — nothing satisfies them all, so no argument could. `UnsatisfiableOperand`, listing each requirement together with what the trait's other operand accepts, that being what narrowed it. +* **One base** — the requirements determine the value. It is deposited as an upper bound, and the obligations there are narrowed by it directly, since an upper bound does not reach them on its own. +* **Several** — the value stays open. + +Before depositing, the pass reads the bounds the value already carries. A base that disagrees is `RequirementContradictsBound`, naming both it and the required type. Left to the write, the same contradiction reaches coalesce as two `IncompatibleBounds` naming no trait: a *bounded* annotation and a monomorphic operator's operand are ordinary bounds, so no intersection of requirements sees them. An *exact* annotation does not reach here at all — it delivers a base, so the obligation narrows and fails on its own ([Annotation kinds: exact and bounded](#annotation-kinds-exact-and-bounded)). + +Both rejections say no argument could work, and they differ in what collides. An empty intersection is the requirements contradicting each other. A bound conflict is the requirements agreeing, on something the program has already ruled out. + +Placement is forced at both ends. **After emission**, because that is when a definition's requirements are all recorded. **Before coalesce**, because a generalized definition's subtree is never coalesced in place, so a walk of the tree would see only use-site clones — and a clone that goes unsatisfiable already fails by delivery. The pass repeats **to a fixpoint**: determining one value can leave a neighbouring obligation with a single row, determining another. -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. +This is the gap [Typechecking a never-called definition](#typechecking-a-never-called-definition) names. The two are complementary. That walk resolves a dead definition's recorded bounds, which catches `λ 𝑎 → (𝑎.0, 𝑎.foo)`; this pass needs no delivery, and does not depend on whether anything calls the definition. + +#### The unit is a place, not a variable + +Every position of a requirement is an ordinary inference variable, but a requirement is *about* a value, and one value is generally several variables. A **place** is that value. It is named by a root variable plus the path of field selections reaching it — each element of the path a **step** — and the empty path names the root's own value. `places_under` returns, per place, the variables standing at it together with the requirements they carry; it is one *place*'s requirements that are read together. + +Places are found by following **upper** bounds: `𝑣 <: 𝑈` means `𝑣`'s value reaches `𝑈`, so a requirement on `𝑈` is one on `𝑣`. A variable bound stays at the same place, `𝑣` and `𝑈` being two variables for one value; a structural one descends, so in `𝑣 <: (𝑈₀, 𝑈₁)` the requirements on `𝑈₀` belong one field deeper and not to `𝑣`. Each `𝑈ᵢ` is itself a variable, which is why the path is load-bearing rather than decorative: it is what separates the value `𝑈₀` stands for from `𝑣`'s, and what lets variables reached by different routes be recognized as one value. + +A variable alone is the wrong unit because the parameter a programmer writes is not one variable. `λ 𝑎 𝑏 → …` uncurries to a lambda over a tuple and rewrites each occurrence of `𝑎` to a projection of that tuple, so each occurrence has its own inference variable and none of them carries both of `𝑎`'s requirements. Written curried, `𝑎` is a binder its occurrences share, and one variable carries both. Only the spelling differs. + +Which positions are steps is decided per type former, by an exhaustive match. The rules are one comment per former at `places_under`, in `src/ccl/infer/solver/traits.rs`. + +A function's **codomain** is a step; its **domain** is not. Descent groups requirements that constrain the same value, and is not how they are reached — every variable is a root, so all requirements are reached regardless. Across `𝑣 <: (𝐷 ⇒ 𝐶)` and `𝑣 <: (𝐷′ ⇒ 𝐶′)`, the codomains `𝐶` and `𝐶′` consume one value, `𝑣`'s result, and so group. `𝐷` and `𝐷′` are two arguments feeding one parameter — two values — and intersecting their requirements would ask a question the program does not pose. `dom(𝑣)` is a root in its own right, so nothing is missed. + +Reading the graph once, at the end, is what [`link_watches`](#delivery-the-watch-follows-the-edge) cannot do: it runs when an edge is **recorded**, so an edge predating an obligation never carries it, and it follows **variable** edges only, stopping at the structural hop a multi-parameter lambda introduces. Two consequences: currying is unobservable, `λ 𝑎 𝑏 → (𝑎 + 1, 𝑎 < 𝑏)` and its curried form taking one type; and `λ 𝑎 𝑏 → (𝑎 + 𝑏, 𝑎 + 1, 𝑏 + "s")` is rejected, where no single requirement is wrong and no variable carries two. Two problems look like they want an obligation of their own, and are not: @@ -1375,12 +1413,6 @@ 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 resolves 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/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index 77446c6c..70f91031 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -111,6 +111,12 @@ impl InferArena { // resolve variables that no longer have bounds. #[cfg(debug_assertions)] crate::ccl::infer::solver::traits::clear_watch_log(); + // So is the requirement sweep's narrowing window, and for a sharper reason: + // its mark indexes a process-global obligation counter, so one left behind by + // an earlier run on this thread sits below everything this run mints and would + // make the check pass without checking. + #[cfg(debug_assertions)] + crate::ccl::infer::solver::traits::unseal_emission(); InferArena { _not_send_sync: std::marker::PhantomData, } @@ -254,6 +260,59 @@ impl DerefMut for TypeInferenceContext { // InferError // --------------------------------------------------------------------------- +/// One trait requirement on a value, as a diagnostic states it. +/// +/// The solver-side [`OperandRequirement`](crate::ccl::infer::solver::traits::OperandRequirement) +/// rendered for display: types instead of bases, and the trait named rather than +/// referenced, so nothing in a message borrows the solver's vocabulary. +#[derive(Clone, PartialEq)] +pub struct StatedRequirement { + /// The trait that placed the requirement. + pub trait_: String, + /// Which of its operand positions the value stands at. + pub position: u8, + /// What that position still accepts. + pub accepted: Vec, + /// The trait's other operand positions and what each still accepts — the reason + /// this position is narrowed the way it is, which is otherwise invisible. + pub siblings: Vec<(u8, Vec)>, +} + +/// `Addable accepts only String as its operand 1 (its operand 2 is String)`. +/// +/// The parenthetical is what makes the line a reason rather than an assertion: a bare +/// "only `String` here" is a *consequence* of what reached the operand beside it, and +/// without naming that the reader is told the conclusion and left to reconstruct the +/// premise. Positions are printed 1-based, as everywhere else in these messages. +/// Omitted for a unary trait, which has no beside. +impl std::fmt::Display for StatedRequirement { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + fn or_list(types: &[Type]) -> String { + types + .iter() + .map(|t| t.to_string()) + .collect::>() + .join(" or ") + } + write!( + f, + "{} accepts only {} as its operand {}", + self.trait_, + or_list(&self.accepted), + self.position + 1, + )?; + let because = self + .siblings + .iter() + .map(|(pos, accepted)| format!("its operand {} is {}", pos + 1, or_list(accepted))) + .collect::>(); + if !because.is_empty() { + write!(f, " ({})", because.join(", "))?; + } + Ok(()) + } +} + /// Errors that can occur during limited type inference. /// /// # The `at` / `ctx` / `origin` label fields are for *display*, not location @@ -385,6 +444,33 @@ pub enum InferError { /// Display label for the message (see the type docs — not the location). at: String, }, + /// One value carries two or more trait requirements that no type satisfies at + /// once — `\a -> (a + 1, a + "s")` needs `a` to be both `Int` and `String`, so the + /// definition is ill-typed for every possible argument and is rejected with no + /// call site. + /// + /// Distinct from [`InferError::NoTraitInstance`] because **nothing arrived**: no + /// operand type is wrong, and there is none to show. What conflicts is the + /// requirements, so the message lists them and what each still accepts. + UnsatisfiableOperand { + /// One entry per requirement on the value. + requirements: Vec, + }, + /// The requirements on one value agree on a type, and the value is already + /// something else — `def f(x: Int): x + "s"` requires `String` of a parameter the + /// annotation fixed at `Int`. + /// + /// The sibling of [`InferError::UnsatisfiableOperand`]: there the requirements + /// contradict each other, here they agree and contradict the program. Both mean no + /// argument could ever work, and this one can name the type that rules it out. + RequirementContradictsBound { + /// The requirements, which together determined `required`. + requirements: Vec, + /// The type they agree the value must be. + required: Box, + /// The type the value already has. + found: Box, + }, /// A partial tuple or partial record was not resolved to a concrete type. UnresolvedPartial { /// Display string of the partial type. @@ -628,6 +714,32 @@ impl std::fmt::Debug for InferError { position + 1, ) } + InferError::UnsatisfiableOperand { requirements } => { + writeln!( + f, + "No type satisfies every requirement placed on this value, so it \ + can never be called:" + )?; + for r in requirements { + writeln!(f, " {r}")?; + } + Ok(()) + } + InferError::RequirementContradictsBound { + requirements, + required, + found, + } => { + writeln!( + f, + "This value is already {found}, but it is required to be \ + {required}, so it can never be called:" + )?; + for r in requirements { + writeln!(f, " {r}")?; + } + Ok(()) + } 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. diff --git a/src/ccl/infer/mod.rs b/src/ccl/infer/mod.rs index ded0edd0..9256bdce 100644 --- a/src/ccl/infer/mod.rs +++ b/src/ccl/infer/mod.rs @@ -142,6 +142,97 @@ pub(super) fn variant_type(tags: BTreeMap) -> Type { Type::Variant(tags.into_iter().collect()) } +/// The node to blame for a fact about a *place* — given the variables standing at it, +/// the first node, in pre-order, whose own type mentions any of them. +/// +/// Several variables because a place is not a variable: the requirements that +/// contradict each other can sit on operator-minted variables no node's type ever +/// names, while the value they constrain is a component of one that is. Each is tried +/// in turn, against the whole tree, and the first that appears anywhere wins — so the +/// result is the earliest *variable* that is named, not the outermost *node* naming +/// any of them. Sharpening that would mean walking the tree once and asking each node +/// about every variable, which buys a better span for a case that already falls back +/// to a coarse one. +/// +/// Blame is read *out of the tree* rather than stamped onto the solver structure that +/// raised it. A `NodeId` is provenance, and a copy of one squirrelled away in the +/// solver would be copied onward by every clone that structure makes — outliving the +/// construct it identifies. The tree cannot go stale that way, because it *is* the +/// thing being described. +/// +/// Falls back to the root, so a span can be coarse but never wrong — an interior place +/// is exactly the case where that can happen. Only reached on a failure path, so the +/// walk costs nothing in the passing case. +fn blame_node_for_place( + expr: &Expr, + uids: &[crate::ccl::InferVarId], +) -> crate::ccl::provenance::NodeId { + /// Structural only — deliberately does **not** follow a variable's bounds. The + /// question is which node's type *is written in terms of* this variable, and + /// chasing bounds would answer a different one (nearly every node, transitively). + /// + /// Exhaustive on purpose: a new [`Type`] variant that can hold a type must break + /// this build rather than silently degrade a span to the program root. + fn mentions(ty: &Type, uid: crate::ccl::InferVarId) -> bool { + match ty { + Type::Infer(v) => v.uid == uid, + Type::Refinement(inner, _) => mentions(inner, uid), + // Unlike the solver walks, this one reads *node type slots* and runs + // before coalesce clears annotations, so a bounded annotation is still + // in place. Its bound is an ordinary type and can name the variable. + Type::BoundedHole(bound) => mentions(bound, uid), + Type::Fun { + domain, codomain, .. + } => mentions(domain, uid) || mentions(codomain, uid), + Type::History { value, domain, .. } => mentions(value, uid) || mentions(domain, uid), + Type::Tuple(elems) => elems.iter().any(|t| mentions(t, uid)), + Type::Record(fields) => fields.iter().any(|(_, t)| mentions(t, uid)), + Type::Variant(arms) => arms.iter().any(|(_, t)| mentions(t, uid)), + Type::Base(_) + | Type::UIntRange(_) + | Type::Hole + | Type::SharedHole(_) + | Type::DataSource(_) + | Type::ChanDom(_, _) + | Type::Txn => false, + } + } + /// The slots that make this node *itself* the place: its own type, an + /// annotation written on it, a cast's target. Deliberately **not** the + /// binder slots [`Expr::walk_type_slots`] also visits — a binder's type is + /// always mirrored either in the node's own type (a lambda's domain is its + /// type's domain) or in a child's (a `let` binder's type is the + /// definition's), so a binder slot never reaches a variable the walk would + /// otherwise miss. It only lets an enclosing node answer for a type its + /// child owns, which costs the span its precision: with the binder slot + /// counted, `f = \a -> …` shadows the `\a -> …` that actually carries the + /// conflicting requirements. + fn owns(e: &Expr, uid: crate::ccl::InferVarId) -> bool { + let own = mentions(&e.ty, uid); + let annotated = e.user_annotation.as_ref().is_some_and(|a| mentions(a, uid)); + let cast = matches!( + &e.node, + crate::ccl::TypedExprNode::Cast { target, .. } if mentions(target, uid) + ); + own || annotated || cast + } + fn go(e: &Expr, uid: crate::ccl::InferVarId) -> Option { + if owns(e, uid) { + return Some(e.node_id()); + } + let mut found = None; + e.walk_children(|child| { + if found.is_none() { + found = go(child, uid); + } + }); + found + } + uids.iter() + .find_map(|uid| go(expr, *uid)) + .unwrap_or_else(|| expr.node_id()) +} + /// Resolve a (possibly variable-laden) [`Type`] to a concrete type for use /// in error messages. Falls back to [`Type::Hole`] if coalesce fails (which /// can happen for types with incompatible bounds that triggered the error). @@ -374,6 +465,67 @@ pub(crate) fn run( #[cfg(debug_assertions)] solver::traits::verify_narrowing_is_complete(|ty| resolve_var_type(ty).ok()); + // Every requirement a definition places on one of its own values is recorded by + // now, so this is where they can be read *together* — the step narrowing cannot + // take, since it only ever sees one contribution at a time. Runs before coalesce + // for two reasons: the tree is still whole, so a conflict can be blamed on a real + // node, and a generalized definition's variables are still reachable, which after + // coalesce they are not. + { + use solver::traits::{OperandFailure, OperandRequirement}; + /// Render a solver-side requirement for display: bases become types, and the + /// trait becomes its name, so no message borrows the solver's vocabulary. + fn stated(r: OperandRequirement) -> StatedRequirement { + StatedRequirement { + trait_: r.trait_.to_string(), + position: r.position, + accepted: r.accepted.into_iter().map(Type::Base).collect(), + siblings: r + .siblings + .into_iter() + .map(|(pos, accepted)| (pos, accepted.into_iter().map(Type::Base).collect())) + .collect(), + } + } + let mut cache = solver::ConstrainCache::new(); + if let Err(failure) = solver::traits::resolve_operand_requirements(&mut cache) { + let (blame_vars, error) = match failure { + OperandFailure::Unsatisfiable { vars, requirements } => ( + vars, + InferError::UnsatisfiableOperand { + requirements: requirements.into_iter().map(stated).collect(), + }, + ), + OperandFailure::ContradictsBound { + vars, + requirements, + required, + found, + } => ( + vars, + InferError::RequirementContradictsBound { + requirements: requirements.into_iter().map(stated).collect(), + required: Box::new(Type::Base(required)), + found: Box::new(Type::Base(found)), + }, + ), + // See `OperandFailure::Conflict`: no program is known to reach this, + // so it takes the generic vocabulary rather than one of its own. + OperandFailure::Conflict { error } => ( + Vec::new(), + map_constrain_err(error, "a value an operator constrains"), + ), + }; + let node_id = blame_node_for_place(expr, &blame_vars); + return Err(vec![LocatedInferError { error, node_id }]); + } + } + // Sealed *after* the requirement sweep, not before: the sweep itself narrows, and + // legitimately so. What must not happen is a later pass narrowing a definition's + // obligation, which would leave the sweep's verdict stale. + #[cfg(debug_assertions)] + solver::traits::seal_emission(); + // 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/solver/traits.rs b/src/ccl/infer/solver/traits.rs index ed5e098b..c08119c5 100644 --- a/src/ccl/infer/solver/traits.rs +++ b/src/ccl/infer/solver/traits.rs @@ -38,10 +38,20 @@ //! [`FunKindVar`](crate::ccl::ty::FunKindVar) already uses for kinds; no phase runs //! "once everything is known". Each operand position carries a **candidate set** of //! 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 -//! ever written back onto an operand. +//! associated type is deposited on its position once every surviving candidate *agrees* +//! on it ([`TraitObligation::try_deposit`]) — agreement, not a lone survivor. +//! +//! Delivery only ever offers one contribution at a time, so it cannot see two +//! requirements that are individually satisfiable and jointly are not. +//! [`resolve_operand_requirements`] is the pass that reads a value's requirements +//! together: an empty intersection is rejected, and a singleton is deposited as an +//! **upper** bound on the operand — the polarity is what keeps that a restatement of +//! the requirement rather than an invented value. +//! +//! Its unit is a [`Place`] — one value, however many variables stand at it — rather +//! than a variable, because a multi-parameter lambda passes its parameters through a +//! tuple and so splits one value's occurrences across several variables. Currying a +//! program must not change what it means. //! //! 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 @@ -51,19 +61,20 @@ //! //! `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, 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. +//! operator's requirement on its own, why the two deposit polarities are not the same +//! move, why the requirement sweep sits between emission and coalesce and runs to a +//! fixpoint, 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; use std::rc::Rc; use std::sync::atomic::{AtomicU32, Ordering}; -use crate::ccl::{BaseType, InferVar, Type}; +use crate::ccl::{BaseType, FieldKey, InferVar, InferVarId, Type}; use super::constrain::{ConstrainCache, ConstrainError, constrain_subtype}; @@ -73,7 +84,9 @@ use super::constrain::{ConstrainCache, ConstrainError, constrain_subtype}; /// Closed and built-in. The set is the operators the language has, not a user /// 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)] +/// `Ord` so a diagnostic can order the requirements it lists. Resolution does not +/// depend on it: a candidate set is a set, and the verdict is an intersection. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum Trait { /// `+` over `(𝐴, 𝐵)`, associating `Output`. The `(String, String) ⇝ String` row is /// why surface `+` on strings types through arithmetic; `simplify` rewrites it to @@ -432,15 +445,23 @@ impl TraitObligation { trait_: self.trait_, position: pos, found: found.clone(), - accepted: self - .candidates - .borrow() - .iter() - .filter_map(|i| i.args.get(pos as usize).cloned()) - .collect(), + accepted: self.accepted_at(pos), }) } + /// The trait's operand positions *other* than `pos`, with what each still accepts. + /// + /// Arity is read off a surviving row rather than stored: every row of a trait has + /// a type at every position that trait declares, which is the same invariant + /// [`accepted_at`](Self::accepted_at) rests on. + fn siblings_of(&self, pos: u8) -> Vec<(u8, Vec)> { + let arity = self.candidates.borrow().first().map_or(0, |i| i.args.len()); + (0..arity as u8) + .filter(|i| *i != pos) + .map(|i| (i, self.accepted_at(i))) + .collect() + } + /// Restrict position `pos` to instances accepting `base`, then deposit the /// output if that settles it. /// @@ -453,15 +474,23 @@ impl TraitObligation { base: &BaseType, cache: &mut ConstrainCache, ) -> Result<(), ConstrainError> { + // Read before the mutable borrow: "what this position could have accepted" is + // only meaningful before the contribution rules rows out. + let accepted = self.accepted_at(pos); { let mut candidates = self.candidates.borrow_mut(); - let accepted: Vec = candidates - .iter() - .filter_map(|i| i.args.get(pos as usize).cloned()) - .collect(); + #[cfg(debug_assertions)] + let before = candidates.len(); // 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)); + // Re-delivery of a fact already recorded is the common case and changes + // nothing; only an actual shrink can move the verdict this obligation + // contributes, so only a shrink is worth policing. + #[cfg(debug_assertions)] + if candidates.len() < before { + assert_narrowing_is_still_open(self); + } if candidates.is_empty() { return Err(ConstrainError::NoTraitInstance { trait_: self.trait_, @@ -507,6 +536,10 @@ impl TraitObligation { /// /// Order follows the instance table, so a caller that picks positionally picks /// reproducibly. + /// + /// Never empty for a position the trait's arity reaches: a candidate set is + /// non-empty by invariant (emptying it is the error), and every instance of a + /// trait carries a type at every position that trait declares. pub fn accepted_at(&self, pos: u8) -> Vec { self.candidates .borrow() @@ -627,6 +660,528 @@ pub fn verify_narrowing_is_complete(resolve: impl Fn(&Type) -> Option) { }); } +#[cfg(debug_assertions)] +thread_local! { + /// The obligation-counter high-water mark at the moment the requirement sweep + /// finished, or `None` before it runs. + /// + /// [`resolve_operand_requirements`] reads candidate sets as final. They are, *for + /// the obligations that matter*: a generalized definition's subtree is never + /// coalesced in place, so its variables take no new bounds afterwards, and the + /// narrowing that does continue during coalesce acts on the per-instantiation + /// clones `freshen_watches` mints — obligations that did not exist when the sweep + /// ran. The mark is what makes that checkable rather than merely argued: see + /// [`assert_narrowing_is_still_open`]. + static EMISSION_MARK: Cell> = const { Cell::new(None) }; +} + +/// Open the narrowing window, discarding any previous run's mark. +/// +/// Called from [`InferArena::new`](crate::ccl::infer::InferArena::new), which is the +/// construct whose lifetime this state shares: the mark is per-run for the same reason +/// the variable capture is. Resetting it is not optional bookkeeping. The mark is a +/// high-water mark of a *process-global* counter, so a stale one left by an earlier run +/// on this thread sits below every obligation the current run mints, and +/// [`assert_narrowing_is_still_open`] would pass vacuously instead of being inert — +/// checking nothing, and silently, which is the failure mode it exists to prevent. +#[cfg(debug_assertions)] +pub fn unseal_emission() { + EMISSION_MARK.with(|m| m.set(None)); +} + +/// Close it, recording which obligations existed at that point. +/// +/// Asserts the window was open, so the pairing with [`unseal_emission`] is checked +/// rather than remembered: a run that reached here without opening one is a run whose +/// mark belongs to a different run. +#[cfg(debug_assertions)] +pub fn seal_emission() { + EMISSION_MARK.with(|m| { + debug_assert!( + m.get().is_none(), + "sealing a window that was never opened — this run inherited mark {:?} from \ + an earlier run on this thread, so `unseal_emission` did not run at arena \ + entry", + m.get(), + ); + m.set(Some(OBLIGATION_COUNTER.load(Ordering::Relaxed))); + }); +} + +/// After emission, only an obligation minted *since* emission — a freshened clone — +/// may still narrow. +/// +/// This is the timing assumption [`resolve_operand_requirements`] rests on, and it is +/// exactly the kind that fails silently: a pass that narrowed a *definition's* +/// obligation during coalesce would leave the check reading a stale candidate set and +/// quietly stop rejecting programs it used to reject. Measured across the suite the +/// violation count is zero; this keeps it that way by name rather than by +/// re-measurement. +#[cfg(debug_assertions)] +fn assert_narrowing_is_still_open(obligation: &Rc) { + EMISSION_MARK.with(|m| { + let Some(mark) = m.get() else { + return; + }; + debug_assert!( + obligation.uid.0 >= mark, + "{obligation:?} was minted during emission but narrowed after it — \ + `resolve_operand_requirements` read this obligation's candidate set as \ + final at end of emission, so whatever narrowed it here is invisible to the \ + check. Either the check has to move later, or this write belongs in \ + emission.", + ); + }); +} + +/// One requirement a single operand carries: which trait asked, at which of its +/// positions, and what that position can still accept. +/// +/// Several on one variable is the ordinary case — `𝑥 + 1 > 2` requires `Addable` and +/// `Orderable` of `𝑥` — and they compose exactly when some type satisfies them all. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)] +pub struct OperandRequirement { + /// The trait that placed the requirement. + pub trait_: Trait, + /// Which of its operand positions this variable stands at. + pub position: u8, + /// The bases still accepted there. + pub accepted: Vec, + /// The trait's *other* operand positions and what each still accepts. + /// + /// A requirement on its own reads as an unexplained demand — "only `Int` here" is + /// a consequence, not a premise. What narrowed the position is the type that + /// reached the operand beside it, so carrying the siblings lets a diagnostic say + /// where the demand came from without any provenance being recorded: they are read + /// off the same candidate set. Empty for a unary trait, which has no beside. + pub siblings: Vec<(u8, Vec)>, +} + +/// Find an operand no type can satisfy: two or more requirements on one variable +/// whose accepted sets have nothing in common. +/// +/// **The one check narrowing cannot make.** Narrowing is push-based, so an obligation +/// learns only what is *delivered*, and in `λ 𝑎 → (𝑎 + 1, 𝑎 + "s")` each of the two +/// obligations was narrowed through its **other** operand — one to `{Int}`, the other +/// to `{String}`. Neither set is empty, so neither failed; nothing compared them, and +/// the definition type-checked despite being ill-typed for every possible argument. +/// Delivery cannot close this, because the hole *is* the case where no type arrives. +/// +/// So the requirements are read together — the move coalesce makes on a variable's +/// bounds, applied to its obligations. `vars` is every variable minted during the run, +/// which is the only enumeration that reaches a definition: a generalized definition's +/// subtree is deliberately never coalesced in place, so walking the tree would see +/// only use-site clones, and a clone that goes unsatisfiable already fails by delivery. +/// +/// Returns the offending variable alongside its requirements; the caller supplies +/// blame, because node identity belongs to the tree and not to the solver. +pub fn resolve_operand_requirements(cache: &mut ConstrainCache) -> Result<(), OperandFailure> { + // A deposit is an ordinary `constrain_subtype`, so it can deliver a base to another + // variable's watches and shrink *their* candidate sets — which can determine a + // value that was open when this pass looked at it. So the sweep runs to a fixpoint + // rather than once. It terminates because candidate sets only shrink and the base + // vocabulary is finite; `deposited` is what makes "nothing new happened" cheap to + // decide, since re-depositing a bound the graph already carries is not progress. + let mut deposited: std::collections::HashSet<(InferVarId, BaseType)> = + std::collections::HashSet::new(); + loop { + let before = deposited.len(); + // Re-read the arena every pass rather than snapshotting once. Every variable + // being a root is what makes the sweep complete — it is why a function's domain + // needs no traversal of its own — and a deposit is an ordinary + // `constrain_subtype`, which is entitled to mint variables (an extrusion proxy, + // which `copy_watches` gives the original's requirements). Measured, the arena + // does not currently grow here; re-reading makes that irrelevant instead of + // load-bearing. + resolve_pass(&crate::ccl::infer_var::arena_vars(), cache, &mut deposited)?; + if deposited.len() == before { + return Ok(()); + } + } +} + +/// One step into a value: how a sub-place is reached from the place above it. +/// +/// Distinguished rather than collapsed onto [`FieldKey`] because a record field and a +/// variant arm of the same name are different positions, and a function's result is +/// neither. Merging any two of them would intersect requirements that constrain +/// different values, which is how a sweep like this produces a *false* rejection. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +enum Step { + /// A tuple position or a record field. + Field(FieldKey), + /// A variant arm's payload. + Arm(FieldKey), + /// A function's result. Its *domain* is deliberately not a step — see + /// [`places_under`]. + Result, + /// A history's value (the cell or element a `Mut`/`Feed` handle carries). + HistoryValue, +} + +/// The descent that reaches one place from the root of a sweep: the path of [`Step`]s +/// taken, empty at the root itself. +/// +/// Only ever a **key**, and only within one [`places_under`] call — two roots' paths +/// name unrelated values and are never compared. Nothing reads it back; it exists so +/// that variables reached by different routes land in the same bucket iff they stand +/// for the same value. +type StepPath = Vec; + +/// A **place**: one value, as the set of variables standing at it and every requirement +/// landing on them. +/// +/// The unit a requirement actually constrains, and the reason it is not the variable: +/// `λ 𝑎 𝑏 → …` uncurries to a lambda over a tuple and rewrites each occurrence of +/// `𝑎` to a projection of it, so each occurrence has its own variable and none carries +/// both of `𝑎`'s requirements, even though both constrain one value. Curried, `𝑎` is a +/// binder its occurrences share and one variable carries both — so a place holds +/// however many variables the spelling happens to split the value across, and the +/// intersection is taken over the whole set. +#[derive(Default)] +struct Place { + vars: Vec>, + reqs: Vec<(Rc, u8)>, +} + +/// Strip every refinement layer, as [`offered`] does: `{𝑇 | 𝑝}` constrains a place +/// exactly as `𝑇` does, so structure underneath a refinement is still structure. +fn peel_refinements(ty: &Type) -> &Type { + let mut cur = ty; + while let Type::Refinement(inner, _) = cur { + cur = inner; + } + cur +} + +/// Group everything reachable from `root` into the [`Place`] it constrains, keyed by +/// the [`StepPath`] that reaches it. +/// +/// Follows **upper** bounds, because `𝑣 <: 𝑈` means `𝑣`'s value reaches `𝑈` and so a +/// requirement on `𝑈` is a requirement on `𝑣`. A variable upper bound stays at the +/// same place; a *structural* one descends — `𝑣 <: (𝑈₀, 𝑈₁)` says `𝑣`'s component 0 +/// reaches `𝑈₀`, so `𝑈₀`'s requirements belong to the place one field deeper, never to +/// `𝑣` itself. +/// +/// Why this reads the graph once at the end rather than reusing `link_watches`, and +/// why the grouping is what licenses each step, are in +/// `src/ccl/design/type-inference.md`, "The unit is a place, not a variable". The arms +/// below carry the per-former reason; the design doc does not repeat them. +/// +/// The match on a bound's type is **exhaustive on purpose**. What the sweep reaches is +/// what "every requirement is read" means, so a new [`Type`] variant that can hold a +/// type has to fail this build and be classified deliberately — a wildcard arm would +/// let the grammar grow while the sweep quietly stopped covering it, and nothing would +/// fail. Peeling refinements at every step is the same concern one level down: matching +/// a bound's type directly would let a refined structural bound fall through to the +/// leaf arm, and the walk would stop at a place it should have descended past. +/// +/// `seen` is keyed on the *pair*, so a variable revisited at a different place is +/// revisited — which is correct, and which means a cycle through a **structural** upper +/// bound (`𝑣 <: (𝑢)`, `𝑢 <: (𝑣)`) would lengthen the path forever rather than being +/// absorbed. A variable cycle is fine: the path does not grow, so `seen` closes it. +/// Nothing builds the structural kind today — source-level recursion does not reach +/// inference (a self-call is an unbound variable) and `LetRec` is born after it — so +/// this is a precondition to re-check when recursive definitions arrive, not a live +/// hazard. +fn places_under(root: &Rc) -> std::collections::BTreeMap { + let mut out: std::collections::BTreeMap = Default::default(); + let mut seen: std::collections::HashSet<(InferVarId, StepPath)> = Default::default(); + let mut frontier = vec![(Rc::clone(root), StepPath::new())]; + while let Some((var, path)) = frontier.pop() { + if !seen.insert((var.uid, path.clone())) { + continue; + } + let entry = out.entry(path.clone()).or_default(); + entry.vars.push(Rc::clone(&var)); + for (obligation, pos) in var.watches.borrow().iter() { + if !entry + .reqs + .iter() + .any(|(o, p)| o.uid == obligation.uid && p == pos) + { + entry.reqs.push((Rc::clone(obligation), *pos)); + } + } + for bound in var.bounds.borrow().upper().iter() { + // Refinements are peeled at every step, for the same reason `offered` peels + // them: `{𝑇 | 𝑝}` constrains a place exactly as `𝑇` does, so a refined + // bound must not hide the structure underneath it. + match peel_refinements(&bound.ty) { + Type::Infer(up) => frontier.push((Rc::clone(up), path.clone())), + Type::Tuple(elems) => { + for (i, elem) in elems.iter().enumerate() { + descend(elem, &path, Step::Field(FieldKey::Index(i)), &mut frontier); + } + } + Type::Record(fields) => { + for (name, ty) in fields { + let key = FieldKey::Name(name.as_str().into()); + descend(ty, &path, Step::Field(key), &mut frontier); + } + } + Type::Variant(arms) => { + for (tag, payload) in arms { + descend(payload, &path, Step::Arm(tag.clone()), &mut frontier); + } + } + // The result only. Two codomains consume one value and group; two + // domains are two arguments and must not — the argument is in + // `src/ccl/design/type-inference.md`, "The unit is a place, not a + // variable". + // + // Measured, so the exclusion is not read as a known counterexample: + // descending into the domain as well changes no test outcome. Two + // incompatible sources for one monomorphic domain are already an + // `IncompatibleBounds`, and a polymorphic one freshens per use. It stays + // out because grouping distinct values is unlicensed, not because a + // program distinguishes the two traversals. + Type::Fun { + domain: _, + codomain, + .. + } => descend(codomain, &path, Step::Result, &mut frontier), + // The value a register or channel carries is a component of it in the + // same sense a field is; the domain beside it is an index, not a value + // this place holds. + Type::History { value, .. } => { + descend(value, &path, Step::HistoryValue, &mut frontier) + } + // Leaves: nothing inside to constrain. `Base`/`UIntRange` are concrete, + // and the rest are placeholders or nullary carriers. + Type::Base(_) + | Type::UIntRange(_) + | Type::Hole + | Type::SharedHole(_) + | Type::DataSource(_) + | Type::ChanDom(_, _) + | Type::Txn => {} + // `peel_refinements` returns a non-refinement by construction. + Type::Refinement(_, _) => unreachable!("refinements are peeled above"), + // `BoundedHole` is a *pre-inference* annotation marker: + // `normalize_annotation` erases it into a bounded variable before any + // constraint is emitted, so it is never a recorded bound. + Type::BoundedHole(_) => unreachable!( + "Type::BoundedHole reached the solver; `normalize_annotation` must erase it" + ), + } + } + } + out +} + +/// A concrete base already on `var` that `required` contradicts, if there is one. +/// +/// Both directions are read, and neither is redundant. A **lower** bound is a value +/// that already reaches the variable — an exact annotation, a literal — and it must be +/// *below* `required`, which for two distinct bases it is not. An **upper** bound is +/// another ceiling — a monomorphic operator's operand, a bounded annotation — and two +/// distinct base ceilings have no common value under them. Either way the requirement +/// cannot be satisfied, and one of the two is what the lattice would have reported. +/// +/// Bases only. A structural bound is a different mistake (a tuple where a trait wants a +/// base) and belongs to `Offered::NotABase`, which narrowing already rejects on arrival. +fn conflicting_base(var: &Rc, required: &BaseType) -> Option { + let bounds = var.bounds.borrow(); + bounds + .lower() + .iter() + .chain(bounds.upper().iter()) + .filter_map(|b| offered_base(&b.ty)) + .find(|base| *base != required) + .cloned() +} + +/// Queue `ty` one `step` below `path`, if it is a variable once refinements are peeled. +fn descend(ty: &Type, path: &StepPath, step: Step, frontier: &mut Vec<(Rc, StepPath)>) { + if let Type::Infer(up) = peel_refinements(ty) { + let mut deeper = path.clone(); + deeper.push(step); + frontier.push((Rc::clone(up), deeper)); + } +} + +fn resolve_pass( + vars: &[Rc], + cache: &mut ConstrainCache, + deposited: &mut std::collections::HashSet<(InferVarId, BaseType)>, +) -> Result<(), OperandFailure> { + for root in vars { + for place in places_under(root).into_values() { + if place.reqs.is_empty() { + continue; + } + let mut requirements: Vec = place + .reqs + .iter() + .map(|(obligation, pos)| OperandRequirement { + trait_: obligation.trait_, + position: *pos, + accepted: obligation.accepted_at(*pos), + siblings: obligation.siblings_of(*pos), + }) + .collect(); + // Sorted so a diagnostic lists them the same way for programs that differ + // only in spelling. `place.reqs` is in traversal order, which currying + // changes; the verdict does not depend on it, and the message should not + // either. + requirements.sort(); + debug_assert!( + requirements.iter().all(|r| !r.accepted.is_empty()), + "a live obligation accepts something at every position its trait \ + declares, but {requirements:?} has an empty set — either a candidate \ + set was emptied without raising, or a watch was placed past its \ + trait's arity", + ); + // The intersection: bases every requirement at this place accepts. + // Commutative, so the verdict does not depend on traversal order. + // Owned rather than borrowed from `requirements`, which the failure arms + // below move into the diagnostic. + let common: Vec = requirements[0] + .accepted + .iter() + .filter(|base| requirements[1..].iter().all(|r| r.accepted.contains(base))) + .cloned() + .collect(); + match common.as_slice() { + // Nothing satisfies every requirement, so no argument ever could. + [] => { + // Narrowest first, then the variable the walk reached them from. + // An *interior* place is reached only through a bound, and blame + // deliberately does not follow bounds, so no node's type can ever + // name a variable standing there — without the root as a candidate + // the walk finds nothing and lands on the tree root, which is a + // different statement entirely rather than a wider one. + let blame = place + .vars + .iter() + .map(|v| v.uid) + .chain(std::iter::once(root.uid)) + .collect(); + return Err(OperandFailure::Unsatisfiable { + vars: blame, + requirements, + }); + } + // Exactly one base left: the requirements *determine* this value, so say + // so on the lattice rather than keeping it to ourselves. This is the + // write-back that makes `λ 𝑥 → 𝑥 + 1` infer `Int ⇒ Int` instead of + // leaving the parameter open, and it is what lets a requirement collide + // with an ordinary bound — an annotation, or a monomorphic operator's + // operand — which comparing requirements against each other cannot do. + // + // An **upper** bound, and the polarity is the whole argument for why + // this is not "recovering information the program should have supplied": + // it states what may flow in, which is exactly what the requirement + // says. It adds no lower bound, so a genuinely under-connected value is + // still under-determined afterwards. + [only] => { + for var in &place.vars { + // Read the lattice before writing to it. `constrain_subtype` + // *records* a bound rather than checking it against the ones + // already there, so a requirement contradicting an annotation or + // a monomorphic operator's operand would otherwise surface at + // coalesce as a bare `IncompatibleBounds` — twice, once per + // direction, and with no mention of the trait that demanded it. + // The facts are all here, so the diagnostic is made here. + if let Some(found) = conflicting_base(var, only) { + return Err(OperandFailure::ContradictsBound { + vars: place + .vars + .iter() + .map(|v| v.uid) + .chain(std::iter::once(root.uid)) + .collect(), + requirements, + required: (*only).clone(), + found, + }); + } + if !deposited.insert((var.uid, (*only).clone())) { + continue; + } + let deposit = Type::Base((*only).clone()); + constrain_subtype(&Type::Infer(Rc::clone(var)), &deposit, cache) + .map_err(|error| OperandFailure::Conflict { error })?; + } + // The bound alone does not reach the obligations at this place: it + // is an *upper* bound and narrowing consumes lower ones. So tell + // them directly. This is not new information — the intersection just + // proved the place accepts nothing else — but recording it is what + // lets the fact travel: pinning `𝑎` to `Int` leaves `Addable(𝑎, 𝑏)` + // with one row, which determines `𝑏` next round. + for (obligation, pos) in &place.reqs { + obligation.narrow(*pos, only, cache).map_err(|error| { + debug_assert!( + false, + "narrowing by a base the intersection just proved \ + acceptable emptied {obligation:?} at operand {pos}", + ); + OperandFailure::Conflict { error } + })?; + } + } + // Several bases still satisfy everything: the requirements genuinely do + // not pin the value, and leaving it open is the honest answer. + _ => {} + } + } + } + Ok(()) +} + +/// Why [`resolve_operand_requirements`] rejected a value. +pub enum OperandFailure { + /// No type satisfies every requirement on it — ill-typed for every argument. + /// + /// Raised for the first such place found, matching emission next door (also + /// fail-fast, also at most one error). *Whether* a program is rejected does not + /// depend on order — the intersection is commutative — but *which* place is named, + /// when a program has several, follows the order variables were minted in. + Unsatisfiable { + /// Blame candidates, narrowest first: the variables standing at the offending + /// place, then the variable the walk reached them from. The caller takes the + /// first one the expression tree actually mentions. + /// + /// The root is on the list because it is the only candidate an *interior* place + /// has. Such a place is reached through a bound, and blame is structural — + /// deliberately not following bounds — so no node's type ever names a variable + /// standing there, and a list of those alone would always come up empty. + vars: Vec, + /// Every requirement landing on that place. + requirements: Vec, + }, + /// The requirements determine one base, and the value already carries a different + /// one — from an annotation, a literal, or a monomorphic operator's operand. + /// + /// Distinct from [`Unsatisfiable`](Self::Unsatisfiable): there the requirements + /// contradict *each other*, and no bound need exist at all. Here each requirement + /// is satisfiable and they agree with one another; what they agree on is what the + /// program has already ruled out. Both are "no argument could work", found by + /// different comparisons, and only this one has a type to point at. + ContradictsBound { + /// Blame candidates, as [`Unsatisfiable::vars`](Self::Unsatisfiable). + vars: Vec, + /// The requirements, which together determined `required`. + requirements: Vec, + /// The base they determine. + required: BaseType, + /// The base already on the value. + found: BaseType, + }, + /// The lattice refused the deposit. + /// + /// **Not known to be reachable.** `constrain_subtype` *records* a bound rather than + /// checking it against those already present, so the contradiction this would name + /// is caught one step earlier, by reading the bounds directly + /// ([`ContradictsBound`](Self::ContradictsBound)). Kept because the call is + /// fallible and swallowing its error would be worse than carrying an arm for it. + Conflict { + /// Whatever the lattice objected to. + error: ConstrainError, + }, +} + /// 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 diff --git a/src/ccl/infer_var.rs b/src/ccl/infer_var.rs index 70ea0058..4928df3e 100644 --- a/src/ccl/infer_var.rs +++ b/src/ccl/infer_var.rs @@ -359,6 +359,16 @@ pub(crate) fn arena_exit() -> Vec> { ACTIVE_ARENA.with(|slot| slot.borrow_mut().take().unwrap_or_default()) } +/// Every variable minted so far this run, *without* ending the arena. +/// +/// The enumeration a whole-graph check needs. Unlike a walk of the expression tree +/// this reaches variables no node's type mentions any more — in particular a +/// generalized definition's, which coalesce deliberately never visits in place. Hands +/// back a snapshot rather than a borrow so a caller is free to touch the arena. +pub(crate) fn arena_vars() -> Vec> { + ACTIVE_ARENA.with(|slot| slot.borrow().clone().unwrap_or_default()) +} + impl InferVar { /// Mint a fresh, unconstrained inference variable at `level`. /// diff --git a/tests/type_check.rs b/tests/type_check.rs index 4e65cb91..09bdbc19 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -508,6 +508,243 @@ fn a_mut_var_that_reads_itself_still_gets_a_type(#[case] code: &str, #[case] bas assert_eq!(mut_var_value_type(code).to_string(), base); } +/// A definition whose requirements no single type satisfies is rejected **with no call +/// site** — it is ill-typed for every possible argument, so there is nothing to wait for. +/// +/// Two mechanisms cover this between them, and the split follows how the program's +/// occurrences share variables. Where one variable carries several requirements (a +/// single-parameter lambda), intersecting the accepted sets rejects directly. Where the +/// occurrences sit on *different* variables (a multi-parameter lambda destructures its +/// tuple parameter, so each use is its own projection), no intersection sees the +/// conflict — the requirement is instead written back as a bound, and the collision is +/// an ordinary one. Neither mechanism subsumes the other; `neither_degenerates` needs +/// the first and `multi_arg` needs the second. +#[rstest] +#[case::two_traits_disjoint("f = \\a -> (a + 1, a + \"s\")")] +#[case::neither_degenerates("f = \\a -> (a // a, a + \"s\")")] +#[case::orderable_vs_addable("f = \\a -> (a < 1, a + \"s\")")] +#[case::negatable_vs_addable("f = \\a -> (-a, a + \"s\")")] +#[case::three_way("f = \\a -> (a + 1, a + \"s\", a and True)")] +#[case::multi_arg("f = \\a, b -> (a + 1, a + \"s\")")] +#[case::multi_arg_def(indoc! {r#" + def f(a, b): + (a + 1, a + "s") +"#})] +// A requirement against an ordinary bound, which comparing requirements cannot see: +// `and` is a monomorphic scheme, and an annotation is a plain bound. +#[case::monomorphic_operator("f = \\a -> (a and True, a + 1)")] +#[case::annotation(indoc! {r#" + def f(x: Int): + x + "s" +"#})] +// The requirement travels through a call: `f`'s instantiated obligation is watched by +// `x`, where it meets the one `x + "a"` placed. +#[case::across_a_call(indoc! {r#" + f = \x -> x + 1 + def g(x): + a = x + "a" + f(x) +"#})] +// Only unsatisfiable transitively: `a + 1` pins `a`, which leaves `a + b` one row and +// so pins `b`, which `b + "s"` then contradicts. Nothing is wrong with any single +// requirement, and no *variable* carries two — the conflict exists only at the place. +#[case::transitively("f = \\a, b -> (a + b, a + 1, b + \"s\")")] +#[case::transitively_def(indoc! {r#" + def f(a, b): + (a + b, a + 1, b + "s") +"#})] +// Two transitive hops: `a + 1` pins `a`, so `a + b` pins `b`, so `b + c` pins `c`, +// which `c + "s"` contradicts. +#[case::two_hops("f = \\a, b, c -> (a + b, b + c, a + 1, c + \"s\")")] +// The place reached by a field selection rather than a tuple position. +#[case::record_field(indoc! {r#" + def f(r): + (r.x + 1, r.x + "s") +"#})] +#[case::tuple_field(indoc! {r#" + def f(p): + (p.0 + 1, p.0 + "s") +"#})] +// A requirement on a function's *result*, reached through the call rather than a field. +#[case::higher_order("f = \\g -> (g(1) + 1, g(1) + \"s\")")] +// The two requirements meet only through an intervening binding. +#[case::through_a_let(indoc! {r#" + def f(a): + c = a + (c + 1, a + "s") +"#})] +fn a_definition_no_argument_satisfies_is_rejected(#[case] defs: &str) { + assert!( + !infer_program_err(&dead_code(defs)).is_empty(), + "no type satisfies every requirement here, so no call site could ever make it \ + well-typed", + ); +} + +/// The rejection above is reported as its **own** error, naming every requirement and +/// what each still accepts. +/// +/// This is what distinguishes it from `NoTraitInstance`, and the distinction is the reason +/// the variant exists: nothing *arrived*, so there is no offending type to show and a +/// message shaped around one would have to invent it. The conflicting demands are the +/// only facts there are, so they are what the message carries — and each requirement +/// names its trait, so a conflict spanning two of them reads as such. +/// +/// (The span this resolves to is `unsatisfiable_operand_carries_resolved_span`, in +/// `src/ccl/context.rs`, where the lowering projection is in scope.) +#[rstest] +#[case::one_trait("f = \\a -> (a + 1, a + \"s\")", &["Addable", "Int", "String"])] +#[case::two_traits("f = \\a -> (a < 1, a + \"s\")", &["Orderable", "Addable", "Int", "String"])] +fn an_unsatisfiable_operand_names_the_requirements(#[case] defs: &str, #[case] expected: &[&str]) { + let errs = infer_program_err(&dead_code(defs)); + let err = errs + .iter() + .find(|e| matches!(e, InferError::UnsatisfiableOperand { .. })) + .unwrap_or_else(|| panic!("expected an UnsatisfiableOperand, got {errs:?}")); + let rendered = format!("{err:?}"); + for want in expected { + assert!( + rendered.contains(want), + "the message must name {want}, since the requirements are the only facts \ + the error has; got:\n{rendered}", + ); + } +} + +/// Each requirement states *why* its position is narrowed, by naming what the trait's +/// other operand accepts — the fact that did the narrowing. +/// +/// Without it a line is a conclusion with its premise removed: "only `String` here" is +/// true because a `String` reached the operand beside it, and a reader who is not told +/// that has to reconstruct it. A **unary** trait has no beside, so it says nothing +/// rather than something vacuous. +#[test] +fn a_requirement_says_what_narrowed_it() { + let errs = infer_program_err(&dead_code("f = \\a -> (-a, a + \"s\")")); + let rendered = format!("{errs:?}"); + assert!( + rendered.contains("Addable accepts only String as its operand 1 (its operand 2 is String)"), + "a binary trait names the operand beside it; got:\n{rendered}", + ); + assert!( + rendered.contains("Negatable accepts only Int as its operand 1\n"), + "a unary trait has no other operand, so the clause is omitted rather than \ + empty; got:\n{rendered}", + ); +} + +/// Currying moves the requirements onto different variables and so changes the order +/// they are found in. The message must not notice. +/// +/// The verdict never depended on traversal order — an intersection is commutative — +/// but the *rendering* did, so two spellings of one program produced two orderings of +/// one explanation. +#[test] +fn the_requirement_list_reads_the_same_in_both_spellings() { + let curried = infer_program_err(&dead_code("f = \\a -> (a + 1, a + \"s\")")); + let uncurried = infer_program_err(&dead_code("f = \\a, b -> (a + 1, a + \"s\")")); + assert_eq!( + format!("{curried:?}"), + format!("{uncurried:?}"), + "the same conflict, spelled two ways, must read identically", + ); +} + +/// A requirement contradicting an *ordinary* bound is its own diagnostic, naming the +/// type the value already has beside the one the requirements agree it must be. +/// +/// This is the deposit's half of the mechanism, and the half no intersection can +/// reach: a *bounded* annotation and a monomorphic operator's operand are plain +/// bounds, not requirements, so comparing requirements with each other sees nothing +/// wrong. (An *exact* annotation is a delivery instead — it puts a base on the +/// operand, so `x: Int` never reaches here and fails by narrowing.) The +/// lattice is therefore read before it is written to — otherwise the contradiction +/// only surfaces at coalesce, as two `IncompatibleBounds` (one per direction) naming +/// neither the trait nor the operator that demanded it. +#[rstest] +#[case::bounded_annotation(indoc! {r#" + def f(x <: Int): + x + "s" +"#}, "Int", "String")] +#[case::monomorphic_operator("f = \\a -> (a and True, a + 1)", "Bool", "Int")] +fn a_requirement_contradicting_a_bound_names_both( + #[case] defs: &str, + #[case] found: &str, + #[case] required: &str, +) { + let errs = infer_program_err(&dead_code(defs)); + assert_eq!( + errs.len(), + 1, + "one mistake is one diagnostic; got {} — {errs:?}", + errs.len(), + ); + assert!( + matches!(errs[0], InferError::RequirementContradictsBound { .. }), + "expected the bound-conflict variant, got {:?}", + errs[0], + ); + let rendered = format!("{:?}", errs[0]); + assert!( + rendered.contains(found) && rendered.contains(required), + "the message must name both the type the value has ({found}) and the one it is \ + required to be ({required}); got:\n{rendered}", + ); +} + +/// The controls for [`a_definition_no_argument_satisfies_is_rejected`]: requirements +/// that *do* have a common type must stay accepted. +#[rstest] +#[case::same_trait_twice("f = \\a -> (a + 1, a + 2)")] +#[case::two_traits_overlap("f = \\a -> (a + 1, a < 2)")] +#[case::annotation_agrees(indoc! {r#" + def f(x: Int): + x + 1 +"#})] +#[case::nothing_determined("f = \\a, b -> a + b")] +#[case::a_chain_that_agrees("f = \\a, b, c -> (a + b, b + c, a + 1)")] +#[case::a_chain_determining_nothing("f = \\a, b, c -> (a + b, b + c)")] +#[case::determined_to_string("f = \\a, b -> (a + b, a + \"s\")")] +#[case::record_field_agrees(indoc! {r#" + def f(r): + (r.x + 1, r.x + 2) +"#})] +#[case::higher_order_agrees("f = \\g -> (g(1) + 1, g(1) + 2)")] +// A generalized binding used at two different types: each use resolves its own copy, +// so the `Int` use must not empty the `String` use's candidate set. +#[case::polymorphic_reuse(indoc! {r#" + id = \x -> x + f = \a, b -> (id(a) + 1, id(b) + "s") +"#})] +fn satisfiable_requirements_are_accepted(#[case] defs: &str) { + infer_program(&dead_code(defs)); +} + +/// A determined operand travels: pinning one value can leave a neighbouring +/// obligation with a single row, which determines *its* other operand in turn. +/// +/// Both orders are checked because the sweep visits variables in mint order. With the +/// binders one way round the cascade completes in a single pass; reversed, `b` is +/// visited before `a` is pinned and only the second round can close it. Ordering the +/// binders must not change the type, which is what makes the fixpoint load-bearing +/// rather than defensive. +#[rstest] +#[case::in_order("f = \\a -> \\b -> (a + 1, a < b)")] +#[case::reversed("f = \\b -> \\a -> (a + 1, a < b)")] +// The same program uncurried. A multi-parameter lambda passes its parameters through a +// tuple, so `a`'s occurrences are separate variables; the answer must not depend on +// that, which is what makes the unit a place rather than a variable. +#[case::uncurried("f = \\a, b -> (a + 1, a < b)")] +#[case::uncurried_through_an_operand("f = \\a, b -> (a + b, a + 1)")] +fn a_determined_operand_cascades(#[case] defs: &str) { + let ty = infer_program(&yielding_f(defs)).to_string(); + assert!( + !ty.contains('?'), + "both parameters are determined — `a` by `+ 1`, then `b` because that leaves \ + `Orderable` one row — so no position should still be open; got {ty}", + ); +} + /// A cycle must not hide a conflict: the seed and the write have to agree, and the /// obligation sees both as ordinary bounds. #[test] @@ -560,16 +797,25 @@ fn test_let(#[case] code: &str, #[case] expected: Type) { /// Close a program over definitions nothing calls: `defs` followed by the program /// value they are dead with respect to. /// -/// Cases below carry the definitions alone, so a one-line definition stays a plain -/// string and only a genuinely multi-line one reaches for `indoc!`. A case that -/// needs a *live* use of one of its definitions binds it (`live = f(1)`) rather -/// than ending the program with it — a monomorphic binding's RHS is walked whether -/// or not the binding is read, so the use specializes exactly as a trailing call -/// would. +/// Every case that uses this carries the definitions alone, so a one-line definition +/// stays a plain string and only a genuinely multi-line one reaches for `indoc!`. A +/// case that needs a *live* use of one of its definitions binds it (`live = f(1)`) +/// rather than ending the program with it — a monomorphic binding's RHS is walked +/// whether or not the binding is read, so the use specializes exactly as a trailing +/// call would. fn dead_code(defs: &str) -> String { format!("{}\n1", defs.trim_end()) } +/// Close a program over definitions and yield `f`, so the program's type *is* `f`'s +/// and a test can assert on what was inferred for the definition itself. +/// +/// The counterpart to [`dead_code`] for tests that read a type rather than a verdict, +/// and it keeps the same discipline: the trailing line lives here, not in every case. +fn yielding_f(defs: &str) -> String { + format!("{}\nf", defs.trim_end()) +} + /// A function nobody calls is still typechecked. Monomorphization drops such a /// definition as dead code, but it resolves it first, which is what makes the /// errors only *resolution* sees reachable in it. @@ -635,54 +881,34 @@ fn dead_code(defs: &str) -> String { f = \a -> a.0 + a.foo f = 3 "#})] -// An *exact* annotation is a delivery, which is what brings this case back within -// reach: `x: Int` puts a base on the operand rather than a bound above it, so the -// obligation narrows to `{(Int, Int)}` and `"s"` empties it, with no call site -// needed. Its bounded twin below is equally ill-typed and is *not* caught here, and -// the difference is in the mechanism, not in the programs. +// The last three are each ill-typed and each caught by a different mechanism, which +// is why they are listed together. +// +// An *exact* annotation is a **delivery**: `x: Int` puts a base on the operand rather +// than a bound above it, so the obligation narrows to `{(Int, Int)}` and `"s"` empties +// it — no call site and no sweep needed. +// +// The other two deliver nothing and are reached by the requirement sweep instead. +// `conflicting_operand_types` puts two requirements on `a` — `a + 1` fixes it at +// `Int`, `a + "s"` at `String` — satisfiable alone and not together, so neither +// narrows and the sweep's intersection is empty. `bounded_annotated_param` is the +// exact case's twin: `x <: Int` bounds the operand from above *without* putting a +// base on it, so narrowing has nothing to consume, and the sweep is what reads the +// requirement against the bound already recorded there. #[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(), - "an ill-typed definition must be rejected whether or not it is called" - ); -} - -/// 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". -/// -/// The body is rejected the moment it is called (`f(1)` names the operand, its type, -/// and what the position accepts), so this is about *when* the conflict is found, not -/// whether. What makes it unreachable here is that no single delivery is impossible: -/// two requirements land on `a` — `a + 1` fixes it at `Int`, `a + "s"` at `String` — -/// each satisfiable alone and jointly not. Reading a value's requirements together is -/// what closes it, and that is a property of the obligation machinery rather than of -/// the discard walk. -/// -/// The bounded parameter pairs with the exact one in the previous test and is here -/// for the same reason as the case above it, not a different one: `x <: Int` bounds -/// the operand from above without putting a base on it, so nothing is delivered and -/// the obligation never narrows, while `x: Int` delivers and rejects. Both programs -/// are ill-typed and both are rejected at a call; what differs is only whether -/// today's narrowing has anything to consume. Reading `x`'s requirements together -/// alongside its `Int` bound closes this one too — measured, it is rejected once the -/// requirement sweep is in the same tree — so this is a gap in reach, not a -/// consequence of the exact/bounded split. -#[rstest] #[case::conflicting_operand_types("f = \\a -> (a + 1, a + \"s\")")] #[case::bounded_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)); +fn a_never_called_function_is_still_typechecked(#[case] defs: &str) { + assert!( + !infer_program_err(&dead_code(defs)).is_empty(), + "an ill-typed definition must be rejected whether or not it is called" + ); } /// The complement, and the guard against the walk over-rejecting: typechecking a @@ -1585,37 +1811,33 @@ 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. +/// An unapplied lambda is typed as precisely as its operators' requirements allow — +/// **both** ends — and no more. /// -/// `\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. +/// `\x -> x + 1` carries `Addable(𝐴, Int ⇝ 𝑂)`. `Int` in the second position leaves +/// only the `Addable(Int, Int ⇝ Int)` row, and a single surviving row determines the +/// first position as much as the associated one: the parameter is `Int` because +/// nothing else could ever be passed. So it is deposited as an *upper* bound and the +/// domain closes. /// -/// `O` is a different matter: the obligation is its only source, and every -/// 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 -/// than as a rule. +/// The polarity is the point. An upper bound states what may flow *in*, which is +/// exactly what the requirement says; it invents no value, so a parameter the program +/// genuinely leaves unconstrained stays open — `open_both_ends` is that case, where +/// three rows survive and neither operand is pinned. +/// +/// How much closes is a fact about today's table, not a stable property: adding +/// `Addable(Float, Int ⇝ Float)` would leave two rows disagreeing on both the operand +/// and the output, reopening both. Hence per-case expectations rather than a rule. #[rstest] -#[case::comparison( - r" -f = \x -> x > 1 -f -", - bool_ty() -)] -#[case::arithmetic( - r" -f = \x -> x + 1 -f -", - int() -)] -fn test_lambda_unapplied(#[case] code: &str, #[case] expected_codomain: Type) { - let ty = infer_program(code); +#[case::comparison("f = \\x -> x > 1", Some(int()), bool_ty())] +#[case::arithmetic("f = \\x -> x + 1", Some(int()), int())] +#[case::arithmetic_string("f = \\x -> x + \"s\"", Some(string()), string())] +fn test_lambda_unapplied( + #[case] defs: &str, + #[case] expected_domain: Option, + #[case] expected_codomain: Type, +) { + let ty = infer_program(&yielding_f(defs)); let Type::Fun { domain, codomain, .. } = &ty @@ -1624,11 +1846,35 @@ fn test_lambda_unapplied(#[case] code: &str, #[case] expected_codomain: Type) { }; assert_eq!( **codomain, expected_codomain, - "the operator's trait determines the result even with an open operand", + "the operator's trait determines the result", ); + match expected_domain { + Some(expected) => assert_eq!( + **domain, expected, + "a single surviving instance determines the operand too", + ), + None => assert!( + matches!(**domain, Type::Infer(_)), + "an operand no single row determines stays open, got {domain}", + ), + } +} + +/// The other half of [`test_lambda_unapplied`]: with every row still standing, a +/// requirement determines nothing and both operands stay open. +#[test] +fn an_undetermined_operand_stays_open() { + let ty = infer_program(&yielding_f("f = \\a, b -> a + b")); + let Type::Fun { domain, .. } = &ty else { + panic!("expected a function type, got {ty}"); + }; + let Type::Tuple(params) = &**domain else { + panic!("expected a tuple domain, got {domain}"); + }; assert!( - matches!(**domain, Type::Infer(_)), - "an operand a trait does not determine stays open, got {domain}", + params.iter().all(|p| matches!(p, Type::Infer(_))), + "`a + b` leaves every Addable row standing, so neither operand is pinned; \ + got {domain}", ); }