From 774616b3140afe1c10946b6d943bc6abb47516e3 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 5 Aug 2026 10:57:53 -0700 Subject: [PATCH 1/4] A register read is an explicit operation, not a subtyping rule MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Mut(T) <: T` held for any non-`History` demand, which made a register a *subtype of its value*. As a lattice fact that is incoherent: `Mut(V)` sat **below** `V` while `Mut` is invariant in `V`. It was a coercion wearing a subtyping rule's clothes, and it fired 796 times across the suite — **769 of them against a bare inference variable**, because `+`/`<` are `∀α. α → α → α`, so `cnt + 1` emits `Mut(Int, D) <: ?α`. That last number is the actual defect. Firing against a fresh variable means the relation cannot distinguish a **read** from a **handle being passed along** — a pass-by-reference argument also meets a fresh variable, since `Typing::apply` records `arg <: ?d`. So the handle was dereffed before the invariance rule could see it, and passing a register to a `Mut(V)` parameter needed `contribute_pbr_writes` to hand-thread back the contribution that had just been thrown away. Dereffing now happens in the rule that emits the operand (`emit::read_operand`), and the arm is gone. **`contribute_pbr_writes` is deleted** — with the handle intact at the argument position, invariance relates the two value types directly and supplies both directions itself. Two mechanisms collapse into one, and the rule the docs already claimed becomes the rule that runs. 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 without inspecting it: - a **pass-by-reference argument**, decided in `emit_apply` by reading the parameter off the head of the application spine (a call is curried, so the applied type says nothing about an argument past the first); - a **write's target**, resolved by name rather than as a subexpression — the written *value* is an ordinary operand and reads. Everything else derefs, including the continuation positions: a node's own type is a value, so a trailing bare register read (`a := a + 5; a`) yields `Int`. Two placements are deliberate and were found by test rather than by reasoning: - **A lambda's result is not dereffed.** That is where rule 2 catches a function returning a `Mut`, whose reference would escape to where its writer set is unknown. Dereffing turned the escape into a read and *accepted* the program — a language change, caught by `rule2_function_returning_mut_is_rejected`. - **A `MutWrite`'s value is dereffed** while its target is not, which is what makes `b := a` between two registers write `a`'s current value. The two `constrain` unit tests that asserted the arm's behaviour are removed, with a note pointing at where the property now lives — `cnt + 1` yielding `Int` rather than leaving a `Mut` on an inference variable is pinned in `tests/type_check.rs` and end to end by the `mutability` suite. The variance tests added in the base PR are what make deleting `contribute_pbr_writes` safe rather than merely green: they fail if narrowing or widening through a `Mut` parameter stops being rejected. `./ci.sh` green. Moving the deref to the emitting rule means asking, at each site, whether it *consumes* a value or *passes one along*. A `Let`'s body, a statement's continuation, and a register introduction's body all pass along: the node's type simply **is** its continuation's, and none of them is a place a handle stops being one. A `Let` in particular owns nothing — it cannot even bind a register — so its body reports whatever the body reports. The register introduction and the effect statement are the exception, and only for the *type they report*: a program whose own tail reads its accumulator yields that accumulator's value, and after `inline` collapses `let b = a in b` to `a`, the statement's recorded type has to keep agreeing with what the node now derives. So those two deref. That leaves a gap the deref would otherwise cover for. Rule 2 catches a function returning a `Mut` by looking at the lambda's codomain — but if a tail dereffed on the way out, the codomain says `Int` and the escape is invisible. Inserting one line before the escape then changed the verdict, and not to an acceptance: the lambda's stamped codomain disagreed with its body's own type at the post-inference consistency wall, so `def f(c: Mut(Int)): y = 1; c` **panicked the compiler** where `def f(c: Mut(Int)): c` is rejected. So the check asks what the body *denotes* — walking the tails to the term that produces the value — rather than what its root node happens to be stamped with. Every tail is walked, the register introduction included: a register does not escape its own introduction either, so returning one declared inside the function is the same escape as returning a parameter, and both are rejected exactly as they were before the deref moved. Removing a mechanism leaves prose describing it, and here that prose had gone past stale into wrong. Nine sites across `ty.rs`, `emit.rs`, `constrain.rs`, `mutability.md` and `type-inference.md` still explained the coercion arm as live — several of them explaining *why* something else had to compensate for it. The worst was inverted rather than merely out of date. `Type::History`'s docs said the invariance rule is **not** what enforces a register's value type across a function boundary, because the deref fired first at an argument position and the rule never ran; invariance was assembled from an application edge plus `contribute_pbr_writes`. With the handle reaching the parameter, the rule is exactly what enforces it, in both directions, and the compensating contribution no longer exists. `type-inference.md` carried the same claim at length. The rest name a mechanism that is gone: a `(_, Mut)` "lenient coercion arm" that would deref a write's value anyway, a `(Mut, _)` deref arm that a feed payload had to be buried from, "the coercion arms in `constrain.rs`" as where a register read derefs, a cross-kind pair falling through to "the deref arms below", and a test contrast pointing at a test this change deletes. Each now says what the code does. One behaviour worth recording because a comment claimed the arm caused it: a `<<` targeting a `:=` register still lands in `NotAFeed`. It used to get there by being dereffed to `(value, feed)`; it now arrives as the handle it is and matches the same `(_, Append)` arm, which accepts any left-hand shape. --- src/ccl/design/mutability.md | 58 ++++++- src/ccl/design/type-inference.md | 4 +- src/ccl/infer/emit.rs | 184 ++++++++++++++--------- src/ccl/infer/solve.rs | 95 +++++++++++- src/ccl/infer/solver/constrain.rs | 82 ++++------ src/ccl/ty.rs | 20 +-- tests/compilation_pipeline/mutability.rs | 33 ++++ tests/type_check.rs | 23 +++ 8 files changed, 350 insertions(+), 149 deletions(-) diff --git a/src/ccl/design/mutability.md b/src/ccl/design/mutability.md index c69b62f1..692401f6 100644 --- a/src/ccl/design/mutability.md +++ b/src/ccl/design/mutability.md @@ -96,6 +96,46 @@ 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 operand 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 tail position — a `Let` body, a statement's +continuation, a mutable variable introduction's body — reports its continuation's *value*, so a +program ending in a read of its accumulator has that accumulator's value rather than a +handle. 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. + +Placing the deref in the relation instead was a coercion wearing a subtyping rule's +clothes. It put `Mut(𝑉)` *below* `𝑉` while `Mut` is invariant in `𝑉`, and — because it +fired against a fresh inference variable — nothing could distinguish a read from a handle +being passed along. That is why passing a mutable variable to a `Mut(𝑉)` parameter used to need a +separate compensating contribution: the handle was gone before invariance could see it. +With the handle intact, invariance supplies both directions and the compensation is +deleted. + ## Surface language The surface syntax and the behaviour a programmer observes — `:=` mutation, `with begin():` @@ -240,12 +280,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 +309,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 operand, 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. diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index 90bc64f3..fd0c8dcb 100644 --- a/src/ccl/design/type-inference.md +++ b/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. @@ -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. diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index 14b5d603..4e724fd6 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -209,11 +209,14 @@ fn emit_node_inner(expr: &mut Expr, ctx: &mut InferCtx) -> Result binding.scheme.instantiate(ctx.level), }; // The written value flows into the mutable variable's *value* type, not - // the `Mut` handle itself. (The `(_, Mut)` lenient coercion arm would - // deref anyway, but naming the mutable variable's value type says what a write - // means — it updates `V`.) + // the `Mut` handle itself — which is what a write means: it updates `V`. + // Nothing would deref it on the way in, since the relation holds no + // mutable variable rule; naming `V` here is the whole of it. let mut_value = var_ty.mut_value_type(); - let value_ty = ctx.subexpr(value)?; + // The *target* is a handle, resolved by name above. The written **value** is + // an ordinary value operand, so a mutable variable mention there reads: `b := a` + // between two mutable variables writes `a`'s current value into `b`. + let value_ty = emit_value_read(value, ctx)?; let write_label = name.clone(); // The written value flows in **verbatim**, as one contribution to the // mutable variable's value type. A refinement is a fact about *a value*, and a @@ -483,7 +486,20 @@ pub(super) fn emit_lambda( // The param is bound in scope under the *unrefined* `param_simple`, so // `Var(param)` body references stay bare; restriction refinements decorate only // the function boundary. + // Deliberately *not* `emit_value_read`: a lambda's result is where rule 2 catches a + // function returning a `Mut`, whose reference would escape to where its writer set + // is no longer statically known. Dereffing here would silently accept that program + // by turning the escape into a read. let body_ty = ctx.scoped(¶m.name, ¶m_simple, |ctx| ctx.subexpr(body))?; + // …and the same reason it is not dereffed here is why the *reported* codomain is + // what the body denotes rather than what its root node happens to be stamped with. + // A statement's type is its continuation's, and `emit_expr_stmt` derefs it; without + // this, inserting a statement before the escape hides the handle from rule 2 — + // `λ c → (c += 1; c)` would pass where `λ c → c` is rejected. + let body_ty = match denoted_expr(body).ty.mut_value_type() { + Some(_) => denoted_expr(body).ty.clone(), + None => body_ty, + }; // Param user-annotation: reconcile the inferred param type with the // annotation (two-way; see `bind_annotation`). @@ -595,8 +611,30 @@ pub(super) fn emit_apply( argument: &mut Expr, ctx: &mut C, ) -> Result { - let arg_ty = ctx.subexpr(argument)?; + let raw_arg_ty = ctx.subexpr(argument)?; let fn_ty = ctx.subexpr(function)?; + // **The one position where a mutable variable's handle survives.** If the parameter is a + // mutable variable the argument is passed *by reference* and the handle must reach the + // parameter, so the invariance rule relates the two value types directly — that is + // what makes the callee's writes and the caller's declaration one constraint rather + // than two edges that have to agree. Every other argument is a value operand, so a + // mutable variable mention there reads. + // + // Deciding it here is sound because the parameter is read off the *head of the + // spine* (`parameter_type`) rather than off the immediately-applied type — a call is + // curried, so the applied type says nothing about an argument past the first — and + // because a pass-by-reference parameter is bound at its `Mut(V, D)` by the only code + // that mints one (`lower::functions::uncurry_params`). Rule 2 guarantees the + // mutable variable is the parameter itself and never nested inside it, so there is no + // composite to walk. + let param_is_register = parameter_type(function, &fn_ty) + .and_then(Type::mut_value_type) + .is_some(); + let arg_ty = if param_is_register { + raw_arg_ty + } else { + read_through(&raw_arg_ty) + }; // The application's type is the function's codomain with its Pi binder // discharged to the argument (dependent application, design §5). `apply` // also pins the function/argument shapes with the one-way Apply edges @@ -605,9 +643,6 @@ pub(super) fn emit_apply( // A morphism's contravariant domain, left under-determined by the one-way // edges, is recovered structurally at coalesce // (`specialize_projection_domain` / `specialize_lambda_domain`). - // A mutable argument is a *contribution* to its mutable variable, not just a value - // flowing in — record that before the ordinary edges (below). - contribute_pbr_writes(function, &fn_ty, &arg_ty, ctx)?; ctx.apply(&fn_ty, &arg_ty, argument, &|| "Apply".to_string()) } @@ -634,50 +669,6 @@ fn require_single_obligation( } } -/// Passing a mutable variable to a `Mut(V)` parameter contributes `V` to the mutable variable's value -/// type, because that is what the call *means*: the callee may write any `V` here. -/// -/// Without this the contribution is simply missing, and the mutable variable's value type is -/// left claiming whatever its lexically-visible writes agree on. The ordinary -/// application edges cannot supply it: `Typing::apply` records `arg <: d` against a -/// **fresh variable** `d`, so a `Mut` argument meets an `Infer` rather than the -/// parameter's `Mut(V)` — and `(History, Infer)` is deliberately the *deref* arm, since -/// a bare read like `cnt + 1` must read through the handle. The handle is dereffed, the -/// invariance rule that would relate the two value types never runs, and `V` arrives -/// only as an *upper* bound. So the mutable variable's value variable ends up with the seed as -/// its sole lower bound: `x := 0` passed to `Mut(Int)` typed as `{Int | __elem == 0}`, -/// which the invariance check then rejected against the parameter. -/// -/// The parameter is read off the head of the application spine rather than off the -/// immediately-applied type ([`parameter_type`]) — otherwise only a call's *first* -/// argument is ever seen. -/// -/// A mutable variable can only ever be the parameter itself, never nested inside one: rule 2 of -/// the mutability discipline (`check_no_nested_mut`) rejects a `Mut` at every position -/// but a function domain's root, so there is no composite to walk into. -/// -/// Reading the parameter's `Mut` syntactically is sound here, and it is the one place -/// that is true of a `Mut`: a pass-by-reference parameter is *bound at* its `Mut(V, D)` -/// by lowering (`lower::functions::uncurry_params`, the only thing that mints one), so -/// the domain is a `History` by construction at every call this needs to see — no -/// annotation is consulted, and none survives inference to consult. -fn contribute_pbr_writes( - function: &Expr, - fn_ty: &Type, - arg_ty: &Type, - ctx: &mut C, -) -> Result<(), LocatedInferError> { - let Some(arg_value) = arg_ty.mut_value_type() else { - return Ok(()); - }; - let Some(param_value) = parameter_type(function, fn_ty).and_then(Type::mut_value_type) else { - return Ok(()); - }; - ctx.require_sub(param_value, arg_value, &|| { - "writes through a mutable parameter".to_string() - }) -} - /// The declared parameter type an argument is passed at, or `None` when the callee is /// opaque here. /// @@ -719,8 +710,8 @@ pub(super) fn emit_binop( sig: &OpSignature, ctx: &mut C, ) -> Result { - let left_ty = ctx.subexpr(left)?; - let right_ty = ctx.subexpr(right)?; + let left_ty = emit_value_read(left, ctx)?; + let right_ty = emit_value_read(right, ctx)?; let at = || "BinOp".to_string(); match sig { OpSignature::Scheme(scheme) => apply_binary_scheme(ctx, scheme, &left_ty, &right_ty, &at), @@ -735,7 +726,7 @@ pub(super) fn emit_unary( sig: &OpSignature, ctx: &mut C, ) -> Result { - let inner_ty = ctx.subexpr(inner)?; + let inner_ty = emit_value_read(inner, ctx)?; let at = || "UnaryOp".to_string(); match sig { OpSignature::Scheme(scheme) => apply_unary_scheme(ctx, scheme, &inner_ty, &at), @@ -758,7 +749,7 @@ pub(super) fn emit_tuple( // carrying `Mut` (rule 1 accepts it; the phase erases the type later) — // only the *composite type* is dereferenced, so a `Mut` never appears // nested in it. A non-`Mut` element is unchanged. - fields.insert(FieldKey::Index(i), read_through(&ctx.subexpr(e)?)); + fields.insert(FieldKey::Index(i), emit_value_read(e, ctx)?); } Ok(product(fields)) } @@ -774,7 +765,7 @@ pub(super) fn emit_record( // takes the dereferenced type so no `Mut` appears in the record type. fields.insert( FieldKey::Name(SmolStr::from(n.as_str())), - read_through(&ctx.subexpr(e)?), + emit_value_read(e, ctx)?, ); } Ok(product(fields)) @@ -788,7 +779,7 @@ pub(super) fn emit_expr_stmt( ctx: &mut C, ) -> Result { ctx.subexpr(e)?; - ctx.subexpr(body) + emit_value_read(body, ctx) } /// Type a `Defer` node: a fresh feed handle. `let d = Defer in body` binds @@ -823,6 +814,47 @@ fn read_through(ty: &Type) -> Type { ty.mut_value_type().unwrap_or(ty).clone() } +/// The expression a body ultimately **denotes**, seen through the tail positions that +/// carry their continuation's value. +/// +/// A tail position reports a value where a mutable variable is read — a program ending in a +/// read of its accumulator has that accumulator's *value* — so the handle is no longer +/// visible in the enclosing node's type. Anything that must reason about the handle +/// rather than the value asks the term instead, which is what this walks to. +/// +/// Every tail is walked, [`TypedExprNode::MutDecl`] included: a mutable variable does not +/// escape its introduction either, so a function whose body ends in a read of a +/// register it declared is the same escape as one that returns a parameter. Each of +/// these nodes reports its continuation's value, and none of them is a place a +/// handle stops being one. +fn denoted_expr(e: &Expr) -> &Expr { + match &e.node { + TypedExprNode::Let { body, .. } + | TypedExprNode::MutDecl { body, .. } + | TypedExprNode::ExprStmt { body, .. } => denoted_expr(body), + _ => e, + } +} + +/// Emit a **value operand**: a mutable variable mention here is a *read*, so its handle +/// derefs to the value it holds. +/// +/// This is the ordinary case. A mutable variable's handle survives in exactly two positions — +/// a pass-by-reference argument (see [`emit_apply`]) and a `MutWrite` target, which is +/// resolved by name rather than as a subexpression — and the mutability discipline is +/// what makes that 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 without inspecting it. +/// +/// Dereffing *here* rather than inside the subtyping relation is the point. A rule +/// `Mut(V) <: τ` reads as "a mutable variable is a subtype of its value", which is a coercion +/// wearing a subtyping rule's clothes: it makes `Mut(V)` sit below `V` while `Mut` is +/// invariant in `V`, and it fires against a fresh inference variable, so it cannot tell +/// a read from a handle being passed along. +fn emit_value_read(e: &mut Expr, ctx: &mut C) -> Result { + Ok(read_through(&ctx.subexpr(e)?)) +} + /// Type a `Feed { name, value }`: the fed value contributes one element to /// the target handle's channel; the feed expression itself is `Unit` (it is /// statement-positioned — channelize extracts the value into a channel and @@ -840,13 +872,15 @@ pub(super) fn emit_feed( ctx: &mut C, ) -> Result { // A feed payload is a *value* (`Mut` never appears in a feed payload — the - // discipline forbids it), so deref a bare mutable reference to its value - // type here. This wrapping into a `Fun` codomain buries the type where the - // solver's `(Mut, _)` deref arm cannot reach it: two contributions to one - // channel become `Fun` lower bounds that are *joined* (codomains lub'd), - // not constrained against a demand, so an undereferenced `Mut(V, D)` would - // collide with a plain-`V` feed to the same channel instead of dereffing. - let value_ty = read_through(&ctx.subexpr(value)?); + // discipline forbids it), so a mutable variable mention here reads. + // + // Dereffing at the emitting rule is what makes that work at all, and this is the + // site that shows why no later fixup could: the payload is wrapped into a `Fun` + // codomain, and two contributions to one channel become `Fun` lower bounds that + // are *joined* (codomains lub'd) rather than constrained against a demand. There + // is no demand for a handle to be reconciled against — an undereferenced + // `Mut(V, D)` would simply collide with a plain-`V` feed to the same channel. + let value_ty = emit_value_read(value, ctx)?; let contribution = fun(ctx.fresh(), value_ty); constrain_into_feed(target_ty, &contribution, label, ctx) } @@ -971,7 +1005,7 @@ pub(super) fn emit_aggregate( kind: AggregateKind, ctx: &mut C, ) -> Result { - let input_ty = ctx.subexpr(input)?; + let input_ty = emit_value_read(input, ctx)?; let at = || "Aggregate".to_string(); let result = apply_unary_scheme(ctx, scheme, &input_ty, &at)?; // `max` returns an element of what it consumes, so the scheme already gives it a @@ -1155,7 +1189,9 @@ pub(super) fn emit_letrec( /// Emit/check a [`TypedExprNode::MutDecl`] — a mutable variable introduction `x := init`. /// /// The binder is bound at the history `Mut(V, D)`, so references to `x` carry -/// `Mut` and reads deref to `V` (the coercion arms in `constrain.rs`). `normalize` +/// `Mut` and a read derefs to `V` at the rule that emits it ([`emit_value_read`], not +/// the subtyping relation — see `src/ccl/design/mutability.md`, "A mutable variable read is +/// an explicit operation"). `normalize` /// mints the declared type's `Hole` value/domain as fresh variables in Emit — so /// `?V` receives the seed and every write — and is the identity in Check. /// @@ -1174,7 +1210,7 @@ pub(super) fn emit_mut_decl( body: &mut Expr, ctx: &mut C, ) -> Result { - let init_ty = ctx.in_let_rhs(|ctx| ctx.subexpr(init))?; + let init_ty = ctx.in_let_rhs(|ctx| emit_value_read(init, ctx))?; let history = ctx.normalize(&binding.ty); debug_assert!( history.mut_value_type().is_some(), @@ -1193,7 +1229,7 @@ pub(super) fn emit_mut_decl( // Monomorphic, like every other non-`let` binder: a mutable variable is a single // object with one writer set, so there is nothing to generalize and // specializing it would duplicate the mutable variable. - let body_ty = ctx.scoped(&binding.name, &history, |ctx| ctx.subexpr(body))?; + let body_ty = ctx.scoped(&binding.name, &history, |ctx| emit_value_read(body, ctx))?; // The body type is returned as-is, *not* through `close_let_type`. A `let`'s // binder can be discharged into the lifted type because the binder simply *is* // its bound expression; a mutable variable is not — its value is the join over the seed @@ -1219,7 +1255,7 @@ pub(super) fn emit_for( body: &mut Expr, ctx: &mut C, ) -> Result { - let iter_ty = ctx.subexpr(iter)?; + let iter_ty = emit_value_read(iter, ctx)?; let iter_label = symbolic(iter); let (_domain, item_ty) = ctx.as_function(&iter_ty, &|| format!("for-loop source `{iter_label}`"))?; @@ -1310,7 +1346,7 @@ pub(super) fn emit_list( // `IncompatibleBounds` at coalesce, reported there rather than here. let elem_ty = ctx.fresh(); for elt in elts.iter_mut() { - let t = ctx.subexpr(elt)?; + let t = emit_value_read(elt, ctx)?; ctx.require_sub(&t, &elem_ty, &|| "List element".to_string())?; } let first_ty = elem_ty; @@ -1349,7 +1385,7 @@ pub(super) fn emit_case( // branch pattern tags, minting one payload var αᵢ per pattern branch and // writing it into the branch's binding slot (coalesce resolves it later). if let Some(scrut) = scrutinee { - let scrut_ty = ctx.subexpr(scrut)?; + let scrut_ty = emit_value_read(scrut, ctx)?; let mut expected_tags: BTreeMap = BTreeMap::new(); for b in branches.iter_mut() { if let Some(p) = &mut b.pattern { @@ -1401,7 +1437,7 @@ pub(super) fn emit_case( /// Emit a single Case branch: its guard must be `Bool`; the node takes the /// body's type. The pattern binding (if any) is already in scope. fn emit_case_branch(b: &mut Branch, ctx: &mut C) -> Result { - let guard_ty = ctx.subexpr(&mut b.guard)?; + let guard_ty = emit_value_read(&mut b.guard, ctx)?; // One-way: a guard must *be* a `Bool`, not be exactly `Bool`. A refined boolean // is still a boolean, and a refinement drops on the way up. ctx.require_sub(&guard_ty, &prim(BaseType::Bool), &|| { @@ -1415,7 +1451,7 @@ pub(super) fn emit_variant_ctor( payload: &mut Expr, ctx: &mut C, ) -> Result { - let payload_ty = ctx.subexpr(payload)?; + let payload_ty = emit_value_read(payload, ctx)?; let mut tags = BTreeMap::new(); tags.insert(FieldKey::Name(SmolStr::from(tag)), payload_ty); Ok(variant_type(tags)) diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index 4aca3623..3f68750c 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1793,12 +1793,44 @@ fn typecheck_discarded_definition(def: &mut Expr, level: Level, ctx: &mut Coales /// cast-target / join-filter predicate case is reached the same way: /// `coalesce_type_predicates` runs `coalesce_node` over each refinement /// predicate, so its projections recover through the `Apply` arm too. +/// The type a use-site domain recovery writes, given the position's own coalesced +/// `domain` and the value `input` flowing in. +/// +/// A recovery overwrites a domain with the type flowing in, read off the argument +/// **node** — and a node's recorded type is the mutable variable *handle* wherever one was +/// passed, because the read [`emit_apply`](super::emit::emit_apply) performed lives +/// in the `arg <: domain` edge, not on the node. So a recovery has to make that same +/// decision again, and it is the same decision: **a mutable variable mention reads, unless +/// the position being specialized is itself a handle position** — which its own +/// coalesced domain states outright, no spine walk required. +/// +/// Both recoveries need this, and they need opposite halves of it: +/// +/// - A **projection**'s domain is never a mutable variable — rule 2 keeps `Mut` out of every +/// composite, so nothing projects *into* one, only through one — so this always +/// derefs there. Without it a projection off a mutable variable (`acc.0` on a compound +/// accumulator) re-acquires the handle here and fails `emit_proj`'s +/// `domain <: {tuple/record}` requirement at the post-inference wall. +/// - A **lambda**'s domain *is* a mutable variable exactly when the parameter was declared +/// `Mut(…)`: pass-by-reference, the one position where the handle must reach the +/// parameter. Overwriting with the handle is right there and wrong everywhere else +/// — and wrong *silently*, since it retypes an ordinary value parameter as a +/// mutable variable that the body still reads at its value type. +fn recovered_input(domain: &Type, input: &Type) -> Type { + if domain.peel_refinements().mut_value_type().is_some() { + input.clone() + } else { + input.mut_value_type().unwrap_or(input).clone() + } +} + pub(super) fn specialize_projection_domain(morphism: &mut Expr, input: &Type) { if matches!(morphism.node, TypedExprNode::Proj(_)) + && let Some(dom) = morphism.ty.domain() && let Some(cod) = morphism.ty.codomain() { // A projection is non-dependent, so the rebuilt arrow keeps `name: None`. - morphism.ty = Type::fun(input.clone(), cod); + morphism.ty = Type::fun(recovered_input(&dom, input), cod); } } @@ -1868,11 +1900,16 @@ pub(super) fn specialize_lambda_domain(lambda: &mut Expr, input: &Type) { input_refinements.push(r); t = inner; } + // A mutable variable mention reads unless this parameter was *declared* one — see + // [`recovered_input`]. `base` is the peeled domain, so a declared `Mut(V, D)` + // parameter is visible here whatever refinements rode in on it. let new_dom = dom_layers .into_iter() .rev() .filter(|r| !input_refinements.contains(&r)) - .fold(input.clone(), |acc, r| Type::Refinement(Box::new(acc), r)); + .fold(recovered_input(&base, input), |acc, r| { + Type::Refinement(Box::new(acc), r) + }); lambda.ty = fn_layers.into_iter().rev().fold( // Preserve the Pi binder: specialization rewrites only the domain // *shape*; a dependent codomain still refers to the same binder. @@ -1909,6 +1946,60 @@ mod tests { use crate::ccl::symbolic::symbolic; use crate::ccl::{ArithmeticKind, BaseType, BinOpKind, Lit, Type, TypedExpr, TypedExprNode}; + // ----- use-site domain recovery (`recovered_input`) ----- + + /// A use-site domain recovery overwrites a morphism's domain with the type read + /// off the argument **node**, and that type is the mutable variable *handle* — the read + /// `emit_apply` performed lives in the `arg <: domain` edge, not on the node. So + /// the recovery has to redo the decision, and it must land on the same answer. + /// + /// Driven at [`recovered_input`] rather than through a program because neither + /// arm is reachable from source today: a lambda in function position is only ever + /// the comprehension shape until `inline` runs (after inference), and a lambda + /// parameter cannot be annotated at all, so a directly-applied `Mut` parameter has + /// no spelling. Both become reachable the moment direct application does, and the + /// wrong answer is silent in both directions — a value parameter retyped as a + /// mutable variable, or a pass-by-reference parameter degraded to a value copy. + #[test] + fn a_recovery_reads_a_register_unless_the_position_is_a_handle() { + use super::recovered_input; + use crate::ccl::{HistoryKind, Refinement}; + let mut_var = |value: Type| Type::History { + value: Box::new(value), + domain: Box::new(Type::Txn), + kind: HistoryKind::Overwrite, + }; + // Refinements are built here rather than via `refined_int`, which is + // `debug_assertions`-only: the rule under test is not. + let refined = |inner: Type| { + Type::Refinement( + Box::new(inner), + Refinement::born(std::rc::Rc::new(TypedExpr::lit(crate::ccl::Lit::Bool( + true, + )))), + ) + }; + let int = Type::Base(BaseType::Int); + let handle = mut_var(int.clone()); + + // An ordinary value position reads through the handle. + assert_eq!(recovered_input(&int, &handle), int); + // ...including one still unresolved, and one carrying body-usage refinements: + // the decision is the *position's*, and neither of those is a handle position. + assert_eq!(recovered_input(&Type::Hole, &handle), int); + assert_eq!(recovered_input(&refined(int.clone()), &handle), int); + + // A declared `Mut(…)` parameter is the one position the handle must reach — + // dereffing here would turn pass-by-reference into a silent value copy. + assert_eq!(recovered_input(&handle, &handle), handle); + // A refinement on the handle does not stop it being one (a refined mutable variable is + // still a mutable variable), so the position is still recognised. + assert_eq!(recovered_input(&refined(handle.clone()), &handle), handle); + + // A non-mutable variable input is untouched either way. + assert_eq!(recovered_input(&int, &int), int); + } + // ----- ordering-invariant comparison (`types_agree_modulo_unread`) ----- // A refinement that appears (or vanishes) between a read and the final graph is diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index d2109eb2..928d9a41 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -620,9 +620,10 @@ fn constrain_go_impl( // Two histories of the **same kind** equate invariantly in both value // and domain (a mutable param reads *and* writes; a feed handle both feeds // and is read). A cross-kind pair (a mutable variable demanded as a feed, or vice - // versa) is *not* matched here: it falls through to the deref arms below, - // where a mutable variable demanded as a feed lands in `NotAFeed` — the type-level - // guardrail that `<<` targets a `defer` channel, not a `:=` mutable variable. + // versa) is *not* matched here: it falls through to the `(_, Append)` arm below, + // which accepts any left-hand shape, so a mutable variable demanded as a feed + // lands in `NotAFeed` — the type-level guardrail that `<<` targets a `defer` + // channel, not a `:=` mutable variable. ( Type::History { value: v0, @@ -640,22 +641,18 @@ fn constrain_go_impl( constrain_go(d0, d1, &Subst::id(), &Subst::id(), cache)?; constrain_go(d1, d0, &Subst::id(), &Subst::id(), cache) } - // Implicit deref (read): a `Mut` handle meeting any non-`Mut` demand — - // concrete OR an inference variable — reads its value. This MUST precede - // the `Infer` arms below: an operator constrains its operand against a fresh - // variable (`cnt + 1` emits `Mut(Int, D) <: ?α` for `Addable`'s first operand - // position), and dereffing here flows `Int` onto `?α` — where the narrowing - // hook can read a base off it. The `(_, Infer)` arm would instead record the - // handle itself as a lower bound, offering the obligation nothing and - // coalescing `?α` to a `Mut`. - ( - Type::History { - value, - kind: HistoryKind::Overwrite, - .. - }, - _, - ) => constrain_go(value, rhs, sl, sr, cache), + // There is deliberately **no deref arm here.** A mutable variable mention that denotes + // its value is dereffed by the rule that emits it (`emit::emit_value_read`), so a + // handle reaching this relation is a handle: the only edges that carry one are + // a pass-by-reference argument against its parameter, which the invariance arm + // above relates, and a write's target. + // + // As a subtyping rule the deref was a coercion in disguise — it made `Mut(V)` + // sit *below* `V` while `Mut` is invariant in `V`, and it fired against a fresh + // inference variable, so nothing downstream could tell a read from a handle + // being passed along. That is precisely why passing a mutable variable to a `Mut(V)` + // parameter needed a separate compensating contribution: the handle was gone + // before the invariance rule could see it. // Variable on lhs, rhs has compatible level: record the upper edge in // native form (`V‹sl› <: rhs‹sr›`, no inversion), then close each @@ -805,8 +802,9 @@ fn constrain_go_impl( } // Any other plain value can never satisfy a feed requirement: reading is // transparent, but the write capability cannot be conjured (`g(5)` where - // `g` feeds its parameter, or a `<<` targeting a `:=` mutable variable — which the - // mutable deref above reduced to `(value, feed)` landing here). + // `g` feeds its parameter). A `<<` targeting a `:=` mutable variable lands here + // too, as the handle it is — the left side matches `_`, so the cross-kind pair + // the invariance arm above declined needs no rule of its own. ( _, Type::History { @@ -1795,8 +1793,9 @@ mod tests { fn feed_var_coalesces_to_feed() { // A var bounded by feed(D, Int) coalesces carrying the Feed // constructor (the `history_slot` survives compact → simplify → - // coalesce). Contrast `mut_derefs_at_a_variable_not_the_handle`, where - // the deref arm collapses an `Overwrite` var to its bare value. + // coalesce). An `Overwrite` handle reaching a variable survives the same + // way — the relation holds no rule that would collapse it to its value, + // because a read derefs at the rule that emits it instead. use crate::ccl::infer::solver::simplify_type; let v = fresh_var(0); let h = feed_ty(Type::UIntRange(3), prim(BaseType::Int)); @@ -1921,36 +1920,13 @@ mod tests { } } - #[test] - fn mut_reads_transparently_as_value() { - // Mut(Int, D) <: Int — a read derefs to the value… - let m = mut_ty(prim(BaseType::Int), prim(BaseType::UInt)); - let mut cache = ConstrainCache::new(); - assert!(constrain_subtype(&m, &prim(BaseType::Int), &mut cache).is_ok()); - // …but the value still has to match the consumer. - let mut cache = ConstrainCache::new(); - assert!(matches!( - constrain_subtype(&m, &prim(BaseType::String), &mut cache), - Err(ConstrainError::Mismatch { .. }) - )); - } - - #[test] - fn mut_derefs_at_a_variable_not_the_handle() { - // THE crux (plan decision #1): `cnt + 1` emits `Mut(Int, D) <: ?α`. The - // deref arm fires *before* the `Infer` arm, so `?α` coalesces to `Int`, - // NOT to a `Mut` handle — the deliberate contrast with - // `feed_var_coalesces_to_feed`. If the deref arm were placed after the - // `Infer` arms, `?α` would carry the `Mut` constructor and reads would - // break. - use crate::ccl::infer::solver::simplify_type; - let v = fresh_var(0); - let m = mut_ty(prim(BaseType::Int), prim(BaseType::UInt)); - let mut cache = ConstrainCache::new(); - constrain_subtype(&m, &v, &mut cache).unwrap(); - let out = coalesce_compact(&simplify_type(compact_type(&v))).unwrap(); - assert_eq!(out, prim(BaseType::Int)); - } + // The deref arm these two tests covered is gone: a mutable variable mention that denotes + // its value is dereffed by the rule that emits it (`emit::emit_value_read`), so + // `Mut(V) <: τ` is no longer a subtyping fact and there is nothing to assert here. + // The property they protected — `cnt + 1` yields `Int` rather than leaving a `Mut` + // on an inference variable — is now pinned where it is decided: + // `a_register_read_yields_its_value_in_an_operand_position` in `tests/type_check.rs`, + // and the `mutability` integration suite end to end. #[test] fn mut_meets_mut_invariantly() { diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index c50f4bb0..e51ab58d 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -652,16 +652,16 @@ pub enum Type { /// provenance, not a property of a type*: a variance rule sees two types and /// cannot ask where either came from. /// - /// **The rule is not what currently enforces that across a function boundary.** - /// At an argument position the deref arm fires first — `Typing::apply` records - /// `arg <: ?d` against a fresh variable, so a mutable variable meets an `Infer` and reads - /// through — so the `(History, History)` arm never runs there. Invariance at a - /// pass-by-reference call is assembled from two other edges instead: the - /// application edge supplies `caller <: callee`, and `emit::contribute_pbr_writes` - /// supplies `callee <: caller`. Equal in strength to the rule, spread across two - /// mechanisms — which is why the property is pinned by test - /// (`a_mut_vars_value_type_is_invariant_across_a_mut_parameter`) rather than - /// argued from this paragraph. + /// **The rule is what enforces that across a function boundary**, and it can be + /// because the handle reaches the parameter: `emit_apply` decides pass-by-reference + /// from the parameter read off the head of the application spine and leaves the + /// argument's `Mut` intact, so the `(History, History)` arm relates the two value + /// types directly. Both directions come from the one rule rather than being + /// assembled from an application edge plus a compensating write contribution — the + /// shape this needed while a deref coercion erased the handle before invariance + /// could see it. The property is still pinned by test + /// (`a_registers_value_type_is_invariant_across_a_mut_parameter`), which is what + /// would catch a future consolidation quietly dropping one direction. /// /// It is also a **transient** variant like `Hole` / `Infer`: it exists only between type /// inference (which stamps it on `:=` / `defer` introductions and every diff --git a/tests/compilation_pipeline/mutability.rs b/tests/compilation_pipeline/mutability.rs index 1618881d..7e375c10 100644 --- a/tests/compilation_pipeline/mutability.rs +++ b/tests/compilation_pipeline/mutability.rs @@ -907,6 +907,39 @@ fn rule2_function_returning_mut_is_rejected() { expect_mut_discipline_error("x := 0\nf = \\z -> x\nf", "inside a composite type"); } +/// The escape is rejected **however many tail positions sit between the function +/// boundary and the read**, which is not free: a tail position reports its +/// continuation's *value*, so an intervening statement or binding derefs the handle +/// out of the enclosing node's type. Rule 2 therefore asks what the body *denotes* +/// rather than what its root node is stamped with. +/// +/// Without that, inserting a line changed the verdict — and not to an acceptance but +/// to a compiler panic, since the lambda's stamped codomain (`Int`) then disagreed +/// with its body's own type (`Mut(Int, ?d)`) at the post-inference consistency wall. +#[rstest] +#[case::through_a_binding("def f(c: Mut(Int)):\n y = 1\n c\nx := 0\nf(x)")] +#[case::through_a_statement("def f(c: Mut(Int)):\n c += 1\n c\nx := 0\nf(x)")] +#[case::through_a_register_introduction("def f(c: Mut(Int)):\n z := 1\n c\nx := 0\nf(x)")] +// A mutable variable does not escape its own introduction either: returning one declared +// *inside* the function is the same escape as returning a parameter. +#[case::its_own_register("def g(n):\n z := n\n z\ng(5)")] +#[case::its_own_register_through_a_binding("def g(n):\n z := n\n y = 2\n z\ng(5)")] +fn rule2_is_not_evaded_by_a_tail_position(#[case] code: &str) { + expect_mut_discipline_error(code, "inside a composite type"); +} + +/// The complement, and why the rule cannot simply refuse to deref a tail: a program +/// whose own tail reads its accumulator yields that accumulator's **value**. Nothing +/// escapes — there is no function boundary — so the deref is what makes the ordinary +/// case work, and the check above is what keeps it from covering for an escape. +#[test] +fn a_programs_tail_read_of_its_accumulator_is_a_value() { + check_scalar( + "x := 0\nfor i in [1, 2, 3]:\n x += i\ny = 1\nx", + cambra::interpreter::Value::Int(6), + ); +} + /// Rule 1: an argument to a `Mut` parameter must be a bare variable reference, /// so a *conditional* selecting between two mutable variables — which one would /// the callee's write target? — is rejected. The check reads the argument node, diff --git a/tests/type_check.rs b/tests/type_check.rs index 6a9c267a..19276c73 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -2444,3 +2444,26 @@ fn a_single_type_fault_prints_no_demand() { "a single-type fault must not invent a demand, got: {missing}" ); } + +/// A mutable variable mention in an operand position yields its **value type**, never the +/// handle — and it does so because the emitting rule derefs, not because subtyping +/// says a mutable variable is a subtype of its value. +/// +/// `cnt + 1` is the case that pins the placement: `+` is `∀α. α → α → α`, so the +/// operand meets a *fresh inference variable*. While the deref lived in the subtyping +/// relation this worked only because that arm was ordered before the `Infer` arms — and +/// that same ordering is what made a pass-by-reference argument indistinguishable from +/// a read, since it too meets a fresh variable. +#[test] +fn a_register_read_yields_its_value_in_an_operand_position() { + assert_eq!(infer_program("x := 5\nx + 1\n"), int()); + // The value still has to satisfy the operand's demand: what reaches the operator's + // obligation is `String`, the *value* the read yielded, so the implementation table + // rejects it at that operand position. A handle arriving here instead would offer no + // base at all and the obligation would have nothing to reject. + let errs = format!("{:?}", infer_program_err("x := 5\nx + \"s\"\n")); + assert!( + errs.contains("Addable") && errs.contains("String"), + "a read's value type is still checked against the operator, got: {errs}" + ); +} From 00d9568ea1a7fe093ff8fd1ab3e822e405766433 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 12 Aug 2026 15:21:58 -0700 Subject: [PATCH 2/4] Neither direction of `Mut` is a subtyping fact MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Deleting `Mut(V) <: V` left its mirror standing. `V <: Mut(V, D)` held for any value meeting a register demand, which puts a register *above* its value exactly as the deleted arm put it below — and `Mut` is invariant in `V`, so neither is a lattice fact. Both also fire against a fresh inference variable, so like the arm this PR removed, this one cannot tell a read from a handle being passed along. It survived because three positions relied on it, and each is a place the *rule* should have read through the handle: **A tail's recorded type contradicted the rule that derived it.** `read_operand` derefs where the operand is emitted, but the coalesce-time lifted type (`solve.rs`) copied the continuation's type verbatim, re-stamping a statement or a register introduction with the handle the read had just looked through. So `a := a + 5; a` derived `Int` and recorded `Mut(Int, D)`, and the post-inference wall — which re-runs the same rule — needed the coercion to accept every read in every program. Measured: 394 of the 395 firings across `compilation_pipeline` were that reconcile. The lift now derefs for the two nodes whose rules report a value; a `Let` deliberately does not, since it reports its body verbatim and that is what leaves rule 2 an escape to catch. **A `Case` arm was not a value position.** `emit_case_branch` ended in `subexpr`, so an arm's handle flowed into the join and `x if c else y` over two registers denoted a `Mut` — the untraceable-writer case rule 2 exists to prevent — while the comment three lines above claimed arms "deref into the join like any other". They do now. The design doc and the discipline check both already described the fixed behaviour: rule 1 rejects `bump(x if c else y)` on the argument *node* precisely because its type is a value. **A `Mut` parameter given a non-register had no value edge.** That program is rejected by the discipline check, which owns the diagnosis, but its argument subtree still needs an upper bound — without one the argument is under-determined and the wall fails on a narrower recorded type. `emit_apply` now emits that edge itself, against the parameter's value, which is the same move as every other read: the rule that knows the position reads through the handle. With those closed the arm is dead and deleted. The relation relates a register only to another register, by invariance, in both directions. `register_value_type` in `tests/type_check.rs` asserted the old behaviour — it read the program's root expecting a `History` — and now pins the corrected one: a handle escaping a tail is a failure. Two tests cover the fixed positions directly, and the deleted arm's unit test becomes the statement that a value does not satisfy a `Mut` demand. The denied fact is also spelled `Mut(V) <: V` throughout now, in the docs and comments this PR touches. It was written `Mut(V) <: τ` for a `τ` nothing introduced, and the sentences carrying it all gloss it as "a subtype of its value" — which is the `τ := V` instance, the one that makes the arm incoherent and the one that mirrors `V <: Mut(V, D)`. `./ci.sh` and `DEEP_TYPECHECK=1 ./ci.sh test` green. --- src/ccl/design/mutability.md | 35 +++++++++++++--------- src/ccl/design/type-inference.md | 2 +- src/ccl/infer/emit.rs | 48 ++++++++++++++++++++++++------- src/ccl/infer/solve.rs | 16 +++++++++-- src/ccl/infer/solver/constrain.rs | 35 ++++++---------------- tests/type_check.rs | 48 ++++++++++++++++++++++++++++--- 6 files changed, 128 insertions(+), 56 deletions(-) diff --git a/src/ccl/design/mutability.md b/src/ccl/design/mutability.md index 692401f6..77d84671 100644 --- a/src/ccl/design/mutability.md +++ b/src/ccl/design/mutability.md @@ -99,7 +99,7 @@ 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 +(`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 @@ -118,23 +118,32 @@ returning a `Mut`, and dereffing would silently accept the escape by turning it read. That check reads what the body **denotes**, not what its root node is stamped with, and -the difference is load-bearing. A tail position — a `Let` body, a statement's -continuation, a mutable variable introduction's body — reports its continuation's *value*, so a -program ending in a read of its accumulator has that accumulator's value rather than a -handle. The same deref would hide an escape one line away from the boundary: reading the +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. -Placing the deref in the relation instead was a coercion wearing a subtyping rule's -clothes. It put `Mut(𝑉)` *below* `𝑉` while `Mut` is invariant in `𝑉`, and — because it -fired against a fresh inference variable — nothing could distinguish a read from a handle -being passed along. That is why passing a mutable variable to a `Mut(𝑉)` parameter used to need a -separate compensating contribution: the handle was gone before invariance could see it. -With the handle intact, invariance supplies both directions and the compensation is -deleted. +**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 operand, 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 @@ -283,7 +292,7 @@ Typing: - **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 + 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 diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index fd0c8dcb..3584cfd7 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -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: diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index 4e724fd6..5182c499 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -627,13 +627,35 @@ pub(super) fn emit_apply( // that mints one (`lower::functions::uncurry_params`). Rule 2 guarantees the // mutable variable is the parameter itself and never nested inside it, so there is no // composite to walk. - let param_is_register = parameter_type(function, &fn_ty) - .and_then(Type::mut_value_type) - .is_some(); - let arg_ty = if param_is_register { - raw_arg_ty - } else { - read_through(&raw_arg_ty) + let param_ty = parameter_type(function, &fn_ty).cloned(); + let arg_ty = match (param_ty, raw_arg_ty.mut_value_type()) { + // A handle reaching its pass-by-reference parameter: invariance relates the two + // value types directly, in both directions. + (Some(param), Some(_)) if param.mut_value_type().is_some() => raw_arg_ty, + // A pass-by-reference parameter given something that is not a mutable variable + // (`bump(x)` for a plain `x`, `bump(x if c else y)` for a selection). The + // program is rejected either way — the discipline requires a `Mut` parameter's + // argument to be a mutable variable, and `check_mut_discipline` owns that diagnosis, + // which is the one worth reading — but the argument still has to be *typed*, + // since its own subtree is under-determined without an upper bound. + // + // So the value edge is emitted here, against the parameter's value, rather than + // left to the relation. A value meeting a handle is not a subtyping fact, and + // making it one is what put a coercion back in the lattice: the rule that knows + // this position is pass-by-reference is the rule that should read through the + // handle. The application edge below then relates handle to handle. + (Some(param), None) if param.mut_value_type().is_some() => { + let value = param + .mut_value_type() + .expect("guarded by the match arm") + .clone(); + ctx.require_sub(&read_through(&raw_arg_ty), &value, &|| { + "pass-by-reference argument".to_string() + })?; + param + } + // Every other position is a value operand, so a mutable variable mention reads. + _ => read_through(&raw_arg_ty), }; // The application's type is the function's codomain with its Pi binder // discharged to the argument (dependent application, design §5). `apply` @@ -810,7 +832,7 @@ pub(super) fn emit_defer(ctx: &mut C) -> Type { /// Deref a mutable variable reference to its value type. A no-op on every other /// type — a feed channel included, since reading one yields its whole stream /// rather than a scalar value ([`Type::mut_value_type`]). -fn read_through(ty: &Type) -> Type { +pub(super) fn read_through(ty: &Type) -> Type { ty.mut_value_type().unwrap_or(ty).clone() } @@ -847,7 +869,7 @@ fn denoted_expr(e: &Expr) -> &Expr { /// operand it is about to constrain is a handle position without inspecting it. /// /// Dereffing *here* rather than inside the subtyping relation is the point. A rule -/// `Mut(V) <: τ` reads as "a mutable variable is a subtype of its value", which is a coercion +/// `Mut(V) <: V` reads as "a mutable variable is a subtype of its value", which is a coercion /// wearing a subtyping rule's clothes: it makes `Mut(V)` sit below `V` while `Mut` is /// invariant in `V`, and it fires against a fresh inference variable, so it cannot tell /// a read from a handle being passed along. @@ -1443,7 +1465,13 @@ fn emit_case_branch(b: &mut Branch, ctx: &mut C) -> Result( diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index 3f68750c..e586378e 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -21,6 +21,7 @@ use crate::ccl::ccl_utils::PredMemo; use crate::ccl::infer::InferError; +use crate::ccl::infer::emit::read_through; use crate::ccl::infer::solver::{ CoalesceError, ConstrainCache, FreshenCache, FreshenLevel, SpecKey, coalesce_compact, compact_type, constrain_subtype, freshen_expr_type_slots, seed_chan_dom_pairings, @@ -1217,7 +1218,16 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { // (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()), + // + // Through the **deref**, because that is what the node's rule reports: an + // effect statement emits its continuation as a value operand + // (`emit_expr_stmt`'s `emit_value_read`), so a tail that reads a mutable variable denotes + // the mutable variable's *value*. Lifting `body.ty` verbatim would re-stamp the node + // with the handle the read just looked through, contradicting the rule that + // typed it — and the wall that re-runs that rule would then have to accept a + // value against a handle. A `Let` needs no deref here because it does not + // deref either (`emit_let` passes its body along; it cannot bind a mutable variable). + TypedExprNode::ExprStmt { body, .. } => Some(read_through(&body.ty)), // 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 @@ -1237,7 +1247,9 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { label, ); } - Some(body.ty.clone()) + // Dereffed for the same reason as `ExprStmt`: `emit_mut_decl` reports its + // body as a value operand, so `x := 0; …; x` denotes `x`'s value. + Some(read_through(&body.ty)) } _ => None, }; diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index 928d9a41..9ede75fc 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -816,24 +816,6 @@ fn constrain_go_impl( required: rhs.clone(), }), - // A non-`Mut` value meeting a `Mut` demand: deref the demand to its - // value. `x: Int = cnt` copies the current value; `MutWrite` - // reconciliation flows a written value into the mutable variable's value. Unlike a - // feed (where the write capability can't be conjured), a `Mut` demand is - // satisfied structurally by its value here, and the *second-class - // discipline check* — not the solver — is what rejects passing a - // non-variable (`bump(5)`, `bump(a + b)`) to a `Mut` parameter. (A - // `Mut`-lhs was already dereffed above; an `Infer`-lhs recorded the `Mut` - // as an upper bound — the `Mut`-param-via-variable case.) - ( - _, - Type::History { - value, - kind: HistoryKind::Overwrite, - .. - }, - ) => constrain_go(lhs, value, sl, sr, cache), - // A nominal channel domain is *deferred-compatible* with any // domain-shaped type it meets — the assembly (channelize) is what // determines the concrete domain, and the strict post-channelize @@ -1922,7 +1904,7 @@ mod tests { // The deref arm these two tests covered is gone: a mutable variable mention that denotes // its value is dereffed by the rule that emits it (`emit::emit_value_read`), so - // `Mut(V) <: τ` is no longer a subtyping fact and there is nothing to assert here. + // `Mut(V) <: V` is no longer a subtyping fact and there is nothing to assert here. // The property they protected — `cnt + 1` yields `Int` rather than leaving a `Mut` // on an inference variable — is now pinned where it is decided: // `a_register_read_yields_its_value_in_an_operand_position` in `tests/type_check.rs`, @@ -1956,16 +1938,17 @@ mod tests { } #[test] - fn value_meets_mut_demand_derefs() { - // Int <: Mut(Int, D) — a plain value meeting a `Mut` demand derefs to the - // value (the discipline check, not the solver, rejects passing a - // non-variable to a `Mut` parameter). A conflicting value still fails. + fn a_value_does_not_satisfy_a_mut_demand() { + // `Int <: Mut(Int, D)` is **not** a subtyping fact, the mirror of + // `Mut(V) <: V` not being one: a mutable variable is neither above nor below its + // value, and a relation that coerces either way cannot tell a read from a + // handle. A position that means the value says so itself — `emit_apply` + // reads through the parameter's handle for a pass-by-reference argument, + // and every other operand derefs at `emit::emit_value_read`. let m = mut_ty(prim(BaseType::Int), prim(BaseType::UInt)); let mut cache = ConstrainCache::new(); - assert!(constrain_subtype(&prim(BaseType::Int), &m, &mut cache).is_ok()); - let mut cache = ConstrainCache::new(); assert!(matches!( - constrain_subtype(&prim(BaseType::String), &m, &mut cache), + constrain_subtype(&prim(BaseType::Int), &m, &mut cache), Err(ConstrainError::Mismatch { .. }) )); } diff --git a/tests/type_check.rs b/tests/type_check.rs index 19276c73..8d100521 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -388,12 +388,20 @@ fn a_concrete_operand_reaches_its_obligation(#[case] code: &str) { infer_and_check(code); } -// The value type of a mutable variable, ignoring the sequencing domain — an `Infer` until the -// mutability-elimination phases resolve it, so it cannot be asserted on here. +// The value type of a mutable variable, read off the program's own type. +// +// Each program below ends in a bare read of its mutable variable, and a tail position emits its +// continuation as a *value* operand, so the program denotes the mutable variable's **value** — +// the handle stops at the read. That makes the program type the value type directly, +// and it is also why a `History` here is a failure rather than the expected shape: it +// would mean a handle escaped a tail position, where the sequencing domain (an `Infer` +// until the mutability-elimination phases resolve it) would ride along with it. fn mut_var_value_type(code: &str) -> Type { match infer_program(code) { - Type::History { value, .. } => *value, - other => panic!("expected a mutable variable type for `{code}`, got {other}"), + ty @ Type::History { .. } => { + panic!("a tail read must denote the mutable variable's value, got the handle {ty} for `{code}`") + } + value => value, } } @@ -2467,3 +2475,35 @@ fn a_register_read_yields_its_value_in_an_operand_position() { "a read's value type is still checked against the operator, got: {errs}" ); } + +/// A **tail** position denotes its continuation's value, so a program ending in a bare +/// read of its mutable variable denotes that mutable variable's value rather than the handle. +/// +/// The type a node reports and the type its rule derives have to agree, and a tail's +/// rule emits its continuation as a value operand (`emit_expr_stmt` / `emit_mut_decl`). +/// A lift that copied the continuation's type verbatim would re-stamp the node with the +/// handle the read just looked through, and the wall that re-runs the rule would then be +/// asked to accept a value against a handle — which is not a subtyping fact. +#[test] +fn a_tail_read_denotes_the_registers_value() { + assert_eq!(infer_program("a := 0\na := a + 5\na"), int()); + // Through an intervening statement too — that is the spine link the lift follows. + assert_eq!(infer_program("a := 0\na := a + 5\nb = 1\na"), int()); + // With no write at all the value is the seed's singleton, and the tail reports + // *that* — still the value, not the handle. + assert_eq!(infer_program("a := 7\na").to_string(), "7"); +} + +/// A `Case` arm is a **value** position: rule 2 keeps `Mut` out of every composite and a +/// join is one, so a conditional over two mutable variables denotes the join of their *values*. +/// A handle surviving the join would be a `Mut` with no traceable writer — and it would +/// reach positions rule 2 exists to keep it out of, which is what the tuple here pins. +#[test] +fn a_conditional_over_two_registers_denotes_their_values() { + // `Int` in the first slot is the join of the two mutable variables' values (`1` ⊔ `2`); a + // surviving handle would render `Mut(…)` there. The literal keeps its singleton. + assert_eq!( + infer_program("x := 1\ny := 2\n(x if True else y, 0)").to_string(), + "(Int, 0)" + ); +} From 30e052098311876e0fd68e1d0ede1ad07886abf1 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 12 Aug 2026 22:09:34 -0700 Subject: [PATCH 3/4] Rebase fallout: `Lit` is now imported where this test qualified it The `solve` test module gained a `Lit` import from main, so the path this test spells in full is redundant and `unused_qualifications` rejects it. --- src/ccl/infer/solve.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index e586378e..3b634375 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1986,9 +1986,7 @@ mod tests { let refined = |inner: Type| { Type::Refinement( Box::new(inner), - Refinement::born(std::rc::Rc::new(TypedExpr::lit(crate::ccl::Lit::Bool( - true, - )))), + Refinement::born(std::rc::Rc::new(TypedExpr::lit(Lit::Bool(true)))), ) }; let int = Type::Base(BaseType::Int); From d33d69a39dd85570eed47d9f6e481ac5ba145231 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Thu, 13 Aug 2026 11:59:19 -0700 Subject: [PATCH 4/4] Tests: embedded programs read as programs, not as escaped newlines Every program this branch adds with `\n` becomes an `indoc!` block, per `CLAUDE.md`. --- src/ccl/design/mutability.md | 6 +-- src/ccl/infer/emit.rs | 8 +-- src/ccl/infer/solve.rs | 6 +-- src/ccl/infer/solver/constrain.rs | 2 +- src/ccl/ty.rs | 2 +- tests/compilation_pipeline/mutability.rs | 47 ++++++++++++++--- tests/type_check.rs | 65 ++++++++++++++++++++---- 7 files changed, 107 insertions(+), 29 deletions(-) diff --git a/src/ccl/design/mutability.md b/src/ccl/design/mutability.md index 77d84671..bb6a2baa 100644 --- a/src/ccl/design/mutability.md +++ b/src/ccl/design/mutability.md @@ -111,7 +111,7 @@ about to constrain is a handle position. 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 operand and reads. + 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 @@ -140,7 +140,7 @@ would put a mutable variable *below* its value and `𝑉 <: Mut(𝑉, 𝐷)` wou 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 operand, and `emit_apply` reading +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). @@ -319,7 +319,7 @@ introduction every write targets. The discipline: 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 (each is a - value operand, above), so `x if c else y` reads their values and types as a plain `V`. + 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. diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index 5182c499..8940b33b 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -214,7 +214,7 @@ fn emit_node_inner(expr: &mut Expr, ctx: &mut InferCtx) -> Result( // mutable variable the argument is passed *by reference* and the handle must reach the // parameter, so the invariance rule relates the two value types directly — that is // what makes the callee's writes and the caller's declaration one constraint rather - // than two edges that have to agree. Every other argument is a value operand, so a + // than two edges that have to agree. Every other argument is a value position, so a // mutable variable mention there reads. // // Deciding it here is sound because the parameter is read off the *head of the @@ -654,7 +654,7 @@ pub(super) fn emit_apply( })?; param } - // Every other position is a value operand, so a mutable variable mention reads. + // Every other position is a value position, so a mutable variable mention reads. _ => read_through(&raw_arg_ty), }; // The application's type is the function's codomain with its Pi binder @@ -858,7 +858,7 @@ fn denoted_expr(e: &Expr) -> &Expr { } } -/// Emit a **value operand**: a mutable variable mention here is a *read*, so its handle +/// Emit a **value read**: a mutable variable mention here is a *read*, so its handle /// derefs to the value it holds. /// /// This is the ordinary case. A mutable variable's handle survives in exactly two positions — diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index 3b634375..2a3d734e 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1220,7 +1220,7 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { // hole in that composition.) // // Through the **deref**, because that is what the node's rule reports: an - // effect statement emits its continuation as a value operand + // effect statement emits its continuation in a value position // (`emit_expr_stmt`'s `emit_value_read`), so a tail that reads a mutable variable denotes // the mutable variable's *value*. Lifting `body.ty` verbatim would re-stamp the node // with the handle the read just looked through, contradicting the rule that @@ -1248,7 +1248,7 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { ); } // Dereffed for the same reason as `ExprStmt`: `emit_mut_decl` reports its - // body as a value operand, so `x := 0; …; x` denotes `x`'s value. + // body in a value position, so `x := 0; …; x` denotes `x`'s value. Some(read_through(&body.ty)) } _ => None, @@ -1973,7 +1973,7 @@ mod tests { /// wrong answer is silent in both directions — a value parameter retyped as a /// mutable variable, or a pass-by-reference parameter degraded to a value copy. #[test] - fn a_recovery_reads_a_register_unless_the_position_is_a_handle() { + fn a_recovery_reads_a_mut_var_unless_the_position_is_a_handle() { use super::recovered_input; use crate::ccl::{HistoryKind, Refinement}; let mut_var = |value: Type| Type::History { diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index 9ede75fc..6a8f9518 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -1907,7 +1907,7 @@ mod tests { // `Mut(V) <: V` is no longer a subtyping fact and there is nothing to assert here. // The property they protected — `cnt + 1` yields `Int` rather than leaving a `Mut` // on an inference variable — is now pinned where it is decided: - // `a_register_read_yields_its_value_in_an_operand_position` in `tests/type_check.rs`, + // `a_mut_var_read_yields_its_value_in_a_value_position` in `tests/type_check.rs`, // and the `mutability` integration suite end to end. #[test] diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index e51ab58d..a914316a 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -660,7 +660,7 @@ pub enum Type { /// assembled from an application edge plus a compensating write contribution — the /// shape this needed while a deref coercion erased the handle before invariance /// could see it. The property is still pinned by test - /// (`a_registers_value_type_is_invariant_across_a_mut_parameter`), which is what + /// (`a_mut_vars_value_type_is_invariant_across_a_mut_parameter`), which is what /// would catch a future consolidation quietly dropping one direction. /// /// It is also a **transient** variant like `Hole` / `Infer`: it exists only between type diff --git a/tests/compilation_pipeline/mutability.rs b/tests/compilation_pipeline/mutability.rs index 7e375c10..2053ab86 100644 --- a/tests/compilation_pipeline/mutability.rs +++ b/tests/compilation_pipeline/mutability.rs @@ -917,13 +917,42 @@ fn rule2_function_returning_mut_is_rejected() { /// to a compiler panic, since the lambda's stamped codomain (`Int`) then disagreed /// with its body's own type (`Mut(Int, ?d)`) at the post-inference consistency wall. #[rstest] -#[case::through_a_binding("def f(c: Mut(Int)):\n y = 1\n c\nx := 0\nf(x)")] -#[case::through_a_statement("def f(c: Mut(Int)):\n c += 1\n c\nx := 0\nf(x)")] -#[case::through_a_register_introduction("def f(c: Mut(Int)):\n z := 1\n c\nx := 0\nf(x)")] +#[case::through_a_binding(indoc! {r#" + def f(c: Mut(Int)): + y = 1 + c + x := 0 + f(x) +"#})] +#[case::through_a_statement(indoc! {r#" + def f(c: Mut(Int)): + c += 1 + c + x := 0 + f(x) +"#})] +#[case::through_a_mut_var_introduction(indoc! {r#" + def f(c: Mut(Int)): + z := 1 + c + x := 0 + f(x) +"#})] // A mutable variable does not escape its own introduction either: returning one declared // *inside* the function is the same escape as returning a parameter. -#[case::its_own_register("def g(n):\n z := n\n z\ng(5)")] -#[case::its_own_register_through_a_binding("def g(n):\n z := n\n y = 2\n z\ng(5)")] +#[case::its_own_mut_var(indoc! {r#" + def g(n): + z := n + z + g(5) +"#})] +#[case::its_own_mut_var_through_a_binding(indoc! {r#" + def g(n): + z := n + y = 2 + z + g(5) +"#})] fn rule2_is_not_evaded_by_a_tail_position(#[case] code: &str) { expect_mut_discipline_error(code, "inside a composite type"); } @@ -935,7 +964,13 @@ fn rule2_is_not_evaded_by_a_tail_position(#[case] code: &str) { #[test] fn a_programs_tail_read_of_its_accumulator_is_a_value() { check_scalar( - "x := 0\nfor i in [1, 2, 3]:\n x += i\ny = 1\nx", + indoc! {r#" + x := 0 + for i in [1, 2, 3]: + x += i + y = 1 + x + "#}, cambra::interpreter::Value::Int(6), ); } diff --git a/tests/type_check.rs b/tests/type_check.rs index 8d100521..cf541738 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -399,7 +399,9 @@ fn a_concrete_operand_reaches_its_obligation(#[case] code: &str) { fn mut_var_value_type(code: &str) -> Type { match infer_program(code) { ty @ Type::History { .. } => { - panic!("a tail read must denote the mutable variable's value, got the handle {ty} for `{code}`") + panic!( + "a tail read must denote the mutable variable's value, got the handle {ty} for `{code}`" + ) } value => value, } @@ -2463,13 +2465,27 @@ fn a_single_type_fault_prints_no_demand() { /// that same ordering is what made a pass-by-reference argument indistinguishable from /// a read, since it too meets a fresh variable. #[test] -fn a_register_read_yields_its_value_in_an_operand_position() { - assert_eq!(infer_program("x := 5\nx + 1\n"), int()); +fn a_mut_var_read_yields_its_value_in_a_value_position() { + assert_eq!( + infer_program(indoc! {r#" + x := 5 + x + 1 + + "#}), + int() + ); // The value still has to satisfy the operand's demand: what reaches the operator's // obligation is `String`, the *value* the read yielded, so the implementation table // rejects it at that operand position. A handle arriving here instead would offer no // base at all and the obligation would have nothing to reject. - let errs = format!("{:?}", infer_program_err("x := 5\nx + \"s\"\n")); + let errs = format!( + "{:?}", + infer_program_err(indoc! {r#" + x := 5 + x + "s" + + "#}) + ); assert!( errs.contains("Addable") && errs.contains("String"), "a read's value type is still checked against the operator, got: {errs}" @@ -2480,18 +2496,40 @@ fn a_register_read_yields_its_value_in_an_operand_position() { /// read of its mutable variable denotes that mutable variable's value rather than the handle. /// /// The type a node reports and the type its rule derives have to agree, and a tail's -/// rule emits its continuation as a value operand (`emit_expr_stmt` / `emit_mut_decl`). +/// rule emits its continuation in a value position (`emit_expr_stmt` / `emit_mut_decl`). /// A lift that copied the continuation's type verbatim would re-stamp the node with the /// handle the read just looked through, and the wall that re-runs the rule would then be /// asked to accept a value against a handle — which is not a subtyping fact. #[test] -fn a_tail_read_denotes_the_registers_value() { - assert_eq!(infer_program("a := 0\na := a + 5\na"), int()); +fn a_tail_read_denotes_the_mut_vars_value() { + assert_eq!( + infer_program(indoc! {r#" + a := 0 + a := a + 5 + a + "#}), + int() + ); // Through an intervening statement too — that is the spine link the lift follows. - assert_eq!(infer_program("a := 0\na := a + 5\nb = 1\na"), int()); + assert_eq!( + infer_program(indoc! {r#" + a := 0 + a := a + 5 + b = 1 + a + "#}), + int() + ); // With no write at all the value is the seed's singleton, and the tail reports // *that* — still the value, not the handle. - assert_eq!(infer_program("a := 7\na").to_string(), "7"); + assert_eq!( + infer_program(indoc! {r#" + a := 7 + a + "#}) + .to_string(), + "7" + ); } /// A `Case` arm is a **value** position: rule 2 keeps `Mut` out of every composite and a @@ -2499,11 +2537,16 @@ fn a_tail_read_denotes_the_registers_value() { /// A handle surviving the join would be a `Mut` with no traceable writer — and it would /// reach positions rule 2 exists to keep it out of, which is what the tuple here pins. #[test] -fn a_conditional_over_two_registers_denotes_their_values() { +fn a_conditional_over_two_mut_vars_denotes_their_values() { // `Int` in the first slot is the join of the two mutable variables' values (`1` ⊔ `2`); a // surviving handle would render `Mut(…)` there. The literal keeps its singleton. assert_eq!( - infer_program("x := 1\ny := 2\n(x if True else y, 0)").to_string(), + infer_program(indoc! {r#" + x := 1 + y := 2 + (x if True else y, 0) + "#}) + .to_string(), "(Int, 0)" ); }