Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind

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

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>,
-        type_b: Box<Type>,
+        /// The type that flowed in — the `lhs` of the failed `lhs <: rhs`.
+        found: Box<Type>,
+        /// 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<Box<Type>>,
         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 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 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 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 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
+    /// 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 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.
+    ///
+    /// 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 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 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
+        /// 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:?}"
         );

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,28 +176,28 @@ 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!(
                 "{ctx_label} (a compute function ⇒ was supplied where a data \
                  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))),
         },
     }
 }

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 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
+        // 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 {

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