Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base

[dpmills]

A mutable variable could not keep a refinement that every one of its contributions establishes. The three contribution sites — MutWrite, a mutable binding's initializer, and a Transact key's seed — stripped refinements at emit, and two later checks read a refined variable as drift. The strip was compensating for an incomplete join: a write reaching a mutable variable through a Mut parameter never contributed to it at all. This records that contribution, deletes all three strips, and fixes both checks, so x := 5 with no other writes types as Mut(5) and reads as 5, while x := 0 written only through a Mut(Int) parameter joins to Int instead of being rejected against that parameter.

The missing contribution

Typing::apply records arg <: d against a fresh variable, so a Mut argument meets an Infer and takes the deliberate deref arm — right for a bare read like cnt + 1, wrong here: the handle is gone before the invariance rule can relate the two value types, and the parameter's V arrives only as an upper bound. emit_apply records it directly instead (contribute_pbr_writes), reading the parameter off the head of the application spine (parameter_type), since a curried call leaves the immediately-applied type a bare Infer for every argument past the first. Why the lattice's join is the whole rule: src/ccl/design/type-inference.md.

Two checks that made a refined mutable variable look unsound

• types_agree_modulo_unread counted refinement layers before reading through a handle, comparing a refined value's one layer against the handle's zero. The read-through runs first now, split out as histories_agree.
• inline's refinement_discharged_by compared the parameter's demand against the argument's Mut stamp — which the mutability phase needs in order to find the read — so it asks what the argument denotes instead.

MutWrite also stopped relaxing its target: the constraint is skipped outright when the target is not a mutable variable, leaving that diagnosis to check_mut_write_targets, so Mut(Int) genuinely demands Int of its writes.

Mechanical, and one known gap

Type::peel_refinements / mut_value_type / as_feed / is_handle replace the hand-rolled peel-then-matches! at every site dispatching on a handle shape, retiring peel_refinements_outer and peel_mut with no behavior change.

An unstripped seed also keeps a filtered comprehension's extent, which then hangs in join planning's insert_iterate_markers — the same unfinished area where a write to a collection-valued mutable variable panics. Mutable collections are unsupported either way; recorded as a planning bug, not a restriction in the type system.

New end-to-end cases cover the computed seed with writes and without, and the pass-by-reference contribution at a non-first argument and through a forwarding chain; the accessors and the read-through are unit-tested, since no program can refine a handle.

[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.}