From 6b246267aa11f3a0ac33aa815eb30fd710e6009d Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 5 Aug 2026 10:57:52 -0700 Subject: [PATCH 1/2] Four defects in how `Mut` is typed: message polarity, an unclosable refinement, and `op=` as a rebind MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four defects in how `Mut` is typed, found by reviewing the base PR and probing what it left. Each is independently reviewable; none changes the lattice — that is the follow-up, which this PR pins the ground for. `x: Mut(Int) := "s"` reported *expected String, found Int* — the sides printed the wrong way round. `constrain_subtype(lhs, rhs)` means `lhs <: rhs`, so the left side is the value that flowed in and the right is the demand it failed; `map_constrain_err` stored the value in `type_a` and the formatter printed `expected {type_a}`. The neutral field names are why this survived: nothing about `type_a` / `type_b` says which is which, so the mapping and the formatter could disagree and still read as deliberate. They are `found` and `expected` now. `expected` is an `Option`, because two of the four mismatches do not relate two types at all. A missing record field and an unaccepted variant tag are faults in a *single* type — the `ctx` already says what is wrong with it — and they had been borrowing the second slot with a `Type::Hole`, rendering as a bare `_` on whichever side the formatter put it. Nothing tested it. Narrowing is the unsound direction and the whole reason `Type::History` is invariant in its value: if `Mut({a: Int, b: Int})` could flow into a `Mut({a: Int})` parameter, the callee's `r := (a=5)` would drop a field the caller's declaration still promises, and a later `x.b` would type-check against a value that no longer has it. Worth pinning now because **the invariance rule is not what enforces this today.** At an argument position the deref arm fires first — `Typing::apply` records `arg <: ?d` against a fresh variable, so a register meets an `Infer` and reads through — so the `(History, History)` arm never runs there. Measured: on one pass-by-reference call every argument edge is `Mut(Int, D) <: ?N`, and the 438 invariance firings across the suite are 338 × `Int vs Int` plus 85 × `?N vs ?N`, i.e. already-equal pairs. The property is assembled instead from the application edge (`caller <: callee`) and `contribute_pbr_writes` (`callee <: caller`) — equal in strength to the rule, spread across two mechanisms. Recorded on `Type::History`, with why the obvious narrowing of the rule is a dead end: "invariant only where the value type is declared" cannot be expressed, because declaredness is *provenance*, not a property of a type, and a variance rule sees two types without being able to ask where either came from. `x := 2; ys = [i for i in [1, 2, 3] if i < x]; ys` did not compile — it tripped `check_scope_valid`, whose own doc says it never fires on a well-typed program. That check is `#[cfg(debug_assertions)]`, so a **release** build had no check at all and carried the ill-scoped type to the pre-desugar wall, where it panicked on a surviving mutable type. A comprehension filter's predicate rides the domain type as a refinement, so filtering on a register produces a type that mentions it. A `let` binder can be discharged into the type it is lifted out of, because the binder *is* its bound expression; a register has no such term **at the point closure is demanded** — and that is the whole obstacle. Closure is required during coalesce, while `mut_elim`, several passes later, is what compiles a write-free register into a `let` and a written one into trailing `let x_final = final_or_default(…)` bindings. The naming exists; it arrives too late to discharge with. So this is a **staging** limitation, and the comment records it as scoped work rather than a dead end: let a predicate reference a register through inference (registers are enumerable — `MutDecl` binders and pass-by-reference params), stage the scope invariant across `mut_elim`, and have that pass rewrite reads inside predicate terms as it already does in the term tree. One sub-case stays genuinely hard — a comprehension *inside* the loop that writes the register needs the refinement to depend on the sequencing position, and a predicate rides a type, which carries no position. And it is worth asking first whether a filter belongs in a type at all: it is there as a *planning channel*, not as a proof obligation the way an index-in-range refinement is. It is now reported where the closing would have happened, as `InferError::MutableInRefinedType` — release-visible, with the introduction's source span and the offending predicate. The message says it is a limitation rather than a mistake, and deliberately **offers no workaround**, because the obvious one does not work: reading the register into an immutable and refining on that discharges `[k ↦ x]`, which puts the register's name straight back into the predicate. **The lifted type now follows every spine link.** Getting the `k = x` case to report correctly exposed a second gap: the `Let` arm composes to fixpoint by reading its *body's* already-coalesced type, but `ExprStmt` did not propagate at all, so a discharge below one never reached the binder above it. A register written in a loop puts the `for` between the two, and the `MutDecl` above saw an undischarged `k` instead of the `x` it could report on. Both loop-lowering paths fell back to a per-iteration shadowing `let` when a `x op= e` target was not a pre-loop accumulator. Wrong twice over: the update is discarded at the iteration boundary, and because `op=` reads the old value, each iteration reads the binding's **initial** value. `y = 0; y += i` in a loop body did not accumulate `y`; it recomputed `0 + i` every time. `op=` now has one outcome per path — the `MutWrite` the phase threads, or a rejection. In the generator path that leaves no fallback at all, since nothing in that body is mutable by construction. This is the `op=` half of the hole whose `:=` half the base PR closed. `./ci.sh` green. New tests cover both mismatch directions and the absence of an invented demand; narrowing, widening, and equal-width through a `Mut` parameter; the refinement rejection directly, through a copy, and after writes; and `op=` rejection in both loop paths. --- docs/chl-spec.md | 15 ++- src/ccl/infer/api.rs | 109 +++++++++++++++----- src/ccl/infer/mod.rs | 28 +++--- src/ccl/infer/solve.rs | 28 ++++++ src/ccl/lower/loops.rs | 62 ++++++++---- src/ccl/ty.rs | 16 ++- tests/compilation_pipeline/mutability.rs | 123 +++++++++++++++++++++-- tests/type_check.rs | 49 +++++++++ 8 files changed, 359 insertions(+), 71 deletions(-) diff --git a/docs/chl-spec.md b/docs/chl-spec.md index 6ac25491..e4160de7 100644 --- a/docs/chl-spec.md +++ b/docs/chl-spec.md @@ -1416,10 +1416,17 @@ nested-recurrence case below: > supported: declare it before the loop (`Y := …`) so its updates carry > across iterations, or bind a per-iteration value immutably with `Y = …`` -Falling back to a per-iteration binding is deliberately *not* what happens, -for the reason a plain `=` to an outer name is rejected: it would silently -discard every update at the iteration boundary, which is the one thing `:=` -exists to rule out. +The same holds for `op=`, which is a mutable write and not a rebind: `x += e` +inside a loop body requires `x` to be a mutable variable declared before the +loop. A target that is not gets the matching error rather than a +per-iteration binding. + +Falling back to a per-iteration binding is deliberately *not* what happens in +either case, for the reason a plain `=` to an outer name is rejected: it would +silently discard every update at the iteration boundary, which is the one thing +`:=` exists to rule out. For `op=` it is worse than a lost update — `op=` reads +the old value, so a per-iteration rebind reads the binding's *initial* value on +every iteration. *Currently unsupported* (see §12): nested for-loops with mutable variables, mutable variables introduced inside a loop body or a `with diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index 759dad8b..bfdbc6bc 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -275,14 +275,22 @@ pub enum InferError { UnboundVariable(String), /// A type mismatch was detected between two solved types. /// - /// The two `Type`s are boxed to keep `InferError` under the - /// `result_large_err` budget: this is the widest variant (two `Type`s plus - /// a `ctx` string), and `Type` grew when [`crate::ccl::ty::FunKind`] gained - /// an inference variable. Boxing here keeps every + /// Named for the roles rather than positionally: `constrain_subtype(lhs, rhs)` + /// means `lhs <: rhs`, so the left side is the *value* that flowed in and the + /// right side is the *demand* it failed. Neutral names (`type_a`/`type_b`) are + /// what let the two get printed the wrong way round. + /// Both `Type`s are boxed to keep `InferError` under the `result_large_err` + /// budget: this is the widest variant, and `Type` grew when + /// [`crate::ccl::ty::FunKind`] gained an inference variable. Boxing keeps every /// `Result<_, InferError>` cheap on the common `Ok` path. TypeMismatch { - type_a: Box, - type_b: Box, + /// The type that flowed in — the `lhs` of the failed `lhs <: rhs`. + found: Box, + /// The demand it failed, when there is one. `None` for the mismatches that + /// name a single offending type instead of relating two (a missing record + /// field, an unaccepted variant tag): there is no second type to print, and + /// inventing one is how the message came to read backwards. + expected: Option>, ctx: String, }, /// A product type lacked a field a structural edge required — the violation of @@ -375,6 +383,49 @@ pub enum InferError { /// Display label for the message (see the type docs — not the location). at: String, }, + /// A **type refinement depends on a mutable variable**, where nothing can close + /// it over the register's scope. + /// + /// A `let` binder can be discharged into the type it is lifted out of, because the + /// binder *is* its bound expression. A register has no such term **at this point in + /// compilation**, which is the precise obstacle: closure is demanded during + /// coalesce, and the term that would discharge it does not exist until `mut_elim` + /// several passes later. That pass compiles a write-free register straight into a + /// `let`, and a written one into a history plus trailing + /// `let x_final = final_or_default(…)` bindings — either of which a predicate could + /// name. Nothing about a register makes it unnameable; the naming just happens too + /// late. + /// + /// So this is a **staging limitation reported as a rejection**, not a compiler bug + /// and not an impossibility. Lifting it would mean letting a predicate reference a + /// register through inference (registers are enumerable — `MutDecl` binders and + /// pass-by-reference params), staging the scope invariant across `mut_elim`, and + /// having that pass rewrite reads inside predicate terms as it already does in the + /// term tree. + /// + /// One sub-case is harder and would stay rejected: a comprehension *inside* the loop + /// that writes the register. There "the value of `x`" is per-iteration, so the + /// refinement would have to depend on the sequencing position rather than on a + /// single binding — and a predicate rides a type, which carries no position. + /// + /// Worth asking first whether the filter belongs in a type at all. It is there as a + /// *planning channel* (planning reifies it off `expr.ty.domain()`), not as a proof + /// obligation the way an index-in-range refinement is; a filter that reached + /// planning as a term would never raise this. + /// + /// There is no surface workaround today: reading the register into an immutable + /// first (`k = x`) does not help, because discharging `[k ↦ x]` puts the register's + /// name straight back into the predicate. Reported here so the program is rejected + /// with its source position instead of tripping the debug-only scope net (and, in + /// release, surviving to panic at the pre-desugar wall). + MutableInRefinedType { + /// The register's name. + name: String, + /// The refinement-bearing type that mentions it. Carries the offending + /// predicate, which is the informative part — the blame span already points + /// at the introduction, so the node is not rendered as well. + ty: Type, + }, /// A node's coalesced type references a term binder that is not in scope /// at that node — a violation of the scope-validity invariant (design /// §6.2). Like [`InferError::UnresolvedHole`], treat as a compiler bug @@ -531,19 +582,24 @@ impl std::fmt::Debug for InferError { InferError::UnboundVariable(name) => write!(f, "Unbound variable: '{}'", name), InferError::TypeMismatch { ctx, - type_a, - type_b, - } => { - write!( - f, - "Type mismatch for {}: expected {}, found {}", - ctx, type_a, type_b - )?; - if let Some(hint) = product_keying_hint(type_a, type_b) { - write!(f, "\n {hint}")?; + found, + expected, + } => match expected { + // Both sides known: name the demand, then the value that failed it. + Some(expected) => { + write!( + f, + "Type mismatch for {ctx}: expected {expected}, found {found}" + )?; + if let Some(hint) = product_keying_hint(expected, found) { + write!(f, "\n {hint}")?; + } + Ok(()) } - Ok(()) - } + // A one-sided violation (`ExtraTag`): the `ctx` says what is wrong and + // there is no second type the demand could be. + None => write!(f, "Type mismatch for {ctx}: found {found}"), + }, InferError::NoTraitInstance { trait_, position, @@ -616,6 +672,15 @@ impl std::fmt::Debug for InferError { InferError::UnresolvedPartial { kind, at } => { write!(f, "Unresolved partial {kind} in expression: {at}") } + InferError::MutableInRefinedType { name, ty } => { + write!( + f, + "a type refinement here depends on the mutable variable `{name}`: \ + {ty}. A mutable variable has no single value for a type to refer \ + to, so a type cannot depend on one — a limitation, not a mistake \ + in the program." + ) + } InferError::ScopeViolation { at, ty, unbound } => { write!( f, @@ -2086,11 +2151,9 @@ mod tests { assert!( errs.iter().any(|e| matches!( e, - InferError::TypeMismatch { type_a, type_b, .. } - if matches!( - (type_a.as_ref(), type_b.as_ref()), - (Type::Base(BaseType::Int), Type::Base(BaseType::String)) - ) + InferError::TypeMismatch { found, expected, .. } + if **found == Type::Base(BaseType::Int) + && expected.as_deref() == Some(&Type::Base(BaseType::String)) )), "expected TypeMismatch Int/String, got {errs:?}" ); diff --git a/src/ccl/infer/mod.rs b/src/ccl/infer/mod.rs index 9e72bf88..ded0edd0 100644 --- a/src/ccl/infer/mod.rs +++ b/src/ccl/infer/mod.rs @@ -166,8 +166,8 @@ pub(super) fn map_constrain_err(err: ConstrainError, ctx_label: &str) -> InferEr } else { InferError::TypeMismatch { ctx: ctx_label.to_string(), - type_a: Box::new(lhs_ty), - type_b: Box::new(rhs_ty), + found: Box::new(lhs_ty), + expected: Some(Box::new(rhs_ty)), } } } @@ -176,19 +176,19 @@ pub(super) fn map_constrain_err(err: ConstrainError, ctx_label: &str) -> InferEr found: coalesce_for_error(&in_type), at: ctx_label.to_string(), }, - // `ExtraTag` is `MissingField`'s dual and has the same shape problem — the - // width violation is a *tag set*, not a second type, so `type_b` is filled - // with a placeholder. Naming it as its own variant is the same fix, and is - // left to whoever next works the variant diagnostics. + // `ExtraTag` is `MissingField`'s dual: the width violation is a *tag set*, + // not a second type, so there is no demand to report and `expected` is + // `None`. Giving it its own variant — as `MissingField` now has — is the + // better fix, and is left to whoever next works the variant diagnostics. ConstrainError::ExtraTag { tag, in_type } => InferError::TypeMismatch { ctx: format!("{ctx_label} (variant tag .{tag} not accepted)"), - type_a: Box::new(coalesce_for_error(&in_type)), - type_b: Box::new(Type::Hole), + found: Box::new(coalesce_for_error(&in_type)), + expected: None, }, ConstrainError::NotAFeed { found, required } => InferError::TypeMismatch { ctx: format!("{ctx_label} (a feed handle is required here, but the value is not one)"), - type_a: Box::new(coalesce_for_error(&found)), - type_b: Box::new(coalesce_for_error(&required)), + found: Box::new(coalesce_for_error(&found)), + expected: Some(Box::new(coalesce_for_error(&required))), }, ConstrainError::ComputeWhereDataRequired { lhs, rhs } => InferError::TypeMismatch { ctx: format!( @@ -196,8 +196,8 @@ pub(super) fn map_constrain_err(err: ConstrainError, ctx_label: &str) -> InferEr collection ⤇ is required — using a capability as a collection \ would iterate a declared domain the value does not cover)" ), - type_a: Box::new(coalesce_for_error(&lhs)), - type_b: Box::new(coalesce_for_error(&rhs)), + found: Box::new(coalesce_for_error(&lhs)), + expected: Some(Box::new(coalesce_for_error(&rhs))), }, ConstrainError::NoTraitInstance { trait_, @@ -218,8 +218,8 @@ pub(super) fn map_constrain_err(err: ConstrainError, ctx_label: &str) -> InferEr domains have no common data-function type, and their lossless join is \ a dependent sum over the candidate domains)" ), - type_a: Box::new(coalesce_for_error(&lhs)), - type_b: Box::new(coalesce_for_error(&rhs)), + found: Box::new(coalesce_for_error(&lhs)), + expected: Some(Box::new(coalesce_for_error(&rhs))), }, } } diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index d9a62d62..c529e920 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1211,6 +1211,34 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { Some(body.ty.clone()) } } + // An effect statement carries its continuation's type, so the lifted type has + // to follow it too: without this the chain breaks at every `ExprStmt`, and a + // discharge performed by a `let` below one never reaches the binder above it. + // (The `Let` arm above composes to fixpoint precisely because it reads its + // *body's* already-coalesced type; a spine link that does not propagate is a + // hole in that composition.) + TypedExprNode::ExprStmt { body, .. } => Some(body.ty.clone()), + // A register introduction lifts its body's type the same way, but has no + // discharge available *here*: the term that names a register's value is minted + // by `mut_elim`, several passes after closure is demanded. So a refinement that + // mentions the binder cannot be closed at this point, and the program is + // rejected with a source position rather than left to trip the debug-only scope + // net or, in release, to reach the pre-desugar wall as a surviving mutable type. + // Why that is staging rather than impossibility, and what lifting it would take: + // see `InferError::MutableInRefinedType`. + TypedExprNode::MutDecl { binding, body, .. } => { + if crate::ccl::subst::type_free_vars(&body.ty).contains(&binding.name) { + let label = format!("mutable `{}`", binding.name); + ctx.push_error( + InferError::MutableInRefinedType { + name: binding.name.base().to_string(), + ty: body.ty.clone(), + }, + label, + ); + } + Some(body.ty.clone()) + } _ => None, }; if let Some(closed) = let_closed { diff --git a/src/ccl/lower/loops.rs b/src/ccl/lower/loops.rs index 8685f604..fe6117da 100644 --- a/src/ccl/lower/loops.rs +++ b/src/ccl/lower/loops.rs @@ -281,6 +281,26 @@ fn in_loop_mut_var_error(span: Span, name: &str) -> LoweringError { ) } +/// Rejection for `x op= e` inside a for-loop body where `x` is not a mutable +/// variable declared before the loop. +/// +/// `op=` is a mutable write and the spec says so — *a `+=` to an immutable binding is +/// a type error, not a silent rebind*. The fallback this replaces was a per-iteration +/// shadowing `let`, which is wrong twice over: the update is discarded at the +/// iteration boundary, and because `op=` reads the old value, each iteration reads the +/// binding's *initial* value rather than the running one. +fn in_loop_aug_assign_error(span: Span, name: &str) -> LoweringError { + LoweringError::unsupported( + span, + format!( + "`{name}` is not a mutable variable, so `{name} op= …` inside a for-loop \ + body cannot accumulate into it: declare it before the loop with \ + `{name} := …` so its updates carry across iterations, or compute a \ + per-iteration value with `{name} = …`" + ), + ) +} + /// `frame_introduced` — names introduced by the current for clause (the /// iteration variable) and any let-bindings accumulated so far. These may /// be re-bound (shadowed) inside the body without triggering a mutation error. @@ -332,24 +352,20 @@ fn lower_for_body_stmts( frame_introduced.insert(name.clone()); bindings.push((name, val, Some(ann), stmt.span)); } - ChlStmt::AugAssign { target, op, value } => { + ChlStmt::AugAssign { target, .. } => { let name = extract_name_target(target, "augmented assignment")?; if mutation_scope.contains(&name) { return Err(outer_binding_write_error(stmt.span, &name)); } - if !frame_introduced.contains(&name) { - // x op= e is only valid if x was already introduced in this frame. - return Err(LoweringError::unsupported( - stmt.span, - format!( - "augmented assignment to `{name}` in for-loop body: \ - `{name}` is not bound in this body. Use `{name} = expr` \ - for a fresh binding.", - ), - )); - } - let val = lower_aug_binop(&name, *op, value, stmt.span, ctx)?; - bindings.push((name, val, None, stmt.span)); + // `op=` is a mutable write, and nothing in this body is mutable: an + // outer-scope target was rejected above, and everything `frame_introduced` + // holds was bound immutably by `=` (or is the iteration variable). + // Rebinding it per iteration is what the spec forbids by name — the + // update is discarded at the boundary, and since `op=` reads the old + // value, each iteration would read the *initial* one. This path has no + // accumulators by construction: a loop with loop-carried writes routes + // to `lower_direct_mirror_loop` instead. + return Err(in_loop_aug_assign_error(stmt.span, &name)); } ChlStmt::Define { .. } => { return Err(LoweringError::unsupported( @@ -800,16 +816,22 @@ fn lower_loop_body_chain( let val = lower_expr(value, ctx)?; ctx.tag_image(Expr::let_bind(name, val, chain), stmt.span) } + // `x op= value` — a mutable write, always. A write to an accumulator + // declared before the loop is the `MutWrite` the phase threads as the + // recurrence; `op=` on anything else is a write to a non-mutable, which + // is a type error and not a rebind. It cannot fall back to a shadowing + // `let` for the same reason `:=` cannot: the update would be discarded + // at the iteration boundary, and `op=` reads the old value, so a + // per-iteration rebind reads the *seed* every time. ChlStmt::AugAssign { target, op, value } => { let name = extract_name_target(target, "augmented assignment")?; + if !acc_names.contains(&name) { + return Err(in_loop_aug_assign_error(stmt.span, &name)); + } check_mut_write_context(&name, stmt.span, ctx)?; let val = lower_aug_binop(&name, *op, value, stmt.span, ctx)?; - if acc_names.contains(&name) { - let write = ctx.tag_image(Expr::mut_write(name, val), stmt.span); - ctx.tag_image(Expr::expr_stmt(write, chain), stmt.span) - } else { - ctx.tag_image(Expr::let_bind(name, val, chain), stmt.span) - } + let write = ctx.tag_image(Expr::mut_write(name, val), stmt.span); + ctx.tag_image(Expr::expr_stmt(write, chain), stmt.span) } // `x := value` — a write to an accumulator declared before the // loop, lowered to the `MutWrite` the phase threads as the diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index a744ce91..215e7ac4 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -647,7 +647,21 @@ pub enum Type { /// write edge reads as a demand *on* the writes rather than a contribution /// *to* them: without it, passing a `Mut({a: Int, b: Int})` mutable variable to a /// parameter declared `Mut({a: Int})` would let the callee's `r := (a=5)` - /// drop a field the caller's declaration requires. + /// drop a field the caller's declaration requires. That cannot be narrowed to + /// "invariant only where the value type is declared", because *declaredness is + /// provenance, not a property of a type*: a variance rule sees two types and + /// cannot ask where either came from. + /// + /// **The rule is not what currently enforces that across a function boundary.** + /// At an argument position the deref arm fires first — `Typing::apply` records + /// `arg <: ?d` against a fresh variable, so a register meets an `Infer` and reads + /// through — so the `(History, History)` arm never runs there. Invariance at a + /// pass-by-reference call is assembled from two other edges instead: the + /// application edge supplies `caller <: callee`, and `emit::contribute_pbr_writes` + /// supplies `callee <: caller`. Equal in strength to the rule, spread across two + /// mechanisms — which is why the property is pinned by test + /// (`a_registers_value_type_is_invariant_across_a_mut_parameter`) rather than + /// argued from this paragraph. /// /// It is also a **transient** variant like `Hole` / `Infer`: it exists only between type /// inference (which stamps it on `:=` / `defer` introductions and every diff --git a/tests/compilation_pipeline/mutability.rs b/tests/compilation_pipeline/mutability.rs index b5540a01..ce9e8f82 100644 --- a/tests/compilation_pipeline/mutability.rs +++ b/tests/compilation_pipeline/mutability.rs @@ -642,27 +642,51 @@ fn mut_annotation_with_non_txn_domain_rejected() { /// boundary, the very thing `:=` exists to avoid. #[rstest] #[case::annotated_mut(indoc! {r#" + t := 0 for i in [1, 2, 3]: - y: Mut(Int) := 0 - y += i - y + y: Mut(Int) := i + t += y + t "#})] #[case::annotated_value(indoc! {r#" + t := 0 for i in [1, 2, 3]: - y: Int := 0 - y += i - y + y: Int := i + t += y + t "#})] #[case::bare(indoc! {r#" + t := 0 for i in [1, 2, 3]: - y := 0 - y += i - y + y := i + t += y + t "#})] fn mut_var_declared_inside_loop_rejected(#[case] code: &str) { expect_compile_error(code, "introduced inside a for-loop body"); } +/// `op=` inside a for-loop body is a **mutable write**, so a target that is not a +/// mutable variable declared before the loop is a type error rather than a rebind — +/// the spec's *"a `+=` to an immutable binding is a type error, not a silent +/// rebind"*. +/// +/// The fallback this replaces was a per-iteration shadowing `let`, wrong twice over: +/// the update is discarded at the iteration boundary, and since `op=` reads the old +/// value, each iteration read the binding's *initial* value rather than the running +/// one. It is the `op=` half of the same hole the `:=` rejection above closes. +#[rstest] +#[case::body_local("t := 0\nfor i in [1, 2, 3]:\n y = 0\n y += i\n t += y\nt")] +#[case::iteration_variable("t := 0\nfor i in [1, 2, 3]:\n i += 1\n t += i\nt")] +// The generator path (a `yield` body with no loop-carried writes) reaches its own +// statement lowering, and had the same fallback. +#[case::generator_body( + "def g(xs):\n for x in xs:\n y = 0\n y += x\n yield y\ng([1, 2, 3])" +)] +fn aug_assign_to_a_non_mutable_inside_a_loop_is_rejected(#[case] code: &str) { + expect_compile_error(code, "is not a mutable variable"); +} + /// The immutable counterpart still works, and is what the rejection above points /// at: a per-iteration value binds with `=`. #[test] @@ -740,6 +764,87 @@ fn writing_through_a_value_copy_of_a_mutable_is_rejected() { ); } +/// A register's **value type is invariant** across a pass-by-reference boundary: +/// the callee's declared value type may be neither narrower nor wider than the +/// caller's register. +/// +/// Narrowing is the unsound direction and the reason invariance exists. If +/// `Mut({a: Int, b: Int})` could flow into a `Mut({a: Int})` parameter, the callee's +/// `r := (a=5)` would drop a field the caller's declaration still promises, and the +/// caller's later `x.b` would type-check against a value that no longer has it. +/// +/// Both directions are rejected today, but *not* by one rule. At an argument position +/// the deref coercion fires first — `apply` records `arg <: ?d` against a fresh +/// variable, so a register meets an `Infer` and reads through — which means the +/// `(History, History)` invariance rule never runs there. Narrowing is caught instead +/// by the write contribution (`emit::contribute_pbr_writes`, `param_value <: +/// arg_value`) and widening by the ordinary application edge. These tests pin the +/// *property* so that consolidating those mechanisms cannot quietly drop it. +#[test] +fn a_registers_value_type_is_invariant_across_a_mut_parameter() { + // Narrowing: the callee would drop `b`, and the diagnostic names that field — + // `.b` is the whole of what makes this unsound, so it is a sharper needle than + // the kind of error it happens to be reported as. + expect_compile_error( + "def narrow(r: Mut({a: Int})):\n r := (a=5)\n\ + x: Mut({a: Int, b: Int}) := (a=1, b=2)\nfor i in [1]:\n narrow(x)\nx.b", + ".b", + ); + // Widening: the callee would demand a field the register does not have — again + // `.b`, from the other side. + expect_compile_error( + "def wide(r: Mut({a: Int, b: Int})):\n r := (a=5, b=6)\n\ + x: Mut({a: Int}) := (a=1)\nfor i in [1]:\n wide(x)\nx.a", + ".b", + ); +} + +/// The equal-width case still works, which is what makes the two rejections above a +/// statement about *variance* rather than about pass-by-reference being broken. +#[test] +fn an_equal_width_mut_parameter_still_accepts_a_register() { + check_scalar( + "def bump(r: Mut(Int)):\n r += 1\nx: Mut(Int) := 0\nfor i in [1, 2, 3]:\n bump(x)\nx", + cambra::interpreter::Value::Int(3), + ); +} + +/// A type refinement cannot depend on a mutable variable — a **staging** limitation, +/// deliberately reported rather than worked around. +/// +/// A comprehension filter's predicate rides the domain type as a refinement, so +/// filtering on a register produces a type mentioning it. A `let` binder can be +/// discharged into the type it is lifted out of, because the binder *is* its bound +/// expression; a register has no such term *at the point closure is demanded*. That is +/// the whole obstacle: closure is required during coalesce, and `mut_elim` — several +/// passes later — is what compiles a write-free register into a `let` and a written one +/// into trailing `let x_final = final_or_default(…)` bindings. The naming exists; it +/// just arrives too late to discharge with. +/// +/// Lifting it is scoped rather than impossible (see +/// [`InferError::MutableInRefinedType`](cambra::ccl::infer::InferError)), with one +/// genuinely hard sub-case left over: a comprehension inside the loop that writes the +/// register, where the value is per-iteration and a predicate — riding a type — has no +/// position to depend on. +/// +/// Reading it into an immutable first does **not** help today, which is why the message +/// offers no workaround: discharging `[k ↦ x]` puts the register's name straight back +/// into the predicate. +/// +/// Before this was reported here it tripped `check_scope_valid`, a debug-only +/// regression net documented as never firing on a well-typed program — so a *release* +/// build had no check at all and reached the pre-desugar wall with a surviving mutable +/// type. +#[rstest] +#[case::direct("x := 2\nys = [i for i in [1, 2, 3] if i < x]\nys")] +#[case::through_a_copy("x := 2\nk = x\nys = [i for i in [1, 2, 3] if i < k]\nys")] +#[case::after_writes( + "x := 0\nfor i in [1, 2]:\n x += i\nk = x\nys = [j for j in [1, 2, 3] if j < k]\nys" +)] +fn a_refinement_cannot_depend_on_a_mutable(#[case] code: &str) { + expect_compile_error(code, "depends on the mutable variable"); +} + /// Rule 2: a function may not return a `Mut` — the mutable-variable reference would /// escape where its writer set is no longer statically known. #[test] diff --git a/tests/type_check.rs b/tests/type_check.rs index cca18379..882ba26b 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -2382,3 +2382,52 @@ mod binder_slot_records_the_bound_at_type { assert!(out.is_empty(), "annotations survived inference: {out:?}"); } } + +/// A mismatch names the demand as `expected` and the value as `found`, in that +/// direction. +/// +/// `constrain_subtype(lhs, rhs)` means `lhs <: rhs`, so the left side is the value +/// that flowed in and the right side is the demand it failed. The two were printed +/// the wrong way round — `x: Mut(Int) := "s"` reported *expected String, found Int* +/// — which the neutral field names `type_a`/`type_b` made easy to miss. +#[test] +fn a_mismatch_names_the_demand_as_expected() { + let rendered = |code: &str| format!("{:?}", infer_program_err(code)); + + // A register's seed: the bound/annotation is the demand, the seed is the value. + let seed = rendered("x: Mut(Int) := \"s\"\nx"); + assert!( + seed.contains("expected Int, found String"), + "the annotation is the demand and the seed is the value, got: {seed}" + ); + + // An argument against a declared parameter, the same way round. + let arg = rendered("def f(a: Int):\n a\nf(\"x\")"); + assert!( + arg.contains("expected Int, found String"), + "the parameter is the demand and the argument is the value, got: {arg}" + ); +} + +/// A mismatch that names *one* offending type prints only that type. +/// +/// A missing field and an unaccepted variant tag are faults in a single type, not a +/// relation between two, so there is no demand to name. They previously borrowed the +/// second slot with a `Type::Hole`, which rendered as a bare `_` on whichever side +/// the formatter happened to put it. +/// +/// A missing field now has its own `InferError::MissingField`, so it states the fault +/// in its own words; what is pinned here is the property both share — no invented +/// demand — rather than either one's wording. +#[test] +fn a_single_type_fault_prints_no_demand() { + let missing = format!("{:?}", infer_program_err("r = (a=1)\nr.b")); + assert!( + missing.contains(".b") && missing.contains("{a: 1}"), + "expected a fault naming the absent field and the record, got: {missing}" + ); + assert!( + !missing.contains("expected _") && !missing.contains("found _"), + "a single-type fault must not invent a demand, got: {missing}" + ); +} From f648152a9e9281840542caeee9d932c91a2d480a Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Thu, 13 Aug 2026 11:58:36 -0700 Subject: [PATCH 2/2] Tests: embedded programs read as programs, not as escaped newlines Every program this branch adds with `\n` becomes an `indoc!` block, per `CLAUDE.md`. --- src/ccl/infer/api.rs | 18 ++--- src/ccl/infer/solve.rs | 4 +- src/ccl/ty.rs | 4 +- tests/compilation_pipeline/mutability.rs | 99 ++++++++++++++++++------ tests/type_check.rs | 21 ++++- 5 files changed, 107 insertions(+), 39 deletions(-) diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index bfdbc6bc..7db70c4b 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -384,27 +384,27 @@ pub enum InferError { at: String, }, /// A **type refinement depends on a mutable variable**, where nothing can close - /// it over the register's scope. + /// it over the mutable variable's scope. /// /// A `let` binder can be discharged into the type it is lifted out of, because the - /// binder *is* its bound expression. A register has no such term **at this point in + /// binder *is* its bound expression. A mutable variable has no such term **at this point in /// compilation**, which is the precise obstacle: closure is demanded during /// coalesce, and the term that would discharge it does not exist until `mut_elim` - /// several passes later. That pass compiles a write-free register straight into a + /// several passes later. That pass compiles a write-free mutable variable straight into a /// `let`, and a written one into a history plus trailing /// `let x_final = final_or_default(…)` bindings — either of which a predicate could - /// name. Nothing about a register makes it unnameable; the naming just happens too + /// name. Nothing about a mutable variable makes it unnameable; the naming just happens too /// late. /// /// So this is a **staging limitation reported as a rejection**, not a compiler bug /// and not an impossibility. Lifting it would mean letting a predicate reference a - /// register through inference (registers are enumerable — `MutDecl` binders and + /// mutable variable through inference (mutable variables are enumerable — `MutDecl` binders and /// pass-by-reference params), staging the scope invariant across `mut_elim`, and /// having that pass rewrite reads inside predicate terms as it already does in the /// term tree. /// /// One sub-case is harder and would stay rejected: a comprehension *inside* the loop - /// that writes the register. There "the value of `x`" is per-iteration, so the + /// that writes the mutable variable. There "the value of `x`" is per-iteration, so the /// refinement would have to depend on the sequencing position rather than on a /// single binding — and a predicate rides a type, which carries no position. /// @@ -413,13 +413,13 @@ pub enum InferError { /// obligation the way an index-in-range refinement is; a filter that reached /// planning as a term would never raise this. /// - /// There is no surface workaround today: reading the register into an immutable - /// first (`k = x`) does not help, because discharging `[k ↦ x]` puts the register's + /// There is no surface workaround today: reading the mutable variable into an immutable + /// first (`k = x`) does not help, because discharging `[k ↦ x]` puts the mutable variable's /// name straight back into the predicate. Reported here so the program is rejected /// with its source position instead of tripping the debug-only scope net (and, in /// release, surviving to panic at the pre-desugar wall). MutableInRefinedType { - /// The register's name. + /// The mutable variable's name. name: String, /// The refinement-bearing type that mentions it. Carries the offending /// predicate, which is the informative part — the blame span already points diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index c529e920..4aca3623 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1218,8 +1218,8 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { // *body's* already-coalesced type; a spine link that does not propagate is a // hole in that composition.) TypedExprNode::ExprStmt { body, .. } => Some(body.ty.clone()), - // A register introduction lifts its body's type the same way, but has no - // discharge available *here*: the term that names a register's value is minted + // A mutable variable introduction lifts its body's type the same way, but has no + // discharge available *here*: the term that names a mutable variable's value is minted // by `mut_elim`, several passes after closure is demanded. So a refinement that // mentions the binder cannot be closed at this point, and the program is // rejected with a source position rather than left to trip the debug-only scope diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index 215e7ac4..c50f4bb0 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -654,13 +654,13 @@ pub enum Type { /// /// **The rule is not what currently enforces that across a function boundary.** /// At an argument position the deref arm fires first — `Typing::apply` records - /// `arg <: ?d` against a fresh variable, so a register meets an `Infer` and reads + /// `arg <: ?d` against a fresh variable, so a mutable variable meets an `Infer` and reads /// through — so the `(History, History)` arm never runs there. Invariance at a /// pass-by-reference call is assembled from two other edges instead: the /// application edge supplies `caller <: callee`, and `emit::contribute_pbr_writes` /// supplies `callee <: caller`. Equal in strength to the rule, spread across two /// mechanisms — which is why the property is pinned by test - /// (`a_registers_value_type_is_invariant_across_a_mut_parameter`) rather than + /// (`a_mut_vars_value_type_is_invariant_across_a_mut_parameter`) rather than /// argued from this paragraph. /// /// It is also a **transient** variant like `Hole` / `Infer`: it exists only between type diff --git a/tests/compilation_pipeline/mutability.rs b/tests/compilation_pipeline/mutability.rs index ce9e8f82..1618881d 100644 --- a/tests/compilation_pipeline/mutability.rs +++ b/tests/compilation_pipeline/mutability.rs @@ -676,12 +676,32 @@ fn mut_var_declared_inside_loop_rejected(#[case] code: &str) { /// value, each iteration read the binding's *initial* value rather than the running /// one. It is the `op=` half of the same hole the `:=` rejection above closes. #[rstest] -#[case::body_local("t := 0\nfor i in [1, 2, 3]:\n y = 0\n y += i\n t += y\nt")] -#[case::iteration_variable("t := 0\nfor i in [1, 2, 3]:\n i += 1\n t += i\nt")] +#[case::body_local(indoc! {r#" + t := 0 + for i in [1, 2, 3]: + y = 0 + y += i + t += y + t +"#})] +#[case::iteration_variable(indoc! {r#" + t := 0 + for i in [1, 2, 3]: + i += 1 + t += i + t +"#})] // The generator path (a `yield` body with no loop-carried writes) reaches its own // statement lowering, and had the same fallback. #[case::generator_body( - "def g(xs):\n for x in xs:\n y = 0\n y += x\n yield y\ng([1, 2, 3])" + indoc! {r#" + def g(xs): + for x in xs: + y = 0 + y += x + yield y + g([1, 2, 3]) + "#} )] fn aug_assign_to_a_non_mutable_inside_a_loop_is_rejected(#[case] code: &str) { expect_compile_error(code, "is not a mutable variable"); @@ -764,9 +784,9 @@ fn writing_through_a_value_copy_of_a_mutable_is_rejected() { ); } -/// A register's **value type is invariant** across a pass-by-reference boundary: +/// A mutable variable's **value type is invariant** across a pass-by-reference boundary: /// the callee's declared value type may be neither narrower nor wider than the -/// caller's register. +/// caller's mutable variable. /// /// Narrowing is the unsound direction and the reason invariance exists. If /// `Mut({a: Int, b: Int})` could flow into a `Mut({a: Int})` parameter, the callee's @@ -775,26 +795,38 @@ fn writing_through_a_value_copy_of_a_mutable_is_rejected() { /// /// Both directions are rejected today, but *not* by one rule. At an argument position /// the deref coercion fires first — `apply` records `arg <: ?d` against a fresh -/// variable, so a register meets an `Infer` and reads through — which means the +/// variable, so a mutable variable meets an `Infer` and reads through — which means the /// `(History, History)` invariance rule never runs there. Narrowing is caught instead /// by the write contribution (`emit::contribute_pbr_writes`, `param_value <: /// arg_value`) and widening by the ordinary application edge. These tests pin the /// *property* so that consolidating those mechanisms cannot quietly drop it. #[test] -fn a_registers_value_type_is_invariant_across_a_mut_parameter() { +fn a_mut_vars_value_type_is_invariant_across_a_mut_parameter() { // Narrowing: the callee would drop `b`, and the diagnostic names that field — // `.b` is the whole of what makes this unsound, so it is a sharper needle than // the kind of error it happens to be reported as. expect_compile_error( - "def narrow(r: Mut({a: Int})):\n r := (a=5)\n\ - x: Mut({a: Int, b: Int}) := (a=1, b=2)\nfor i in [1]:\n narrow(x)\nx.b", + indoc! {r#" + def narrow(r: Mut({a: Int})): + r := (a=5) + x: Mut({a: Int, b: Int}) := (a=1, b=2) + for i in [1]: + narrow(x) + x.b + "#}, ".b", ); - // Widening: the callee would demand a field the register does not have — again + // Widening: the callee would demand a field the mutable variable does not have — again // `.b`, from the other side. expect_compile_error( - "def wide(r: Mut({a: Int, b: Int})):\n r := (a=5, b=6)\n\ - x: Mut({a: Int}) := (a=1)\nfor i in [1]:\n wide(x)\nx.a", + indoc! {r#" + def wide(r: Mut({a: Int, b: Int})): + r := (a=5, b=6) + x: Mut({a: Int}) := (a=1) + for i in [1]: + wide(x) + x.a + "#}, ".b", ); } @@ -802,9 +834,16 @@ fn a_registers_value_type_is_invariant_across_a_mut_parameter() { /// The equal-width case still works, which is what makes the two rejections above a /// statement about *variance* rather than about pass-by-reference being broken. #[test] -fn an_equal_width_mut_parameter_still_accepts_a_register() { +fn an_equal_width_mut_parameter_still_accepts_a_mut_var() { check_scalar( - "def bump(r: Mut(Int)):\n r += 1\nx: Mut(Int) := 0\nfor i in [1, 2, 3]:\n bump(x)\nx", + indoc! {r#" + def bump(r: Mut(Int)): + r += 1 + x: Mut(Int) := 0 + for i in [1, 2, 3]: + bump(x) + x + "#}, cambra::interpreter::Value::Int(3), ); } @@ -813,22 +852,22 @@ fn an_equal_width_mut_parameter_still_accepts_a_register() { /// deliberately reported rather than worked around. /// /// A comprehension filter's predicate rides the domain type as a refinement, so -/// filtering on a register produces a type mentioning it. A `let` binder can be +/// filtering on a mutable variable produces a type mentioning it. A `let` binder can be /// discharged into the type it is lifted out of, because the binder *is* its bound -/// expression; a register has no such term *at the point closure is demanded*. That is +/// expression; a mutable variable has no such term *at the point closure is demanded*. That is /// the whole obstacle: closure is required during coalesce, and `mut_elim` — several -/// passes later — is what compiles a write-free register into a `let` and a written one +/// passes later — is what compiles a write-free mutable variable into a `let` and a written one /// into trailing `let x_final = final_or_default(…)` bindings. The naming exists; it /// just arrives too late to discharge with. /// /// Lifting it is scoped rather than impossible (see /// [`InferError::MutableInRefinedType`](cambra::ccl::infer::InferError)), with one /// genuinely hard sub-case left over: a comprehension inside the loop that writes the -/// register, where the value is per-iteration and a predicate — riding a type — has no +/// mutable variable, where the value is per-iteration and a predicate — riding a type — has no /// position to depend on. /// /// Reading it into an immutable first does **not** help today, which is why the message -/// offers no workaround: discharging `[k ↦ x]` puts the register's name straight back +/// offers no workaround: discharging `[k ↦ x]` puts the mutable variable's name straight back /// into the predicate. /// /// Before this was reported here it tripped `check_scope_valid`, a debug-only @@ -836,10 +875,26 @@ fn an_equal_width_mut_parameter_still_accepts_a_register() { /// build had no check at all and reached the pre-desugar wall with a surviving mutable /// type. #[rstest] -#[case::direct("x := 2\nys = [i for i in [1, 2, 3] if i < x]\nys")] -#[case::through_a_copy("x := 2\nk = x\nys = [i for i in [1, 2, 3] if i < k]\nys")] +#[case::direct(indoc! {r#" + x := 2 + ys = [i for i in [1, 2, 3] if i < x] + ys +"#})] +#[case::through_a_copy(indoc! {r#" + x := 2 + k = x + ys = [i for i in [1, 2, 3] if i < k] + ys +"#})] #[case::after_writes( - "x := 0\nfor i in [1, 2]:\n x += i\nk = x\nys = [j for j in [1, 2, 3] if j < k]\nys" + indoc! {r#" + x := 0 + for i in [1, 2]: + x += i + k = x + ys = [j for j in [1, 2, 3] if j < k] + ys + "#} )] fn a_refinement_cannot_depend_on_a_mutable(#[case] code: &str) { expect_compile_error(code, "depends on the mutable variable"); diff --git a/tests/type_check.rs b/tests/type_check.rs index 882ba26b..6a9c267a 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -2394,15 +2394,22 @@ mod binder_slot_records_the_bound_at_type { fn a_mismatch_names_the_demand_as_expected() { let rendered = |code: &str| format!("{:?}", infer_program_err(code)); - // A register's seed: the bound/annotation is the demand, the seed is the value. - let seed = rendered("x: Mut(Int) := \"s\"\nx"); + // A mutable variable's seed: the bound/annotation is the demand, the seed is the value. + let seed = rendered(indoc! {r#" + x: Mut(Int) := "s" + x + "#}); assert!( seed.contains("expected Int, found String"), "the annotation is the demand and the seed is the value, got: {seed}" ); // An argument against a declared parameter, the same way round. - let arg = rendered("def f(a: Int):\n a\nf(\"x\")"); + let arg = rendered(indoc! {r#" + def f(a: Int): + a + f("x") + "#}); assert!( arg.contains("expected Int, found String"), "the parameter is the demand and the argument is the value, got: {arg}" @@ -2421,7 +2428,13 @@ fn a_mismatch_names_the_demand_as_expected() { /// demand — rather than either one's wording. #[test] fn a_single_type_fault_prints_no_demand() { - let missing = format!("{:?}", infer_program_err("r = (a=1)\nr.b")); + let missing = format!( + "{:?}", + infer_program_err(indoc! {r#" + r = (a=1) + r.b + "#}) + ); assert!( missing.contains(".b") && missing.contains("{a: 1}"), "expected a fault naming the absent field and the record, got: {missing}"