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

src/ccl/design/mutability.md

@@ -96,6 +96,55 @@ contributing loop's domain, free to reference the letrec's bindings. (They are o
 history by the same eliminator — it is only the *append* merge law, with no carry-forward, that
 lets a feed be a plain output rather than a cyclic binding.)
 
+### A mutable variable read is an explicit operation
+
+A mutable variable mention that denotes its **value** is dereffed by the rule that emits it
+(`infer::emit::emit_value_read`), not by the subtyping relation. `Mut(𝑉) <: 𝑉` is not a
+subtyping fact.
+
+The handle survives in exactly **two** positions, and the second-class discipline is what
+makes them enumerable: rule 1 forces a `Mut`-typed value to be a bare `Var` and rule 2
+keeps `Mut` out of every composite, so a parent always knows whether the operand it is
+about to constrain is a handle position.
+
+- A **pass-by-reference argument**, decided in `emit_apply` by reading the parameter off
+  the head of the application spine. The handle reaches the parameter, so the invariance
+  rule relates the two value types directly.
+- A **write's target**, which is resolved by name rather than as a subexpression. The
+  written *value* is an ordinary value position and reads.
+
+A lambda's result is deliberately *not* dereffed: that is where rule 2 catches a function
+returning a `Mut`, and dereffing would silently accept the escape by turning it into a
+read.
+
+That check reads what the body **denotes**, not what its root node is stamped with, and
+the difference is load-bearing. A **statement's continuation** and a **mutable variable
+introduction's body** report their continuation's *value* — they emit it as a value
+operand — so a program ending in a read of its accumulator has that accumulator's value
+rather than a handle. Their coalesce-time lifted type derefs for the same reason
+(`solve.rs`): a lift that copied the continuation's type verbatim would re-stamp the node
+with the handle the read just looked through, leaving the node's recorded type
+contradicting the rule that typed it. A **`Let` body** is the one tail that does *not*
+deref: a `Let` owns nothing — it cannot even bind a mutable variable — so it reports whatever its
+body reports, handle included, which is what leaves rule 2 an escape to catch. The same
+deref would hide an escape one line away from the boundary: reading the
+type alone, `λ 𝑐 → (𝑐 += 1; 𝑐)` looks like it returns an `Int` while `λ 𝑐 → 𝑐` returns the
+handle. So the escape check walks the tails to the term that actually produces the value.
+Every tail is walked, the mutable variable introduction included — a mutable variable does not escape its
+own introduction either, so returning one declared inside the function is the same escape
+as returning a parameter.
+
+**Neither direction is a subtyping fact**, and the symmetry is the point: `Mut(𝑉) <: 𝑉`
+would put a mutable variable *below* its value and `𝑉 <: Mut(𝑉, 𝐷)` would put it *above*, while
+`Mut` is invariant in `𝑉`. Either one is a coercion wearing a subtyping rule's clothes,
+and — because both fire against a fresh inference variable — neither can distinguish a
+read from a handle being passed along. The relation therefore relates a mutable variable only to
+another mutable variable, by invariance, and every position that means the *value* says so in the
+rule that emits it: `emit::emit_value_read` for an ordinary value position, and `emit_apply` reading
+through the parameter's handle for the one position where a `Mut` parameter is given
+something that is not a mutable variable (a program the second-class discipline rejects, but which
+still has to be typed to be reported well).
+
 ## Surface language
 
 The surface syntax and the behaviour a programmer observes — `:=` mutation, `with begin():`
@@ -240,12 +289,14 @@ wrapper variant carried on the introduction's binding and on every reference to
 
 Typing:
 
-- **Reads are implicit derefs**: `Mut(𝑉, 𝐷)` coerces to `𝑉` wherever a non-`Mut` type is demanded
-  (a coercion arm in `constrain`, not structural subtyping). `cnt + 1`, `f(cnt)` for an `Int`
-  parameter, and a trailing `cnt` all read; only a position that *expects* `Mut` (a `Mut`-annotated
-  parameter) receives the handle. After inlining, no `Mut`-expecting positions remain, so the
-  phase's rewrite is purely structural — every surviving `Mut`-typed occurrence is a write target
-  or a read, decided by context.
+- **Reads deref at the rule that emits them**: `cnt + 1`, `f(cnt)` for an `Int` parameter, and a
+  trailing `cnt` all read, and each reads because the rule typing that position asks for a value
+  operand (`emit::emit_value_read`). Only a position that *expects* `Mut` — a pass-by-reference
+  argument, a write's target — receives the handle. `Mut(𝑉) <: 𝑉` is deliberately not a subtyping
+  fact; see [A mutable variable read is an explicit operation](#a-mutable-variable-read-is-an-explicit-operation)
+  for why putting it in the relation could not distinguish a read from a handle passed along.
+  After inlining, no `Mut`-expecting positions remain, so the phase's rewrite is purely structural
+  — every surviving `Mut`-typed occurrence is a write target or a read, decided by context.
 - **A read derefs the constraint, not the node.** The deref decides what an operand is
   *constrained against*; the operand's own type slot keeps `Mut(𝑉, 𝐷)`, because that stamp is
   how the phase finds the read in the first place. So the parameter a mutable variable was passed to
@@ -267,8 +318,8 @@ introduction every write targets. The discipline:
 1. A `Mut`-typed expression must be a **bare variable reference** — an argument to a `Mut`
    parameter is a variable, never a conditional or computed expression. The two halves catch
    different things, because a *conditional* over two mutable variables is not itself `Mut`-typed: a
-   mutable read derefs into the arms' join exactly as it derefs into a tuple element (see *Reads
-   are implicit derefs* above), so `x if c else y` reads their values and types as a plain `V`.
+   mutable read derefs into the arms' join exactly as it derefs into a tuple element (each is a
+   value position, above), so `x if c else y` reads their values and types as a plain `V`.
    What the rule is protecting is the write capability travelling somewhere its target can't be
    traced, and that is the **argument** half: `bump(x if c else y)` is rejected on the argument's
    node, not its type.

src/ccl/design/type-inference.md

@@ -725,7 +725,7 @@ For the reconcile to hold, the passes that *introduce* refined types post-infere
 
 A feed handle is `Type::History { value: 𝑇, domain: 𝐷, kind: HistoryKind::Append }` (displayed `feed(𝐷 ⇒ 𝑉)`) — a function `𝐷 ⇒ 𝑇` carried as two children plus a two-valued `kind` marker. It **shares the `Type::History` variant with a mutable variable** (`kind: Overwrite`, displayed `Mut(𝑉, 𝐷)`); the two were unified from the former `Type::Feed(ρ)` / `Type::Mut{…}` pair (see [`Mut` is a CCL type](mutability.md#mut-is-a-ccl-type)). `let 𝑑 = Defer in body` gives `𝑑` a `Feed`-kind history whose channel `𝐷 ⇒ 𝑇` is the *post-desugar result type* of the binding (a `𝐷 ⇒ 𝑇` channel for fed defers, the defined value's type for `<<=`-defined defers). Like `Hole` and `Infer` the `Feed` kind is **transient**, scoped to inference: `channelize` (which runs after inference) eliminates every defer construct along with its feed histories, and no pass downstream of it may observe one. (This is the feed-handle type of [`Feed` is a CCL type](mutability.md#feed-is-a-ccl-type) — what a defer-mediating UDF parameter carries.)
 
-Below, **`Feed(ρ)`** abbreviates a `kind: Feed` history whose reconstructed channel is `ρ = 𝐷 ⇒ 𝑇`; the `value`/`domain` children are the two halves of `ρ`. The overwrite kind is deref-transparent instead (an `Overwrite` history meeting a demand for its value coerces to the scalar `𝑉`), so the four invariance rules below are specifically the `Feed`-kind behavior.
+Below, **`Feed(ρ)`** abbreviates a `kind: Feed` history whose reconstructed channel is `ρ = 𝐷 ⇒ 𝑇`; the `value`/`domain` children are the two halves of `ρ`. An `Overwrite` history reaches the relation as a handle — a read has already dereffed at the rule that emitted it — so the four invariance rules below are specifically the `Feed`-kind behavior.
 
 The typing rules (`infer_simple_sub::emit_defer` / `emit_feed` / `emit_define`): `Defer` emits `Feed(fresh ρ)`; `Feed{name, value}` and `Define{name, value}` type as `Unit`, resolve `name` from the scope like a `Var` use, and constrain their contribution into the target's payload (`Fun(fresh δ, value_ty)` for a feed — the channel *domain* is a desugar artifact, so `δ` stays unconstrained and coalesces to `Infer`; the bare `value_ty` for a define). A target that isn't structurally a feed handle (a lambda parameter — ParamAsTarget) is demanded to be one via the upper bound `target <: Feed(ρf)`; the call-site argument edge meets it there and invariance carries the contribution back to the caller's channel. A bare `Defer` RHS is never generalized (`should_generalize` wants a lambda RHS), so feeds and reads of one defer share one `ρ`; a defer minted inside a generalized function instantiates fresh per call site.
 
@@ -736,7 +736,7 @@ The typing rules (`infer_simple_sub::emit_defer` / `emit_feed` / `emit_define`):
 3. **`Fun(…) <: Feed(a)`** ⇒ `Fun(…) <: a` — a *channel-shaped* lhs is the read view of the feed handle (coalescing a use position that both held and read the handle surfaces the bare channel; monomorphization's two-way pin then meets that view against the definition's `Feed`).
 4. **`𝑇 <: Feed(a)`** for any other non-feed `𝑇` ⇒ `ConstrainError::NotAFeed` — the write capability cannot be conjured from a plain value (`g(5)` where `g` feeds its parameter).
 
-The shared variant keeps the overwrite/feed operator discipline **on the type**: rule 1's invariance arm matches only *same-`kind`* `History`/`History` pairs, so an `Overwrite` history demanded as a feed (or a feed as an overwrite history) is not equated — the `Overwrite` history first derefs to its scalar value (its own arm, ahead of the `Infer` arms), which then meets rule 4's `NotAFeed`. So `<<` into a `:=` mutable variable, or `+=` on a `defer` channel, is a type error with no separate structural check (see [`Mut` is a CCL type](mutability.md#mut-is-a-ccl-type)).
+The shared variant keeps the overwrite/feed operator discipline **on the type**: rule 1's invariance arm matches only *same-`kind`* `History`/`History` pairs, so an `Overwrite` history demanded as a feed (or a feed as an overwrite history) is not equated — the `Overwrite` history arrives as the handle it is and meets rule 4, whose left-hand side is any non-feed shape, as `NotAFeed`. So `<<` into a `:=` mutable variable, or `+=` on a `defer` channel, is a type error with no separate structural check (see [`Mut` is a CCL type](mutability.md#mut-is-a-ccl-type)).
 
 Invariance has no MLsub-blessed polar story, so the two polarity-sensitive mechanisms treat it specially:
 
@@ -1247,7 +1247,7 @@ Two problems look like they want an obligation of their own, and are not:
 
 * **A mutable variable's value type** is the *join* over its seed and every write, and the join is already the lattice's: every contribution is a *lower* bound of the mutable variable's value variable, and a positive-position read intersects refinement sets, so a refinement survives exactly when every contribution establishes it. Nothing needs to weaken a contribution to get that — the three sites (`MutWrite`, a mutable binding's initializer, a `Transact` key's seed) flow their contribution in verbatim. A mutable variable with a single contribution therefore *keeps* its refinement (`x := 1` is a `Mut(1)`), which is correct: it really does hold that value at every position.
 
-  The one contribution the lattice could not see was a write reaching a mutable variable **through a `Mut` parameter**. `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 (`cnt + 1` must read through the handle), but it drops the handle here, so the invariance rule that would relate the two value types never runs and the parameter's `V` arrives only as an *upper* bound. `emit_apply` records the missing contribution directly (`contribute_pbr_writes`): passing a mutable variable to a `Mut(V)` parameter contributes `V`, because that is what the call means. Reading the parameter's `Mut` syntactically is sound at that one site, since the mutability discipline requires a pass-by-reference parameter to be annotated.
+  A write reaching a mutable variable **through a `Mut` parameter** is one of those contributions, and it arrives by the ordinary invariance rule rather than by a mechanism of its own. `emit_apply` decides pass-by-reference from the parameter read off the head of the application spine, and passes the argument's handle through intact; the `(History, History)` arm then relates the two value types in both directions, which is what makes the callee's writes and the caller's declaration one constraint. Reading the parameter's `Mut` syntactically is sound at that one site, since a pass-by-reference parameter is bound at its `Mut(V, D)` by the only code that mints one. While a deref *coercion* sat in the relation this could not work — the handle met a fresh variable and was read through before invariance could see it — so the contribution had to be supplied separately.
 
   The parameter is read off the **head of the application spine**, not off the function being applied. An n-ary surface call lowers to a curried `Apply` spine, and `apply` types every application as a fresh variable, so the immediately-applied type is a bare `Infer` for every argument after the first — reading it there would contribute for `fw(x, out)` and silently skip `fw(out, x)`. The spine's length is the argument's position, and its parameter is the domain reached by peeling that many codomains off the head (`parameter_type`). For the same reason there is no composite to walk into: rule 2 of the mutability discipline rejects a `Mut` at every position but a domain's root, so a mutable variable is the parameter or it is nowhere.