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

[dpmills]

Four defects in how Mut is typed, found by probing what the base PR left. None changes the lattice; each is independently reviewable.

• A mismatch named the demand as found — x: Mut(Int) := "s" reported expected String, found Int. constrain_subtype(lhs, rhs) means lhs <: rhs, so the fields are found and expected now, with expected an Option: a missing field and an unaccepted tag are faults in a single type, and had been borrowing the second slot with a Type::Hole that rendered as a bare _.

• A refinement depending on a mutable variable is a rejection, not a compiler bug. x := 2; ys = [i for i in [1, 2, 3] if i < x] tripped the debug-only check_scope_valid, so release builds panicked at the pre-desugar wall instead. It is InferError::MutableInRefinedType now, whose docs record why this is staging — the term that would discharge the binder is minted by mut_elim, passes after closure is demanded. Reporting it needed ExprStmt to propagate the lifted type, which it did not.

• op= inside a loop body is a mutable write. Both loop-lowering paths fell back to a per-iteration shadowing let for a target that was not a pre-loop accumulator, and since op= reads the old value, y = 0; y += i recomputed 0 + i rather than accumulating. Each path now threads the MutWrite or rejects — the op= half of the hole whose := half the base PR closed.

• A mutable variable's value type is invariant across a Mut parameter — now pinned. Narrowing is the unsound direction and nothing tested it. Both directions are rejected today but not by the invariance rule, since the deref arm fires first at an argument position, so Type::History's docs name the two edges that assemble the property instead.

[dpmills]

This change is part of the following stack:

• Freshening asks a different question than type_level, so it needs its own #71
  • SharedHole: let lowering state that two type positions are the same #72
    • Traits: state what an operator requires of its operands, not that they are the same #73
      • Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
        • Annotations stop standing in for binder structure, and stop outliving inference #60
          • Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63 ◀
            • A mutable variable read is an explicit operation, not a subtyping rule #64
              • Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it #62
                • constrain_go asserts the uniquely-keyed invariant it rests on #74
                  • Update the value-Case fan-out's prose to the DisjointJoin it builds #75
                  • Canonicalize each arrow's Pi binder as the solver flattens types #76
                  • Hold a refined type's refinements in one unordered set instead of nested layers #77
                  • Derive a Cast's refinements from its term instead of overwriting the target #78
                  • Add a Lean model of the CCL type system and fuzz the solver against it #79
              • Split transactional commit stores by connected components of transaction blocks #91
                • Build the await_final terminal read as a completion-point sample, and give the as-of read its own term #92
                  • Feed both writers' decision bodies through tiles, retiring WriterBuffer #93
                  • Add an end-to-end walkthrough of mutability, from CHL source to operators #97

_{Change managed by git-spice.}