diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs index 993d3481..c857058b 100644 --- a/src/ccl/ccl_utils.rs +++ b/src/ccl/ccl_utils.rs @@ -560,9 +560,17 @@ pub(crate) fn strip_refinements(ty: &Type) -> Type { domain: Box::new(strip_refinements(domain)), kind: *kind, }, + // Strip *inside* the arguments — a structural rewrite, not a reduction. + // Every operator's reduction already drops value-level claims, so this is + // belt-and-braces rather than the mechanism. + Type::App { fun, args } => Type::App { + fun: fun.clone(), + args: args.iter().map(strip_refinements).collect(), + }, Type::Base(_) | Type::UIntRange(_) | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) | Type::DataSource(_) | Type::ChanDom(..) diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index 0b20fd23..6d95671c 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -1045,6 +1045,138 @@ Recorded so a reader can tell a deliberate boundary from an oversight. program's own value reaches the second). --- +## 4.7 Type functions + +The constraint lattice can state that two positions are **equal** or **related by subtyping**. It cannot state that one position is **computed from** others. Every operator whose result type is a non-identity function of its operand types therefore has no scheme the lattice can express — arithmetic and comparison today, field projection and collection union next. + +A **type function** is that missing statement. `Type::App { fun, args }` is the type "whatever `fun` computes from `args`", carried unreduced until the arguments are known: `1 + x` types as `Add({Int | __elem == 1}, α)` instead of forcing both operands and the result onto one variable. + +### What a shared variable gets wrong + +The obvious encoding is to share a lattice position — arithmetic as `∀α. α → α → α`. It is wrong once per polarity, and how it fails is what a type function has to fix. + +* The operand occurrences are *domains* — negative positions, where refinement sets **union** — so one operand's refinement becomes a *requirement* on the other: `λ 𝑥 → 𝑥 + 1` infers `𝑥 : {Int | __elem == 1}`. +* The result occurrence is positive, where refinement sets **intersect**, so a refinement *both* operands carry survives onto the result: `𝑥 + 𝑥` where `𝑥` is `2` claims the sum is `2`. Distinct refinements intersect to none, which is why this hides — it needs two operands carrying the *same* refinement, where intersecting a set with itself returns it. + +Reconstructing the result *after* coalesce instead needs a walk order that respects data flow, and the coalesce walk deliberately has none: `coalesce_node`'s `Apply` arm visits function before argument, for [monomorphization's ordering invariant](#keying-a-specialization), so a projection's codomain is read before an operand nested in the argument has been coalesced. + +### The representation + +An `App` **denotes** a type; it does not construct one. `Add(Int, Int)` *is* `Int`, written in a form that does not yet know it — so it adds no inhabitants and no subtyping edges, and **reduction is normalization** rather than an observable step. Nothing in the solver ever has to decide `Add(α, β) <: Add(γ, δ)` structurally; it decides the reduced types once the arguments are known. `App` is therefore **transient** in the same sense as `Infer`: every `Type` that escapes inference is `App`-free, and a survivor at the strict wall is a compiler bug (`UnreducedApp`), distinct from an application whose arguments the program never determined (`UnresolvedInfer` — the arguments are missing, not the rule). + +Reduction is **demand-driven**: materializing an `App` resolves each argument through the ordinary pipeline and applies the rule, depositing nothing, so no phase ordering can make the answer wrong. + +### What a reduction rule must satisfy + +A rule is a pure function of resolved argument types, and is sound only if it is **pure**, **monotone** in the subtype order, **normalizing** (its result contains no `App`), and **declares a [`CycleTolerance`](#cycles-are-recurrences-in-the-program)**. Each is checkable by reading the rule; what each one buys inference is stated normatively in `src/ccl/infer/solver/reduce.rs`, "The laws a rule must satisfy", and is not repeated here. + +**There is deliberately no law about refinements.** Whether a rule may carry an argument's refinement into its result is not a property of reduction but a question about what the operator *means*, decided per operator in [Which operators need one](#which-operators-need-one). As a law it would forbid the selecting rules outright, and would still miss the failure that actually threatens soundness — a rule that *invents* a claim its arguments do not support inherits nothing and is monotone, so it passes every law above. + +### Where an operand requirement lives + +**In the result rule, and nowhere else.** An operator's operands are two *unrelated* scheme variables; nothing in the scheme relates them. What checks them is the rule that reduces the result, because the result is the one thing guaranteed to be looked at. + +#### An operand requirement must be reachable from the result type + +A rule runs when something **materializes** the application it belongs to, and an application is materialized only when some node's type reaches it. A scheme's operand variables are nobody's node type: a use site records `left <: α` and `right <: β`, so `α` and `β` are reachable *from* the operands, but nothing walks *from* them. The only thing that can reach them is the result. + +Hence: **a scheme that wants its operands checked must mention them in its result**, as an `App` over them. + +`1 + "a"` is rejected because the addition's result is `Add(α, β)`, so materializing the node runs the rule and finds the conflict. A comparison declaring a bare `Bool` mentions neither operand, so nothing ever materializes them, the rule never runs, and `1 > "a"` types cleanly and then panics in the interpreter. A comparison's result is accordingly `Compare(kind, α, β)`, reducing to `Bool` for any operands that share a base and to an error for any that do not. A rule constant on its domain is still a rule — the whole of a comparison's content *is* its domain — and stating it as one is what gets the check to happen at all. + +Every other scheme in the registry states its requirement **structurally**, inside an operand's own shape — `Sum`'s `∀α. (α ⇒ Int) ⇒ Int` puts the `Int` in the argument's codomain position, so `constrain_go` records it on the argument expression's variable, which is a node's type and materializes like any other. Those need nothing. + +#### An operand nothing else determines stays undetermined + +`λ 𝑥 → 𝑥 + 1` does not infer `𝑥 : Int`. Its result resolves — the rule answers from the literal operand — but the parameter is determined by nothing, because nothing determines it: the operands are unrelated variables and only the result is checked. + +That is the honest type. The lambda works for any two things `+` accepts, so it is polymorphic in its parameter, and `Type` has no `∀` to say so; as a program value it is therefore an **ambiguous program**, rejected downstream exactly as `λ 𝑥 → [𝑥, 𝑥]` is. Inferring `Int` would read as precision, but it is really the one-numeric-type lattice showing through — and would be wrong the moment `Int + Float → Float` existed. + +### Cycles are recurrences in the program + +An argument is **cyclic** when resolving it would re-enter the resolution already computing it. That is not an edge case: a register that reads itself in its own write makes one, so `𝑥 += 1` gives + +```text +value(𝑥) = join(seed, Add(value(𝑥), 1)) +``` + +a fixpoint equation, because an accumulator *is* one. Measured, 1,910 cyclic arguments arise across the test suite, and a self-read is exactly what creates them — `x := 7; x` has none, `x := 7; x += 1; x` has ten. All of them reach arithmetic; a comparison can be cyclic too (`b := (b == True)`) but nothing in the suite writes one. + +`compact.rs`'s in-flight set cuts the recursion, and each rule declares a **`CycleTolerance`** saying whether that cut-off leaves it able to answer: + +| | Meaning | Today | +|---|---|---| +| `Any` | answers from what is known; a cycle costs precision, not the answer | `Compare` loses *nothing* (constant on its domain); arithmetic loses the agreement check but keeps a usable type — which is what lets an accumulator have one | +| `AllKnown` | cannot answer at all without every argument, so the cycle is reported | none yet; `FieldOf(ρ, 𝑘)` is the first, since there is no field type to name without `ρ` | + +Deliberately **not per-argument**. Every rule's condition is about *how many* arguments are cyclic rather than which — arithmetic's operands are interchangeable to its rule, and a rule needing one argument needs it whichever position it occupies. A rule wanting "at least 𝑛 known" would generalize this to a count; none does. + +The cut is an **unrolling, not an iteration**: it unrolls the equation a number of times fixed by the shape of the program and stops. Whether any frame sees *every* argument known is shape-dependent — `x := 2; x := x * x` reaches `[Int, Int]`, while `x := "a"; x := x * x` never reaches `[String, String]` — so a rule check must be written against the operands it *does* have rather than against the joined base. So whatever a rule answers at a cut is what the unrolling carries, and a rule must be *sound* there rather than merely improvable; widening is not the remedy, because there is no iteration to widen. `reduce.rs`, "What the cut actually is" has the trace and the consequences for a rule author — it is the thing to read before writing the range-aware `Arithmetic` in [Known gaps](#known-gaps). + +### Obligations that are not decidable yet are parked + +`constrain_go` cannot compare an unreduced `App` against anything: reduction resolves the application's arguments off the bound graph, and emission runs while that graph is still being built, so an answer read there could be superseded by an edge recorded a moment later. Reducing at emission is exactly the staleness the demand-driven design exists to rule out. + +So the obligation is **parked** rather than decided or dropped. `constrain_go` records it with the in-flight substitutions applied; `require_sub` tags it with the node to blame; `InferCtx::check_parked_obligations` retries it between emission and coalesce — the point at which every edge the program implies has been recorded and reduction is meaningful. Each side materializes to an `App`-free type and the obligation becomes an ordinary subtyping check. + +Only **fully determined** obligations are checked, which is what keeps the retry from perturbing the graph it reads: a side still holding a variable is one the program never determined, and coalesce reports that as `UnresolvedInfer` anyway. Both directions park, because the arm's rule is "undecidable now" rather than a claim about which shapes arrive. + +This is what makes `(1 + 2) and True` an ordinary diagnostic. It closes to `Add(α, β) <: Bool`, which nothing downstream re-derives, so accepting it silently turned a user type error into a panic at the `check_pre_desugar` wall — which cannot tell one from a compiler bug. + +### Which operators need one + +Sharing a lattice position between an input and the result is right exactly when the operator **selects** an existing value or **merges** several — the result then *is* one of those values, so a fact about it survives — and wrong when the operator **computes** a new one. `test_operator_result_inherits_a_refinement_only_when_it_selects` pins the table; half its cases assert a refinement is *still there*, since dropping it would be the same bug from the other side. + +| Operator | Shares | Verdict | +|---|---|---| +| `Sum` | nothing — result is a concrete `Int` | computes; inherits nothing ✔ | +| `Neg`, `Not`, `Concat`, `BoolLogic` | nothing — monomorphic | nothing to inherit ✔ | +| `Max` | element type with the result | *selects* an element — `max([1, 1])` really is `1` ✔ | +| `final_or_default`, `get_prev_seq`, `get_prev_txn` | value type across stream, default, result | *merges* — the result is whichever the runtime supplies, so the refinement set intersects, which is the join rule ✔ | +| `List` | element type across elements | *merges* — `[1, 1]` is a collection of `1`s, `[1, 2]` of `Int`s ✔ | +| `CollectionUnion` | codomain across operands | *merges* on the codomain; its **domain** is a computation and is hand-rolled for that reason ✔ | +| `Proj` | codomain with the projected field | *selects* the field, refinement included ✔ | +| `Arithmetic`, `Compare` | nothing — operands are unrelated variables | *computes*; the rule both checks the operands and builds the result ✔ | + +An arithmetic rule's check is **two** obligations, not one: the operands must agree with each other *and* their shared base must be one the operation is defined on. Having only the first is how `"a" * "b"` typed as `String` — the operands agree perfectly, and multiplication still has nothing to say about strings. `Add` accepts `Int` and `String` (it is concatenation until `lambda_elim` rewrites it to `Concat`); `Sub`, `Mul` and `FloorDiv` accept `Int`. That is what the `kind` on `TypeFn::Arithmetic` earns today, ahead of the range-aware rule it was recorded for. + +`Sum`'s concrete `Int` is a simplifying assumption of the current numeric tower, not a property of summation. When `Sum` becomes numeric-polymorphic its result stops being a constant and becomes a computation over the element type, at which point it moves to the last row and takes a rule of its own. Nothing about the design has to change for that: it is the same shape as `Compare`, whose rule is also constant on its domain today. + +`CollectionUnion` is the instructive row, because it needs a join **and** a computation in one signature: its codomain is a real join (a fresh variable with each operand's codomain as a lower bound), while its domain is a real computation (`Variant({𝑖: dom_𝑖})` over the operands' domains). It is a hand-rolled `emit_node` rule precisely because no scheme can say the second half. Type functions therefore **coexist** with variable sharing rather than replacing it. + +Two problems look like this one and are not: + +* **A register's value type** (`MutWrite`, a mutable binding's initializer, a `Transact` key's seed) is the *join* over its seed and every write, so no single contribution's refinement may survive. Those three sites strip refinements at emit, and [A literal is refined by its own value](#a-literal-is-refined-by-its-own-value) already records that this over-approximates. It is not a computation, so a rule here would be re-implementing the lattice's own join; the fix is to make every writer's contribution a *lower* bound of the register's value variable, at which point the positive-position intersection *is* the rule. +* **A projection's domain** resolving to its open-product *demand* rather than to the value flowing in. Replacing the codomain with a `FieldOf(ρ, 𝑘)` rule does not fix this, because the demand is load-bearing *inference*: `λ 𝑟 → 𝑟.x` infers `{x: ?} ⇒ ?` from that demand alone. See [Closing the single-sided blind spots](#closing-the-single-sided-blind-spots-no-separate-pass). + +### Alternatives considered + +| Alternative | Why not | +|---|---| +| Share a lattice variable between operands and result | Inherits every lattice dimension in both directions — see above. This is the shape being replaced. | +| Reconstruct the result after coalesce | Needs a data-flow-respecting walk order that the coalesce walk deliberately does not have. | +| Reduce at constraint emission | Reads a graph that is still being built; an answer could be superseded by the next edge. This is the reason obligations are parked instead. | +| A bound on the operand variables relating them | Redundant: the result rule already checks the operands, by the reachability argument above. It also hard-codes *which* operands are acceptable outside the rule that should decide it, and, being self-referential, makes argument resolution re-enter on ordinary programs. | +| Named predicate constraints — `(SameBase α β) ⇒ …` | **Not rejected, deferred**, and only worth revisiting if an operand requirement turns out to be needed at all. A predicate *states* a requirement rather than encoding it, and is the shape a user-facing schema language wants; but it has to **propagate** — push `β`'s base onto `α` — and propagating is a deposit, needing its own phase between emission and resolution to stay order-independent. The `App` representation is unchanged by the choice, so it stays a widening rather than a rewrite. | +| Open, user-declared rule set | The rule signature is already a pure function of resolved argument types, so a user-supplied rule fits without change. Keeping the set closed for now avoids the confluence and termination *conditions* an open set forces on the checker (see the prior work below); law 4 is checkable by inspection for a closed set and would have to become a side condition on user code. | + +### Prior work + +**Type functions in the GHC sense** — [associated type synonyms](https://dl.acm.org/doi/10.1145/1090189.1086397) (Chakravarty, Keller & Peyton Jones, ICFP 2005) and [open type functions](https://dl.acm.org/doi/10.1145/1411204.1411215) (Schrijvers, Peyton Jones, Chakravarty & Sulzmann, ICFP 2008) — are the closest analogue, and the name here is deliberately theirs. The substantive difference is openness. GHC's families are user-declared and open, so the checker must decide entailment between *unreduced* applications (`F a ~ G b`) and the rule set needs confluence and termination side conditions to keep that decidable. Cambra's set is closed and every rule is normalizing (law 4), so there is never an equality to decide between two unreduced applications: reduce, then compare. That is what buys demand-driven reduction, and it is also what an open rule set would cost. + +**The lattice underneath** is MLsub ([Dolan & Mycroft, POPL 2017](https://dl.acm.org/doi/10.1145/3093333.3009882)) as presented by [Parreaux, ICFP 2020](https://dl.acm.org/doi/10.1145/3409006), which the whole engine is based on (§1). Neither has type-level computation; a `Type::App` that reduces to an ordinary lattice element is the delta, and it is deliberately small — because reduction is normalization, the lattice is unchanged. + +**Function application in dependent types.** A dependent type checker compares types up to **conversion**: it normalizes before comparing, rather than giving applications structural equality ([Coquand, *An algorithm for type-checking dependent types*, Science of Computer Programming 26, 1996](https://www.sciencedirect.com/science/article/pii/0167642395000216)). Reduction-at-materialization is that discipline restricted to a closed first-order rule set. What is *not* inherited is conversion checking on open terms, because law 4 makes every normal form `App`-free. + +**The interaction with inference** — a computation blocked on an unsolved metavariable — is Agda's **constraint postponement** (Norell, *Towards a practical programming language based on dependent type theory*, Chalmers, 2007): a constraint that cannot be decided because a meta blocks reduction is suspended and retried when the meta is solved. Parking is the same move at coarser granularity, retried once after emission rather than woken per-solution. The coarser version is sound here because emission is a single bounded phase with no solving after it; a system that solved incrementally would need the finer wake-up. + +**Refinements** are inferred elsewhere by predicate abstraction over a fixed qualifier set ([Rondon, Kawaguchi & Jhala, *Liquid Types*, PLDI 2008](https://dl.acm.org/doi/10.1145/1375581.1375602)). The discipline here is deliberately weaker: a refinement is never *inferred* for a computed type, only *derived* by a rule that knows how. Range-aware arithmetic is where deriving would start. + +### Known gaps + +* **Compound arguments need a different agreement test.** `shared_base` decides agreement with `==`, which is correct only for leaf arguments: two bases differing solely in an unresolved position (`(?1, Int)` vs `(?2, Int)`) compare unequal, which is a claim about placeholder identity rather than about types. Nothing reaches it today, since every operand the runtime accepts for arithmetic or comparison is a scalar. `FieldOf(ρ, 𝑘)` and `CollectionUnion` — the named next clients — must not reuse it. +* **`UIntRange` passes through untouched**, because it is an *atom* rather than a refinement, so `[0,2] + [0,2]` reports `[0,2]` — wrong for the same reason `2 + 2 ≠ 2`. `Arithmetic` records its kind precisely so the rule that fixes this has somewhere to live: `+` and `*` map operand ranges differently, and `([0,2], [5,7]) ⇒ [5,9]` is a claim *derived* from the operands rather than inherited from one, which is what a computing rule may do. +* **A refined record's field does not inherit a projection of the record's refinement.** `Proj` carries the field's *own* refinement, which is the `selects` row above; a fact stated about the record as a whole (`{{i: Int, l: List(Int)} | _.i < len(_.l)}`) is not projected onto `x.i`. Recovering it needs the refinement predicate to be split along the projection — a `FieldOf`-style rule could carry the syntactic half, but a predicate relating *two* fields has no sound projection onto one, so this wants predicate-level machinery rather than a reduction rule. ## 5. CCL-specific inference rules @@ -1054,13 +1186,15 @@ Recorded so a reader can tell a deliberate boundary from an oversight. `groupby` is not a dedicated node. It lowers to a cast-wrapped key lambda — `λ k → cast({I | i ▷ c ▷ key == k} ⇒ A, λ i → c(i))` — so its typing falls out of the ordinary `Lambda`/`Cast` rules plus the dependent-refinement machinery of [§4.5](#45-dependent-refinements-via-pi-types); planning's `convert_groupby_pointful` then recognizes the resulting Pi-const source. +One thing the shape does not say is that the partition's **domain is the type of its keys** — `k`'s only occurrence is an operand of that `==`, and a comparison does not relate its operands ([§4.7](#47-type-functions)). Lowering states it with a `Type::SharedHole(id)`: a `Hole` with an identity, where every occurrence of one id normalizes to the same inference variable. It is carried by the key application and by the domain of the group-by's own `data_fun` annotation, so the edge runs `key_ty <: ⟨the parameter⟩` through the annotation's contravariance rather than forcing the two equal. + ### BinOp type rules | Op kind | Operand constraint | Result type | |---|---|---| -| `Arithmetic` | both operands constrained `<: α` (joined into a shared variable) | operand type | +| `Arithmetic` | none — the result rule checks the operands | `Add(α, β)` and siblings, a [type function](#47-type-functions) | | `Concat` | both operands constrained to `String` | `String` | -| `Compare` | both operands constrained `<: α` (joined into a shared variable) | `Bool` | +| `Compare` | none — the result rule checks the operands | `Greater(α, β)` and siblings — a type function reducing to `Bool`, so the check is reachable | | `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. diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index 2f1dd776..ad2a01e1 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -122,7 +122,7 @@ impl Drop for InferArena { // Take back every variable minted during the run and sever its bound // edges, so the (otherwise cyclic) refcounts can all reach zero. for var in crate::ccl::arena_exit() { - let mut bounds = var.bounds.borrow_mut(); + let mut bounds = var.bounds_mut(); bounds.lower.clear(); bounds.upper.clear(); } @@ -337,6 +337,52 @@ pub enum InferError { /// Display label for the message (see the type docs — not the location). at: String, }, + /// A type function's operands have no base in common — `1 + "a"`. + /// + /// Distinct from [`InferError::IncompatibleBounds`], and the distinction is the + /// reason this is its own variant rather than that one reused. There, a + /// *variable* collected two bounds that cannot meet, and the rejection is about + /// what inference declines to invent (an untagged sum). Here each operand is + /// perfectly well typed and nothing was inferred badly — the operator simply has + /// no rule relating an `Int` to a `String`, which is a statement about the + /// operator. + NoCommonBase { + /// The type function, as it is spelled in a type (`Add`, `Greater`). + fun: String, + /// The operand bases, rendered, in argument order. + bases: Vec, + /// Display label for the message (see the type docs — not the location). + at: String, + }, + /// The operands agree on a base the operation is not defined for — `"a" * "b"`. + /// + /// The dual of [`NoCommonBase`](InferError::NoCommonBase): there the operands + /// disagree, here they agree and the *operator* is what has nothing to say. + UndefinedForBase { + /// The type function, as it is spelled in a type (`Mul`, `Sub`). + fun: String, + /// The offending base, rendered. + base: String, + /// Display label for the message (see the type docs — not the location). + at: String, + }, + /// A [`Type::App`] survived inference without reducing — the strict wall's + /// guard on a transient type, like the [`Type::History`](crate::ccl::Type) and + /// [`Type::ChanDom`](crate::ccl::Type) checks beside it rather than a diagnosis + /// a program earns. + /// + /// Materialization always either reduces an operator or poisons the position it + /// sits at (`compact_go`'s `Compute` arm), and every stamped type is + /// materialized, so nothing should reach here. An operator whose arguments the + /// program never determined does *not*: it reduces to the unresolved position + /// itself and is reported as [`InferError::UnresolvedInfer`], which is the + /// honest description — the arguments are undetermined, not the rule. + UnreducedApp { + /// Display string of the unreduced type-function application. + ty: String, + /// 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. @@ -572,6 +618,23 @@ impl std::fmt::Debug for InferError { InferError::UnresolvedInfer { id, at } => { write!(f, "Unresolved inference variable {id} in expression: {at}") } + InferError::NoCommonBase { fun, bases, at } => { + write!( + f, + "Operands of {fun} have no base in common: {} in expression: {at}", + bases.join(" vs ") + ) + } + InferError::UndefinedForBase { fun, base, at } => { + write!(f, "{fun} is not defined on {base} in expression: {at}") + } + InferError::UnreducedApp { ty, at } => { + write!( + f, + "Type function {ty} never reduced in expression: {at} \ + (a compiler bug — materialization reduces or rejects)" + ) + } InferError::UnresolvedPartial { kind, at } => { write!(f, "Unresolved partial {kind} in expression: {at}") } @@ -832,7 +895,17 @@ fn collect_type_errors( seen_refinements: &mut HashSet, ) { match ty { - Type::Hole => errors.push(InferError::UnresolvedHole { + // A `SharedHole` is a `Hole` with an identity, and just as transient: + // `normalize_annotation` resolves both. A survivor means the annotation + // never reached normalization, which is the same compiler bug either way. + Type::Hole | Type::SharedHole(_) => errors.push(InferError::UnresolvedHole { + at: context_sym.to_string(), + }), + // A type function that never reduced. Reported like an unresolved + // variable — it is the same failure (the program did not determine + // enough), one level up: the arguments are missing rather than the type. + Type::App { .. } => errors.push(InferError::UnreducedApp { + ty: ty.to_string(), at: context_sym.to_string(), }), Type::Infer(var) => { @@ -2983,6 +3056,33 @@ mod tests { ); } + /// Corrupting an operator's result type is caught by `typecheck`, for both + /// operators whose result is a [`Type::App`]. + /// + /// The wall sees through the operator only because Check *resolves* a + /// rule-derived variable before reconciling it: the rule hands back a fresh + /// variable whose lower bound is `Add(α, β)` / `Less(α, β)`, and an unreduced + /// operator is opaque to `constrain_subtype`, so without the resolve the + /// bound-closure walk stops there and the corruption goes unnoticed. + #[test] + fn test_typecheck_operator_wrong_result_type() { + for (op, corrupted) in [ + (BinOpKind::Arithmetic(ArithmeticKind::Add), BaseType::String), + (BinOpKind::Compare(CompareKind::Less), BaseType::Int), + ] { + let mut ctx = TypeInferenceContext::new(); + let mut expr = Expr::binop(Expr::lit(Lit::Int(1)), op, Expr::lit(Lit::Int(2))); + infer(&mut expr, &mut ctx).unwrap(); + expr.ty = Type::Base(corrupted.clone()); + let errs = typecheck(&expr).expect_err("a wrong result type must be caught for {op:?}"); + assert!( + errs.iter() + .any(|e| matches!(e, InferError::TypeMismatch { .. })), + "expected a TypeMismatch for {op:?}, got {errs:?}" + ); + } + } + /// Corrupting a `Compare` result type away from `Bool` is caught by `typecheck`. #[test] fn test_typecheck_compare_wrong_result_type() { diff --git a/src/ccl/infer/check.rs b/src/ccl/infer/check.rs index 6bd84115..789dcf00 100644 --- a/src/ccl/infer/check.rs +++ b/src/ccl/infer/check.rs @@ -16,6 +16,7 @@ use super::emit::{ emit_variant_ctor, }; use super::schemes::OperatorSchemes; +use super::solve::resolve_var_type; use super::typing::{Typing, peel_refinements_outer}; use super::{lit_base, map_constrain_err}; @@ -425,6 +426,23 @@ fn check_node_rule(expr: &mut Expr, ctx: &mut CheckCtx) -> Result resolve_var_type(&ty).unwrap_or(ty), + _ => ty, + }; if ty != expr.ty { // Refinements included: this is the plain strict relation, like every other // check here. A rule that rebuilds a node's type from its children rebuilds diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs index 47e4872f..26a4f89b 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -2,6 +2,7 @@ // InferCtx (Step 7c) // --------------------------------------------------------------------------- +use std::cell::RefCell; use std::collections::HashMap; use crate::ccl::ccl_utils::TermMemo; @@ -112,6 +113,40 @@ pub(super) struct InferCtx { /// which is what lets `LocatedInferError` require a node instead of carrying /// an `Option` that every consumer must then interpret. current_node_id: NodeId, + /// Obligations the solver could not decide during emission because one side + /// was an unreduced [`Type::App`], each tagged with the node and label of the + /// rule that raised it. Drained by + /// [`check_parked_obligations`](Self::check_parked_obligations) once emission + /// completes; see [`require_sub`](Self::require_sub). + parked: Vec, + /// The variable each [`Type::SharedHole`] id normalizes to, so every + /// occurrence of one id resolves to the *same* variable — which is the whole + /// content of the marker (see [`Type::SharedHole`]). + /// + /// A `RefCell` because [`normalize_annotation`](Self::normalize_annotation) + /// takes `&self` and is called from a dozen places; threading `&mut` through + /// all of them to memoize one map would be churn for no gain. + /// + /// **First occurrence fixes the level.** Ids are minted per lowered construct + /// and every occurrence of one id sits in the same expression, so the level is + /// the same at each — but nothing here enforces that, and a future desugaring + /// that shared an id across a `let` RHS boundary would silently take the first + /// level it saw. + shared_holes: RefCell>, +} + +/// A subtyping obligation deferred out of constraint emission, with the blame it +/// will need if it turns out to fail. +/// +/// The types are held **by variable**, not by value: a `Type::Infer` clone shares +/// its `Rc`, so a parked obligation sees every bound recorded after it +/// was parked. That is the whole point — parking exists to read the graph once it +/// has stopped moving. +struct ParkedObligation { + lhs: Type, + rhs: Type, + node: NodeId, + label: String, } impl InferCtx { @@ -127,6 +162,8 @@ impl InferCtx { pred_memo: Default::default(), lit_singletons: HashMap::new(), current_node_id: root, + parked: Vec::new(), + shared_holes: RefCell::new(HashMap::new()), } } @@ -151,6 +188,17 @@ impl InferCtx { match ty { // A `Hole` annotation means "infer this" → fresh variable. Type::Hole => fresh_var(self.level), + // A `SharedHole` means "infer this, and it is the same one as that": + // the *first* occurrence of an id mints the variable and every later + // one reuses it. That identity is the entire mechanism — it is how a + // desugaring relates two positions whose common type only inference + // will learn (see [`Type::SharedHole`]). + Type::SharedHole(id) => self + .shared_holes + .borrow_mut() + .entry(*id) + .or_insert_with(|| fresh_var(self.level)) + .clone(), // Refinements ride the lattice: keep the wrapper, normalize the // inner (so a `Refinement(Hole, r)` source annotation becomes // `Refinement(?fresh, r)` rather than losing the refinement). @@ -196,6 +244,11 @@ impl InferCtx { kind: *kind, }, // Leaves and existing inference vars pass through unchanged. + // A type function normalizes argumentwise; the function itself is data. + Type::App { fun, args } => Type::App { + fun: fun.clone(), + args: args.iter().map(|a| self.normalize_annotation(a)).collect(), + }, Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) @@ -221,6 +274,106 @@ impl InferCtx { }; Type::Refinement(Box::new(base), Refinement::sharing(&predicate)) } + + /// Record one emission-time subtyping obligation, claiming whatever the solver + /// parks while doing so. + /// + /// **Every** emission-time `constrain_subtype` goes through here. A parked + /// obligation is only ever retried if something tagged it with a node to blame, + /// and the solver has no node cursor — so a call that bypassed this would + /// silently drop its obligation, which is the exact defect parking exists to + /// fix. [`check_parked_obligations`](Self::check_parked_obligations) asserts the + /// solver's park list is empty on the way out, which is what makes a future + /// bypass loud instead of silent. + fn constrain_and_claim( + &mut self, + sub: &Type, + sup: &Type, + label: &dyn Fn() -> String, + ) -> Result<(), crate::ccl::infer::solver::ConstrainError> { + let mark = self.cache.parked_len(); + let result = constrain_subtype(sub, sup, &mut self.cache); + let newly_parked = self.cache.take_parked_from(mark); + if !newly_parked.is_empty() { + let node = self.current_node_id; + let label = label(); + self.parked + .extend(newly_parked.into_iter().map(|(lhs, rhs)| ParkedObligation { + lhs, + rhs, + node, + label: label.clone(), + })); + } + result + } + + /// Discharge the obligations emission could not decide, now that the graph has + /// stopped moving. + /// + /// Every entry has an unreduced [`Type::App`] on one side or the other, which + /// `constrain_go` cannot see through *during* emission: reduction resolves the + /// application's arguments off the bound graph, and reading that graph while it + /// is still being built is the staleness the demand-driven design exists to rule + /// out. Between emission and coalesce there is no such hazard — every edge the + /// program implies has been recorded — so each side materializes to an + /// `App`-free type and the obligation becomes an ordinary subtyping check. + /// + /// **Only fully-determined obligations are checked**, and that is what keeps + /// this pass from perturbing the very graph it is reading. A side that still + /// contains a variable after materialization is one the program never + /// determined; re-constraining it would *record* a bound, which is a graph + /// mutation after emission and would make a later resolution's answer depend on + /// whether this pass ran. Skipping is not a hole in the check either — an + /// undetermined operand is an ambiguous program, and coalesce reports it as + /// `UnresolvedInfer`. With both sides variable-free the check cannot deposit + /// anything: there is nothing left to bound. + /// + /// A side that fails to materialize is skipped for a different reason: the + /// failure *is* the diagnostic (`NoCommonBase` for `1 + "a"`), and coalesce + /// raises it on the node whose type it is, which is a better blame than this + /// pass could give. + pub(super) fn check_parked_obligations(&mut self) -> Vec { + use crate::ccl::infer::solver::ConstrainCache; + use crate::ccl::subst::type_contains_infer; + + let mut errors = Vec::new(); + for ParkedObligation { + lhs, + rhs, + node, + label, + } in std::mem::take(&mut self.parked) + { + let (Ok(lhs), Ok(rhs)) = ( + super::solve::resolve_var_type(&lhs), + super::solve::resolve_var_type(&rhs), + ) else { + continue; + }; + if type_contains_infer(&lhs) || type_contains_infer(&rhs) { + continue; + } + // Kind-blind for the same reason the post-inference structural check is + // (see `ConstrainCache`): both sides have been through coalesce, which + // canonicalizes every reconstructed arrow's kind, so a kind edge here + // would be re-deciding a question inference already settled on the + // pre-coalesce types. + if let Err(e) = constrain_subtype(&lhs, &rhs, &mut ConstrainCache::new_kind_blind()) { + errors.push(LocatedInferError { + error: map_constrain_err(e, &label), + node_id: node, + }); + } + } + debug_assert_eq!( + self.cache.parked_len(), + 0, + "an emission-time `constrain_subtype` bypassed `constrain_and_claim`: its \ + parked obligation has no node to blame and would be dropped unchecked" + ); + errors + } } impl Typing for InferCtx { @@ -254,7 +407,7 @@ impl Typing for InferCtx { sup: &Type, at: &dyn Fn() -> String, ) -> Result<(), LocatedInferError> { - constrain_subtype(sub, sup, &mut self.cache) + self.constrain_and_claim(sub, sup, at) .map_err(|e| self.raise(map_constrain_err(e, &at()))) } @@ -360,7 +513,11 @@ impl Typing for InferCtx { // the error shows what was actually inferred, not the partially // modified state after a failed constrain_subtype. let inferred_ty = coalesce_for_error(inferred); - constrain_subtype(inferred, &ann_simple, &mut self.cache).map_err(|_| { + let ann_label = ann.to_string(); + self.constrain_and_claim(inferred, &ann_simple, &|| { + format!("annotation `{ann_label}`") + }) + .map_err(|_| { self.raise(InferError::AnnotationMismatch { annotation: ann.clone(), inferred: inferred_ty, @@ -456,13 +613,10 @@ impl Typing for InferCtx { let Type::Infer(v) = &applied else { unreachable!("fresh() yields a Type::Infer var"); }; - v.bounds - .borrow_mut() - .lower - .push(crate::ccl::Bound::with_subst( - result, - crate::ccl::subst::Subst::discharge(&x, argument.clone()), - )); + v.bounds_mut().lower.push(crate::ccl::Bound::with_subst( + result, + crate::ccl::subst::Subst::discharge(&x, argument.clone()), + )); Ok(applied) } } diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index 454a8427..2be276e2 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -335,12 +335,20 @@ fn emit_annotation_predicates(ty: &mut Type, ctx: &mut InferCtx) -> Result<(), L emit_annotation_predicates(value, ctx)?; emit_annotation_predicates(domain, ctx) } + // Arguments can carry refinements of their own; reach them. + Type::App { args, .. } => { + for a in args.iter_mut() { + emit_annotation_predicates(a, ctx)?; + } + Ok(()) + } Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => Ok(()), } } @@ -406,19 +414,20 @@ 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. +/// Operand types enter **verbatim**. Keeping an operator's refinements from +/// crossing to its other operand or to its result is the *scheme*'s business, and +/// it needs nothing here: the operands are two unrelated variables, so there is no +/// channel between them, and the result is a type function whose rule computes a +/// fresh answer rather than inheriting one (see +/// [`OperatorSchemes::arithmetic`](super::schemes::OperatorSchemes)). /// -/// 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 tempting shortcut here is `strip_refinements` on each operand type, and it +/// is worth recording why it cannot work: it peels *syntactic* `Type::Refinement` +/// layers and returns a `Type::Infer` untouched, so it erases a literal's +/// refinement and does nothing at all for an operand whose type is still an +/// inference variable — every operand that is not a literal. A syntactic peel +/// cannot implement a semantic relation, because at emit time the thing it needs to +/// look through has not been resolved yet. fn apply_binary_scheme( ctx: &mut C, scheme: &PolyScheme, @@ -428,10 +437,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) } @@ -1537,7 +1543,7 @@ mod review_tests { let Type::Infer(v) = t else { panic!("fresh() yields a variable"); }; - let b = v.bounds.borrow(); + let b = v.bounds(); b.lower.len() + b.upper.len() }; assert!( diff --git a/src/ccl/infer/mod.rs b/src/ccl/infer/mod.rs index 40d2a7f3..88478e59 100644 --- a/src/ccl/infer/mod.rs +++ b/src/ccl/infer/mod.rs @@ -59,7 +59,7 @@ //! //! 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 +//! (`Compare : ∀α β. α → β → Greater(α, β)`, `Max : ∀α γ. (α → γ) → γ`, etc.). Each scheme //! is `instantiate`d at every use site, minting fresh vars per use. //! //! Most `Builtin` nodes are introduced post-inference by @@ -91,7 +91,7 @@ use std::collections::{BTreeMap, HashMap}; use std::rc::Rc; use crate::ccl::FieldKey; -use crate::ccl::infer::solver::{CoalesceError, ConstrainError, prim}; +use crate::ccl::infer::solver::{CoalesceError, ConstrainError, ReduceError, prim}; use crate::ccl::{BaseType, BinOpKind, CompareKind, Lit, Refinement, Type, TypedExpr}; use context::InferCtx; @@ -235,6 +235,40 @@ pub(super) fn map_coalesce_err(err: CoalesceError, ctx_label: &str) -> InferErro does not cover)", ctx_label, details )), + // A reduction conflict is an ordinary type error about the operands, and it + // says so in its own words. Routing it through `IncompatibleBounds` — the + // shape the shared-variable scheme used to produce for `1 + "a"` — would + // reuse that variant's rendering along with its shape, and the rendering is + // a specific claim ("won't infer an untagged sum from a collision") that is + // not what happened here: each operand is well typed and nothing collided + // on a variable. + CoalesceError::Reduce(ReduceError::NoCommonBase { fun, bases }) => { + InferError::NoCommonBase { + fun, + bases, + at: ctx_label.to_string(), + } + } + // A rule that cannot answer through a cycle. The program defined something + // in terms of itself in a way this rule has no answer for, which is a user + // error about the *program*, not a conflict between two types — so it is + // reported in its own words rather than as a mismatch. + CoalesceError::Reduce(ReduceError::CyclicArgument { fun }) => { + InferError::Unsupported(format!( + "{fun} cannot be computed at {ctx_label}: one of its arguments is \ + defined in terms of this very application, and {fun} has no answer \ + without it" + )) + } + // The operands agree and the *operator* is what has nothing to say, so the + // message names one base rather than a conflicting pair. + CoalesceError::Reduce(ReduceError::UndefinedForBase { fun, base }) => { + InferError::UndefinedForBase { + fun, + base, + at: ctx_label.to_string(), + } + } } } @@ -346,6 +380,21 @@ pub(crate) fn run( // the node whose rule raised it (`Typing::raise`). emit_node(expr, &mut sub_ctx).map_err(|e| vec![e])?; + // Emission's leftovers. An obligation whose two sides could not be compared + // during emission — one of them was an unreduced `Type::App`, and reducing it + // would have read a graph that was still being built — was parked instead of + // decided. This is the point the parking was for: every edge has been recorded, + // so reduction is meaningful and each side materializes to an `App`-free type. + // + // It runs *before* coalesce so that a violation is reported as an inference + // diagnostic rather than reaching the `check_pre_desugar` wall, where a plain + // user type error would be indistinguishable from a compiler bug and panic as + // one. See `InferCtx::check_parked_obligations`. + let parked_errors = sub_ctx.check_parked_obligations(); + if !parked_errors.is_empty() { + return Err(parked_errors); + } + // 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 6bc8b1e2..dacf863a 100644 --- a/src/ccl/infer/schemes.rs +++ b/src/ccl/infer/schemes.rs @@ -6,7 +6,10 @@ use std::collections::BTreeMap; use crate::ccl::FieldKey; 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, TypeFn, + UnaryOpKind, +}; use super::product; @@ -18,14 +21,72 @@ 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. +/// +/// # An operand requirement must be reachable from the result type +/// +/// **A scheme that states a requirement on its operand variables must mention +/// those variables in its result**, as a [`Type::App`] over them. Writing a +/// concrete result instead compiles, infers, and silently accepts programs the +/// requirement was written to reject. +/// +/// The reason is the solver's, not the operator's. A rule runs when something +/// **materializes** the application it belongs to, and an application is +/// materialized only when some node's type reaches it. A scheme's operand +/// variables are nobody's node type: a use site records `left <: α` and +/// `right <: β`, so `α` and `β` are reachable *from* the operands, but nothing +/// walks *from* them. The only thing that can reach them is the result, because +/// the result is the node's type. +/// +/// So arithmetic's result is `Add(α, β)` and a comparison's is `Greater(α, β)`, +/// reducing to `Bool` for any operands that share a base and to an error for any +/// that do not. A bare `Bool` there would let `1 > "a"` type-check and then panic +/// in the interpreter — a rule that is never run rejects nothing. +/// +/// This is also why an operand requirement stated *beside* the result rather than +/// in it does not work, and [`binary_operands`] records what happened when one was. +/// +/// Every other scheme here states its requirement **structurally**, in an operand's +/// own shape — `Sum`'s `∀α. (α ⇒ Int) ⇒ Int` puts the `Int` in the argument's +/// codomain position, so `constrain_go` records it on the argument expression's +/// variable, which is a node's type and is materialized like any other. Those need +/// nothing. 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, + /// One scheme per arithmetic operator: `∀α β. α → β → Add(α, β)` and siblings, + /// over two **unrelated** operand variables. + /// + /// **Nothing is shared between the operands and the result**, and that is the + /// point. A shared variable (`∀α. α → α → α`) states *equality*, which drags + /// the whole lattice along with the base, once per polarity: the operand + /// occurrences are negative positions where refinement sets union, so one + /// operand's refinement becomes a *requirement* on the other (`\x -> x + 1` + /// demanding `x : {Int | __elem == 1}`), while the result occurrence is positive + /// where they intersect, so a refinement both operands carry survives onto the + /// result (`x + x` where `x` is `2` claiming the sum is `2`). Arithmetic + /// *computes* a new value, so it may inherit neither. + /// + /// The result is a [`Type::App`] instead: `Add(α, β)`, whose rule reduces to the + /// operands' shared base once they resolve and rejects operands that have none. + /// Deciding what is addable is that rule's job, which is what the reachability + /// section above is for — the result *is* the node's type, so it is the one + /// thing guaranteed to be materialized. It keeps the operator kind because a + /// sharper rule needs it (`+` and `*` map operand ranges to different result + /// ranges, so `([0,2], [5,7]) ⇒ [5,9]` will live there), and one scheme per kind + /// follows from the kind being part of the type. + arithmetic: BTreeMap, + /// One scheme per comparison: `∀α β. α → β → Greater(α, β)` and siblings, over + /// two unrelated operand variables like [`arithmetic`](Self::arithmetic). + /// + /// A comparison is exposed to only the *operand* half of the shared-variable + /// problem — its result is `Bool`, so it could never inherit a refinement — but + /// that half is the same shared variable, so it takes the same treatment. + /// + /// The result is an application even though it reduces to a constant, and that + /// is the reachability section in miniature: a bare `Bool` mentions neither + /// operand, so nothing would ever materialize them and the rule that checks them + /// would never run. `Compare(kind, α, β)` reduces to `Bool` for operands that + /// share a base and to an error for operands that do not, which is both what a + /// comparison means and what gets the check to happen at all. + compare: BTreeMap, /// `Bool → Bool → Bool`. bool_logic: PolyScheme, /// `String → String → String`. @@ -65,6 +126,23 @@ pub struct OperatorSchemes { get_prev_txn: PolyScheme, } +/// Two fresh, **unrelated** operand variables for a binary operator. +/// +/// Nothing here states a requirement between them, and nothing needs to: the +/// operator's *result* is a [`Type::App`] over both, so materializing the node +/// reduces it, and the rule decides whether the operands are acceptable. That is +/// the whole content of "an operand requirement must be reachable from the result +/// type" — the reachability is what makes the check happen, and the rule is where +/// the check belongs. +/// +/// An operand nothing else determines therefore stays undetermined — `\x -> x + 1` +/// leaves its parameter open. That lambda *is* polymorphic and `Type` has no way to +/// say so, which makes it an ambiguous program, exactly as `\x -> [x, x]` is. +fn binary_operands() -> (Type, Type) { + const BODY_LEVEL: Level = 1; + (fresh_var(BODY_LEVEL), fresh_var(BODY_LEVEL)) +} + impl OperatorSchemes { /// Build the registry. Schemes are quantified at level 0; their /// internal fresh vars live at level 1 so `instantiate(0)` mints @@ -73,17 +151,40 @@ 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))); + // Arithmetic: one scheme per operator, ∀α β. α → β → (α, β), with the + // operand requirement recorded as a bound on α and β (see the field doc). + let arithmetic = ArithmeticKind::ALL + .into_iter() + .map(|kind| { + let (alpha, beta) = binary_operands(); + let result = Type::App { + fun: TypeFn::Arithmetic(kind), + args: vec![alpha.clone(), beta.clone()], + }; + ( + kind, + PolyScheme::poly(SCHEME_LEVEL, fun(alpha, fun(beta, result))), + ) + }) + .collect(); - // Compare: ∀α. α → α → Bool - let alpha = fresh_var(BODY_LEVEL); - let compare = PolyScheme::poly( - SCHEME_LEVEL, - fun(alpha.clone(), fun(alpha, prim(BaseType::Bool))), - ); + // Compare: one scheme per operator, ∀α β. α → β → (α, β), same operand + // requirement. The result is an operator rather than a bare `Bool` so that + // the requirement is reachable from it — see the type doc. + let compare = CompareKind::ALL + .into_iter() + .map(|kind| { + let (alpha, beta) = binary_operands(); + let result = Type::App { + fun: TypeFn::Compare(kind), + args: vec![alpha.clone(), beta.clone()], + }; + ( + kind, + PolyScheme::poly(SCHEME_LEVEL, fun(alpha, fun(beta, result))), + ) + }) + .collect(); // BoolLogic: Bool → Bool → Bool let bool_logic = PolyScheme::mono(fun( @@ -189,8 +290,14 @@ impl OperatorSchemes { pub(super) fn binop(&self, op: BinOpKind) -> &PolyScheme { match op { - BinOpKind::Arithmetic(_) => &self.arithmetic, - BinOpKind::Compare(_) => &self.compare, + BinOpKind::Arithmetic(k) => self + .arithmetic + .get(&k) + .expect("every ArithmeticKind has a scheme"), + BinOpKind::Compare(k) => self + .compare + .get(&k) + .expect("every CompareKind has a scheme"), BinOpKind::BoolLogic(_) => &self.bool_logic, BinOpKind::Concat => &self.concat, } diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index cf284d07..836182dd 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1197,12 +1197,19 @@ fn coalesce_type_predicates(ty: &mut Type, level: Level, ctx: &mut CoalesceCtx) coalesce_type_predicates(value, level, ctx); coalesce_type_predicates(domain, level, ctx); } + // Arguments can carry refinements of their own; reach them. + Type::App { args, .. } => { + for a in args.iter_mut() { + coalesce_type_predicates(a, level, ctx); + } + } Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => {} } } diff --git a/src/ccl/infer/solver/coalesce.rs b/src/ccl/infer/solver/coalesce.rs index 05d544a1..4c555b09 100644 --- a/src/ccl/infer/solver/coalesce.rs +++ b/src/ccl/infer/solver/coalesce.rs @@ -38,6 +38,9 @@ pub enum CoalesceError { /// Pretty representation of the conflicting bounds. details: String, }, + /// A type function could not reduce — its arguments have no common base, or a + /// strict type function's argument was cyclic. See [`ReduceError`](super::ReduceError). + Reduce(super::ReduceError), /// A record-shaped variable still had open width at coalesce time — /// no closing equality constraint pinned its full set of fields. /// Mirrors today's `UnresolvedPartial` error so existing callers see @@ -117,6 +120,13 @@ pub fn coalesce_compact(graph: &CompactGraph) -> Result { } fn coalesce_compact_go(ct: &CompactType, polarity: bool) -> Result { + // A type function at this position failed to reduce. Raise it here, where a + // `Type` is produced: this is the point the coalesce walk blames on a node, so + // `1 + "a"` reports "no common base" against the addition rather than + // resurfacing later as an unresolved variable with no span. + if let Some(e) = &ct.reduce_error { + return Err(CoalesceError::Reduce(e.clone())); + } // Transparent read at joins: a feed handle meeting *non-feed* // contributions at one position is being read — `x + 1` joins x's // payload with `Int` through a shared join variable, so the handle @@ -725,7 +735,7 @@ mod tests { // the path is defensive. let v = fresh_var(0); if let Type::Infer(state) = &v { - state.bounds.borrow_mut().lower.push(Bound::conc(v.clone())); + state.bounds_mut().lower.push(Bound::conc(v.clone())); } match coalesce_compact(&compact_type(&v)).unwrap() { Type::Infer(_) => {} diff --git a/src/ccl/infer/solver/compact.rs b/src/ccl/infer/solver/compact.rs index d70e1a45..7040151f 100644 --- a/src/ccl/infer/solver/compact.rs +++ b/src/ccl/infer/solver/compact.rs @@ -15,6 +15,118 @@ use crate::ccl::{BaseType, HistoryKind, InferVarId, Name, Refinement, Type, fres use crate::ccl::FieldKey; +// Type-function arguments whose resolution is currently in flight, so an argument +// that would re-enter the resolution already computing it is reported as +// unavailable instead of recursing forever. +// +// Thread-local rather than threaded through `compact_go`'s state, and that is +// forced: reducing an argument re-enters the whole compact → simplify → coalesce +// pipeline with a *fresh* `CompactState`, so a per-walk set could not see the outer +// resolution that is already computing this argument. The set is keyed on the +// argument's variable, which is what identifies the in-flight resolution. +// +// This is a **termination** device, not an optimization: without it, ordinary +// programs overflow the stack (`x := 7; for i in []: x += 1; x` is enough). +thread_local! { + static ARGS_IN_FLIGHT: std::cell::RefCell> = + const { std::cell::RefCell::new(BTreeSet::new()) }; +} + +/// Marks `uid` as in flight for as long as it is held. +/// +/// RAII rather than a straight-line insert/remove: this is a thread-local that +/// outlives any one call, so a panic between the two halves — anywhere inside +/// [`compact_type`] or [`coalesce_compact`](super::coalesce_compact) — would leave +/// `uid` marked for the rest of the thread's life. Nothing would crash; every +/// later reduction that reached `uid` would silently answer without it and coarsen +/// (see [`super::reduce`]'s "Missing arguments"), which is wrong types rather than +/// a failure. +struct InFlight(InferVarId); + +impl InFlight { + fn mark(uid: InferVarId) -> InFlight { + ARGS_IN_FLIGHT.with(|s| { + s.borrow_mut().insert(uid); + }); + InFlight(uid) + } +} + +impl Drop for InFlight { + fn drop(&mut self) { + ARGS_IN_FLIGHT.with(|s| { + s.borrow_mut().remove(&self.0); + }); + } +} + +/// Resolve one type-function argument to a concrete `Type`, or `None` if its +/// resolution is already in flight. +/// +/// This is the **demand-driven** step: it runs the full resolution pipeline on the +/// argument, so it pulls whatever the graph knows at the moment the enclosing type +/// is materialized — no bound is deposited and no walk order can change the answer. +/// +/// # Nothing is memoized, deliberately +/// +/// Resolution is re-entrant and deposits nothing, so the same variable is +/// re-derived along every path that reaches it. A cache keyed on the variable was +/// tried and removed: it bought 13–22% and cost a generation counter on +/// [`InferVar`](crate::ccl::InferVar) that every future write to the bound graph +/// would have had to keep correct. It did not change the *shape* of the cost — an +/// applied chain of generic wrappers is exponential in depth with the cache or +/// without it (37s vs 45s at depth 10), so the thing worth attacking is that, not +/// the constant. +/// Resolve one argument of a [`Type::App`]. +/// +/// The three outcomes are genuinely different and the signature keeps them apart: +/// `Ok(Some(t))` resolved, `Ok(None)` re-entered the resolution already computing it +/// (a cycle), and `Err(e)` the argument's *own* reduction failed. Collapsing the last +/// two — which `.ok()` did — hands a rule `Arg::Cyclic` for an argument that is not +/// cyclic but poisoned, and the rule then coarsens past a real type error: `x := "a"; +/// x := x * x` typed as `Mut(String)` because the inner `Mul` rejection arrived as +/// "unavailable". Poisoned stays poisoned, the same rule [`CompactType::merge`] follows. +fn resolve_argument(arg: &Type, subst_acc: &Subst) -> Result, super::ReduceError> { + // The argument rides the application through whatever substitutions the edges + // walked so far composed; force them before resolving, exactly as the + // refinement arm forces them on a predicate. + // `apply_type` rebuilds the whole type, and the overwhelmingly common case is a + // vacuous substitution on a bare variable — where rebuilding is a deep clone of + // something that comes back identical. Borrow instead, and only own a rewritten + // copy when there is a rewrite to do. + let owned; + let arg: &Type = if subst_acc.is_id() { + arg + } else { + owned = subst_acc.apply_type(arg); + &owned + }; + // A concrete argument is neither cyclic nor memoizable: resolving it cannot + // re-enter *this* argument, and there is no variable to key an entry on. + let Type::Infer(v) = arg else { + return resolved_or_poisoned(arg); + }; + let uid = v.uid; + // This resolution is already running further up the stack: answering would + // recurse forever, so report the argument as unavailable and let the rule + // coarsen. + if ARGS_IN_FLIGHT.with(|s| s.borrow().contains(&uid)) { + return Ok(None); + } + let _in_flight = InFlight::mark(uid); + resolved_or_poisoned(arg) +} + +/// Run the resolution pipeline, keeping a reduction failure as a failure and treating +/// every other coalesce outcome as "nothing known at this position". +fn resolved_or_poisoned(arg: &Type) -> Result, super::ReduceError> { + match super::coalesce_compact(&super::simplify_type(compact_type(arg))) { + Ok(t) => Ok(Some(t)), + Err(super::CoalesceError::Reduce(e)) => Err(e), + Err(_) => Ok(None), + } +} + // --------------------------------------------------------------------------- // CompactType + compact_type: bound-graph flattening // --------------------------------------------------------------------------- @@ -295,6 +407,18 @@ pub struct CompactType { /// onto each child's variables, and compaction only needs a deterministic /// materialization, not a second polarity analysis. pub history_slot: Option<(Box, Box, HistoryKind)>, + /// A [`ReduceError`](super::ReduceError) from a type function at this position. + /// + /// Compaction has no error channel — it returns a bag of contributions, not a + /// `Result` — but a failed reduction is a *real type error* (`1 + "a"` has no + /// common base) and must not degrade into "this position is unknown", which + /// would surface later as an unresolved variable with no blame. So the failure + /// rides the position it poisoned and [`coalesce_compact`](super::coalesce_compact) + /// raises it where the type is materialized — which is a node, with a span. + /// + /// Propagates through [`merge`](Self::merge): a poisoned side keeps its error, + /// since merging cannot un-fail a reduction. + pub reduce_error: Option, } impl CompactType { @@ -347,6 +471,14 @@ impl CompactType { )) } }; + // A poisoned side stays poisoned, at **both** polarities, and the positive + // one is the case worth being explicit about: there the merge is a join, so + // absorbing a failed operand looks like the sound direction. It is not. + // Merging cannot un-fail a reduction — the operands genuinely have no common + // base — and dropping the error would turn a real type error back into an + // unknown position, which resurfaces later as an unresolved variable with no + // span. Either side's error will do; the first is the one to report. + let reduce_error = lhs.reduce_error.or(rhs.reduce_error); CompactType { vars, atoms, @@ -355,6 +487,7 @@ impl CompactType { fun, refinements, history_slot, + reduce_error, } } @@ -585,7 +718,50 @@ fn compact_go( } // A bare `Hole` shouldn't reach the solver (emission turns it into a // fresh var), but treat it as no contribution for exhaustiveness. - Type::Hole => CompactType::empty(), + Type::Hole | Type::SharedHole(_) => CompactType::empty(), + // A type function **reduces here**, which is the whole point of putting the + // computation in the type: materialization is demand-driven, so by the time + // anything asks what this position is, resolving the arguments pulls + // whatever the graph knows. The reduced type then compacts at the current + // polarity like any other, so a type function's result participates in merging + // and subtyping as an ordinary type. + // + // A reduction failure contributes nothing rather than raising: this walk has + // no error channel, and the unreduced type surfaces at the strict wall as + // `UnreducedApp` (a real base conflict shows up there too, as the + // position it poisoned). Keeping the failure silent *here* also means a + // cyclic argument degrades to "no information at this position", which is + // what lets the enclosing read fall back to its other bounds. + Type::App { fun, args } => { + let mut resolved: Vec = Vec::with_capacity(args.len()); + let mut poisoned = None; + for a in args { + match resolve_argument(a, subst_acc) { + Ok(Some(t)) => resolved.push(super::reduce::Arg::Known(t)), + Ok(None) => resolved.push(super::reduce::Arg::Cyclic), + // An argument that failed to reduce poisons this position too: + // there is no answer to compute from it, and reporting the inner + // failure is more use than a coarsened outer one. + Err(e) => { + poisoned = Some(e); + break; + } + } + } + if let Some(e) = poisoned { + return CompactType { + reduce_error: Some(e), + ..Default::default() + }; + } + match super::reduce::reduce(fun, &resolved) { + Ok(reduced) => compact_go(&reduced, pol, subst_acc, parents, st), + Err(e) => CompactType { + reduce_error: Some(e), + ..Default::default() + }, + } + } Type::Fun { name, kind, @@ -719,7 +895,7 @@ fn compact_go( // coalesces per-use *clones* pinned to one resolved use type); // only those clones and the per-use instantiations reach here, // each fixed by a single use site. - let s = state.bounds.borrow(); + let s = state.bounds(); let primary = if pol { &s.lower } else { &s.upper }; // When the polarity-correct list is empty we fall back to the // opposite-polarity bounds (see the rationale above). Track which diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index 0aae1984..7b6ed2d0 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -142,6 +142,7 @@ pub enum ConstrainError { pub struct ConstrainCache { edges: HashMap<(Type, Type), Vec<(Subst, Subst)>>, kind_aware: bool, + parked: Vec<(Type, Type)>, } impl ConstrainCache { @@ -152,6 +153,7 @@ impl ConstrainCache { Self { edges: HashMap::new(), kind_aware: true, + parked: Vec::new(), } } @@ -161,9 +163,27 @@ impl ConstrainCache { Self { edges: HashMap::new(), kind_aware: false, + parked: Vec::new(), } } + /// Hold an obligation the solver cannot decide yet because one side is an + /// unreduced [`Type::App`] — see [`constrain_go`]'s `App` arm. + fn park(&mut self, lhs: Type, rhs: Type) { + self.parked.push((lhs, rhs)); + } + + /// How many obligations are parked, so a caller can claim the ones its own + /// call added and tag them with the node to blame. + pub fn parked_len(&self) -> usize { + self.parked.len() + } + + /// Take the obligations parked at or after `mark`. + pub fn take_parked_from(&mut self, mark: usize) -> Vec<(Type, Type)> { + self.parked.split_off(mark.min(self.parked.len())) + } + /// The composite-substitution bridges recorded for a subtyping edge, /// inserting an empty list on first visit. This is the cycle breaker: a /// re-entry on the same `(lhs, rhs)` pair finds its in-progress entry rather @@ -629,7 +649,7 @@ fn constrain_go( // onto the two content sides. (Type::Infer(lv), _) if type_level(rhs) <= lv.level => { let lows = { - let mut s = lv.bounds.borrow_mut(); + let mut s = lv.bounds_mut(); s.upper .push(Bound::edge(sl.clone(), rhs.clone(), sr.clone())); s.lower.clone() @@ -657,7 +677,7 @@ fn constrain_go( // Here the forward morphism is read directly off the edge. (_, Type::Infer(rv)) if type_level(lhs) <= rv.level => { let ups = { - let mut s = rv.bounds.borrow_mut(); + let mut s = rv.bounds_mut(); s.lower .push(Bound::edge(sr.clone(), lhs.clone(), sl.clone())); s.upper.clone() @@ -882,6 +902,31 @@ fn constrain_go( } } + // An unreduced type-function application on either side. **Deliberately not + // reduced here**: constraint emission runs while the graph is still being + // built, and reduction resolves its arguments off that graph — an answer read + // now could be superseded by an edge recorded a moment later, which is exactly + // the staleness the demand-driven design exists to rule out. + // + // So the obligation is **parked**, not dropped: held until emission completes, + // then retried against the finished graph, where reduction is meaningful + // (`InferCtx::check_parked_obligations`). Two same-function applications of + // equal arguments already short-circuited as trivially equal above. + // + // Both directions are parked, because the arm's rule is "undecidable now" + // rather than a claim about which shapes arrive. The one that matters is an + // application on the *lower* side against a concrete demand: `(1 + 2) and + // True` closes to `Add(α, β) <: Bool`, which nothing downstream re-derives, + // so accepting it silently turned an ordinary user type error into a panic + // at the `check_pre_desugar` wall. + // + // The substitutions in flight are applied on the way in: a parked obligation + // outlives this frame, so it must not depend on morphisms the frame carries. + (Type::App { .. }, _) | (_, Type::App { .. }) => { + cache.park(sl.apply_type(lhs), sr.apply_type(rhs)); + Ok(()) + } + _ => Err(ConstrainError::Mismatch { lhs: lhs.clone(), rhs: rhs.clone(), @@ -936,7 +981,8 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn - | Type::Hole => ty.clone(), + | Type::Hole + | Type::SharedHole(_) => ty.clone(), Type::Fun { name, kind, @@ -964,6 +1010,17 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac .map(|(k, t)| (k.clone(), extrude(t, pol, target_level, cache))) .collect(), ), + // A type function extrudes argumentwise. Arguments keep the enclosing + // polarity: an operator declares no variance, and extrusion only needs to + // copy structure across a level boundary — reduction is what eventually + // interprets the arguments, and it runs on the copy just as on the original. + Type::App { fun, args } => Type::App { + fun: fun.clone(), + args: args + .iter() + .map(|a| extrude(a, pol, target_level, cache)) + .collect(), + }, Type::Refinement(inner, r) => Type::Refinement( Box::new(extrude(inner, pol, target_level, cache)), r.clone(), @@ -992,7 +1049,7 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac // Snapshot the bounds we'll need to extrude before we mutate // the original; otherwise we'd race the borrow checker. let (lows, ups) = { - let s = tv.bounds.borrow(); + let s = tv.bounds(); (s.lower.clone(), s.upper.clone()) }; @@ -1000,8 +1057,7 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac // Positive: original flows into new var. Original gains // `nvs` as an upper bound; new var inherits original's // lower bounds (extruded at the same polarity). - tv.bounds - .borrow_mut() + tv.bounds_mut() .upper .push(Bound::conc(Type::Infer(Rc::clone(&nvs)))); let new_lows: Vec<_> = lows @@ -1012,13 +1068,12 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac ty_subst: b.ty_subst.clone(), }) .collect(); - nvs.bounds.borrow_mut().lower = new_lows; + nvs.bounds_mut().lower = new_lows; } else { // Negative: new var flows into original. Original gains // `nvs` as a lower bound; new var inherits original's // upper bounds. - tv.bounds - .borrow_mut() + tv.bounds_mut() .lower .push(Bound::conc(Type::Infer(Rc::clone(&nvs)))); let new_ups: Vec<_> = ups @@ -1029,7 +1084,7 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac ty_subst: b.ty_subst.clone(), }) .collect(); - nvs.bounds.borrow_mut().upper = new_ups; + nvs.bounds_mut().upper = new_ups; } Type::Infer(nvs) } @@ -1095,7 +1150,7 @@ fn extrude_invariant(ty: &Type, target_level: Level, cache: &mut ExtrudeCache) - // `tv`); re-seeding from it would create a spurious `proxy <: proxy` // self-edge. let (lows, ups) = { - let s = tv.bounds.borrow(); + let s = tv.bounds(); let not_proxy = |b: &Bound| !matches!(&b.ty, Type::Infer(v) if v.uid == nvs.uid); ( s.lower @@ -1112,8 +1167,7 @@ fn extrude_invariant(ty: &Type, target_level: Level, cache: &mut ExtrudeCache) - }; // Positive link: `tv <: proxy`; proxy inherits `tv`'s lower bounds. if !has_pos_link { - tv.bounds - .borrow_mut() + tv.bounds_mut() .upper .push(Bound::conc(Type::Infer(Rc::clone(&nvs)))); let new_lows: Vec<_> = lows @@ -1124,12 +1178,11 @@ fn extrude_invariant(ty: &Type, target_level: Level, cache: &mut ExtrudeCache) - ty_subst: b.ty_subst.clone(), }) .collect(); - nvs.bounds.borrow_mut().lower.extend(new_lows); + nvs.bounds_mut().lower.extend(new_lows); } // Negative link: `proxy <: tv`; proxy inherits `tv`'s upper bounds. if !has_neg_link { - tv.bounds - .borrow_mut() + tv.bounds_mut() .lower .push(Bound::conc(Type::Infer(Rc::clone(&nvs)))); let new_ups: Vec<_> = ups @@ -1140,7 +1193,7 @@ fn extrude_invariant(ty: &Type, target_level: Level, cache: &mut ExtrudeCache) - ty_subst: b.ty_subst.clone(), }) .collect(); - nvs.bounds.borrow_mut().upper.extend(new_ups); + nvs.bounds_mut().upper.extend(new_ups); } Type::Infer(nvs) } @@ -1373,9 +1426,9 @@ mod tests { let Type::Infer(v) = &a else { unreachable!() }; let expected = refined(prim(BaseType::Int), p); assert!( - v.bounds.borrow().upper.iter().any(|u| u.ty == expected), + v.bounds().upper.iter().any(|u| u.ty == expected), "?a should carry {{Int | p}} as an upper bound, got {:?}", - v.bounds.borrow().upper + v.bounds().upper ); } @@ -1482,7 +1535,7 @@ mod tests { let mut cache = ConstrainCache::new(); constrain_subtype(&v, &p, &mut cache).unwrap(); if let Type::Infer(state) = &v { - let s = state.bounds.borrow(); + let s = state.bounds(); assert_eq!(s.upper.len(), 1); assert!(s.lower.is_empty()); } else { @@ -1498,7 +1551,7 @@ mod tests { let mut cache = ConstrainCache::new(); constrain_subtype(&p, &v, &mut cache).unwrap(); if let Type::Infer(state) = &v { - let s = state.bounds.borrow(); + let s = state.bounds(); assert!(s.upper.is_empty()); assert_eq!(s.lower.len(), 1); } else { @@ -1524,7 +1577,7 @@ mod tests { constrain_subtype(&beta, &alpha, &mut cache).unwrap(); if let Type::Infer(state) = &beta { - let s = state.bounds.borrow(); + let s = state.bounds(); assert_eq!(s.upper.len(), 1); // The recorded upper bound is α itself, not Int. assert!(matches!(&s.upper[0].ty, Type::Infer(_))); @@ -1769,7 +1822,7 @@ mod tests { let Type::Infer(orig) = &v1 else { unreachable!("fresh_var yields Type::Infer"); }; - let bounds = orig.bounds.borrow(); + let bounds = orig.bounds(); let proxy_ty = Type::Infer(Rc::clone(proxy)); assert!( bounds.upper.iter().any(|b| b.ty == proxy_ty), @@ -1822,7 +1875,7 @@ mod tests { ); // Both bound directions must survive the cache hit. let proxy_ty = Type::Infer(Rc::clone(feed_proxy)); - let bounds = orig.bounds.borrow(); + let bounds = orig.bounds(); assert!( bounds.upper.iter().any(|b| b.ty == proxy_ty), "original is missing the upper (positive) link to its proxy" @@ -2008,7 +2061,7 @@ mod tests { let Type::Infer(gamma_var) = &gamma else { unreachable!() }; - gamma_var.bounds.borrow_mut().lower.push(Bound::with_subst( + gamma_var.bounds_mut().lower.push(Bound::with_subst( Type::Infer(Rc::clone(result_var)), Subst::discharge("x", TypedExpr::lit(Lit::Int(0))), )); @@ -2061,7 +2114,7 @@ mod tests { let Type::Infer(gamma_var) = &gamma else { unreachable!() }; - gamma_var.bounds.borrow_mut().lower.push(Bound::with_subst( + gamma_var.bounds_mut().lower.push(Bound::with_subst( Type::Infer(Rc::clone(result_var)), Subst::discharge("x", TypedExpr::lit(Lit::Int(0))), )); @@ -2108,14 +2161,14 @@ mod tests { let Type::Infer(av) = &app else { unreachable!() }; - av.bounds.borrow_mut().lower.push(Bound::with_subst( + av.bounds_mut().lower.push(Bound::with_subst( r.clone(), Subst::discharge("k", TypedExpr::lit(Lit::Int(lit))), )); constrain_subtype(&app, &v, &mut cache).expect("app <: V"); } - let lows = vv.bounds.borrow().lower.clone(); + let lows = vv.bounds().lower.clone(); let rendered: Vec = lows .iter() .map(|b| format!("{}", b.materialize())) diff --git a/src/ccl/infer/solver/mod.rs b/src/ccl/infer/solver/mod.rs index 1d1ab66e..d0090473 100644 --- a/src/ccl/infer/solver/mod.rs +++ b/src/ccl/infer/solver/mod.rs @@ -43,6 +43,7 @@ use crate::ccl::{BaseType, InferVar, Level, Type}; pub mod coalesce; pub mod compact; pub mod constrain; +pub mod reduce; pub mod scheme; pub mod simplify_type; pub mod spec_key; @@ -53,6 +54,7 @@ pub mod spec_key; pub use coalesce::{CoalesceError, coalesce_compact}; pub use compact::{CompactGraph, CompactType, compact_type}; pub use constrain::{ConstrainCache, ConstrainError, ExtrudeCache, constrain_subtype, extrude}; +pub use reduce::{ReduceError, reduce}; pub use scheme::{ FreshenCache, FreshenLevel, PolyScheme, freshen_above, freshen_expr_type_slots, seed_chan_dom_pairings, @@ -91,7 +93,16 @@ pub fn type_level(ty: &Type) -> Level { // instantiation), which reads it directly and is exempted from the // `type_level` short-circuit. Type::ChanDom(..) => 0, - Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) | Type::Txn | Type::Hole => 0, + // A type function is as deep as its deepest argument: the operator itself + // introduces no variable, and generalization must see the arguments' + // levels or a scheme would quantify over a variable its own bound uses. + Type::App { args, .. } => args.iter().map(type_level).max().unwrap_or(0), + Type::Base(_) + | Type::UIntRange(_) + | Type::DataSource(_) + | Type::Txn + | Type::Hole + | Type::SharedHole(_) => 0, } } @@ -181,7 +192,7 @@ mod tests { #[test] fn fresh_var_has_no_bounds() { let v = InferVar::fresh(0); - let s = v.bounds.borrow(); + let s = v.bounds(); assert!(s.lower.is_empty()); assert!(s.upper.is_empty()); assert_eq!(v.level, 0); diff --git a/src/ccl/infer/solver/reduce.rs b/src/ccl/infer/solver/reduce.rs new file mode 100644 index 00000000..d033a15e --- /dev/null +++ b/src/ccl/infer/solver/reduce.rs @@ -0,0 +1,476 @@ +//! Reduction of [`Type::App`] — running a [`TypeFn`] on resolved argument types. +//! +//! # What a type function is +//! +//! A type function **denotes** a type; it does not construct one. `Add(Int, Int)` +//! is not a new type sitting beside `Int` in the lattice — it is `Int`, written in +//! a form that does not yet know it. Reduction is therefore *normalization*, not a +//! computation step that could be observed: [`Type::App`] is transient in exactly +//! the sense [`Type::Infer`] is, and every `Type` that escapes inference is +//! `App`-free. +//! +//! That is what keeps type functions out of the lattice's way. They add no +//! inhabitants and no subtyping edges, so [`constrain`](super::constrain) never has +//! to decide `Add(α, β) <: Add(γ, δ)` structurally — it decides the reduced types +//! instead, once the arguments are known. +//! +//! # The laws a rule must satisfy +//! +//! Adding a [`TypeFn`] variant means writing a rule in [`reduce`], and the rule is +//! only sound if it obeys all four. Each is a property of the reduction +//! *mechanism*, checkable by reading the rule, and each buys a specific guarantee +//! for inference. +//! +//! What is deliberately **not** here is a law about refinements. Whether a rule may +//! carry an argument's refinement into its result is not a property of reduction — +//! it is a question about what the operator *means*, and the answer differs per +//! operator: a rule that **selects** one of its arguments (`Max`, and `FieldOf` when +//! it lands) must carry it, because the result really is that value, while a rule +//! that **computes** a new one must not. That distinction is stated where it can be +//! decided, in `src/ccl/design/type-inference.md`, "Which operators need one". A +//! blanket prohibition here would forbid the selecting rules outright, and would +//! still not catch the failure that actually threatens soundness — a rule that +//! *invents* a claim its arguments do not support, which is monotone (law 2) and +//! inherits nothing. +//! +//! 1. **Pure.** A rule is a function of `(fun, args)` and nothing else: no +//! inference context, no bound graph, no fresh variables, no recorded +//! constraints. *Buys:* reduction can run at any point in any walk, so it can be +//! demand-driven rather than scheduled into a phase. +//! +//! 2. **Monotone** in the subtype order: if `aᵢ <: bᵢ` for every `i`, then +//! `f(a⃗) <: f(b⃗)`. *Buys:* an argument only ever gets more precise as the graph +//! fills in, so a later reduction refines an earlier one rather than +//! contradicting it. +//! +//! 3. **Declares a [`CycleTolerance`].** A rule states whether it can answer while +//! an argument is [`Arg::Cyclic`], and [`reduce`] enforces it. *Buys:* a rule +//! that cannot answer reports the cycle instead of guessing, and one that can is +//! never asked to. See "Cycles" below — this is a property of the *program*, not +//! an edge case. +//! +//! 4. **Normalizing.** The result contains no [`Type::App`]. *Buys:* one `reduce` +//! call terminates without a fixpoint, because the rule set is closed and no +//! rule feeds itself. +//! +//! # Cycles +//! +//! An argument arrives [`Cyclic`](Arg::Cyclic) when resolving it would re-enter the +//! resolution *already computing it*. This is not an edge case and not a scheduling +//! artifact — it is a **recurrence in the program**. +//! +//! A register that reads itself in its own write makes one. `x += 1` gives the +//! register's value type as the join over its seed and its writes, and one write is +//! `x + 1`, typed `Add(value(x), 1)` — so `value(x)` satisfies +//! +//! ```text +//! value(x) = join(seed, Add(value(x), 1)) +//! ``` +//! +//! a fixpoint equation, because an accumulator *is* one. Measured: 1,910 cyclic +//! arguments across the test suite, and adding a self-read is exactly what creates +//! them (`x := 7; x` has none, `x := 7; x += 1; x` has ten). +//! +//! [`compact.rs`](super::compact)'s in-flight set cuts the recursion — without it a +//! program that small overflows the stack — and the [`CycleTolerance`] a rule +//! declares is what decides whether the cut-off is usable or fatal *for that rule*. +//! +//! # What the cut actually is +//! +//! The cut is a **bounded unrolling of the equation, not an iteration towards its +//! fixpoint**. Nothing re-enters and re-answers until the answer stops changing; the +//! depth is fixed by the shape of the program and the walk terminates there. Traced +//! on `x := 0; x := x + 1; x`, one materialization reduces exactly +//! +//! ```text +//! Add(⟨cyclic⟩, 1) → Int the cut +//! Add(Int, 1) → Int the frame that asked for it +//! ``` +//! +//! and stops. `x + x` reaches three levels because each operand re-enters +//! separately; a second write adds more. Always finite. +//! +//! Whether a frame ever sees *every* argument known is **shape-dependent**, and a rule +//! must not rely on it: `x := 2; x := x * x` does reach `[Int, Int]`, while +//! `x := "a"; x := x * x` never reaches `[String, String]` — every reduction of it has +//! at least one cyclic operand. So a check written against the joined base alone can +//! simply never fire. Judge each **available** operand instead; a known operand is not +//! going to become something else. +//! +//! The consequence for a rule author is the part worth stating, because it is the +//! opposite of the familiar one: since nothing iterates, **whatever a rule answers +//! at a cut is what the unrolling carries** — there is no later pass that widens it. +//! A rule must therefore already be sound at the cut rather than merely +//! *improvable*. Both of today's rules are, for free and for different reasons: +//! arithmetic drops to the shared base, which is the top of the chain the missing +//! operand could have contributed to, and comparison is constant on its domain. +//! +//! A sharper rule that instead kept what it could see at the cut would return +//! whatever a bounded unrolling happened to reach — sound only by accident of how +//! far the program unrolled. That is the check to run when writing the range-aware +//! `Arithmetic` that "Known gaps" promises, and *widening does not answer it*, since +//! there is no iteration to widen. Either answer the base at a cut, or declare +//! [`AllKnown`](CycleTolerance::AllKnown) and report. +//! +//! `FieldOf(ρ, 𝑘)` is the first rule expected to declare `AllKnown`: it has no field +//! type to name without `ρ`, and it *selects* rather than computes, so it has no +//! base to fall back to either. Nothing constructs it yet, which is why +//! [`check_cycle_tolerance`] is factored out of [`reduce`] — reaching the `AllKnown` +//! arm through `reduce` would need a rule that declares it. + +use crate::ccl::ccl_utils::strip_refinements; +use crate::ccl::{ArithmeticKind, BaseType, Type, TypeFn}; + +/// One resolved argument, or the fact that resolving it re-entered the resolution +/// **already computing it**. +/// +/// Named rather than an `Option` because the distinction a rule has to reason about +/// is not "absent" but *cyclic*: the argument is not unknown-for-now, it is being +/// defined in terms of this very application, and there is no later point at which +/// more is known. See the module docs, "Cycles". +#[derive(Debug, Clone)] +pub enum Arg { + /// Resolved to a type. + Known(Type), + /// Resolving this argument would re-enter the resolution computing it. + Cyclic, +} + +/// Whether a rule can answer while some of its arguments are [`Arg::Cyclic`]. +/// +/// Deliberately **not** per-position. Every rule's condition is a statement about +/// *how many* arguments are cyclic, not which — arithmetic's operands are +/// interchangeable to its rule, and a rule that needs one argument needs it whether +/// it is written first or second. Today every rule sits at one extreme or the +/// other; a rule that needed "at least `n` of them" would generalize this to a +/// count, and nothing yet does. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum CycleTolerance { + /// Answers from whatever is known. A cyclic argument costs **precision**, never + /// the answer — and for a rule constant on its domain, not even that. + Any, + /// Cannot answer unless every argument is known, so a cyclic one is reported + /// rather than guessed. + AllKnown, +} + +/// Reject a cyclic argument on behalf of a rule that cannot answer through one. +/// +/// Checked here, once, rather than by each rule: the obligation belongs to the +/// rules that *cannot* answer, and those are exactly the rules whose author is most +/// likely to reach for a plausible guess instead. Declaring the tolerance and +/// enforcing it centrally is what makes forgetting impossible rather than merely +/// discouraged. +fn check_cycle_tolerance( + tolerance: CycleTolerance, + args: &[Arg], + fun: &str, +) -> Result<(), ReduceError> { + if tolerance == CycleTolerance::AllKnown && args.iter().any(|a| matches!(a, Arg::Cyclic)) { + return Err(ReduceError::CyclicArgument { + fun: fun.to_string(), + }); + } + Ok(()) +} + +/// Why a reduction could not produce a type. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ReduceError { + /// The arguments' bases have no join below `⊤` — `1 + "a"`. A genuine type + /// error in the program. + NoCommonBase { + /// The type function that could not reduce, as it is spelled in a type. + fun: String, + /// The conflicting bases, rendered, in argument order. + bases: Vec, + }, + /// An argument of a [`CycleTolerance::AllKnown`] rule was [`Arg::Cyclic`]. + /// + /// The program defined something in terms of itself in a way this rule cannot + /// answer through — a projection whose record is its own field type, say. Not a + /// conflict between types: a genuine cycle, reported rather than guessed at. + CyclicArgument { + /// The type function that could not answer, as it is spelled in a type. + fun: String, + }, + /// The operands agree on a base the operation is not defined for — `"a" * "b"`. + /// + /// The dual of [`NoCommonBase`](ReduceError::NoCommonBase): there the operands + /// disagree with each other, here they agree perfectly and the *operator* is what + /// has nothing to say, so the message names one base rather than a pair. + UndefinedForBase { + /// The type function that could not reduce, as it is spelled in a type. + fun: String, + /// The offending base, rendered. + base: String, + }, +} + +/// Run `fun` on `args`, where `None` marks an argument whose resolution is already +/// in flight (see the module docs). +/// +/// Returns `Err` only for a real conflict, which the caller that materialized the +/// type reports. A missing argument is not one: every rule today satisfies law 3. +pub fn reduce(fun: &TypeFn, args: &[Arg]) -> Result { + check_cycle_tolerance(fun.cycle_tolerance(), args, fun.name())?; + let available: Vec<&Type> = args + .iter() + .filter_map(|a| match a { + Arg::Known(t) => Some(t), + Arg::Cyclic => None, + }) + .collect(); + match fun { + // Arithmetic's result *is* the operands' shared base today, so deciding + // what is addable and computing the result are one step. The kind is kept + // because a range-aware rule needs it (`+` and `*` map operand ranges + // differently), which is also where the two stop coinciding. + TypeFn::Arithmetic(kind) => { + let base = shared_base(fun, &available)?; + // Judged per **available operand**, not on the joined base. At a cycle the + // join reflects only what is known — for `x := "a"; x := x * x` every + // reduction sees at least one cyclic operand, so the join is never + // `String ⊔ String` and a check on it alone never fires. A *known* operand + // outside the operation's domain is a violation whatever the others turn + // out to be, which is what makes this sound at a cut. + for operand in &available { + check_arithmetic_domain(*kind, &strip_refinements(operand), fun)?; + } + Ok(base) + } + // A comparison **checks and then discards**: its result is `Bool` for any + // operands that share a base and undefined for any that do not, so the rule + // is constant on its domain and the whole of its content is the domain. + // + // That is not a rule contorted to force a check — it is what comparison + // means — but the check is the reason the result is `Compare(α, β)` rather + // than a bare `Bool`. A bare `Bool` mentions neither operand, so nothing + // would ever materialize them and nothing would ever run this rule; see + // `OperatorSchemes`'s "An operand requirement must be reachable from the + // result type". + // + // Unavailable arguments weaken the check, not the answer: `Bool` is the + // result whether or not the operands have resolved. + TypeFn::Compare(_) => { + shared_base(fun, &available)?; + Ok(Type::Base(BaseType::Bool)) + } + } +} + +/// `⊔ᵢ base(argᵢ)` — the join of the arguments' bases, defined only where it is not +/// `⊤` (see the module docs, "What \"the operands share a base\" is, and is not"). +/// +/// Stripping refinements is not an approximation to be improved on — it is what +/// makes this the *base* join. A refinement is a fact about a value, and neither +/// the join of several types nor the result of computing with them is any of the +/// values the arguments described. (A range-aware arithmetic rule would *derive* a +/// new claim rather than inherit one, which is a different operation and belongs to +/// that rule, not here.) +/// +/// The `debug_assert` below is this function's **postcondition**, not a rule every +/// reduction obeys: a join taken in the base sublattice lands in the base +/// sublattice. It is asserted because the strip and the join are separate steps, so +/// a refinement surviving one of them would otherwise be silent. A rule that +/// *selects* an argument (`Max`, `FieldOf`) is supposed to carry that argument's +/// refinement through and must not reuse this postcondition — see +/// `src/ccl/design/type-inference.md`, "Which operators need one". +/// +/// Missing and unresolved arguments are skipped rather than treated as `⊥`, which +/// is law 3: the join over a subset is a supertype of the join over all of them. With +/// nothing available at all the answer is `Hole`, the "nothing is known here" type — +/// reachable only for a fully cyclic application, and it lets the enclosing +/// resolution fall back to whatever else it can see rather than failing outright. +/// +/// **The join is computed with `==`, which is only right for leaf arguments.** In a +/// discrete sublattice the join of two types is either one of them or `⊤`, so `==` +/// decides it — but only when the arguments have no *interior*. Two bases differing +/// solely in an unresolved position inside them — `(?1, Int)` and `(?2, Int)` — +/// compare unequal and would be reported as a conflict, which is a claim about +/// placeholder identity rather than about types. Nothing can reach that today: every +/// operand of an arithmetic or comparison operator that the runtime accepts is a +/// scalar, so a stripped argument is a leaf or a bare `Infer`, and a bare `Infer` is +/// skipped. A compound-argument type function — `FieldOf(ρ, 𝑘)` and +/// `CollectionUnion` are the named next clients — must not reuse this test; it needs +/// agreement *modulo* unresolved positions, the way the lattice itself compares. +/// Reject a base the operation is not defined on. +/// +/// **Agreement is not the whole requirement.** [`shared_base`] answers "do the operands +/// describe the same thing", which `"a" * "b"` satisfies perfectly — so on its own the +/// rule reported `String` for it. Each operation carries its own domain, which is why +/// the kind rides on [`TypeFn::Arithmetic`] rather than being erased at lowering. +/// +/// Only a resolved [`Type::Base`] is judged: an unresolved position is one the graph has +/// not filled in rather than a violation, and a non-scalar shape reaching arithmetic is +/// [`shared_base`]'s own leaf-argument gap (see the module docs) rather than this rule's +/// to decide. +fn check_arithmetic_domain( + kind: ArithmeticKind, + base: &Type, + fun: &TypeFn, +) -> Result<(), ReduceError> { + let Type::Base(b) = base else { return Ok(()) }; + let defined = match kind { + // `+` is also string concatenation. `lambda_elim` rewrites it to `Concat` + // *after* inference, so at this point it is still the arithmetic scheme. + ArithmeticKind::Add => matches!(b, BaseType::Int | BaseType::String), + ArithmeticKind::Sub | ArithmeticKind::Mul | ArithmeticKind::FloorDiv => { + matches!(b, BaseType::Int) + } + }; + if defined { + return Ok(()); + } + Err(ReduceError::UndefinedForBase { + fun: fun.name().to_string(), + base: b.to_string(), + }) +} + +fn shared_base(fun: &TypeFn, args: &[&Type]) -> Result { + let mut bases = args.iter().map(|t| strip_refinements(t)); + let Some(first) = bases.next() else { + return Ok(Type::Hole); + }; + let mut result = first; + for base in bases { + // An unresolved argument contributes no constraint on the base: it is a + // position nothing concrete reached, not a conflicting one. + if matches!(result, Type::Hole | Type::Infer(_)) { + result = base; + continue; + } + if matches!(base, Type::Hole | Type::Infer(_)) || base == result { + continue; + } + return Err(ReduceError::NoCommonBase { + fun: fun.name().to_string(), + bases: args + .iter() + .map(|t| strip_refinements(t).to_string()) + .collect(), + }); + } + debug_assert!( + !matches!(result, Type::Refinement(..)), + "{fun} reduced to a refined type ({result}) — a computed type must carry no \ + value-level claim of its own" + ); + Ok(result) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::ccl::infer::lit_singleton; + use crate::ccl::{ArithmeticKind, BaseType, Lit}; + + fn int() -> Type { + Type::Base(BaseType::Int) + } + fn add() -> TypeFn { + TypeFn::Arithmetic(ArithmeticKind::Add) + } + + /// The reported bug, at the level of the rule: two operands that are each the + /// *same* singleton must still compute to the base. Sharing a lattice position + /// intersects refinement sets, and intersecting a set with itself returns it — + /// which is how `1 + 1` came to claim it was `1`. + #[test] + fn arithmetic_on_identical_singletons_is_the_base() { + let one = lit_singleton(&Lit::Int(1)); + let out = reduce(&add(), &[Arg::Known(one.clone()), Arg::Known(one)]).expect("reduces"); + assert_eq!(out, int()); + } + + #[test] + fn arithmetic_drops_refinements_and_keeps_the_base() { + let out = reduce( + &add(), + &[ + Arg::Known(lit_singleton(&Lit::Int(1))), + Arg::Known(lit_singleton(&Lit::Int(5))), + ], + ) + .expect("reduces"); + assert_eq!(out, int()); + } + + #[test] + fn conflicting_bases_are_an_error() { + let err = reduce( + &add(), + &[Arg::Known(int()), Arg::Known(Type::Base(BaseType::String))], + ) + .expect_err("Int and String share no base"); + assert!(matches!(err, ReduceError::NoCommonBase { .. }), "{err:?}"); + } + + /// Law 3: an argument the program has not determined weakens the check, not + /// the answer. `\x -> x > 1` still has result type `Bool` with its operand + /// undetermined, and `\x -> x + 1` still has result type `Int`. + #[test] + fn a_missing_argument_answers_from_the_rest() { + let out = reduce( + &add(), + &[Arg::Cyclic, Arg::Known(lit_singleton(&Lit::Int(1)))], + ) + .expect("coarsens"); + assert_eq!(out, int()); + } + + /// And with nothing available it is the empty answer, not an error — the + /// enclosing resolution may still have another way to see the position. + #[test] + fn all_arguments_missing_is_the_empty_answer() { + let out = reduce(&add(), &[Arg::Cyclic, Arg::Cyclic]).expect("coarsens"); + assert_eq!(out, Type::Hole); + } + + /// The two tolerances are different in kind, and the dispatch between them is + /// checked directly — no rule reports `AllKnown` yet, so going through + /// [`reduce`] would only ever exercise one arm. + /// + /// [`CycleTolerance::Any`] is what lets an accumulator have a type at all: a + /// register that reads itself in its own write makes `Add(value(x), 1)` where + /// `value(x)` is what is being computed, and a rule that refused to answer + /// would reject every `x += 1`. + /// + /// [`CycleTolerance::AllKnown`] is the case `FieldOf(ρ, 𝑘)` will be: no answer + /// exists without `ρ`, so the cycle is reported rather than guessed at. + #[test] + fn a_rule_that_cannot_answer_through_a_cycle_reports_it() { + let cyclic = [Arg::Cyclic, Arg::Known(int())]; + let known = [Arg::Known(int()), Arg::Known(int())]; + + assert!(check_cycle_tolerance(CycleTolerance::AllKnown, &cyclic, "FieldOf").is_err()); + assert!(check_cycle_tolerance(CycleTolerance::AllKnown, &known, "FieldOf").is_ok()); + assert!(check_cycle_tolerance(CycleTolerance::Any, &cyclic, "Add").is_ok()); + } + + /// Today's rules both tolerate a cycle, for reasons worth keeping apart: a + /// comparison is *constant on its domain* so a cyclic operand costs nothing, + /// while arithmetic answers from the operand it can see and loses only the + /// agreement check. + #[test] + fn todays_rules_tolerate_a_cycle() { + assert_eq!(add().cycle_tolerance(), CycleTolerance::Any); + assert_eq!( + TypeFn::Compare(crate::ccl::CompareKind::Equals).cycle_tolerance(), + CycleTolerance::Any + ); + assert_eq!( + reduce(&add(), &[Arg::Cyclic, Arg::Known(int())]).expect("answers"), + int() + ); + assert_eq!( + reduce( + &TypeFn::Compare(crate::ccl::CompareKind::Equals), + &[Arg::Cyclic, Arg::Cyclic] + ) + .expect("constant on its domain"), + Type::Base(BaseType::Bool) + ); + } +} diff --git a/src/ccl/infer/solver/scheme.rs b/src/ccl/infer/solver/scheme.rs index fb06a2e3..c0815b4d 100644 --- a/src/ccl/infer/solver/scheme.rs +++ b/src/ccl/infer/solver/scheme.rs @@ -13,8 +13,6 @@ use crate::ccl::subst::Subst; use crate::ccl::ty::{FunKind, FunKindVar, FunKindVarId}; use crate::ccl::{Bound, InferVar, InferVarId, Level, Refinement, Type, TypedExpr}; -use super::type_level; - // --------------------------------------------------------------------------- // Polymorphic schemes // --------------------------------------------------------------------------- @@ -29,7 +27,7 @@ use super::type_level; /// # Usage /// /// Two sources of schemes: (1) operator/projection signatures that are -/// inherently polymorphic (`Compare : ∀α. α → α → Bool`, +/// inherently polymorphic (`Compare : ∀α β. α → β → Greater(α, β)`, /// `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 @@ -165,27 +163,87 @@ fn freshen_kind_var(kv: &Rc, cache: &mut FreshenCache) -> Rc Level { + fn predicate_level(expr: &TypedExpr) -> Level { + let mut lvl = 0; + expr.walk_type_slots(|t| lvl = lvl.max(freshen_level(t))); + expr.walk_children(|c| lvl = lvl.max(predicate_level(c))); + lvl + } + // One walk, not `type_level` plus a second descent: `walk_children` already + // reaches every structural position, so the only thing to add is the + // predicate it documents itself as skipping. `ChanDom` needs no arm — it has + // no children and is not an `Infer`, so it contributes 0, which is the same + // answer `type_level` gives it and for the same reason. + let mut lvl = match ty { + Type::Infer(v) => v.level, + _ => 0, + }; + if let Type::Refinement(_, r) = ty { + lvl = lvl.max(predicate_level(&r.predicate)); + } + ty.walk_children(|c| lvl = lvl.max(freshen_level(c))); + lvl +} + pub fn freshen_above( lim: Level, ty: &Type, target: FreshenLevel, cache: &mut FreshenCache, ) -> Type { - // A `Refinement`'s `type_level` reflects only its base, but its predicate - // term carries its own type slots (which may hold quantified variables a - // low base hides). So never short-circuit a refinement on `type_level`; - // descend and freshen the predicate slots too (each leaf slot still - // short-circuits on its own level). A `ChanDom` is likewise exempt: it - // deliberately reports `type_level` 0 (its level must not trigger - // extrusion — see `type_level`), so its quantification is decided by the - // arm below from its *stored* introduction level. - if !matches!(ty, Type::Refinement(..) | Type::ChanDom(..)) && type_level(ty) <= lim { + // The short-circuit asks [`freshen_level`], not `type_level`: a refinement's + // predicate holds type slots whose quantified variables a low base hides, and + // freshening has to copy them (see [`freshen_level`] for why the two levels + // are different questions). A `ChanDom` is exempt outright: it deliberately + // reports level 0 (its level must not trigger extrusion — see `type_level`), + // so its quantification is decided by the arm below from its *stored* + // introduction level. + if !matches!(ty, Type::ChanDom(..)) && freshen_level(ty) <= lim { return ty.clone(); } match ty { - Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) | Type::Txn | Type::Hole => { - ty.clone() - } + Type::Base(_) + | Type::UIntRange(_) + | Type::DataSource(_) + | Type::Txn + | Type::Hole + | Type::SharedHole(_) => ty.clone(), + // A type function freshens argumentwise, so an instantiation applies the + // same function to *its own* variables (`Add(α', β')`). A bound whose type + // is an application is freshened through this same cache, for the same + // reason. + Type::App { fun, args } => Type::App { + fun: fun.clone(), + args: args + .iter() + .map(|a| freshen_above(lim, a, target, cache)) + .collect(), + }, // A channel domain minted inside the generalized definition // (level > lim) is *quantified* exactly like a variable — each // instantiation is its own channel. But a rigid name cannot be @@ -276,7 +334,7 @@ pub fn freshen_above( // Snapshot bounds before recursing — the recursion may touch // other variables but must not see partially-mutated state. let (lows, ups) = { - let s = tv.bounds.borrow(); + let s = tv.bounds(); (s.lower.clone(), s.upper.clone()) }; // Freshen the bound's type *and* its edge substitutions' discharge @@ -301,7 +359,7 @@ pub fn freshen_above( }) .collect(); { - let mut s = v.bounds.borrow_mut(); + let mut s = v.bounds_mut(); s.lower = new_lows; s.upper = new_ups; } @@ -410,7 +468,7 @@ fn seed_pairings_go( if let Type::Infer(dv) = peel(def_ty) { if seen.insert(dv.uid) { let (lows, ups) = { - let s = dv.bounds.borrow(); + let s = dv.bounds(); (s.lower.clone(), s.upper.clone()) }; for b in lows.iter().chain(ups.iter()) { @@ -422,7 +480,7 @@ fn seed_pairings_go( if let Type::Infer(uv) = peel(use_ty) { if seen.insert(uv.uid) { let (lows, ups) = { - let s = uv.bounds.borrow(); + let s = uv.bounds(); (s.lower.clone(), s.upper.clone()) }; for b in lows.iter().chain(ups.iter()) { @@ -490,6 +548,27 @@ fn seed_pairings_go( seed_pairings_go(uv, dv, lim, out, seen); seed_pairings_go(ud, dd, lim, out, seen); } + // A type function's arguments are ordinary child types, so they pair + // argumentwise. Nothing reaches this today — an `App` is materialized + // away before a use type is resolved, and today's type functions take scalar + // arguments that could not hold a `ChanDom` anyway — but a compound-argument + // type function (`FieldOf`, `CollectionUnion`) could, and falling into the + // structural-disagreement arm below would silently leave a definition's + // channel unpaired. + ( + Type::App { + fun: ufun, + args: ua, + }, + Type::App { + fun: dfun, + args: da, + }, + ) if ufun == dfun => { + for (u, d) in ua.iter().zip(da) { + seed_pairings_go(u, d, lim, out, seen); + } + } // A feed handle reads through to its stream `Fun(domain, value)` // during coalescing (`dissolve_read_feeds`), so the use side may be // the dissolved `Fun` where the definition still carries the @@ -544,6 +623,7 @@ fn freshen_subst_payloads( #[cfg(test)] mod tests { + use super::super::type_level; use super::*; use crate::ccl::ty::{FunKind, FunKindVar}; use crate::ccl::{BaseType, InferVar}; @@ -589,6 +669,64 @@ mod tests { ); } + /// A quantified variable reachable *only* through a refinement predicate must + /// still be freshened. + /// + /// The shape is the one a comprehension produces: a `Fun` whose every + /// structural position is ground (`[0,2] ⇒ Int`), carrying a refinement whose + /// base is also ground — so `type_level` reports 0 for the whole thing — while + /// the predicate holds a level-5 variable. Short-circuiting on `type_level` + /// returns the type verbatim and the clone keeps pointing at the definition's + /// live variable, which shows up downstream as a *duplicate* specialization: + /// the clone reaches one generalized `let` through both the freshened variable + /// and the original. + /// + /// Guarding a top-level `Refinement` is not enough — one level of nesting is + /// what the real shape has, and what this pins. + #[test] + fn a_variable_reachable_only_through_a_predicate_is_freshened() { + let quantified = InferVar::fresh(5); + // A predicate term whose *type slot* holds the quantified variable. + let predicate = Rc::new( + TypedExpr::lit(crate::ccl::Lit::Bool(true)) + .with_ty(Type::Infer(Rc::clone(&quantified))), + ); + let refined_domain = Type::Refinement( + Box::new(Type::UIntRange(3)), // ground base: hides the predicate's level + Refinement::sharing(&predicate), + ); + let ty = Type::Fun { + name: None, + kind: FunKind::Compute, + domain: Box::new(refined_domain), + codomain: Box::new(Type::Base(BaseType::Int)), + }; + assert_eq!( + type_level(&ty), + 0, + "precondition: `type_level` cannot see the predicate's variable" + ); + + let mut cache = FreshenCache::new(); + let fresh = freshen_above(0, &ty, FreshenLevel::At(1), &mut cache); + + let Type::Fun { domain, .. } = &fresh else { + panic!("expected a function type"); + }; + let Type::Refinement(_, r) = &**domain else { + panic!("expected the refinement to survive freshening"); + }; + let Type::Infer(v) = &r.predicate.ty else { + panic!("expected the predicate's type slot to stay a variable"); + }; + assert_ne!( + v.uid, quantified.uid, + "a quantified variable reachable only through a predicate must be \ + freshened — sharing it with the definition mints a duplicate \ + specialization" + ); + } + #[test] fn freshening_mirrors_kind_var_links_onto_instantiation() { // Two `<:`-linked kind vars in one scheme must stay linked after diff --git a/src/ccl/infer/solver/simplify_type.rs b/src/ccl/infer/solver/simplify_type.rs index 31b7e560..9206b4db 100644 --- a/src/ccl/infer/solver/simplify_type.rs +++ b/src/ccl/infer/solver/simplify_type.rs @@ -344,6 +344,7 @@ fn simplify_reconstruct( fun: new_fun, refinements: ct.refinements, history_slot: new_history_slot, + reduce_error: ct.reduce_error, } } diff --git a/src/ccl/infer/solver/spec_key.rs b/src/ccl/infer/solver/spec_key.rs index 11a1c5b2..2b267602 100644 --- a/src/ccl/infer/solver/spec_key.rs +++ b/src/ccl/infer/solver/spec_key.rs @@ -357,7 +357,25 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView // no `Hole` reaches a use's instantiation type in the first place. The // arm is for exhaustiveness, and "no information here" is the honest // reading if one ever did. - Type::Hole => KeyView::default(), + Type::Hole | Type::SharedHole(_) => KeyView::default(), + // An unreduced application contributes **nothing**, and cannot: it has no + // discriminating power at all. + // + // Keys are only ever compared within one [`SpecializeFrame`], so both sides + // come from uses of one definition, whose body is fixed — every [`TypeFn`] + // at every position is therefore identical across them (`FieldOf(.a)` stays + // `FieldOf(.a)`), and function identity can never decide. Only the type + // arguments can differ, and each is either a variable that also appears + // elsewhere in the definition's type — where this walk already reads it, so + // recording it here says the same thing twice — or one that appears *only* + // inside the application, which no use site can bound (an obligation against + // an `App` is parked, not decomposed) and which therefore resolves alike for + // every use. + // + // Recording them was measured as well as argued: instrumenting + // `specialize_use` to choose a specialization with and without this + // contribution picks the same one every time, across the whole suite. + Type::App { .. } => KeyView::default(), // A refinement rides the position it refines. The accumulated substitution // is forced on it exactly as `compact_go` does, so a suspended // dependent-application discharge lands in the key as the predicate the @@ -458,7 +476,7 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView return KeyView::default(); } let bounds = { - let b = state.bounds.borrow(); + let b = state.bounds(); if pol { b.lower.clone() } else { @@ -625,7 +643,7 @@ mod tests { let Type::Infer(v) = var else { unreachable!("fresh_var yields Type::Infer"); }; - v.bounds.borrow_mut().lower.push(Bound::conc(ty)); + v.bounds_mut().lower.push(Bound::conc(ty)); } let a = fresh_var(0); let b = fresh_var(0); diff --git a/src/ccl/infer_var.rs b/src/ccl/infer_var.rs index ae53a829..4379fded 100644 --- a/src/ccl/infer_var.rs +++ b/src/ccl/infer_var.rs @@ -206,14 +206,34 @@ pub struct InferBounds { /// borrow-free and never inspects the bound graph — which is what lets /// [`Type`] keep deriving `PartialEq`/`Eq`/`Hash`/`Debug` even while a /// variable's bounds are cyclic (a recursive type, pre-rejection) or -/// mutably borrowed mid-constraint. Only [`InferVar::bounds`] is mutable. +/// mutably borrowed mid-constraint. Only the bound lists are mutable, and only +/// through [`InferVar::bounds_mut`]. pub struct InferVar { /// Stable, globally-unique identity. pub uid: InferVarId, /// Scope level at which the variable was minted. pub level: Level, - /// Mutable lower/upper bound lists. - pub bounds: RefCell, + /// Mutable lower/upper bound lists. **Private on purpose** — see + /// [`InferVar::bounds_mut`]. + bound_lists: RefCell, +} + +impl InferVar { + /// Read the bound lists. + pub fn bounds(&self) -> std::cell::Ref<'_, InferBounds> { + self.bound_lists.borrow() + } + + /// Mutate the bound lists. + /// + /// Every write to the graph goes through here, `bound_lists` being private + /// rather than merely discouraged: the two accessors are what make "who writes + /// the bound graph" a question with a grep-able answer, and the answer is short + /// — `constrain_subtype`, the scheme registry's declared bounds, and the + /// monomorphization pin. + pub fn bounds_mut(&self) -> std::cell::RefMut<'_, InferBounds> { + self.bound_lists.borrow_mut() + } } thread_local! { @@ -268,7 +288,7 @@ impl InferVar { let var = Rc::new(InferVar { uid: fresh_infer_var_id(), level, - bounds: RefCell::new(InferBounds::default()), + bound_lists: RefCell::new(InferBounds::default()), }); ACTIVE_ARENA.with(|slot| { if let Some(vars) = slot.borrow_mut().as_mut() { diff --git a/src/ccl/lower/exprs.rs b/src/ccl/lower/exprs.rs index 522b4ddc..bab879dc 100644 --- a/src/ccl/lower/exprs.rs +++ b/src/ccl/lower/exprs.rs @@ -72,6 +72,24 @@ pub(super) fn lower_call( let collection = lower_expr(&args[0], ctx)?; let key_fn = lower_expr(&args[1], ctx)?; + // A partition function's **domain is the type of its keys**, and nothing + // in the lowered shape says so: `__gb_k`'s only occurrence is as an + // operand of the `==` below, so its type could otherwise only arrive + // backwards through the comparison — via an operand relation a + // comparison deliberately does not have. + // + // One `SharedHole` states it, at the two places the claim is *about*: the + // key application produces a key, and the group-by's own type has that + // key type as its domain. Both are facts about the group-by; `__gb_k` is + // an artifact of this desugaring, so the binder stays a plain `Hole` and + // takes its type from the annotation like any other. + // + // Placing it on the annotation's domain also makes the edge **directional + // without new machinery**: `bind_annotation` records `inferred <: ann`, + // and a function type is contravariant in its domain, so this reduces to + // `key_ty <: ⟨the parameter⟩` — produced keys flow *into* the domain. The + // earlier placement (the id on the binder itself) forced the two equal. + let key_ty = ctx.fresh_shared_hole(); // `bare_pred` (and the `collection` clone inside it) lives in the // cast target's refinement predicate — a type slot outside the // `walk_children` domain — so its nodes are deliberately untagged. @@ -79,7 +97,8 @@ pub(super) fn lower_call( Expr::apply( Expr::apply(Expr::var(Name::elem()), collection.clone()), key_fn, - ), + ) + .with_user_annotation(key_ty.clone()), BinOpKind::Compare(CompareKind::Equals), Expr::var("__gb_k"), ); @@ -100,7 +119,7 @@ pub(super) fn lower_call( // concrete-kind stamp — see `emit_node`), so its kind is data-by- // construction rather than guessed from its (scalar key) domain. Ok(Expr::lambda("__gb_k", Type::Hole, cast) - .with_user_annotation(Type::data_fun(Type::Hole, Type::Hole))) + .with_user_annotation(Type::data_fun(key_ty, Type::Hole))) } "sum" | "max" => { if args.len() != 1 { diff --git a/src/ccl/lower/mod.rs b/src/ccl/lower/mod.rs index 730ddae3..c2c699d5 100644 --- a/src/ccl/lower/mod.rs +++ b/src/ccl/lower/mod.rs @@ -81,7 +81,7 @@ use std::{ use crate::{ ccl::{ - Branch, Expr, Lit, TypedExprNode, + Branch, Expr, Lit, Type, TypedExprNode, lineage::{Nature, RewriteLabel}, }, chl_parser::ast::{Expr as ChlExpr, RecordField, Span, Spanned, Stmt as ChlStmt}, @@ -327,9 +327,23 @@ pub struct LoweringContext { /// enclosing or sibling scope. Within a block, the *last* definition of a name /// wins (see [`pre_register_mut_param_fns`]). pub(super) mut_param_fns: HashSet, + + /// Counter behind [`fresh_shared_hole`](Self::fresh_shared_hole). + next_shared_hole: u32, } impl LoweringContext { + /// A fresh [`Type::SharedHole`] id, unique within this lowering. + /// + /// Use one id per *relation* a desugaring wants to state, and stamp it on + /// every position that relation covers: inference normalizes equal ids to one + /// variable, so two positions carrying the same id are held to the same type. + /// Ids are meaningless outside the tree they were minted for. + pub(super) fn fresh_shared_hole(&mut self) -> Type { + let id = self.next_shared_hole; + self.next_shared_hole += 1; + Type::SharedHole(id) + } /// Register a data source so that `name()` lowers to `Source(name)`. pub fn register_source( &mut self, diff --git a/src/ccl/ops.rs b/src/ccl/ops.rs index 8fcb0113..5f65ccd8 100644 --- a/src/ccl/ops.rs +++ b/src/ccl/ops.rs @@ -82,7 +82,12 @@ pub enum Lit { } /// Arithmetic sub-operations for [`BinOpKind::Arithmetic`]. -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +/// +/// `Ord` carries no semantics — the operators are unordered alternatives. It exists +/// so a kind can key the per-operator scheme map in `infer`'s `OperatorSchemes`, +/// which is per-kind because the kind is part of the result *type* +/// ([`TypeFn::Arithmetic`](crate::ccl::TypeFn::Arithmetic)). +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum ArithmeticKind { /// Integer addition (`+`). Add, @@ -94,8 +99,40 @@ pub enum ArithmeticKind { FloorDiv, } +impl ArithmeticKind { + /// Every kind, for the registry that builds one scheme per operator. + /// + /// A list rather than a derive, so it has to be maintained by hand — but not + /// silently: [`type_fn_name`](Self::type_fn_name)'s match is exhaustive, so a + /// new variant stops compiling there first, right beside this. The registry + /// looking a kind up in a map is what makes an omission matter, and + /// `every_arithmetic_kind_has_a_scheme` is the backstop. + pub const ALL: [ArithmeticKind; 4] = [ + ArithmeticKind::Add, + ArithmeticKind::Sub, + ArithmeticKind::Mul, + ArithmeticKind::FloorDiv, + ]; + + /// The spelling of this operator when it appears as a **type** operator + /// ([`TypeFn::Arithmetic`](crate::ccl::TypeFn::Arithmetic)) — i.e. inside the + /// unreduced result type of an arithmetic expression. Ordinary type names, not + /// the source symbols, because a type reads as a type: `Add(Int, Int)`. + pub fn type_fn_name(&self) -> &'static str { + match self { + ArithmeticKind::Add => "Add", + ArithmeticKind::Sub => "Sub", + ArithmeticKind::Mul => "Mul", + ArithmeticKind::FloorDiv => "FloorDiv", + } + } +} + /// Comparison sub-operations for [`BinOpKind::Compare`]. -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +/// +/// `Ord` carries no semantics, exactly as on [`ArithmeticKind`] — it exists so a +/// kind can key the per-operator scheme map in `infer`'s `OperatorSchemes`. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum CompareKind { /// Equality (`==`). Equals, @@ -111,6 +148,33 @@ pub enum CompareKind { GreaterOrEq, } +impl CompareKind { + /// Every kind — see [`ArithmeticKind::ALL`], including why this is a + /// hand-maintained list that cannot silently fall behind. + pub const ALL: [CompareKind; 6] = [ + CompareKind::Equals, + CompareKind::NotEquals, + CompareKind::Less, + CompareKind::LessOrEq, + CompareKind::Greater, + CompareKind::GreaterOrEq, + ]; + + /// The spelling of this operator when it appears as a **type** operator + /// ([`TypeFn::Compare`](crate::ccl::TypeFn::Compare)) — see + /// [`ArithmeticKind::type_fn_name`]. + pub fn type_fn_name(&self) -> &'static str { + match self { + CompareKind::Equals => "Equals", + CompareKind::NotEquals => "NotEquals", + CompareKind::Less => "Less", + CompareKind::LessOrEq => "LessOrEq", + CompareKind::Greater => "Greater", + CompareKind::GreaterOrEq => "GreaterOrEq", + } + } +} + /// Boolean logic sub-operations for [`BinOpKind::BoolLogic`]. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub enum LogicKind { diff --git a/src/ccl/subst.rs b/src/ccl/subst.rs index 4e53df09..aabdc140 100644 --- a/src/ccl/subst.rs +++ b/src/ccl/subst.rs @@ -761,6 +761,7 @@ impl Subst { | Type::DataSource(_) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => {} // a nominal channel domain names its defer @@ -769,6 +770,14 @@ impl Subst { // otherwise the type slot would keep naming the dead binder. Type::ChanDom(name, _) => *name = self.handle_target(name), + // A type function: rewrite its arguments in place. The function is + // data and binds nothing, so there is no scope to restrict. + Type::App { args, .. } => { + for arg in args.iter_mut() { + self.rewrite_type_go(arg, memo); + } + } + // A transient history handle (an `Overwrite` erased by the unified phase, // a `Feed` by `channelize`): rewrite both children in place. Renaming // does not cross the kind — the value and domain are ordinary types. @@ -979,12 +988,19 @@ impl Subst { | Type::DataSource(_) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => ty.clone(), // rename the named defer binder, mirroring the // in-place mode (`rewrite_type_go`). Type::ChanDom(name, lvl) => Type::ChanDom(self.handle_target(name), *lvl), + // A type function applies argumentwise; the function binds nothing. + Type::App { fun, args } => Type::App { + fun: fun.clone(), + args: args.iter().map(|a| self.apply_type(a)).collect(), + }, + Type::Fun { name: None, domain, @@ -1089,7 +1105,8 @@ pub fn type_contains_infer(ty: &Type) -> bool { | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn - | Type::Hole => false, + | Type::Hole + | Type::SharedHole(_) => false, Type::Infer(_) => true, Type::Fun { domain, codomain, .. @@ -1101,6 +1118,11 @@ pub fn type_contains_infer(ty: &Type) -> bool { Type::Record(fs) => fs.iter().any(|(_, t)| type_contains_infer(t)), Type::Variant(tags) => tags.iter().any(|(_, t)| type_contains_infer(t)), Type::Refinement(base, _) => type_contains_infer(base), + // An unreduced application is ground exactly when every argument is: an + // undetermined argument is precisely where the `Infer` a caller is asking + // about lives, and it is what leaves the application unreduced in the first + // place. + Type::App { args, .. } => args.iter().any(type_contains_infer), } } @@ -1137,7 +1159,15 @@ fn collect_type_fv( | Type::ChanDom(..) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => {} + // A type function binds nothing, so its arguments' free variables are + // free in the application. + Type::App { args, .. } => { + for a in args { + collect_type_fv(a, bound, visited, out); + } + } Type::Fun { name, domain, diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index 96f2e80b..e701aec5 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -268,6 +268,7 @@ pub fn reset_kind_var_counter() { /// | `History` (`kind: Overwrite`) | Type checker only | "Mutable variable: a `value` cell tracked over a `domain` (loop index or transaction time)" | the unified phase (`transact_phase` / `mut_elim`, which runs *before* `channelize`; a survivor downstream is a compiler bug) | /// | `History` (`kind: Feed`) | Type checker only | "Feed channel `domain ⇒ value`: the defer binding's post-desugar stream type" | `channelize` (which runs after inference; a survivor downstream is a compiler bug) | /// | `ChanDom(d, _)` | Type checker only | "Rigid nominal domain of feed channel `d` — its domain resolves at channel assembly" | `channelize` (substituted to the concrete channel domain; a survivor downstream is a compiler bug) | +/// | `Compute { op, args }` | Type checker only | "The type `op` computes from `args`, not yet reduced" | Reduction, whenever the type is materialized (flagged as `UnreducedApp` by `collect_type_errors`; a survivor means either a cycle with no coarser answer or a program that never determined the arguments) | #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum Type { /// A primitive base type. @@ -336,6 +337,41 @@ pub enum Type { /// `UnresolvedHole` (treat as a compiler bug, not a user-facing error). /// Created exclusively by [`TypedExpr::new`] and [`crate::ccl::TypedBinding::new_unannotated`]. Hole, + /// A [`Hole`](Type::Hole) with an **identity**: every occurrence carrying the + /// same id normalizes to the *same* inference variable. + /// + /// This is how lowering states a relation between two type positions it cannot + /// name. A plain `Hole` says "infer this", and each occurrence gets its own + /// fresh variable; `SharedHole(id)` says "infer this, and it is the same one as + /// that" — the weakest thing that lets a desugaring relate two positions whose + /// common type only inference will learn. + /// + /// The motivating site is `groupby`, whose partition domain *is* the type of the + /// keys its predicate compares: + /// + /// ```text + /// λ __gb_k → cast({_ | __elem ▷ coll ▷ key_fn == __gb_k} ⤇ _, …) + /// ``` + /// + /// Nothing in that shape says so — `__gb_k`'s only occurrence is an operand of + /// the `==`, and a comparison does not relate its operands — so the id is + /// carried by the key application and by the domain of the group-by's own + /// `data_fun` annotation. Both are facts about the group-by; `__gb_k` is a name + /// this lowering invented, which is why the *binder* is not where the relation + /// is stated (see `lower_call`'s `groupby` arm for the direction that buys). + /// + /// Lowering cannot mint a [`Type::Infer`] itself for three reasons: the + /// `InferArena` that owns every variable is created *inside* `infer`, so a + /// variable minted earlier would escape the `Drop` that breaks its `Rc` cycles; + /// `fresh_var` needs a polymorphism level, which is an inference-time notion; + /// and an annotation is contractually a *request* for a variable, not one + /// already made. + /// + /// **Transient, like `Hole`**: `normalize_annotation` resolves it, and a + /// survivor is a compiler bug (`UnresolvedHole`). Ids are minted per + /// [`LoweringContext`](crate::ccl::lower::LoweringContext) and are meaningless + /// outside the tree they were minted for. + SharedHole(u32), /// Unresolved type variable, identified by a unique [`crate::ccl::InferVarId`]. /// /// Created during inference by the inference pass @@ -425,10 +461,126 @@ pub enum Type { /// off-path positions carry forward. kind: HistoryKind, }, + /// A [`TypeFn`] applied to type arguments, awaiting *reduction*: the type + /// "whatever `fun` computes from `args`". + /// + /// A lattice of type variables can state that two positions are *equal* or + /// *related by subtyping*. It cannot state that one is **computed from** + /// others, so an operator whose result type is a non-identity function of its + /// operand types has no scheme the lattice can express. `App` is that missing + /// statement: `1 + x` types as `Add({Int | __elem == 1}, α)`, which is the + /// answer, unreduced. + /// + /// An `App` **denotes** a type rather than constructing one — `Add(Int, Int)` + /// *is* `Int`, written in a form that does not yet know it — so it adds no + /// inhabitants and no subtyping edges to the lattice, and reduction is + /// normalization. It is **transient** in the same sense as [`Type::Infer`]: + /// every `Type` that escapes inference is `App`-free, and a survivor at the + /// strict wall is a compiler bug or an ambiguous program. + /// + /// **Reduction is demand-driven.** Materializing an `App` resolves each + /// argument through the ordinary pipeline — pulling whatever the graph knows, + /// wherever the walk happens to be — and then applies the function's rule. + /// Nothing is deposited, so no phase ordering can make the answer wrong. The + /// four laws a rule must obey are in + /// [`reduce`](mod@crate::ccl::infer::solver::reduce); the design is + /// `src/ccl/design/type-inference.md`, "4.7 Type functions". + App { + /// Which function. Carries its own non-type parameters (an + /// [`ArithmeticKind`](crate::ccl::ArithmeticKind), a field key, …). + fun: TypeFn, + /// The type arguments, in the function's declared parameter order. + args: Vec, + }, // Planned: // Pi { param: String, param_ty: Box, body_ty: Box } } +/// A function from types to a type: the computation a [`Type::App`] is waiting to +/// run. +/// +/// The set is closed and lives in the compiler. Keeping the function as *data*, +/// and its rule a pure function of resolved argument types, is what leaves room +/// for user-declared type schemas on UDFs later — a user-defined function becomes +/// another variant whose rule is looked up rather than matched. +/// +/// Adding a variant means writing a rule, and a rule is sound only if it obeys the +/// four laws in [`reduce`](mod@crate::ccl::infer::solver::reduce), "The laws a rule +/// must satisfy". +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +pub enum TypeFn { + /// The result of an arithmetic operator applied to operands of the given + /// types. + /// + /// Reduces to the operands' shared base today, and rejects operands that have + /// none — deciding what is addable is *this rule's* job, which is what makes + /// the reachability rule above buy anything. + /// Arithmetic *computes* a new value rather than selecting one of its + /// operands, so it inherits none of their refinements — a fact about a value + /// no longer in play. The `kind` is recorded because it is the function's + /// *identity*, and a sharper rule needs it: `+` and `*` map operand ranges to + /// different result ranges, so this is where `([0,2], [5,7]) ⇒ [5,9]` will + /// live. That is a claim *derived* from the operands, which is exactly what a + /// computing rule may do and inheriting is not. + Arithmetic(crate::ccl::ArithmeticKind), + /// The result of a comparison applied to operands of the given types. + /// + /// Reduces to `Bool` — for *any* operands that share a base, and to an error + /// for any that do not. A rule constant on its domain is still a rule, and + /// stating it as one is what gets the operand requirement checked: the solver + /// reads a bound only when something materializes the variable it sits on, and + /// a comparison's operand variables are nobody's node type. A bare `Bool` + /// result leaves nothing to reach them, so `1 > "a"` types and then panics in + /// the interpreter. See `OperatorSchemes`'s "An operand requirement must be + /// reachable from the result type". + /// + /// The `kind` is recorded for the same reason as + /// [`Arithmetic`](TypeFn::Arithmetic)'s: it is the function's identity, and a + /// sharper rule needs it — comparing two singletons has a known answer, so + /// `(1, 2) ⇒ {Bool | __elem == true}` belongs here. + Compare(crate::ccl::CompareKind), +} + +impl TypeFn { + /// Whether this rule can answer while some of its arguments are cyclic. + /// + /// A cycle is not exotic: a register that reads itself in its own write makes + /// one, so `x += 1` types as `Add(value(x), 1)` where `value(x)` is what is + /// being computed. Every rule has to have an answer to it, and the two possible + /// answers are different in kind — see + /// [`CycleTolerance`](crate::ccl::infer::solver::reduce::CycleTolerance). + /// + /// Both of today's rules are [`Any`](crate::ccl::infer::solver::reduce::CycleTolerance::Any), + /// for different reasons worth keeping straight. A comparison is *constant on + /// its domain*, so a cyclic operand costs nothing at all — the answer is `Bool` + /// either way. Arithmetic answers the shared base of whatever it can see, so a + /// cyclic operand costs the agreement **check** while keeping a usable type; + /// that is what lets an accumulator have one. + /// + /// `FieldOf(ρ, 𝑘)` will be the first `AllKnown` rule: there is no answer at all + /// without `ρ`, so guessing would invent a field type. + pub fn cycle_tolerance(&self) -> crate::ccl::infer::solver::reduce::CycleTolerance { + use crate::ccl::infer::solver::reduce::CycleTolerance; + match self { + TypeFn::Arithmetic(_) | TypeFn::Compare(_) => CycleTolerance::Any, + } + } + + /// The function's spelling, for [`Display`](fmt::Display) and diagnostics. + pub fn name(&self) -> &'static str { + match self { + TypeFn::Arithmetic(k) => k.type_fn_name(), + TypeFn::Compare(k) => k.type_fn_name(), + } + } +} + +impl fmt::Display for TypeFn { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.name()) + } +} + /// Which flavour of [`Type::History`] a handle is — a mutable variable (`:=`) or a /// feed channel (`defer` / `<<`). The two are the same object (a `domain ⇒ /// value` history) but read and materialize differently; see [`Type::History`]. @@ -554,10 +706,19 @@ impl fmt::Display for Type { None => write!(f, "{{{t} | {}}}", symbolic::symbolic(&r.predicate)), }, Type::Hole => write!(f, "_"), + // A hole with an identity renders as one: `_#0` and `_#1` are distinct + // requests, two `_#0`s are the same one. + Type::SharedHole(id) => write!(f, "_#{id}"), Type::Infer(var) => write!(f, "?{}", var.uid), Type::DataSource(name) => write!(f, "source({name})"), Type::ChanDom(name, _) => write!(f, "chan({name})"), Type::Txn => write!(f, "Txn"), + // `Add(Int, [0, 2])` — the function applied to its arguments, which is + // exactly what the type *is* until reduction runs. + Type::App { fun, args } => { + let rendered: Vec = args.iter().map(|a| a.to_string()).collect(); + write!(f, "{fun}({})", rendered.join(", ")) + } Type::History { value, domain, @@ -731,9 +892,14 @@ impl Type { domain: Box::new(domain.without_pi_names()), kind: *kind, }, + Type::App { fun, args } => Type::App { + fun: fun.clone(), + args: args.iter().map(|a| a.without_pi_names()).collect(), + }, Type::Base(_) | Type::UIntRange(_) | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) | Type::DataSource(_) | Type::ChanDom(..) @@ -768,10 +934,19 @@ impl Type { Type::Base(_) | Type::UIntRange(_) | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn => {} + // A type function's arguments are ordinary child types: every + // structural walk reaches them, so a pass that rewrites types + // rewrites what the application will later reduce. + Type::App { args, .. } => { + for a in args { + f(a); + } + } Type::Fun { domain, codomain, .. } => { @@ -809,10 +984,19 @@ impl Type { Type::Base(_) | Type::UIntRange(_) | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn => {} + // A type function's arguments are ordinary child types: every + // structural walk reaches them, so a pass that rewrites types + // rewrites what the application will later reduce. + Type::App { args, .. } => { + for a in args { + f(a); + } + } Type::Fun { domain, codomain, .. } => { diff --git a/tests/compilation_pipeline/generators_udf_poly.rs b/tests/compilation_pipeline/generators_udf_poly.rs index cbd5518f..917cafa1 100644 --- a/tests/compilation_pipeline/generators_udf_poly.rs +++ b/tests/compilation_pipeline/generators_udf_poly.rs @@ -73,6 +73,12 @@ fn test_function_def_polymorphic_used_at_two_types() { // to compile to the right answer, so this case pins the *result* while the // unit-level `SpecKey` tests pin the keying. #[case("f = \\x -> x + 1\nf(1) + f(2)", Value::Int(5))] +// The same shape, but where the UDF *returns* its refined argument, so the +// addition's two operands are both `{Int | __elem == 1}` — one refinement, reached +// twice. That combination needed both fixes: the specialization key to stop the two +// calls sharing a clone, and arithmetic's result to stop inheriting a refinement its +// operands agreed on. It failed at the post-inference wall before either. +#[case("h = \\a, b -> a\nh(1, 2) + h(1, 5)", Value::Int(2))] fn test_polymorphic_udf_calls_differing_only_in_a_literal( #[case] code: &str, #[case] expected: Value, diff --git a/tests/type_check.rs b/tests/type_check.rs index ab3a946d..9b6c2c98 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -11,6 +11,7 @@ //! → Type (test assertion here) //! ``` +use std::time::Duration; use std::{cell::RefCell, rc::Rc}; use cambra::ccl::{ @@ -585,6 +586,37 @@ fn test_collection_union_heterogeneous_rejected() { // GroupBy + aggregate tests // --------------------------------------------------------------------------- +// A group-by's key type is its key function's codomain, and the lowering says so +// **directly** rather than leaving it to be recovered through the partition +// predicate's `==`. +// +// `__gb_k`'s only occurrence in the lowered shape is as an operand of that +// comparison, so without a stated relation its type can only arrive backwards +// along the operand requirement that relates a comparison's two sides — making a +// group-by's key inference depend on an operator's internals. One +// `Type::SharedHole` states it, carried by the key application and by the domain of +// the group-by's own `data_fun` annotation; these cases pin that the key resolves +// to the key function's result type and not to the collection's element type. +// +// The relation is **not** visible in `test_lower_groupby`'s snapshots, because +// `symbolic` does not render annotations. These are the tests that cover it. +#[rstest] +#[case("groupby([1, 2, 3], \\x -> x)", "Int key from an Int element")] +#[case( + "groupby([(a=1, b=\"w\"), (a=2, b=\"e\")], \\r -> r.b)", + "String key from a String field of a record element" +)] +fn test_groupby_key_type_comes_from_the_key_function(#[case] code: &str, #[case] why: &str) { + let ty = infer_program(code); + let Type::Fun { domain, .. } = &ty else { + panic!("a group-by is a function from key to partition, got {ty}"); + }; + assert!( + !matches!(**domain, Type::Infer(_) | Type::Hole), + "the key type must be determined ({why}), got {ty}" + ); +} + #[test] fn test_groupby_aggregate() { // groups = groupby([1, 2, 3], \x -> x) @@ -775,25 +807,375 @@ fn test_self_application_types() { ); } +// An operator constrains its operands through its **result**, so a lambda whose +// parameter only feeds an operator is genuinely polymorphic in that parameter — and +// `Type` has no way to say so. +// +// `\x -> x + 1` works for any two things `+` accepts. Under a single-numeric-type +// lattice that happens to be `Int` alone, and inferring `Int ⇒ Int` reads as +// precision; it is really the lattice's poverty showing through. Add an +// `Int + Float → Float` widening and the honest domain stops being `Int`, with +// nothing about the lambda having changed. +// +// So the result resolves and the parameter does not, the same shape +// `self_application_types_without_a_recursive_type` asserts just above for +// `\x -> x(x)`. As a program value that makes it an **ambiguous program**, rejected +// downstream exactly as `\x -> [x, x]` already is +// (`test_unexercised_generic_definition_is_an_error_not_a_panic`) — inference +// tolerates the residue, the strict wall does not. #[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()) } -)] -#[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()) } +#[case::comparison("f = \\x -> x > 1\nf", bool_ty())] +#[case::arithmetic("f = \\x -> x + 1\nf", int())] +fn test_lambda_unapplied_is_polymorphic_in_its_operand( + #[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!( + matches!(**domain, Type::Infer(_)), + "the parameter is determined by nothing, so it must stay a variable: {ty}" + ); + assert_eq!( + **codomain, expected_codomain, + "the result is still determined — the rule answers from the literal operand" + ); +} + +// Nested generic arithmetic that never resolves must still **finish**. +// +// An unapplied generic function leaves its operand types unresolved, which is an +// ambiguous program and rejected downstream — but rejected, not hung on. +// +// Resolution is re-entrant: an argument resolves through the ordinary pipeline, +// which reaches other applications, so a chain of them nests. `compact.rs`'s +// in-flight set is what terminates that, and these are the programs that would +// catch it going away — or a future type function whose operand requirement is a +// self-referential bound, which makes the nesting dense enough to matter again. +// +// The timeout is the assertion, since the failure mode is unbounded rather than slow. +#[rstest] +#[timeout(Duration::from_secs(20))] +#[case::shared_operand("f = \\x, y -> x + y\ng = \\a -> f(a, a)\ng")] +#[case::distinct_operands("f = \\x, y -> x + y\ng = \\a, b -> f(a, b)\ng")] +#[case::self_addition("f = \\x -> x + x\ng = \\a -> f(a)\ng")] +#[case::comparison("g = \\a -> a > a\ng")] +fn test_unresolved_operand_chains_terminate(#[case] code: &str) { + // The type itself is uninteresting — it is residual `Infer`, which the strict + // wall rejects. Reaching this line is the property under test. + infer_program(code); +} + +// A chain of generic wrappers that *does* resolve stays cheap, which is the +// everyday half of the same property: each nesting level adds instantiations whose +// operand bounds are self-referential, and resolving them must not compound. +#[rstest] +#[timeout(Duration::from_secs(20))] +#[case(2)] +#[case(6)] +fn test_applied_generic_chain_stays_cheap(#[case] depth: usize) { + let mut code = String::from("f0 = \\x, y -> x + y\n"); + for i in 1..=depth { + code.push_str(&format!("f{i} = \\a, b -> f{}(a, b)\n", i - 1)); + } + code.push_str(&format!("f{depth}(1, 2)")); + assert_eq!(infer_program(&code), int()); +} + +// Operands with no base in common are rejected, and say so in their own words. +// +// This is the reduction error channel's only user, and the diagnostic is the point: +// routing it through `IncompatibleBounds` would borrow that variant's rendering +// ("won't infer an untagged sum from a collision") along with its shape, and that +// is not what happened — each operand is well typed and nothing collided on a +// variable. The operator simply has no rule relating an `Int` to a `String`. +// +// The comparison cases are the ones that would regress silently. A comparison's +// result is `Bool` no matter what its operands are, so a scheme that *said* `Bool` +// left nothing to materialize its operand variables and the requirement relating +// them was never read: `1 > "a"` type-checked and then panicked in the interpreter. +// Stating the result as `Less(α, β)` — a rule constant on its domain, erroring off +// it — is what puts the requirement on a path something walks. See +// `OperatorSchemes`, "An operand requirement must be reachable from the result type". +#[rstest] +#[case::literals(r#"1 + "a""#, "Add")] +#[case::through_bindings("y = \"a\"\nz = 1\ny + z", "Add")] +#[case::through_a_udf("f = \\x -> x + 1\nf(\"a\")", "Add")] +#[case::comparison(r#"1 > "a""#, "Greater")] +#[case::comparison_through_bindings("y = 1\nz = \"a\"\ny < z", "Less")] +#[case::comparison_through_a_udf("f = \\x -> x > 1\nf(\"a\")", "Greater")] +fn test_operands_with_no_common_base_are_rejected(#[case] code: &str, #[case] expected_fn: &str) { + let errs = infer_program_err(code); + assert!( + errs.iter().any(|e| matches!( + e, + InferError::NoCommonBase { fun, bases, .. } + if fun == expected_fn + && bases.iter().any(|b| b == "Int") + && bases.iter().any(|b| b == "String") + )), + "expected NoCommonBase({expected_fn}) over Int and String, got {errs:?}" + ); +} + +// The *other* direction: well-typed operands, but the result flows somewhere it +// cannot go. `(1 + 2) and True` needs `Add(α, β) <: Bool`, and `sum(["a" + "b"])` +// needs `Add(α, β) <: Int` with `α = β = String`. +// +// Neither is decidable while the constraint graph is being built — reducing the +// application there would read a half-built graph — so `constrain_go` parks the +// obligation and `check_parked_obligations` retries it once emission completes. +// Without the park store the obligation was silently accepted, inference returned +// `Ok`, and the conflict resurfaced at the `check_pre_desugar` wall, which panics +// on anything that is not `UnresolvedInfer`: an ordinary user type error rendered +// as a compiler bug. +// +// The assertion is therefore that inference *reports* rather than what it reports — +// the failure mode being guarded is a panic, not a wrong message. +#[rstest] +#[case::result_into_bool("(1 + 2) and True")] +#[case::result_into_an_aggregate(r#"sum(["a" + "b"])"#)] +#[case::result_into_an_annotation("x: Bool = 1 + 2\nx")] +fn test_an_operator_result_against_a_wrong_demand_is_a_diagnostic(#[case] code: &str) { + assert!( + !infer_program_err(code).is_empty(), + "expected a diagnostic, not a panic at the consistency wall" + ); +} + +// Every arithmetic operator has a scheme. The registry holds one per kind (the kind +// is part of the result *type*, `TypeFn::Arithmetic`) and looks it up in a map, so +// a kind added to `ArithmeticKind` without a matching `ArithmeticKind::ALL` entry +// compiles and then panics at the lookup. +#[rstest] +#[case("7 + 2", 9)] +#[case("7 - 2", 5)] +#[case("7 * 2", 14)] +#[case("7 // 2", 3)] +fn every_arithmetic_kind_has_a_scheme(#[case] code: &str, #[case] _expected: i64) { + assert_eq!(infer_program(code), int()); +} + +// An arithmetic result is the operands' **base**, never one of their refinements. +// +// Arithmetic *computes* a new value rather than selecting one of its operands, so a +// refinement either operand carries is a fact about a value that is no longer in play. +// +// The cases are chosen for the one shape that catches a scheme sharing a lattice +// position between the operands and the result. A result position **intersects** +// refinement sets, and distinct refinements intersect to none — so operands that +// merely differ hide the bug. It takes two operands carrying the *same* refinement, +// where intersecting a set with itself returns it: `y` and `z` are separate bindings +// of the same literal, so both are `{Int | __elem == 1}` and a sharing scheme reports +// the sum as `1`. +// +// `f(1) + f(1)` is that shape one level up, with the operand types variables rather +// than literals. It is why the fix has to be `TypeFn::Arithmetic` reducing once the +// arguments resolve, and not a syntactic refinement strip at emit: a strip covers the +// literal case and cannot see through a variable. +#[rstest] +#[case("1 + 1")] +#[case("y = 1\nz = 1\ny + z")] +#[case("y = 2\ny + y")] +#[case("f = \\a, b -> a\nf(1, 2) + f(1, 5)")] +fn test_arithmetic_result_is_the_base(#[case] code: &str) { + assert_eq!(infer_program(code), int()); +} + +// An operand does not inherit its *sibling's* refinement, because nothing relates +// the two operands at all. +// +// Under a shared-variable scheme they were one lattice position, and the operand +// positions are function domains — negative, where refinement sets union — so +// `\x -> 1 + x` inferred `x : {Int | __elem == 1}`, demanding the parameter *be* +// the literal. The property now holds for a structural reason rather than a +// careful one: the operands are two unrelated variables, so there is no channel +// for a refinement to cross. +// +// What that costs is the parameter's type entirely, which is +// `test_lambda_unapplied_is_polymorphic_in_its_operand`. What it must *not* cost is +// the result: `1 + x` is an `Int` and not the sibling's singleton, which is what +// these cases pin at the one place a type still lands. +#[rstest] +#[case("f = \\x -> 1 + x\nf(5)")] +#[case("f = \\x -> x - 7\nf(5)")] +fn test_an_operator_result_does_not_inherit_an_operand_refinement(#[case] code: &str) { + assert_eq!( + infer_program(code), + int(), + "the result is the base, not either operand's singleton" + ); +} + +// For every operator in the scheme registry: does its result inherit an input's +// refinement, and *should* it? +// +// The distinction is what decides whether an operator needs a type function at all. +// Sharing a lattice position between an input and the result is correct exactly when +// the operator **selects** an existing value or **merges** several — the result *is* +// one of those values, so a fact about it survives. It is wrong when the operator +// **computes** a new value, which is what arithmetic did. +// +// So these cases are not all asserting "the refinement is gone": half of them assert +// it is still there, because dropping it would be the bug in the other direction. +#[rstest] +// Computing: the result is a value none of the inputs is, so the base and nothing more. +#[case::sum("sum([1, 1])", int())] +#[case::neg("x = 1\n-x", int())] +#[case::not("b = True\nnot b", bool_ty())] +// `+` on strings is still the arithmetic scheme at inference time — the rewrite to +// `Concat` happens in `lambda_elim` — so this exercises a non-`Int` reduction. +#[case::string_addition(r#""a" + "b""#, string())] +// Selecting: `max` returns one of the elements, so a fact every element establishes +// is a fact about the result. +#[case::max_of_identical("max([1, 1])", int_lit(1))] +// And when the elements differ, the element join has already dropped them. +#[case::max_of_differing("max([1, 2])", int())] +// Selecting: a projection returns the field, refinement included. +#[case::projection("(x=1, y=2).x", int_lit(1))] +fn test_operator_result_inherits_a_refinement_only_when_it_selects( + #[case] code: &str, + #[case] expected: Type, +) { + assert_eq!(infer_program(code), expected); +} + +// 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)`, so resolving the operand re-enters the +// resolution computing it and the operand arrives `Arg::Cyclic`. Both rules today +// declare `CycleTolerance::Any`, and these pin what that buys — every shape below is a +// register whose type would be unknowable if a rule refused to answer through a cycle. +// +// The loop-carried accumulator (`for i in …: x := x + i`) is well covered end-to-end in +// `compilation_pipeline::mutability`; what is pinned here is the *typing* of the harder +// shapes, which no test reached: both operands cyclic at once, a cycle routed through a +// user function, mutual recursion between two 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 — the rule answers with no operand type at all to work from. +#[case::self_multiply("x := 2\nx := x * x\nx", "Int")] +#[case::self_subtract("x := 10\nx := x - x\nx", "Int")] +// Nested, so an inner application's result 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 in both operands. +#[case::through_functions( + "def f(a):\n a + 1\ndef g(a):\n a * 2\nx := 0\nx := f(x) + g(x)\nx", + "Int" )] -fn test_lambda_unapplied(#[case] code: &str, #[case] expected: Type) { +#[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 is the operands' shared base and not a hardcoded `Int`. +#[case::string_accumulator("s := \"a\"\ns := s + \"b\"\ns", "String")] +// A **comparison** cycle. `Compare` is constant on its domain, so a cyclic operand costs +// it nothing at all — unlike arithmetic, which loses the agreement check. Nothing else in +// the suite writes one, which is why it is here: the tolerance is a claim about every +// rule, not just the arithmetic ones. +#[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 test_a_register_that_reads_itself_still_gets_a_type(#[case] code: &str, #[case] base: &str) { + assert_eq!(register_value_type(code).to_string(), base); +} + +// Agreement is necessary and **not sufficient**: `"a" * "b"` has operands that agree +// perfectly, and multiplication still has nothing to say about strings. Checking only +// that the operands share a base reported `String` for all three of these. +#[rstest] +#[case::multiply_strings(r#""a" * "b""#, "Mul", "String")] +#[case::subtract_strings(r#""a" - "b""#, "Sub", "String")] +#[case::divide_strings(r#""a" // "b""#, "FloorDiv", "String")] +#[case::add_bools("True + True", "Add", "Bool")] +fn test_an_operation_is_rejected_on_a_base_it_is_not_defined_for( + #[case] code: &str, + #[case] fun: &str, + #[case] base: &str, +) { + let errs = infer_program_err(code); + assert!( + errs.iter().any(|e| matches!( + e, + InferError::UndefinedForBase { fun: f, base: b, .. } if f == fun && b == base + )), + "expected {fun} to be rejected on {base}, got {errs:?}" + ); +} + +// `+` is the one arithmetic operator with a second base: it is string concatenation +// until `lambda_elim` rewrites it to `Concat`, which happens after inference. +#[rstest] +#[case(r#""a" + "b""#, string())] +#[case("1 + 2", int())] +#[case("1 * 2", int())] +#[case("7 // 2", int())] +fn test_an_operation_is_accepted_on_a_base_it_is_defined_for( + #[case] code: &str, + #[case] expected: Type, +) { assert_eq!(infer_program(code), expected); } +// The domain check must survive a **cycle**, and it cannot be left to the frame that +// sees every argument — for `x := "a"; x := x * x` there is no such frame. Traced, every +// reduction of that program sees at least one cyclic operand (`[⟨cyclic⟩, String]` and +// `[String, ⟨cyclic⟩]`, never `[String, String]`), where the same shape over `Int` does +// reach `[Int, Int]`. So the rule judges each *available* operand: a known operand +// outside the operation's domain is a violation whatever the others turn out to be. +#[test] +fn test_a_cycle_does_not_hide_an_undefined_operation() { + let errs = infer_program_err("x := \"a\"\nx := x * x\nx"); + assert!( + errs.iter().any( + |e| matches!(e, InferError::UndefinedForBase { fun, base, .. } + if fun == "Mul" && base == "String") + ), + "a cyclic operand must not hide that Mul is undefined on String, got {errs:?}" + ); +} + +// The cut-off costs the agreement **check**, not the answer — so a disagreement inside a +// cycle must still be caught. It is, though *not* by the reduction rule: for these shapes +// the register's own value join rejects first (`Incompatible lower bounds`), because the +// seed and the write contribute conflicting bases to one variable. Measured: the rule +// never fires on any of them. +#[test] +fn test_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" + ); +} + +// Merging: a collection's element type is the *join* of its elements, so a refinement +// survives only when every element establishes it. This is the rule the singleton made +// load-bearing — a merge point is not one value, it is whichever the runtime supplies. +#[rstest] +#[case("[1, 1]", int_lit(1))] +#[case("[1, 2]", int())] +fn test_collection_element_type_is_the_join(#[case] code: &str, #[case] expected: Type) { + let ty = infer_program(code); + let Type::Fun { codomain, .. } = &ty else { + panic!("expected a collection (function) type, got {ty}"); + }; + assert_eq!(**codomain, expected); +} + #[test] fn test_generic_identity() { // f = \x -> x; f -> Fun(?a, ?b)