A mutable variable read is an explicit operation, not a subtyping rule

[dpmills]

A mutable variable was related to its value by subtyping, in both directions, and neither is a lattice fact: Mut(V) <: V puts a mutable variable below its value, V <: Mut(V, D) puts it above, and Mut is invariant in V. Both fire against a fresh inference variable — cnt + 1 emits Mut(Int, D) <: ?α — so the relation cannot tell a read from a handle being passed along, since a pass-by-reference argument meets a fresh variable too. The deref moves to the rule that emits the operand (emit::emit_value_read), both arms are deleted, and the relation relates a mutable variable only to another mutable variable.

Where a handle survives

Rules 1 and 2 of the second-class discipline make the handle positions enumerable — a pass-by-reference argument and a write's target — so a parent knows without inspecting the operand. Everything else derefs, tail positions included; a lambda's result deliberately does not, since that is where rule 2 catches an escape. See mutability.md. Invariance now supplies both directions at a call, so contribute_pbr_writes is deleted.

The three positions that made the upward coercion look necessary

Each is a place the rule should have read through the handle:

• the coalesce-time lifted type copied a tail's continuation type verbatim, re-stamping a statement or a mutable-variable introduction with the handle the read had just looked through: a := a + 5; a derived Int and recorded Mut(Int, D). 394 of the arm's 395 firings across compilation_pipeline were the wall reconciling that;
• a Case arm was not a value position, so a conditional over two mutable variables denoted a Mut whose writer cannot be traced — the case rule 2 exists to prevent;
• a Mut parameter given something that is not one had no value edge, leaving an argument the discipline check rejects under-determined.

mut_var_value_type asserted the old behaviour and now pins the corrected one, two tests cover the fixed tail and Case positions, and the arm's unit test becomes the statement that a value does not satisfy a Mut demand.

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