From fe19227c0405a75178fb7fa95b90dcb524146243 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 5 Aug 2026 10:57:53 -0700 Subject: [PATCH 1/4] Exact and bounded binder annotations: `x: T` fixes the type, `x <: T` bounds it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CHL gets two binder-annotation forms, meaning the same thing at every binder position: - `x: T` is **exact** — the binder's type *is* `T`. The initializer (or argument) must be a subtype of it, and nothing downstream sees more than `T`. - `x <: T` is **bounded** — the type is inferred with `T` as an upper bound, so the value's own type flows through. Both are accepted wherever a binder is introduced — `=`, `:=`, and `def` parameters — which closes the asymmetry that motivated the work. `def f(v: {a: Int}): v.b` and `x: {a: Int} = (a=1, b=2); x.b` now agree, and both are written with `<:` when the value's wider type should survive. The two forms coincide only where the value's type already **is** the annotation, leaving nothing to discard. They differ wherever the value's type is a *strict* subtype of it, and the annotation's own shape does not decide that — a Cambra type carries more than a base: - **Width.** `x : {a: Int} = (a=1, b=2)` binds `x` at `{a: Int}`, so `x.b` is an error; `x <: {a: Int} = (a=1, b=2)` binds at `{a: 1, b: 2}` and `x.b` is `2`. - **Literal singletons.** `x : Int = 5` binds `x` at `Int` — the annotation is precisely what discards the singleton — while `x <: Int = 5` leaves it at `5`, and only the second still discharges `arr[x]`'s index-range obligation. Note that the second example annotates a bare `Int` and the forms still differ, because `5` is a strict subtype of `Int`. A "simple" annotation is no guarantee that the two agree; only a value that knows nothing beyond the annotation is. **The bounded column is the behaviour both positions already had**, so existing programs keep working under `<:`; what is new is `:` meaning what it says. The whole corpus and test suite needed no migration — only four assertions changed, each asserting the old reading of `:` directly. In annotation position only; `normalize_annotation` erases it into a fresh variable bounded above by `T`. It is `Type::Hole` one rung up — `Hole` is the unbounded case, and the two compose wherever a compound annotation is partly specified. **It is not a type**, and that is the first thing to know about it. `Hole`, `Infer`, and `Below` all inhabit the `Type` enum because annotation and binder positions are typed positions, not because they denote anything: `Below(T)` is not "the type of values below `T`" — no such type exists, since a bound picks out no set of values on its own. It records an obligation, and inference discharges it by minting a variable and giving it `T` as an upper bound, after which the bound lives where bounds belong, on a variable in the constraint graph. So **no typing rule may take a `Below`**: nothing to subtype against, nothing to reduce, nothing to compact, and the solver asserts that at four sites rather than inventing a rule. Only the structural walks that rewrite every slot uniformly — substitution, free-variable collection, refinement stripping — pass through one, because they are indifferent to what a slot means. Putting the bound *in the type* is forced by the **multi-parameter encoding** rather than chosen for symmetry. A `def` with several parameters uncurries to one tuple parameter with a single `Type::Tuple` annotation, so `def f(x: A, y <: B, z)` must express three modes *inside one type*: `Tuple([A, Below(B), Hole])` does it with no new plumbing. Carrying the mode alongside the type would need a mode *tree* mirroring the type's shape — this variant in a worse spelling. A parameter binds at `normalize(annotation)`: exact normalizes to `T` itself, bounded to a variable bounded by `T`. The old two-step — bind at a fresh variable, *then* reconcile against the annotation — is what made an exact annotation behave as neither reading, contributing one upper bound among several instead of *being* the type. `emit_lambda` loses that reconcile entirely. A `let` binds at the same normalization of its completed annotation, and two special cases fall out as consequences rather than tests: a **deref-copy** (`y: Int = x` off a register) binds at the annotation because that is what exact *means*, so the `bound_ty.is_handle()` test is gone; and a bare `_` completes to the initializer's type, so the `annotation_is_unspecified` gate is gone too. Completed structurally from the initializer (`emit::complete_annotation`), so `x: _ = e` is exactly `x = e` and `x: List(_) = [1, 2, 3]` binds at `List(Int)`. It is a function on types rather than a constraint because the constraint version does not work: binding at a normalized annotation and relying on the one-way `rhs <: ann` edge to drive its variables leaves them minted after the RHS's level is popped, so they escape inference unresolved. Records complete by *name*, so a field the annotation omits is dropped rather than completed — exactly the width an exact annotation discards. A parameter has no initializer, so a `Hole` there is a fresh variable resolved from the call sites. `x <: Mut(V) := e` declares a register whose **value type is inferred, subject to `<: V`** — the same declaration as `x <: V := e`, and the same as writing no annotation whenever the inferred type already satisfies `V`. So `x <: Mut(Int) := 5` binds the value at `5`, exactly as the unannotated `x := 5` does, while `x: Mut(Int) := 5` binds it at `Int`. The bound remains an obligation on every contribution to the value type: the seed and each write. The mode has to land on the value because a `Mut(…)` annotation is not lowered as one type — `mut_annotation_parts` splits it into a value type and a domain — so lowering applies the binder's mode to the value it extracts (`apply_annotation_mode`, shared with `lower_type_annotation` and with the pass-by-reference parameter path). That is what makes `<: Mut(V)` and `<: V` agree by construction. The value position is also the *only* place the bound can go, and that is a pipeline fact rather than a variance one. A register binder's slot must stay structurally a `History`: `as_register`, the deref coercion, `mut_elim`, and `transact_phase` all dispatch on that shape, and a variable standing for the whole handle would skip a write's `value <: V` edge, so the register would never receive its writes. The value position carries no such requirement — a variable there is the ordinary case, since an unannotated `x := 5` binds at `Mut(?v, ?d)`. A bound therefore never wraps a history, and `normalize_annotation` asserts it rather than collapsing one: a lowering path that builds a history without routing its annotation through the mode trips the assert instead of silently reading as exact. An exact parameter annotation is a specialization boundary, and it is the only lever a program has over clone count. Measured through the surface: `def f(v <: Int): v + 1` called at `f(1)` and `f(2)` produces **two** specializations — the domain is a variable, so each argument's *literal singleton* reaches `SpecKey`'s negative read — while `def f(v: Int)` produces **one**. Pinned as a test. Two caveats recorded in the design. The win is confined to the domain, and the key's codomain read follows the consumer's demand — deliberately, since a key blind to the consumer would under-split — so the collapse reaches only as far as the consumers agree. And the bounded form is checked per call site rather than once, because `freshen_above` copies the bound into every instantiation. What that no longer has to survive is a *contentless* disagreement in the codomain. Two uses landing in the two operand slots of one `+` reached the enclosing operator's shared `CommonBase(α, β)` requirement from opposite sides and recorded it in opposite argument order, splitting clones of identical code — `f(1) + f(1)` produced two. A symmetric operator's arguments are compared as a multiset now; pinned here alongside the bounded form, which still splits under the same consumer because there the argument reaches the domain. - A bounded parameter's type is still the **meet** of its bound and its body's demands — that is what bounded means, so `def f(v <: {a: Int}): v.b` requires callers to supply both fields. - `<:` is not writable in nested positions, because it describes a *binder*, not a type. `Below` cannot outlive inference: the annotation slots it occupies do not survive it (the base PR clears them), so a binder `ty` is the only place a survivor could hide, where `collect_type_errors` reports `UnresolvedBelow`. That check is a backstop and its test says so — a `Below` reaching the solver un-normalized is rejected earlier, since nothing can be constrained against one. `bind_annotation` now returns the normalized annotation, because normalizing is **not idempotent**: `Hole` and `Below` mint a fresh variable per call, so a caller that both reconciles against an annotation and binds at it must use one normalization or it relates two unrelated variables. A new spec section, "Two annotation forms: exact and bounded", plus corrections to §3.1 (which documented the bounded reading of `:` as the only one) and §4.1 ("they refine the inferred parameter type"). The design of record is a new section in `src/ccl/design/type-inference.md`, committed separately ahead of the implementation. `./ci.sh` green. The register-read cases in the mutability suite carried one `annotated` case written before the split; it becomes two. A **bounded** parameter is inferred with `Int` as an upper bound, so an unwritten register's seed singleton still reaches it. An **exact** parameter is a specialization boundary that fixes the domain at `Int`, so the singleton never arrives — which is the difference worth pinning, and the reason to keep the two side by side. The spec gains a "Two annotation forms: exact and bounded" section covering both forms at every binder, the cases where they differ (width, literal singletons, register value types), `_` as declaring nothing, and the specialization-count consequence. It opens with a note marking the *spelling* `[Open]` while the distinction itself is implemented and pinned by tests. Two things make `:` / `<:` unsatisfying, and they are worth writing down before the tokens harden. `<:` reads as a type operator but describes a **binder**, which is why it cannot appear in a nested position — a restriction that falls out of the implementation rather than out of anything the notation suggests. And the bounded reading is arguably the more common intent, yet it carries the heavier spelling. Nothing in the design depends on which tokens win: the mode is a two-valued property of a binder that lowering reads off the surface and turns into `Below`-or-not, so a respelling is a parser change. `type-inference.md` says so where it introduces the two forms. --- docs/chl-spec.md | 102 ++++++++++- src/ccl/ccl_utils.rs | 9 +- src/ccl/design/type-inference.md | 90 ++++++++++ src/ccl/infer/api.rs | 105 ++++++++---- src/ccl/infer/check.rs | 9 +- src/ccl/infer/context.rs | 45 ++++- src/ccl/infer/emit.rs | 165 +++++++++++++++--- src/ccl/infer/solve.rs | 6 + src/ccl/infer/solver/compact.rs | 5 + src/ccl/infer/solver/constrain.rs | 5 + src/ccl/infer/solver/mod.rs | 4 + src/ccl/infer/solver/scheme.rs | 6 + src/ccl/infer/solver/spec_key.rs | 6 + src/ccl/infer/typing.rs | 11 +- src/ccl/lower/functions.rs | 6 +- src/ccl/lower/loops.rs | 4 +- src/ccl/lower/stmts.rs | 74 ++++++-- src/ccl/subst.rs | 10 ++ src/ccl/ty.rs | 39 +++++ src/chl_parser/ast.rs | 36 +++- src/chl_parser/lexer.rs | 7 + src/chl_parser/parser.rs | 36 ++-- tests/chl_parser_roundtrip.rs | 4 +- tests/compilation_pipeline/mutability.rs | 48 ++++-- tests/type_check.rs | 206 ++++++++++++++++++++++- 25 files changed, 911 insertions(+), 127 deletions(-) diff --git a/docs/chl-spec.md b/docs/chl-spec.md index e4160de7..6cbc3246 100644 --- a/docs/chl-spec.md +++ b/docs/chl-spec.md @@ -628,10 +628,17 @@ of the partiality disappears entirely.) for the unit type `{}` (§6.6). A literal's **type says which literal it is**, not merely its base: `5` has type -`{Int where _ == 5}` (§6.4), the refinement pinning that one value. An annotation -only has to *admit* it — `x: Int = 5` is accepted, widening being the -annotation's business and not the value's. Unit is the exception with nothing to -say: it has one inhabitant, so pinning it would add nothing to the base. +`{Int where _ == 5}` (§6.4), the refinement pinning that one value. So `x = 5` +gives `x` the type `5`, and it keeps that unless a binder discards it: +`x: Int = 5` binds `x` at `Int` (an exact annotation *is* the binder's type), +while `x <: Int = 5` leaves `x` at `5` (a bounded annotation only has to admit +the value) — see +[Two annotation forms: exact and bounded](#two-annotation-forms-exact-and-bounded). Any +operation that computes a *new* value drops it, since it is a fact about one +value and not about the operation: `x + x` is an `Int`, and a mutable register +never takes it (a register is the sequence its writes produce, so no one write's +value describes it). Unit is the exception with nothing to say: it has one +inhabitant, so pinning it would add nothing to the base. > **Direction [Decided] — `true`/`false`.** The boolean literals are spelled > `True`/`False` today, the one exception to the capitalization rule above. They @@ -1054,8 +1061,11 @@ def f(x: Int, y): return x + y ``` -Annotations are arbitrary expressions evaluated in the surrounding -scope; they refine the inferred parameter type. Annotations on the +Annotation types are arbitrary expressions evaluated in the surrounding +scope. `p: T` fixes the parameter's type at `T`; `p <: T` leaves it +inferred and bounded above by `T` (see +[Two annotation forms: exact and bounded](#two-annotation-forms-exact-and-bounded)). +The two forms may be mixed across a parameter list. Annotations on the function's *return type* are not yet supported. A function whose body contains a `yield` expression anywhere is a @@ -1522,8 +1532,9 @@ read-only. This section is a sketch. The authoritative type system lives in [`src/ccl/infer/`](../src/ccl/infer/) — see [src/ccl/design/type-inference.md](../src/ccl/design/type-inference.md). -CHL types are inferred; user-written annotations refine the inferred -type. +CHL types are inferred; a user-written annotation either *fixes* the +binder's type or *bounds* it — see +[Two annotation forms: exact and bounded](#two-annotation-forms-exact-and-bounded). Built-in surface types. (The names below are this spec's vocabulary for talking about the checker; annotations are writable on `def` @@ -1641,6 +1652,81 @@ element `{T,}`), record type `{f: T}`, variant type > instead of repeating asserts at every function; the declaration > syntax for that invariant is not yet settled. +### Two annotation forms: exact and bounded + +An annotation at a binder answers one of two questions, and the two +have different spellings because the answers differ. + +> **Note.** The *distinction* below is implemented and pinned by tests — +> that a binder can either fix its type or bound it, and what each means +> at every binder form. The **spelling** is **[Open]**: `:` versus `<:` +> is not a syntax we are satisfied with, and it may change without the +> semantics changing. Two things make it unsatisfying. `<:` reads as a +> type operator but describes a *binder*, which is why it cannot be +> written in a nested position — a restriction that falls out of the +> implementation rather than out of anything a reader would expect from +> the notation. And the more common intent is arguably the bounded one, +> yet it carries the heavier spelling. Read the semantics as settled and +> the two tokens as provisional; code written against them may need a +> mechanical rename. + +`x: T` is **exact**: the binder's type *is* `T`. The initializer (or, +at a parameter, the argument) must be a subtype of `T`, and nothing +downstream of the binder sees more than `T`. + +`x <: T` is **bounded**: the binder's type is *inferred*, with `T` as +an upper bound. The value's own type flows through; `T` only +constrains what may reach the binder. + +Both forms are accepted wherever a binder is introduced — an +assignment (`x: T = e`, `x <: T = e`), a mutable introduction +(`x: Mut(V) := e`), and a `def` parameter — and mean the same thing in +each. `<:` is **not** written in nested positions: it describes a +binder, not a type, so `{a <: Int}` is not a type. + +The two coincide only when the value's type already **is** the +annotation — when there is nothing for the annotation to discard. They +differ whenever the value's type is a *strict* subtype of it, which is +more often than it sounds, because a CHL type carries more than a base: + +- **Width.** `x: {a: Int} = (a=1, b=2)` binds `x` at `{a: Int}`, so + `x.b` is an error — the annotation is what discards the field. + `x <: {a: Int} = (a=1, b=2)` binds `x` at `{a: 1, b: 2}`, and `x.b` + is `2`. +- **Literal singletons** (§3.1). `i: Int = 0` binds `i` at `Int`; + `i <: Int = 0` leaves it at `0`. Only the second still carries the + fact a totality proof needs, so an exact annotation on an index + discards the proof that a lookup is in range. + +Note that the second example annotates a bare `Int` and the two forms +still differ. The annotation's own shape is not what decides it: `0` is +a strict subtype of `Int`, so there is something to discard. What makes +the forms coincide is the *value* knowing nothing beyond what the +annotation says. + +A `_` position **declares nothing** and is completed from the +initializer, so `x: _ = e` means exactly `x = e`. That holds nested +too: `x: List(_) = [1, 2, 3]` binds `x` at `List(Int)`. Consequently +`_` does not suppress the mutable-alias rule (§8.1): `b: _ = a` off a +mutable `a` is the same error as a bare `b = a`. + +On a mutable introduction the mode applies to the **value type**, which +is what the annotation names: `x <: Mut(V) := e` declares a mutable +whose value type is inferred subject to `<: V`, and is the same +declaration as `x <: V := e`. So `x <: Mut(Int) := 5` binds the value at +`5` — as the unannotated `x := 5` does — while `x: Mut(Int) := 5` binds +it at `Int`. The bound still constrains every contribution to the value: +the seed and each write. + +> **Note.** An exact parameter annotation also fixes how many times +> the function is compiled. A bounded or absent one leaves the +> parameter's type open, so each call site's argument type — down to +> *which literal* it is — can produce its own specialization; an exact +> one gives every call site one shared definition. Recommended style +> therefore annotates a top-level `def`'s parameters exactly and +> reaches for `<:` where a caller's more precise type has to survive +> the boundary. + ### 6.2 Non-purity as type wrappers (2026-06-29 §4.) diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs index b5727136..380d5913 100644 --- a/src/ccl/ccl_utils.rs +++ b/src/ccl/ccl_utils.rs @@ -683,14 +683,17 @@ pub fn refined_data_fun(base_domain: Type, predicate: Expr, codomain: Type) -> T /// it wanting are elsewhere: /// /// - "these are related on their base, not on their refinements" during inference: -/// a [`TypeFn`](crate::ccl::TypeFn) over the positions, whose rule defers the same -/// question until the arguments resolve. `Arithmetic`'s does exactly this, via -/// `shared_base`. +/// a trait obligation over them, which defers the same question until the operands +/// resolve and reads the base off each as it arrives +/// ([`solver::traits`](crate::ccl::infer::solver::traits)). /// - "look *past* the outer layers" — what a shape test wants, since a refinement is /// not part of the shape: [`Type::peel_refinements`](crate::ccl::Type::peel_refinements), /// which borrows rather than dropping. pub(crate) fn strip_refinements(ty: &Type) -> Type { match ty { + // Annotation-position only, and structural: keep the wrapper and strip + // inside it, so a bounded annotation's bound is stripped like any other. + Type::Below(t) => Type::Below(Box::new(strip_refinements(t))), Type::Refinement(base, _) => strip_refinements(base), Type::Fun { domain, codomain, .. diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index 3584cfd7..1f926cc6 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -125,6 +125,7 @@ def identity(x): **Implemented today:** * **Let-polymorphism (functions).** A `let` whose RHS is a *function definition* is generalized: the RHS is typed one level deeper, generalized into a `PolyScheme` at the binding site, and instantiated freshly per use. Because Cambra targets fully-monomorphized output, generalization is paired with **monomorphization**, integrated into the coalesce walk (`infer::specialize_use`): a use of a generalized binding is specialized at first visit — clone + `freshen_expr_type_slots`, a two-way pin against the use's *live* instantiation type, and a re-entrant coalesce of the clone — and the binding's `let` rebuilds itself as the chain of demanded specializations. Specialization is keyed on the use's **instantiation identity** (a `SpecKey`, not a resolved type — see [Keying a specialization](#keying-a-specialization)), so uses that instantiate the definition identically **share** one definition. So `def f(x): x == x; f(1); f("foo")` type-checks and runs, a generator used at two element types compiles to two cached specializations (see F2), and a generalized UDF used only inside *another* generalized definition (poly-calls-poly) specializes by plain recursion — its use becomes concrete inside each wrapper clone's re-entrant walk. Levels are live (extrude fires on a genuine level mismatch). +* **Two binder-annotation forms.** Exact `𝑥 : 𝑇` fixes the binder's type; bounded `𝑥 <: 𝑇` infers it under an upper bound. Both apply at `let` and at a function parameter, carried by `Type::Below` in annotation position and erased by `normalize_annotation`. See [Annotation kinds: exact and bounded](#annotation-kinds-exact-and-bounded). * **Tagged variants.** The dual of records, natively supporting sum types and pattern-match exhaustiveness inside the structural solver (see §4). Both named (`.Tag(...)`) and positional (`++`-style) sums are handled. * **Lattice-carried refinements.** Refinements ride the lattice natively (compared by structural predicate equality) rather than being stitched on by a post-pass; see §4 and [`crate::ccl::infer::solver`]'s `# Refinements`. * **Dependent refinements (Pi types).** Refinement predicates may close over an outer binder; `Type::Fun` carries an optional Pi binder, the solver derives binder correspondences when constraining function types, and dependent application discharges the binder to its argument at coalesce. Group-by lookup `groupby(xs, key)(𝑘₀)` types as `{𝑖 | 𝑖 ▷ xs ▷ key == 𝑘₀} ⇒ 𝑉`. See §4.5. @@ -761,11 +762,100 @@ Both readers compensated by consulting `user_annotation`, which held the user's Nothing has to outlive the annotation. The one fact a later pass used to need from it — *is this binder a mutable variable?* — is answered structurally instead: only `MutDecl` (a `:=` introduction) and a pass-by-reference `Lambda` param bind one, and a `Let` cannot, because `emit_let` reads through an initializer that is a mutable variable. That retired the `Mut` discipline's rule 3 along with the bit that stood in for the declaration (see `src/ccl/design/mutability.md`, "No aliasing: `Mut` values are second-class (downward-only)"). +### Annotation kinds: exact and bounded + +An annotation at a binder answers one of two different questions, and CHL spells them differently because the answers diverge. + +`𝑥 : 𝑇` is **exact**: the binder's type *is* `𝑇`. The initializer (or, at a parameter, the argument) must satisfy `rhs <: 𝑇`, and everything downstream of the binder sees `𝑇` — the value's own type is not observable through it. + +`𝑥 <: 𝑇` is **bounded**: the binder's type is *inferred*, with `𝑇` as an upper bound. The value's own type flows through; `𝑇` only constrains what may reach the binder. + +The two coincide only where the value's type already *is* the annotation, leaving nothing to discard. They differ wherever the value's type is a **strict** subtype of it — and the annotation's own shape does not decide that, because a Cambra type carries more than a base: + +* **Width.** `x : {a: Int} = (a=1, b=2)` binds `x` at `{a: Int}`, so `x.b` is an error. `x <: {a: Int} = (a=1, b=2)` binds `x` at `{a: 1, b: 2}`, and `x.b` is `2`. +* **Refinements.** A literal is typed by its own value ([A literal is refined by its own value](#a-literal-is-refined-by-its-own-value)), so `x : Int = 5` binds `x` at `Int` — the annotation is precisely what discards the singleton — while `x <: Int = 5` leaves it at `5`. Only the second still discharges `arr[x]`'s index-range obligation. + +The refinement case is worth reading twice: the annotation is a bare `Int` and the forms still differ, because `5` is a strict subtype of `Int`. A "simple" annotation is no guarantee that the two agree — only a value that knows nothing beyond the annotation is. + +Both kinds apply at both binder positions, `let` and function parameter, with one rule each. The *distinction* is settled and implemented; the two **spellings** are provisional, and the spec records them as `[Open]` ([chl-spec.md](../../../docs/chl-spec.md), "Two annotation forms: exact and bounded"). Nothing below depends on which tokens win: the mode is a two-valued property of a binder that lowering reads off the surface and turns into `Below`-or-not, so a respelling is a parser change. + +| | `𝑥 : 𝑇` (exact) | `𝑥 <: 𝑇` (bounded) | +|---|---|---| +| `let` | bind at `𝑇`; require `rhs <: 𝑇` | bind at the inferred RHS type; require it `<: 𝑇` | +| parameter | bind at `𝑇`; every call site requires `arg <: 𝑇` | bind at a fresh variable; require it `<: 𝑇` | + +The bounded column is the *only* behaviour that existed before the split, at both positions: a binder annotation contributed one upper bound and nothing else, because `bind_annotation` is one-way (`inferred <: ann` — an annotation has to admit the value, not equal it). A parameter's type was therefore the **meet** of its annotation and whatever its body demanded, which is worth stating plainly because it is neither of the two readings one expects: in `def f(v <: {a: Int}): v.b`, the annotation admits the argument and the projection widens the demand, so `𝑣` ends up at `{a: Int, b: 𝑇}` and callers must supply both fields. That is still what the bounded form means; the split gave it its own spelling and gave `:` the exact reading. + +Neither rule needs a mode test at its binder. A parameter binds at `normalize(annotation)`: exact normalizes to `𝑇` itself, bounded to a variable bounded by `𝑇`, and the old two-step (bind at a fresh variable, *then* reconcile against the annotation) is what made an exact annotation behave as neither reading — it contributed one upper bound among several instead of being the type. A `let` binds at the same normalization of its (completed) annotation, and two special cases fall out as consequences rather than tests: a **deref-copy** (`y: Int = x` off a register) binds at the annotation because that is what exact *means*, and a bare `_` completes to the initializer's type — so it stays a register, and the mutable-alias rule still rejects `y: _ = x`. + +#### Below is a marker in a type slot, not a type + +The bounded form is represented by a `Type::Below(𝑇)`, which `normalize_annotation` erases into a fresh variable carrying `𝑇` as an upper bound. It is the same kind of object as `Type::Hole` one rung up: `Hole` is the unbounded case, and the two compose in exactly the positions where a compound annotation is partly specified. + +Neither is a type, and that is the first thing to know about `Below`. `Hole`, `Infer`, and `Below` all inhabit the `Type` enum because *annotation and binder positions are typed positions*, not because they denote anything: `Below(𝑇)` is not "the type of values below `𝑇`" — no such type exists, since a bound picks out no set of values on its own. It records an obligation for inference to discharge, and inference discharges it by minting a variable and giving it `𝑇` as an upper bound; the bound then lives where bounds belong, on a variable in the constraint graph. + +The consequence is that no *typing* rule may take a `Below`. There is nothing to subtype against, nothing to narrow, nothing to compact — the solver asserts this rather than inventing a rule (`constrain::extrude`, `compact`). Only the structural walks that rewrite every slot uniformly — substitution, free-variable collection, refinement stripping — pass through one, and they do so because they are indifferent to what a slot means. + +Putting the bound *in the type* rather than beside it is forced by the **multi-parameter encoding**, not chosen for symmetry. A `def` with more than one parameter uncurries to a single tuple parameter whose annotation is one `Type::Tuple`, with `Hole` at each unannotated position (`lower::functions::uncurry_params`). So `def f(x: 𝐴, y <: 𝐵, z)` has to express three distinct annotation modes *inside one type*, and `Tuple([𝐴, Below(𝐵), Hole])` does it with no new plumbing. Carrying the mode alongside the type instead would need a mode *tree* mirroring the type's shape, which is this variant in a worse spelling. + +#### Below cannot outlive inference + +`Below` is inference's to erase: Pass 1 replaces it with an `Infer` variable, and nothing downstream can observe one — not by convention but because **the slot it would live in does not survive inference at all**. See [The binder slot, and why annotations do not outlive inference](#the-binder-slot-and-why-annotations-do-not-outlive-inference); the bounded form needs no lifecycle rule of its own. + +That the slot does not survive is what makes the guarantee structural, and following `Hole`'s precedent instead would *not* have sufficed. `Hole`'s discipline is erasure plus a check on `ty` slots (`UnresolvedHole`) — which leaves annotation slots covered by neither, so an un-erased marker can sit in one to the end of inference whenever a compound annotation is partly unspecified. That is survivable for `Hole`, which means "unspecified" and is read as such; it is not survivable for `Below`, which carries a *bound* that something must discharge. A marker whose whole content is a constraint cannot be left somewhere nothing looks. + +The remaining backstop is therefore narrow: a binder `ty` is the only slot a `Below` could reach, and `collect_type_errors` reports `UnresolvedBelow` there. Nothing is expected to trip it — a `Below` reaching the solver un-normalized fails earlier, since there is no rule for constraining against one. + +#### A Hole inside an exact annotation is still inferred + +An exact annotation may be partly unspecified — `x: List(_) = [1, 2, 3]`, or the `Feed(_)` bindings the corpus uses. A `Hole` there means "infer this position", so the binder's type is the annotation **with each `Hole` filled from the corresponding position of the inferred RHS type** (`emit::complete_annotation`). That makes `x: _ = e` exactly equivalent to `x = e`, and `x: List(_) = [1, 2, 3]` bind at `List(Int)`. Records complete by *name*, so a field the annotation does not mention is dropped rather than completed — which is exactly the width an exact annotation discards. A **parameter** has no initializer to complete from, so a `Hole` there is simply a fresh variable resolved from the call sites. + +The filling is a structural function on the two types, deliberately not a constraint: binding at a normalized annotation and relying on the one-way `rhs <: ann` edge to drive the annotation's fresh variables does *not* work — those variables are minted at the outer level, after the RHS's level has been popped, and escape inference unresolved. Shape disagreements need no handling here, because a `rhs` that cannot flow into `ann` at all is already an `AnnotationMismatch`. + +#### A bound on a register bounds its value type + +`𝑥 <: Mut(𝑉) := 𝑒` declares a register whose **value type is inferred, subject to +`<: 𝑉`** — the same declaration as `𝑥 <: 𝑉 := 𝑒`, and the same as writing no +annotation whenever the inferred type already satisfies `𝑉`. Lowering applies the +binder's mode to the value type it extracts from the annotation +(`lower::stmts::apply_annotation_mode`), so a bounded register arrives as +`Mut(Below(𝑉), 𝐷)` and the bound is consumed in the value position like any other. + +The value position is the only place the bound can go, and that is a fact about the +pipeline rather than about variance. A register binder's slot must stay structurally +a `History`: `as_register`, the deref coercion in `constrain`, `mut_elim`, and +`transact_phase` all dispatch on that shape, and a variable standing for the whole +handle would skip a write's `value <: 𝑉` edge, so the register would never receive +its writes. The value position carries no such requirement — a variable there is the +*ordinary* case, since an unannotated `x := 5` binds at `Mut(?v, ?d)` — and it is +where a strict subtype can differ at all. + +Distributing is also what makes the bound mean *bounded*. A register's value type is +invariant in **subtyping between two registers** — the call-site rule relating a +caller's register to a `Mut` parameter, where covariance would let a callee narrow a +value the caller's declaration still promises. That is a different question from +bounding one register's own value, and treating them as the same made +`x <: Mut(Int) := 5` bind at `Mut(Int)`: it discarded the singleton that the wholly +unannotated `x := 5` keeps — a register's value type is the join over its seed and +every write, so a single contribution keeps its refinement and `x := 1` is a +`Mut(1)`. The bound *lost* information rather than admitting it. + +#### Exact annotations bound monomorphization + +An exact parameter annotation is the program's only lever over specialization count, and this is the sharpest practical consequence of the split. + +Specialization is keyed on instantiation identity ([Keying a specialization](#keying-a-specialization)), whose negative read follows a domain's *lower* bounds — the argument that flowed in. With a bounded (or absent) parameter annotation the domain is a variable, so each call site's argument type reaches the key, and the definition splits **per distinct argument type, including per literal value**: `let f = λ 𝑣 → 𝑣 + 1 in let a = f(1) in let b = f(2) in a` yields two clones of one body, distinguished only by the singletons `1` and `2`. + +An exact annotation binds the parameter at a concrete, level-0 type. `freshen_above` short-circuits it, every instantiation shares one domain, no argument refinement can reach the domain position, and the uses collapse to a single specialization. + +Two caveats keep that from being a blanket guarantee. First, the win is confined to the domain, and the key's *codomain* read follows the consumer's demand — deliberately, since the clone is coalesced under this use's pin and a key blind to the consumer would under-split. So an exact annotation collapses the uses only as far as their consumers agree. Second, the bounded form is genuinely per-call-site checked rather than checked once: `freshen_above` copies a variable's bounds, so the `<: 𝑇` obligation is instantiated with each use and enforced at every argument position. + ### Flowing In: normalizing annotations There is no conversion *into* a solver type — the solver consumes `ccl::Type` as-is. The only adjustment Pass 1 makes is `normalize_annotation`, which readies a user annotation / expected type for constraint solving: * **Holes (`Type::Hole`):** become fresh `Type::Infer` variables at the current level. +* **Bounds (`Type::Below(𝑇)`):** become fresh `Type::Infer` variables at the current level, carrying `𝑇` as an upper bound — `Hole` with a ceiling (see [Annotation kinds: exact and bounded](#annotation-kinds-exact-and-bounded)). * **Refinements:** are **kept** (recursing to normalize the inner) — they ride the lattice natively (above). A `Refinement(Hole, r)` source annotation thus becomes `Refinement(?fresh, r)`. * **Everything else** — including existing `Type::Infer` vars, `Tuple`/`Record` products, and `Type::Variant` sums — is kept verbatim and handled by the solver's structural constraint rules. Tuples and records are width-subtyped positionally/by name; variants are admissible at both polarities (the dual of records), so they need no fresh-var indirection. diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index 7db70c4b..10121c07 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -346,6 +346,15 @@ pub enum InferError { /// Display label for the message (see the type docs — not the location). at: String, }, + /// A [`Type::Below`] bounded-annotation marker survived past inference. + /// + /// Like [`InferError::UnresolvedHole`], a compiler bug rather than a + /// user-facing error: `normalize_annotation` erases every `Below` it is handed, + /// so a survivor means a slot inference never normalized. + UnresolvedBelow { + /// Display label for the message (see the type docs — not the location). + at: String, + }, /// An unresolved [`Type::Infer`] variable survived past inference. UnresolvedInfer { /// The unresolved variable's id. @@ -666,6 +675,9 @@ impl std::fmt::Debug for InferError { InferError::UnresolvedHole { at } => { write!(f, "Unresolved type hole in expression: {at}") } + InferError::UnresolvedBelow { at } => { + write!(f, "Unresolved bounded annotation `<:` in expression: {at}") + } InferError::UnresolvedInfer { id, at } => { write!(f, "Unresolved inference variable {id} in expression: {at}") } @@ -1031,6 +1043,12 @@ fn collect_type_errors( Type::Hole | Type::SharedHole(_) => errors.push(InferError::UnresolvedHole { at: context_sym.to_string(), }), + // A bounded annotation inference never normalized. Reported at every + // strictness, exactly like `Hole`: both are lowering markers whose whole + // contract is that inference consumes them. + Type::Below(_) => errors.push(InferError::UnresolvedBelow { + at: context_sym.to_string(), + }), Type::Infer(var) => { // Pre-desugar, an induction accumulator's domain is still `Infer` (a // `Mut(V)` with no annotated domain — the unified phase resolves it @@ -2561,38 +2579,51 @@ mod tests { // AnnotationMismatch: user_annotation conflicts with inferred type // ----------------------------------------------------------------------- - /// Constructs a `Lambda` with `user_annotation: Some(Int)` but a body that - /// constrains the param to `String`. Inference should return `AnnotationMismatch`. + /// A parameter annotation conflicting with the body's demand is caught, and + /// **which** error it is follows from the annotation's form. /// - /// This path is not yet reachable from the pipeline (lowering always sets - /// `user_annotation: None`), but the conflict must be exercised directly so the - /// annotation-binding rule does not bitrot. - #[test] - fn test_infer_annotation_mismatch() { - let mut ctx = TypeInferenceContext::new(); - // λ [x : annotated Int] → Apply(λ s : String → s, x) - // x starts as Infer(id); body inference applies x as an arg to a - // String-expecting function, constraining Infer(id) → String. - // - // The conflict surfaces at **coalesce**, as `Int` and `String` colliding on - // one variable, rather than eagerly as `AnnotationMismatch`. That is the - // consequence of `bind_annotation` being one-way (`inferred <: ann`): the - // reverse edge used to detect this immediately, at the cost of also - // rejecting sound widenings. What matters is that the conflict is caught. - let inner = Expr::lambda("s", Type::Base(BaseType::String), Expr::var("s")); - let mut expr = TypedExpr::new(TypedExprNode::Lambda { - param: TypedBinding { - name: "x".into(), - ty: Type::infer(), - user_annotation: Some(Type::Base(BaseType::Int)), - }, - body: Box::new(Expr::apply(Expr::var("x"), inner)), - }); - let errs = infer_bare(&mut expr, &mut ctx).expect_err("Int and String cannot meet"); + /// `λ [x : Int] → x(λ s : String → s)`: the body uses `x` where a `String` is + /// expected, while the annotation says `Int`. + /// + /// Under the **exact** form the parameter *is* `Int` — a concrete type, not a + /// variable — so the body's demand fails immediately at the application, naming + /// both types. Under the **bounded** form the parameter is a variable carrying + /// `Int` as an upper bound, so `Int` and `String` accumulate on that one + /// variable and the conflict surfaces at coalesce as `IncompatibleBounds`. + /// Neither is more correct; the exact form simply localizes the blame to the + /// use, because there is no variable for the two demands to meet on. + #[test] + fn test_infer_param_annotation_conflict() { + let param_annotation = |ann: Type| { + let mut ctx = TypeInferenceContext::new(); + let inner = Expr::lambda("s", Type::Base(BaseType::String), Expr::var("s")); + let mut expr = TypedExpr::new(TypedExprNode::Lambda { + param: TypedBinding { + name: "x".into(), + ty: Type::infer(), + user_annotation: Some(ann), + }, + body: Box::new(Expr::apply(Expr::var("x"), inner)), + }); + infer_bare(&mut expr, &mut ctx).expect_err("Int and String cannot meet") + }; + + let exact = param_annotation(Type::Base(BaseType::Int)); assert!( - errs.iter() + exact + .iter() + .any(|e| matches!(e, InferError::TypeMismatch { .. })), + "an exact param is the concrete type, so the body's demand fails at the \ + use; got {exact:?}" + ); + + let bounded = param_annotation(Type::Below(Box::new(Type::Base(BaseType::Int)))); + assert!( + bounded + .iter() .any(|e| matches!(e, InferError::IncompatibleBounds { .. })), - "expected the Int/String collision, got {errs:?}" + "a bounded param is a variable, so the two demands collide on it at \ + coalesce; got {bounded:?}" ); } @@ -2918,6 +2949,22 @@ mod tests { assert_eq!(check_fully_typed(&expr), Ok(())); } + /// A `Type::Below` surviving inference fails with `UnresolvedBelow`. + /// + /// A backstop, like `UnresolvedHole`: `normalize_annotation` erases every + /// `Below` it is handed, and a bounded annotation that somehow reaches the + /// solver un-normalized is rejected earlier (nothing can be constrained against + /// a `Below`, so it surfaces as an `AnnotationMismatch`). This pins the check + /// itself, which the pipeline therefore cannot reach. + #[test] + fn test_check_fully_typed_below_survivor() { + let expr = Expr::lit(Lit::Int(1)).with_ty(Type::Below(Box::new(Type::Base(BaseType::Int)))); + assert_eq!( + check_fully_typed(&expr), + Err(vec![InferError::UnresolvedBelow { at: "1".into() }]) + ); + } + /// A `Type::Hole` on the root node fails with `UnresolvedHole`. /// /// The context string is the symbolic representation of the offending expression, diff --git a/src/ccl/infer/check.rs b/src/ccl/infer/check.rs index eeca7293..c031e9b4 100644 --- a/src/ccl/infer/check.rs +++ b/src/ccl/infer/check.rs @@ -244,10 +244,13 @@ impl Typing for CheckCtx { } } - fn bind_annotation(&mut self, _inferred: &Type, _ann: &Type) -> Result<(), LocatedInferError> { + fn bind_annotation(&mut self, _inferred: &Type, ann: &Type) -> Result { // The annotation was already folded into the binder's type during - // inference; nothing to re-check here. - Ok(()) + // inference; nothing to re-check here. Check's `normalize` is the + // identity, so handing the annotation straight back matches what Emit + // returns for an annotation with nothing left to normalize. (In practice + // Check never sees one: `infer` clears every annotation on success.) + Ok(ann.clone()) } fn binding_slot(&mut self, slot: &mut Type) -> Type { diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs index fa451b50..0642e5ce 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -179,6 +179,47 @@ impl InferCtx { .entry(*id) .or_insert_with(|| fresh_var(self.level)) .clone(), + // A bounded annotation `𝑥 <: 𝑇` means "infer this, subject to `<: 𝑇`" + // → the same fresh variable, carrying `𝑇` as an upper bound. This is + // the *only* place `Below` is consumed; every other pass either + // rewrites through it structurally or treats it as unreachable. + // + // A bound never wraps a **history**: lowering applies a binder's mode to + // the history's *value* type (`lower::stmts::apply_annotation_mode`), so + // `x <: Mut(V) := e` arrives as `Mut(Below(V), D)` and the `Below` is + // consumed by the value position below. + // + // That is not merely where it happens to sit — it is the only place it + // can. A register binder's slot must stay structurally a `History`: + // `as_register`, the deref coercion, `mut_elim`, and `transact_phase` all + // dispatch on the shape, and a variable standing for the whole history + // would skip a write's `value <: V` edge, so the register would never + // receive its writes. The value position has no such constraint — a + // variable there is the ordinary case, since an unannotated `x := 5` binds + // at `Mut(?v, ?d)` too — and it is where a strict subtype can differ at + // all. A wrapper here means a lowering path built a history without + // routing its annotation through the mode. + Type::Below(bound) if bound.is_handle() => { + unreachable!( + "a bounded annotation wraps a history ({bound}); lowering applies \ + the binder's mode to the history's value type instead" + ) + } + Type::Below(bound) => { + let v = fresh_var(self.level); + let bound = self.normalize_annotation(bound); + // A **local** cache, not `self.cache`: this method takes `&self`, + // and the memo exists only to break recursion on cyclic bounds. + // `v` is brand new, so the sole action is pushing one upper edge — + // there are no lower bounds to close against and nothing to + // recurse into, so a fresh memo is equivalent to the shared one. + // + // The result is discarded because a fresh variable cannot conflict + // with its first upper bound; a genuine mismatch surfaces later, + // when a value flows in and fails against this bound. + let _ = constrain_subtype(&v, &bound, &mut ConstrainCache::new()); + v + } // Refinements ride the lattice: keep the wrapper, normalize the // inner (so a `Refinement(Hole, r)` source annotation becomes // `Refinement(?fresh, r)` rather than losing the refinement). @@ -395,7 +436,7 @@ impl Typing for InferCtx { body_ty } - fn bind_annotation(&mut self, inferred: &Type, ann: &Type) -> Result<(), LocatedInferError> { + fn bind_annotation(&mut self, inferred: &Type, ann: &Type) -> Result { // Shared by *binder* annotations (trait call sites in the emit rules) // and *node* annotations (`emit_node`'s `user_annotation` tail) — the // reconciliation is identical: annotation wins on success, conflict @@ -429,7 +470,7 @@ impl Typing for InferCtx { inferred: inferred_ty, }) })?; - Ok(()) + Ok(ann_simple) } fn binding_slot(&mut self, slot: &mut Type) -> Type { diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index 8940b33b..3c6af0a7 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -317,6 +317,10 @@ fn stamp_kind_from(target: &mut Type, reference: &Type) { /// place ([`emit_bare_predicate`]) so the typed term lands on the annotation. fn emit_annotation_predicates(ty: &mut Type, ctx: &mut InferCtx) -> Result<(), LocatedInferError> { match ty { + // Runs *before* `normalize_annotation`, so a bounded annotation is still a + // `Below` here: recurse into the bound, or a predicate written inside one + // (`x <: {Int | p}`) never gets typed. + Type::Below(bound) => emit_annotation_predicates(bound, ctx), Type::Refinement(inner, r) => { // The annotation's refinement is bare over REFINEMENT_BINDER, just // like a cast target's — bind the element over the refined base and @@ -470,18 +474,125 @@ fn apply_unary_scheme( Ok(result) } +/// Complete an **exact** annotation with the type inferred for its initializer: +/// every unspecified position (`_`, a [`Type::Hole`]) takes the corresponding +/// position of `inferred`. +/// +/// `x: T = e` binds `x` at `T`, but an annotation may be only *partly* specified +/// — `x: List(_) = […]`, or the `Feed(_)` bindings the corpus uses — and there a +/// `Hole` means "infer this position", exactly as it does when it stands alone +/// (`x: _ = e` is then equivalent to `x = e`). +/// +/// This is a structural function rather than a constraint, and deliberately so: +/// binding at a *normalized* annotation and relying on the one-way `inferred <: +/// ann` edge to drive its fresh variables does not work — they are minted at the +/// outer level, after the RHS's level has been popped, and escape inference +/// unresolved. +/// +/// Positions where the two shapes disagree keep the annotation's: a value that +/// cannot flow into its annotation at all is already an `AnnotationMismatch`, so +/// there is no second diagnosis to make here. +fn complete_annotation(ann: &Type, inferred: &Type) -> Type { + match (ann, inferred) { + (Type::Hole, _) => inferred.clone(), + // A refinement's base can be the unspecified part (`{_ | p}`); the + // refinement itself is the user's claim and is kept. `peel_refinements` + // on the inferred side because its own refinements describe the *value*, + // and this is filling in a *shape*. + (Type::Refinement(base, r), _) => Type::Refinement( + Box::new(complete_annotation(base, inferred.peel_refinements())), + r.clone(), + ), + // The arrow's binder and kind come from the *annotation*, per the rule + // above: a kind is something an annotation can state (`List(T)` is a data + // arrow by construction), so it is a claim to keep rather than a shape to + // fill in. + ( + Type::Fun { + domain: ad, + codomain: ac, + .. + }, + Type::Fun { + domain: id, + codomain: ic, + .. + }, + ) => Type::fun_like( + ann, + complete_annotation(ad, id), + complete_annotation(ac, ic), + ), + (Type::Tuple(ats), Type::Tuple(its)) if ats.len() == its.len() => Type::Tuple( + ats.iter() + .zip(its) + .map(|(a, i)| complete_annotation(a, i)) + .collect(), + ), + // Records match by *name*, not position, and width-subtyping means the + // inferred record may carry fields the annotation does not mention. Those + // are exactly what an exact annotation discards, so only the annotated + // fields are completed. + (Type::Record(afs), Type::Record(ifs)) => Type::Record( + afs.iter() + .map(|(n, a)| { + let i = ifs.iter().find(|(m, _)| m == n).map(|(_, t)| t); + ( + n.clone(), + i.map_or_else(|| a.clone(), |i| complete_annotation(a, i)), + ) + }) + .collect(), + ), + ( + Type::History { + value: av, + domain: ad, + kind, + }, + Type::History { + value: iv, + domain: id, + .. + }, + ) => Type::History { + value: Box::new(complete_annotation(av, iv)), + domain: Box::new(complete_annotation(ad, id)), + kind: *kind, + }, + _ => ann.clone(), + } +} + pub(super) fn emit_lambda( param: &mut TypedBinding, body: &mut Expr, ctx: &mut C, ) -> Result { - // Param type: convert any explicit annotation/Hole/Infer into a - // the solver. A Hole turns into a fresh Var that will accumulate - // bounds from body usage and call sites. Link `param.ty` to that - // (shared) var so `coalesce_node` can resolve the binding slot in - // place. Domain refinements ride the type lattice (introduced by `cast`), - // not the lambda node, so the param binds under its bare type here. - let param_simple = ctx.normalize(¶m.ty); + // The parameter binds at its **declared** type when there is one, and at its + // slot otherwise. Normalizing does the work of both annotation forms with no + // dispatch here: + // + // - exact `p: 𝑇` normalizes to `𝑇` itself, so the body sees exactly `𝑇` and + // every call site owes `arg <: 𝑇`. A `Hole` position inside it becomes a + // fresh variable resolved from the call sites — a parameter has no + // initializer, so there is nothing to complete it from the way + // `complete_annotation` completes a `let`'s. + // - bounded `p <: 𝑇` normalizes to a fresh variable carrying `𝑇` as an upper + // bound, which *is* "inferred, and no wider than `𝑇`": body usage and call + // sites add their own bounds, so the parameter lands on the meet. + // + // Reconciling the slot against the annotation afterwards — what this used to + // do — is what made an exact annotation behave as neither reading: it + // contributed one upper bound among several instead of being the type. + // + // A Hole (no annotation) turns into a fresh Var accumulating bounds from body + // usage and call sites. Either way `param.ty` is linked to that type so + // `coalesce_node` resolves the binding slot in place. Domain refinements ride + // the type lattice (introduced by `cast`), not the lambda node, so the param + // binds under its bare type here. + let declared = param.user_annotation.clone().unwrap_or(param.ty.clone()); + let param_simple = ctx.normalize(&declared); param.ty = param_simple.clone(); // The param is bound in scope under the *unrefined* `param_simple`, so // `Var(param)` body references stay bare; restriction refinements decorate only @@ -501,12 +612,6 @@ pub(super) fn emit_lambda( None => body_ty, }; - // Param user-annotation: reconcile the inferred param type with the - // annotation (two-way; see `bind_annotation`). - if let Some(ann) = param.user_annotation.clone() { - ctx.bind_annotation(¶m_simple, &ann)?; - } - // Emit a *named* Pi: the parameter binds in the codomain, so a refinement // predicate nested in `body_ty` that closes over the parameter (the // dependent-refinement case) stays bound. The binder is cosmetic for @@ -1110,21 +1215,35 @@ pub(super) fn emit_let( let bound_ty = read_through(&bound_ty); // The type the variable is bound at over the body. let scheme_ty = match &binding.user_annotation { - // The annotation reconciles the initializer as an ascription. The - // deref-copy case that used to be special here (`y: Int = x` off a - // mutable variable, bound at the annotation rather than at the mutable - // type) is gone: `bound_ty` was already read through above, so annotation - // and initializer agree and there is nothing to choose between. + // Every other annotation: the variable binds at what the annotation + // *declares*, and the two forms differ only in what that is. An exact + // `x: 𝑇` is completed from the initializer at its unspecified positions + // and then declares that; a bounded `x <: 𝑇` declares a variable bounded + // above by `𝑇`, whose lower bound is the initializer — so it resolves to + // the initializer's type, and `𝑇` only has to admit it. + // + // One normalization serves both the reconcile and the binding, which is why + // `bind_annotation` hands it back: normalizing is not idempotent, and + // minting a second variable here would leave the one the binder is bound at + // unrelated to the one the initializer flowed into. + // + // There is no register arm and no deref-copy case. A mutable variable introduction + // is a `MutDecl` (see `emit_mut_decl`), and a mutable-variable-typed initializer was + // already deref'd above — so `y: Int = x` off a mutable variable needs no special + // handling, and `y: _ = x` completes from the *value* rather than the + // history, which is what makes it mean exactly `y = x`. Some(ann) => { - ctx.bind_annotation(&bound_ty, ann)?; - bound_ty + let declared = match ann { + Type::Below(_) => ann.clone(), + _ => complete_annotation(ann, &bound_ty), + }; + ctx.bind_annotation(&bound_ty, &declared)? } None => bound_ty, }; // The binder slot records the type the variable is *bound at*, not its - // initializer's type — the two differ for exactly the annotated cases above - // (a deref-copy binds at the value type, a mutable variable introduction at the - // history). Writing it here, for coalesce to resolve in place, is the same + // initializer's type — an exact annotation binds at the annotation, not at + // what flowed in. Writing it here, for coalesce to resolve in place, is the same // binder-slot discipline `emit_lambda` uses for `param.ty` and `emit_letrec` // for its declared types; `let` was the one binder whose slot was // reconstructed from its RHS afterwards instead, which is what forced the diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index 2a3d734e..54a840d8 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1325,6 +1325,12 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { /// uses `TermMemo` instead (`emit_bare_predicate`). fn coalesce_type_predicates(ty: &mut Type, level: Level, ctx: &mut CoalesceCtx) { match ty { + // `Below` is a *pre-inference* annotation marker: `normalize_annotation` + // erases it into a bounded variable before any constraint is emitted, so + // the solver never sees one. + Type::Below(_) => { + unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + } Type::Refinement(inner, r) => { // A handle clone, so `ctx` stays freely borrowable for the rebuild — // which re-enters this same memo through `coalesce_node` → diff --git a/src/ccl/infer/solver/compact.rs b/src/ccl/infer/solver/compact.rs index 246db66b..31a787b0 100644 --- a/src/ccl/infer/solver/compact.rs +++ b/src/ccl/infer/solver/compact.rs @@ -589,6 +589,11 @@ fn compact_go( st: &mut CompactState, ) -> CompactType { match ty { + // Not a type — an annotation-position obligation, erased by + // `normalize_annotation` before any constraint is emitted (see `Type::Below`). + Type::Below(_) => { + unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + } // Atomic types contribute a single atom. A term substitution never // touches an atom, so `subst_acc` is irrelevant here. Type::Base(_) diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index 6a8f9518..16883af2 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -985,6 +985,11 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac return ty.clone(); } match ty { + // Not a type — an annotation-position obligation, erased by + // `normalize_annotation` before any constraint is emitted (see `Type::Below`). + Type::Below(_) => { + unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + } Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) diff --git a/src/ccl/infer/solver/mod.rs b/src/ccl/infer/solver/mod.rs index a6533f4c..0228c5dd 100644 --- a/src/ccl/infer/solver/mod.rs +++ b/src/ccl/infer/solver/mod.rs @@ -69,6 +69,10 @@ pub use spec_key::{SpecKey, spec_key}; pub fn type_level(ty: &Type) -> Level { match ty { Type::Infer(v) => v.level, + // A bounded annotation's level is its bound's: the variable it becomes is + // minted at the *use* level by `normalize_annotation`, so the bound is all + // there is to report here. + Type::Below(t) => type_level(t), Type::Fun { domain: d, codomain: c, diff --git a/src/ccl/infer/solver/scheme.rs b/src/ccl/infer/solver/scheme.rs index 0a1a8298..8740db85 100644 --- a/src/ccl/infer/solver/scheme.rs +++ b/src/ccl/infer/solver/scheme.rs @@ -235,6 +235,12 @@ pub fn freshen_above( return ty.clone(); } match ty { + // `Below` is a *pre-inference* annotation marker: `normalize_annotation` + // erases it into a bounded variable before any constraint is emitted, so + // the solver never sees one. + Type::Below(_) => { + unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + } Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) diff --git a/src/ccl/infer/solver/spec_key.rs b/src/ccl/infer/solver/spec_key.rs index 53f39e37..acf93d47 100644 --- a/src/ccl/infer/solver/spec_key.rs +++ b/src/ccl/infer/solver/spec_key.rs @@ -343,6 +343,12 @@ pub fn spec_key(ty: &Type) -> SpecKey { fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView { match ty { + // `Below` is a *pre-inference* annotation marker: `normalize_annotation` + // erases it into a bounded variable before any constraint is emitted, so + // the solver never sees one. + Type::Below(_) => { + unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + } Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) diff --git a/src/ccl/infer/typing.rs b/src/ccl/infer/typing.rs index 458864b8..74b524b2 100644 --- a/src/ccl/infer/typing.rs +++ b/src/ccl/infer/typing.rs @@ -157,8 +157,15 @@ pub(super) trait Typing { /// mode this records the **one-way** obligation `inferred <: ann` — /// an annotation has to *admit* the value, not equal it — surfacing /// [`InferError::AnnotationMismatch`] on conflict. See the implementation - /// for why the reverse direction is wrong. - fn bind_annotation(&mut self, inferred: &Type, ann: &Type) -> Result<(), LocatedInferError>; + /// for why the reverse direction is wrong, and + /// `src/ccl/design/type-inference.md`, "Annotation kinds: exact and bounded" + /// for the two forms this obligation serves. + /// + /// **Returns the normalized annotation**, because normalizing is not + /// idempotent: a `Hole` or a [`Type::Below`] mints a fresh variable each time, + /// so a caller that both reconciles against an annotation and binds at it must + /// use one normalization for both or it relates two unrelated variables. + fn bind_annotation(&mut self, inferred: &Type, ann: &Type) -> Result; /// Obtain the type for a binder slot that lives on a /// [`TypedBinding`](crate::ccl::TypedBinding) rather than an [`Expr`] (a diff --git a/src/ccl/lower/functions.rs b/src/ccl/lower/functions.rs index 1f462c2d..215fb1fe 100644 --- a/src/ccl/lower/functions.rs +++ b/src/ccl/lower/functions.rs @@ -27,10 +27,12 @@ use crate::{ /// time (the block-classification decision runs before inference). fn mut_param_history_type(param: &Param) -> Option> { let annotation = param.annotation.as_ref()?; - match mut_annotation_parts(annotation) { + match mut_annotation_parts(&annotation.ty) { + // The mode rides the *value* type, as at a `:=` introduction: a bounded + // `def f(v <: Mut(V))` infers the parameter's value type under `<: V`. Some(Ok((value, is_txn))) => Some(Ok(( Type::History { - value: Box::new(value), + value: Box::new(apply_annotation_mode(annotation.mode, value)), domain: Box::new(Type::Hole), kind: crate::ccl::HistoryKind::Overwrite, }, diff --git a/src/ccl/lower/loops.rs b/src/ccl/lower/loops.rs index fe6117da..c567fc04 100644 --- a/src/ccl/lower/loops.rs +++ b/src/ccl/lower/loops.rs @@ -344,7 +344,7 @@ fn lower_for_body_stmts( if mutation_scope.contains(&name) { return Err(outer_binding_write_error(stmt.span, &name)); } - if mut_annotation_parts(annotation).is_some() { + if mut_annotation_parts(&annotation.ty).is_some() { return Err(in_loop_mut_var_error(stmt.span, &name)); } let ann = lower_type_annotation(annotation)?; @@ -865,7 +865,7 @@ fn lower_loop_body_chain( value, } => { let name = extract_name_target(target, "annotated assignment")?; - if mut_annotation_parts(annotation).is_some() { + if mut_annotation_parts(&annotation.ty).is_some() { return Err(in_loop_mut_var_error(stmt.span, &name)); } let ann = lower_type_annotation(annotation)?; diff --git a/src/ccl/lower/stmts.rs b/src/ccl/lower/stmts.rs index 5d063502..654eda50 100644 --- a/src/ccl/lower/stmts.rs +++ b/src/ccl/lower/stmts.rs @@ -6,7 +6,9 @@ use std::{cell::RefCell, collections::HashSet, rc::Rc, sync::Arc}; use super::*; use crate::{ ccl::{BaseType, Branch, Expr, Lit, Type, TypedExprNode}, - chl_parser::ast::{AssignTarget, IfBranch, Span, Spanned, Stmt as ChlStmt}, + chl_parser::ast::{ + AnnotationMode, AssignTarget, IfBranch, Span, Spanned, Stmt as ChlStmt, TypeAnnotation, + }, interpreter::{DataSink, HttpServerDataSource, http_server::SharedHttpServer}, }; @@ -499,7 +501,7 @@ pub(super) fn lower_middle_stmt( value, } => { let name = extract_name_target(target, "annotated assignment")?; - if mut_annotation_parts(annotation).is_some() { + if mut_annotation_parts(&annotation.ty).is_some() { // `x: Mut(V) = init` / `x: Mut(V, Txn) = init` — a `Mut` // annotation with the *immutable* `=` operator. This is // contradictory under the cutover: `=` is a plain immutable @@ -580,10 +582,18 @@ pub(super) fn lower_middle_stmt( // `x: Mut(V) := e` → induction accumulator at value type `V` // `x: Mut(V, Txn)` → transactional mutable variable at value type `V` // `x: T := e` → induction accumulator at value type `T` + // `x <: T := e` → value type inferred, bounded above by `T` + // + // In every annotated case the mode applies to the *value* type, which is + // what the annotation names: `Mut(V)` contributes `V` and the domain is + // decided below, so `x <: Mut(V) := e` and `x <: V := e` agree. let (value_ty, is_txn) = match annotation { None => (Type::Hole, false), - Some(ann) => match mut_annotation_parts(ann) { - Some(parts) => parts?, + Some(ann) => match mut_annotation_parts(&ann.ty) { + Some(parts) => { + let (value, is_txn) = parts?; + (apply_annotation_mode(ann.mode, value), is_txn) + } None => (lower_type_annotation(ann)?, false), }, }; @@ -864,9 +874,9 @@ pub(super) fn mut_annotation_parts( return None; } match args.as_slice() { - [value] => Some(lower_type_annotation(value).map(|t| (t, false))), + [value] => Some(lower_type_expr(value).map(|t| (t, false))), [value, domain] => { - let value_ty = match lower_type_annotation(value) { + let value_ty = match lower_type_expr(value) { Ok(t) => t, Err(e) => return Some(Err(e)), }; @@ -924,7 +934,7 @@ pub(super) fn pre_register_txn_decls(stmts: &[Spanned], ctx: &mut Lower // A malformed `Mut(…)` annotation (`Err`) surfaces its real error // when the `MutAssign` itself is lowered; not registering it here // is harmless. - if matches!(mut_annotation_parts(annotation), Some(Ok((_, true)))) { + if matches!(mut_annotation_parts(&annotation.ty), Some(Ok((_, true)))) { ctx.register_transactional(id.as_str()); } } @@ -950,12 +960,46 @@ pub(super) fn pre_register_txn_decls(stmts: &[Spanned], ctx: &mut Lower } } -/// Whether a type annotation is a pass-by-reference `Mut(…)` form. -fn is_mut_annotation(annotation: &Spanned) -> bool { - mut_annotation_parts(annotation).is_some() +/// Whether a binder annotation is a pass-by-reference `Mut(…)` form. +/// +/// Reads the annotation's *type* only: the mode is orthogonal to whether the +/// binder names a register (`x <: Mut(V) := e` introduces one just as +/// `x: Mut(V) := e` does). +fn is_mut_annotation(annotation: &TypeAnnotation) -> bool { + mut_annotation_parts(&annotation.ty).is_some() +} + +/// Lower a binder's type annotation, applying its [`AnnotationMode`]. +/// +/// `x: T` lowers to `T`; `x <: T` lowers to [`Type::Below`], the marker +/// `normalize_annotation` turns into an inference variable bounded above by `T`. +/// The mode is a property of the *binder*, not of a type: `<:` is grammatical only +/// where a binder is introduced, so nested positions inside `T` are always exact +/// and [`lower_type_expr`] needs no mode parameter. (Design: +/// `src/ccl/design/type-inference.md`, "Annotation kinds: exact and bounded".) +pub(super) fn lower_type_annotation(annotation: &TypeAnnotation) -> Result { + Ok(apply_annotation_mode( + annotation.mode, + lower_type_expr(&annotation.ty)?, + )) +} + +/// Wrap a lowered annotation type in its binder's mode. +/// +/// Separate from [`lower_type_annotation`] because a `Mut(…)` annotation is not +/// lowered as one type: `mut_annotation_parts` splits it into a *value* type and a +/// domain, and the binder's mode belongs to the value — `x <: Mut(V) := e` bounds +/// the register's value type, exactly as `x <: V := e` does. Applying the mode in +/// one place is what keeps those two spellings from disagreeing, which is how the +/// `Mut` form came to silently drop its mode and read as exact. +pub(super) fn apply_annotation_mode(mode: AnnotationMode, ty: Type) -> Type { + match mode { + AnnotationMode::Exact => ty, + AnnotationMode::Bounded => Type::Below(Box::new(ty)), + } } -/// Lower a CHL type annotation expression to a CCL [`Type`]. +/// Lower a CHL type *expression* to a CCL [`Type`]. /// /// Recognised forms: /// - Capitalized primitive names (`Caps` means type — `docs/chl-spec.md`): @@ -971,7 +1015,7 @@ fn is_mut_annotation(annotation: &Spanned) -> bool { /// comma is what makes it a product, and the parser rejects a comma-free /// `{T}`. /// - The empty group `{}` — the unit type, `Unit`. -pub(super) fn lower_type_annotation(annotation: &Spanned) -> Result { +pub(super) fn lower_type_expr(annotation: &Spanned) -> Result { match &annotation.node { ChlExpr::Name(id) => name_type(id.as_str()).ok_or_else(|| { LoweringError::unsupported(annotation.span, format!("unknown type annotation: {id}")) @@ -989,7 +1033,7 @@ pub(super) fn lower_type_annotation(annotation: &Spanned) -> Result) -> Result Ok(Type::Tuple( parts .iter() - .map(lower_type_annotation) + .map(lower_type_expr) .collect::>()?, )), // A parenthesised comma list `(T, U)` is a *term* product; the tuple @@ -1077,7 +1121,7 @@ fn lower_type_application( name: None, kind: crate::ccl::ty::FunKind::Data, domain: Box::new(Type::Hole), - codomain: Box::new(lower_type_annotation(elem)?), + codomain: Box::new(lower_type_expr(elem)?), }) } // `Mut(…)` in a nested position is handled by `mut_annotation_parts` diff --git a/src/ccl/subst.rs b/src/ccl/subst.rs index 2cac3740..79b16d65 100644 --- a/src/ccl/subst.rs +++ b/src/ccl/subst.rs @@ -756,6 +756,7 @@ impl Subst { fn rewrite_type_go(&self, ty: &mut Type, memo: &PredMemo) { match ty { + Type::Below(t) => self.rewrite_type_go(t, memo), Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) @@ -975,6 +976,7 @@ impl Subst { fn apply_type_inner(&self, ty: &Type) -> Type { match ty { + Type::Below(t) => Type::Below(Box::new(self.apply_type_inner(t))), Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) @@ -1104,6 +1106,10 @@ pub fn type_contains_infer(ty: &Type) -> bool { Type::Record(fs) => fs.iter().any(|(_, t)| type_contains_infer(t)), Type::Variant(tags) => tags.iter().any(|(_, t)| type_contains_infer(t)), Type::Refinement(base, _) => type_contains_infer(base), + // Annotation position only, and normalized away before solving. Answering + // for the bounded type is the honest reading of the question; a `Below` that + // reaches here at all is reported as `UnresolvedBelow`, not by this test. + Type::Below(t) => type_contains_infer(t), } } @@ -1134,6 +1140,10 @@ fn collect_type_fv( out: &mut BTreeSet, ) { match ty { + // A bounded annotation binds nothing, so its bound's free variables are + // free in it — a name referenced only from inside an annotation is still + // referenced. + Type::Below(t) => collect_type_fv(t, bound, visited, out), Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index a914316a..40fe9c4c 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -483,6 +483,7 @@ pub fn reset_kind_var_counter() { /// | Variant | Owner | Meaning | Must be eliminated by | /// |---|---|---|---| /// | `Hole` | Lowering | "This slot needs a type; not yet known" | End of inference (compiler bug if survives — flagged as `UnresolvedHole`) | +/// | `Below(𝑇)` | Lowering | "A bounded annotation `𝑥 <: 𝑇`: infer this, subject to `<: 𝑇`" — an obligation, not a shape | Pass 1's `normalize_annotation` (flagged as `UnresolvedBelow` if it survives) | /// | `Infer(id)` | Type checker only | "Inference variable N from the coalesce pass" | End of inference for any type reachable from the program's root output (flagged as `UnresolvedInfer` by `collect_type_errors`); an induction accumulator's *domain* is necessarily `Infer` until the unified phase resolves it (see `Strictness::PreDesugar`) | /// | `History` (`kind: Overwrite`) | Type checker only | "Mutable variable: a `value` cell tracked over a `domain` (loop index or transaction time)" | the unified phase (`transact_phase` / `mut_elim`, which runs *before* `channelize`; a survivor downstream is a compiler bug) | /// | `History` (`kind: Feed`) | Type checker only | "Feed channel `domain ⇒ value`: the defer binding's post-desugar stream type" | `channelize` (which runs after inference; a survivor downstream is a compiler bug) | @@ -569,6 +570,34 @@ pub enum Type { /// [`LoweringContext`](crate::ccl::lower::LoweringContext) and are meaningless /// outside the tree they were minted for. SharedHole(u32), + /// Pre-inference placeholder for a **bounded** annotation `𝑥 <: 𝑇`: "some + /// type that is a subtype of `𝑇`", to be inferred. + /// + /// [`Hole`](Self::Hole) with a ceiling — `Hole` is the unbounded case, and + /// the two compose wherever a compound annotation is only partly specified + /// (the per-position modes of a multi-parameter `def`'s single tuple + /// annotation are exactly this). `normalize_annotation` erases it into a + /// fresh [`Infer`](Self::Infer) carrying `𝑇` as an upper bound. + /// + /// **This is not a type.** Like [`Hole`](Self::Hole) and [`Infer`](Self::Infer) + /// it denotes no set of values — it is a *slot* inhabiting the `Type` enum + /// because annotations are typed positions, and it states an obligation for + /// inference rather than a shape. `Below(𝑇)` is not "the type of values below + /// `𝑇`": there is no such type, which is why nothing may subtype against one, + /// narrow against one, or compact one. The solver has no rule for it and asserts + /// so (`constrain::extrude`, `compact`); only the + /// *structural* walks that rewrite every slot uniformly — substitution, + /// free-variable collection, refinement stripping — pass through it. + /// + /// **Annotation position only, and transient**: lowering writes it, inference + /// erases it, and no pass downstream may observe one. The annotation slots it + /// occupies do not survive inference at all + /// (`infer::api::debug_assert_annotations_cleared`), so a binder `ty` is the + /// only place a survivor could hide — flagged there by `collect_type_errors` + /// as [`InferError::UnresolvedBelow`](crate::ccl::infer::InferError::UnresolvedBelow). + /// + /// See `src/ccl/design/type-inference.md`, "Annotation kinds: exact and bounded". + Below(Box), /// Unresolved type variable, identified by a unique [`crate::ccl::InferVarId`]. /// /// Created during inference by the inference pass @@ -750,6 +779,7 @@ impl fmt::Display for Type { Type::Base(b) => write!(f, "{}", b.keyword()), // `n == 0` means an empty range (e.g. the domain of `[]`); render // it as `∅` instead of computing `n - 1` and underflowing. + Type::Below(t) => write!(f, "<:{t}"), Type::UIntRange(0) => write!(f, "∅"), Type::UIntRange(n) => write!(f, "[0, {}]", n - 1), // The arrow reflects the resolved `kind`: `⇒` for a compute @@ -1071,6 +1101,7 @@ impl Type { domain: Box::new(domain.without_pi_names()), codomain: Box::new(codomain.without_pi_names()), }, + Type::Below(t) => Type::Below(Box::new(t.without_pi_names())), Type::Tuple(ts) => Type::Tuple(ts.iter().map(|t| t.without_pi_names()).collect()), Type::Record(fs) => Type::Record( fs.iter() @@ -1137,6 +1168,10 @@ impl Type { | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn => {} + // A bounded annotation's bound is an ordinary child type — a pass + // that rewrites types (uniquify's α-renaming, `subst`) must reach + // inside it exactly as it reaches inside a `Refinement`. + Type::Below(t) => f(t), Type::Fun { domain, codomain, .. } => { @@ -1179,6 +1214,10 @@ impl Type { | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn => {} + // A bounded annotation's bound is an ordinary child type — a pass + // that rewrites types (uniquify's α-renaming, `subst`) must reach + // inside it exactly as it reaches inside a `Refinement`. + Type::Below(t) => f(t), Type::Fun { domain, codomain, .. } => { diff --git a/src/chl_parser/ast.rs b/src/chl_parser/ast.rs index f33f2671..fbaf1e16 100644 --- a/src/chl_parser/ast.rs +++ b/src/chl_parser/ast.rs @@ -162,14 +162,14 @@ pub enum Stmt { value: Spanned, }, - /// Annotated assignment: `target: ty = value`. + /// Annotated assignment: `target: ty = value` or `target <: ty = value`. /// /// CHL (unlike Python) requires a value; bare annotations are a parse - /// error. `ty` is itself an [`Expr`] (Python's type expressions are + /// error. The annotation type is itself an [`Expr`] (type expressions are /// arbitrary expressions); interpretation lives in lowering. AnnAssign { target: Spanned, - annotation: Spanned, + annotation: TypeAnnotation, value: Spanned, }, @@ -189,7 +189,7 @@ pub enum Stmt { /// mutable variable (the annotation carries the `Txn` domain, exactly as before). MutAssign { target: Spanned, - annotation: Option>, + annotation: Option, value: Spanned, }, @@ -266,7 +266,33 @@ pub struct IfBranch { pub struct Param { pub name: SmolStr, pub name_span: Span, - pub annotation: Option>, + pub annotation: Option, +} + +/// A user-written type annotation at a binder, and which of the two readings it +/// asks for. +/// +/// The two spellings differ only in the mode; the type expression is parsed +/// identically. Lowering turns [`AnnotationMode::Bounded`] into a +/// [`crate::ccl::Type::Below`] wrapper and leaves `Exact` bare. +#[derive(Debug, Clone, PartialEq)] +pub struct TypeAnnotation { + pub mode: AnnotationMode, + pub ty: Spanned, +} + +/// Which reading a binder annotation asks for. +/// +/// Spec: `docs/chl-spec.md`, "Two annotation forms: exact and bounded". +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum AnnotationMode { + /// `x: T` — the binder's type **is** `T`. The initializer (or argument) must + /// be a subtype of `T`, and nothing downstream of the binder sees more than + /// `T`. + Exact, + /// `x <: T` — the binder's type is *inferred*, with `T` as an upper bound. + /// The value's own type flows through. + Bounded, } /// The left-hand side of an assignment, augmented assignment, defer-define, diff --git a/src/chl_parser/lexer.rs b/src/chl_parser/lexer.rs index 228abc70..2a304a58 100644 --- a/src/chl_parser/lexer.rs +++ b/src/chl_parser/lexer.rs @@ -93,6 +93,12 @@ pub enum Token { NotEq, #[token("<=")] LtE, + /// Subtype-bound annotation `<:` — `x <: T` declares an *inferred* type + /// bounded above by `T`, where `x: T` declares `T` exactly. Two chars, so + /// maximal munch takes it over `Lt` then `Colon`; no expression can put a + /// `:` directly after a `<`, so the two never compete. + #[token("<:")] + LtColon, #[token(">=")] GtE, #[token("++")] @@ -222,6 +228,7 @@ impl fmt::Display for Token { Token::EqEq => "==", Token::NotEq => "!=", Token::LtE => "<=", + Token::LtColon => "<:", Token::GtE => ">=", Token::PlusPlus => "++", Token::PlusEq => "+=", diff --git a/src/chl_parser/parser.rs b/src/chl_parser/parser.rs index d92017b3..d6b12333 100644 --- a/src/chl_parser/parser.rs +++ b/src/chl_parser/parser.rs @@ -59,8 +59,8 @@ use chumsky::prelude::*; use smol_str::SmolStr; use crate::chl_parser::ast::{ - AssignTarget, AugOp, BinOp, BoolOp, CmpOp, CompClause, Comprehension, Expr, IfBranch, Lit, - Module, Param, RecordField, Span, Spanned, Stmt, UnaryOp, + AnnotationMode, AssignTarget, AugOp, BinOp, BoolOp, CmpOp, CompClause, Comprehension, Expr, + IfBranch, Lit, Module, Param, RecordField, Span, Spanned, Stmt, TypeAnnotation, UnaryOp, }; use crate::chl_parser::lexer::{self, Token}; @@ -918,10 +918,21 @@ where }); // ---- def name(params): body --------------------------------- + // `x: T` (exact) or `x <: T` (bounded) — the mode is the only difference. + let annotation_mode = choice(( + just(Token::Colon).to(AnnotationMode::Exact), + just(Token::LtColon).to(AnnotationMode::Bounded), + )); let param = select! { Token::Ident(s) => s } .map_with(|s, e| (s, e.span())) .labelled("parameter name") - .then(just(Token::Colon).ignore_then(expr.clone()).or_not()) + .then( + annotation_mode + .clone() + .then(expr.clone()) + .map(|(mode, ty)| TypeAnnotation { mode, ty }) + .or_not(), + ) .map(|((name, name_span), annotation)| Param { name, name_span, @@ -984,10 +995,12 @@ where just(Token::Eq) .ignore_then(expr.clone()) .map(AssignTail::Plain), - // `: ty = value` (immutable) or `: ty := value` (mutable): parse - // the annotation, then branch on the assignment operator. - just(Token::Colon) - .ignore_then(expr.clone()) + // An annotated binding: `: ty` (exact) or `<: ty` (bounded), + // then `=` (immutable) or `:=` (mutable). The annotation's mode + // and the assignment operator are independent choices. + annotation_mode + .then(expr.clone()) + .map(|(mode, ty)| TypeAnnotation { mode, ty }) .then(choice(( just(Token::Eq) .ignore_then(expr.clone()) @@ -1124,12 +1137,13 @@ where #[derive(Clone)] enum AssignTail { Plain(Spanned), - Annotated(Spanned, Spanned), + /// `: ty = value` / `<: ty = value` — an annotated immutable binding. + Annotated(TypeAnnotation, Spanned), /// `:= value` — a bare mutable assignment (`MutAssign` with no annotation). MutPlain(Spanned), - /// `: ty := value` — an annotated mutable assignment (`MutAssign` carrying - /// the annotation, e.g. `Mut(V, Txn)`). - MutAnnotated(Spanned, Spanned), + /// `: ty := value` / `<: ty := value` — an annotated mutable assignment + /// (`MutAssign` carrying the annotation, e.g. `Mut(V, Txn)`). + MutAnnotated(TypeAnnotation, Spanned), Aug(AugOp, Spanned), Define(Spanned), None, diff --git a/tests/chl_parser_roundtrip.rs b/tests/chl_parser_roundtrip.rs index d57ebe7c..0ae033b3 100644 --- a/tests/chl_parser_roundtrip.rs +++ b/tests/chl_parser_roundtrip.rs @@ -644,8 +644,8 @@ fn mut_txn_annotation_parses_as_type_application() { let Stmt::AnnAssign { annotation, .. } = &m.body[0].node else { panic!("expected an AnnAssign, got {:?}", m.body[0].node); }; - let Expr::Call { func, args } = &annotation.node else { - panic!("expected a Call annotation, got {:?}", annotation.node); + let Expr::Call { func, args } = &annotation.ty.node else { + panic!("expected a Call annotation, got {:?}", annotation.ty.node); }; assert!( matches!(&func.node, Expr::Name(n) if n == "Mut"), diff --git a/tests/compilation_pipeline/mutability.rs b/tests/compilation_pipeline/mutability.rs index 2053ab86..3f053350 100644 --- a/tests/compilation_pipeline/mutability.rs +++ b/tests/compilation_pipeline/mutability.rs @@ -662,7 +662,21 @@ fn mut_annotation_with_non_txn_domain_rejected() { t += y t "#})] -fn mut_var_declared_inside_loop_rejected(#[case] code: &str) { +#[case::bounded_mut(indoc! {r#" + t := 0 + for i in [1, 2, 3]: + y <: Mut(Int) := i + t += y + t +"#})] +#[case::bounded_value(indoc! {r#" + t := 0 + for i in [1, 2, 3]: + y <: Int := i + t += y + t +"#})] +fn register_declared_inside_loop_rejected(#[case] code: &str) { expect_compile_error(code, "introduced inside a for-loop body"); } @@ -1220,17 +1234,21 @@ fn deref_copy_is_a_value_not_a_mutable_alias() { /// value type all the way through inlining. /// /// The mutable variable is unwritten, so its value type is still its seed's singleton -/// (`Mut({Int | __elem == 5}, ?d)`), and the parameter — whose type is inferred, since an -/// annotation bounds rather than fixes it — takes that refinement, because the call site -/// is typed against the dereferenced value. Beta-reduction then has to discharge a -/// refinement demanded of the value against an argument node still stamped with the -/// handle: the `Mut` survives on the bare `Var` for the phase to find the read. Reading -/// through the handle is what makes the two comparable; comparing the stamp directly asks -/// a handle to entail a fact about a value and trips `inline`'s entailment assert. +/// (`Mut({Int | __elem == 5}, ?d)`), and a parameter whose type is left to inference takes +/// that refinement, because the call site is typed against the dereferenced value. +/// Beta-reduction then has to discharge a refinement demanded of the value against an +/// argument node still stamped with the handle: the `Mut` survives on the bare `Var` for +/// the phase to find the read. Reading through the handle is what makes the two +/// comparable; comparing the stamp directly asks a handle to entail a fact about a value +/// and trips `inline`'s entailment assert. /// -/// The last case is the surrounding one that reaches the same parameter *without* a -/// refinement — the use demands `Int`, which widens it — so a future narrowing of the -/// read shows up as a difference between the cases rather than as silence. +/// The last two cases are the surrounding ones that reach the same parameter *without* a +/// refinement, so a future narrowing of the read shows up as a difference between the +/// cases rather than as silence. Each is a distinct reason for the singleton not to +/// arrive: an exact annotation is a specialization boundary that fixes the domain at +/// `Int`, and a use demanding `Int` widens an inferred parameter. A **bounded** +/// annotation is not one of them — it constrains without fixing, so it lands on the +/// singleton exactly as no annotation does. #[rstest] #[case::unannotated(indoc! {r#" def id(v): @@ -1238,7 +1256,13 @@ fn deref_copy_is_a_value_not_a_mutable_alias() { x := 5 id(x) "#})] -#[case::annotated(indoc! {r#" +#[case::bounded(indoc! {r#" + def id(v <: Int): + v + x := 5 + id(x) +"#})] +#[case::exact(indoc! {r#" def id(v: Int): v x := 5 diff --git a/tests/type_check.rs b/tests/type_check.rs index cf541738..fe74fd15 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -970,7 +970,12 @@ sum(f)", fn test_def_param_annotation_enforced() { // A scalar annotation is enforced at the call site: an identity body infers // nothing on its own, so without the annotation any argument was accepted. - assert_eq!(infer_program("def g(a: Int):\n a\ng(1)"), int_lit(1)); + // The parameter binds *at* `Int` (exact), so the argument's singleton does not + // flow through it — that erasure is what makes an annotated parameter a + // monomorphization boundary (see `test_exact_param_shares_one_specialization`). + assert_eq!(infer_program("def g(a: Int):\n a\ng(1)"), int()); + // The bounded form keeps it: `a` is inferred, bounded above by `Int`. + assert_eq!(infer_program("def g(a <: Int):\n a\ng(1)"), int_lit(1)); assert!(!infer_program_err("def g(a: Int):\n a\ng(\"x\")").is_empty()); // A `List(Int)` annotation enforces the element type through the annotation. assert_eq!( @@ -987,6 +992,11 @@ fn test_multiarg_def_param_annotation_enforced() { // Each tupled parameter's annotation is enforced independently. assert_eq!( infer_program("def g(a: Int, b: String):\n a\ng(1, \"x\")"), + int() + ); + // Per-position modes inside the one tupled annotation: `a` exact, `b` bounded. + assert_eq!( + infer_program("def g(a <: Int, b: String):\n a\ng(1, \"x\")"), int_lit(1) ); // Wrong type on `a` is rejected. @@ -1098,14 +1108,25 @@ fn test_tuple_index() { // Type annotation tests // --------------------------------------------------------------------------- -/// An ascription is one-way: it must *admit* the value, and the value keeps whatever -/// more precise type it already had. So annotating a literal at its base does not -/// widen it, while an expression that computes a new value has nothing to keep. +/// An **exact** annotation (`x: T`) binds the variable *at* `T`: the value must be +/// admitted by it, and anything more precise the value carried is discarded — so +/// annotating a literal at its base widens it. The **bounded** form (`x <: T`) is +/// the one that keeps the value's own type; see `test_bounded_annotation_keeps_the_inferred_type`. +/// +/// A `_` position declares nothing and is completed from the initializer, which is +/// what makes `x: _ = e` equivalent to `x = e`. #[rstest] #[case::literal( r" x: Int = 2 x +", + int() +)] +#[case::bounded_literal( + r" +x <: Int = 2 +x ", int_lit(2) )] @@ -1984,14 +2005,19 @@ fn positional_and_named_projection_compose() { /// The brace *type* forms and `.` agree on keying: `{T, U}` is a tuple type, projected /// positionally; `{name: T}` is a record type, projected by name. +/// +/// Both are **exact** annotations (`x: T`), so each binds its variable *at* the declared +/// type and the literals' singletons are discarded — the projection yields the declared +/// field type rather than the value that went in (`test_ann_assign_ok` pins that rule +/// directly). The keying is what is at issue here, not the precision. #[test] fn brace_type_annotations_project_by_their_keying() { - assert_eq!(infer_program("t: {Int, Bool} = (1, True)\nt.0"), int_lit(1)); - assert_eq!(infer_program("r: {a: Int} = (a=1)\nr.a"), int_lit(1)); + assert_eq!(infer_program("t: {Int, Bool} = (1, True)\nt.0"), int()); + assert_eq!(infer_program("r: {a: Int} = (a=1)\nr.a"), int()); // A *one*-element tuple type carries the trailing comma, like the `(e,)` term. - assert_eq!(infer_program("t: {Int,} = (1,)\nt.0"), int_lit(1)); + assert_eq!(infer_program("t: {Int,} = (1,)\nt.0"), int()); // A one-*field* record type needs no comma — `a: Int` already marks the form. - assert_eq!(infer_program("r: {a: Int,} = (a=1)\nr.a"), int_lit(1)); + assert_eq!(infer_program("r: {a: Int,} = (a=1)\nr.a"), int()); } /// The empty product is `Unit`, and it is the *only* empty product: `{}` in an @@ -2550,3 +2576,167 @@ fn a_conditional_over_two_mut_vars_denotes_their_values() { "(Int, 0)" ); } + +/// The two binder-annotation forms: exact `x: T` binds *at* `T`; bounded `x <: T` +/// infers and only bounds. +/// +/// Design: `src/ccl/design/type-inference.md`, "Annotation kinds: exact and bounded". +mod annotation_kinds { + use super::*; + use cambra::ccl::symbolic::symbolic; + + /// Record **width** is the clearest case: an exact annotation is the type, so a + /// field it does not mention is not reachable through the binder; a bounded one + /// lets the value's own wider type through. + #[test] + fn exact_narrows_record_width_and_bounded_does_not() { + assert!( + !infer_program_err("x: {a: Int} = (a=1, b=2)\nx.b").is_empty(), + "an exact annotation is the binder's type, so `b` is not reachable" + ); + assert_eq!(infer_program("x <: {a: Int} = (a=1, b=2)\nx.b"), int_lit(2)); + } + + /// Same at a parameter, which is the asymmetry that motivated the split: the + /// two positions now read an annotation the same way. + #[test] + fn the_two_binder_positions_agree() { + assert!( + !infer_program_err("def f(v: {a: Int}):\n v.b\nf((a=1, b=2))").is_empty(), + "an exact parameter is the annotation, so `v.b` is not typeable" + ); + assert_eq!( + infer_program("def f(v <: {a: Int}):\n v.b\nf((a=1, b=2))"), + int_lit(2) + ); + } + + /// A literal is typed by its own value, so the two forms differ on whether the + /// annotation discards that: only the bounded form keeps the singleton. + /// + /// This is the difference that matters for proofs — an index-range obligation + /// discharges only when the index's type says *which* index it is — though a + /// variable subscript is not yet accepted by the surface (`x[i]` is "only + /// integer subscripts are supported"), so that consequence is not assertable + /// here yet. + #[test] + fn only_bounded_keeps_a_literals_singleton() { + assert_eq!(infer_program("i: Int = 0\ni"), int()); + assert_eq!(infer_program("i <: Int = 0\ni"), int_lit(0)); + } + + /// An unspecified position declares nothing and is completed from the + /// initializer, so `x: _ = e` is exactly `x = e` — including when the `_` is + /// nested inside a compound annotation. + #[test] + fn an_unspecified_position_is_completed_from_the_initializer() { + assert_eq!(infer_program("x: _ = 2\nx"), infer_program("x = 2\nx")); + assert_eq!(infer_program("x: _ = 2\nx"), int_lit(2)); + // `List(_)` completes its element type rather than leaving a variable that + // nothing resolves. + assert_eq!(infer_program("x: List(_) = [1, 2, 3]\nsum(x)"), int()); + } + + /// An exact parameter annotation is a **monomorphization boundary**: it binds + /// the parameter at a concrete type, so no argument's type reaches the domain + /// and every call site shares one specialization. A bounded (or absent) one + /// leaves the domain a variable, and the argument's singleton splits the key — + /// one clone per literal. + #[test] + fn exact_param_collapses_specializations() { + fn clones(code: &str) -> usize { + let mut lctx = LoweringContext::default(); + let stmts = parse_module(code); + let mut expr = lower_stmts(&stmts, &mut lctx) + .into_result() + .expect("lowering failed"); + infer(&mut expr, &mut TypeInferenceContext::new()).expect("inference failed"); + symbolic(&expr).matches("let __mono").count() + } + let body = "\n v + 1\n\na = f(1)\nb = f(2)\na\n"; + assert_eq!( + clones(&format!("def f(v <: Int):{body}")), + 2, + "a bounded param's domain is a variable, so each argument's singleton \ + splits the specialization key" + ); + assert_eq!( + clones(&format!("def f(v: Int):{body}")), + 1, + "an exact param's domain is concrete, so both call sites share one clone" + ); + // …and the collapse survives a consumer that reaches the two uses through + // *one* operator, each result flowing into a different operand slot of the + // enclosing `+`. Nothing about the uses differs — same function, same + // annotation, same literal — so a split here would be two clones of + // identical code. + assert_eq!( + clones("def f(v: Int):\n v + 1\nf(1) + f(1)"), + 1, + "which operand slot a use lands in is not information about the use" + ); + // The bounded form still splits under the same consumer: there the argument + // reaches the *domain*, which is a real difference between the clones. + assert_eq!( + clones("def f(v <: Int):\n v + 1\nf(1) + f(2)"), + 2, + "a bounded param still splits per argument, operator consumer or not" + ); + } + + /// A binder's mode applies to a register's **value** type, so `a <: Mut(V)` and + /// `a <: V` are the same declaration — and both agree with writing no annotation + /// at all, since a bound the inferred type already satisfies admits it rather + /// than replacing it. + /// + /// The `Mut(…)` spelling used to read as *exact*: lowering split the annotation + /// into a value type and a domain and dropped the mode on the way, so the bounded + /// form discarded the singleton that the unannotated form keeps — a bound that + /// lost information. + #[test] + fn a_bound_on_a_register_bounds_its_value_type() { + // Compared by register *value* type. Each program ends in a bare read, and a + // tail denotes the register's *value*, so the program type is that value type + // directly — which also keeps the per-run domain variable, whose id differs + // every time, out of the comparison. + let register_value = |code: &str| { + let ty = infer_program(code); + assert!( + ty.as_register().is_none(), + "a tail read denotes the register's value, got the handle {ty}" + ); + ty + }; + // No writes, so the value type is the seed's — the bound admits `5`. + let bare = register_value("a := 5\na"); + assert_eq!(register_value("a <: Mut(Int) := 5\na"), bare); + assert_eq!(register_value("a <: Int := 5\na"), bare); + // The exact form is what discards the singleton. + assert_eq!(register_value("a: Mut(Int) := 5\na"), int()); + assert_ne!(register_value("a <: Mut(Int) := 5\na"), int()); + // With a write, the value type is the join over seed and writes, so both + // modes land on `Int` — the bound is satisfied, not doing the widening. + assert_eq!(register_value("a <: Mut(Int) := 0\na += 1\na"), int()); + // And it is still a *declaration*, so the deref-copy below it is a read. + assert_eq!(infer_program("a <: Mut(Int) := 0\nb: Int = a\nb"), int()); + } + + /// The bound is a real obligation on a bounded register, discharged against both + /// contributions to its value type: the seed and every write. + #[test] + fn a_bounded_registers_bound_constrains_seed_and_writes() { + let rejects = |code: &str, needle: &str| { + let errs = infer_program_err(code); + let rendered = format!("{errs:?}"); + assert!( + rendered.contains(needle), + "expected an error mentioning {needle:?}, got: {rendered}" + ); + }; + rejects("a <: Mut(Int) := \"s\"\na", "initializer of mutable `a`"); + rejects( + "a <: Mut(Int) := 0\nfor i in [1, 2]:\n a := \"s\"\na", + "write to mutable variable `a`", + ); + } +} From 90be237b2b161eded5c958c39031688453889fa5 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Wed, 12 Aug 2026 22:07:22 -0700 Subject: [PATCH 2/4] Rebase fallout: an exact annotation delivers, so it catches a trait conflict uncalled MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The traits branch below this one leaves a never-called definition's trait conflicts unreached, because narrowing consumes bases that *arrive* at an operand and a definition nobody calls delivers none. An exact annotation is a delivery — it binds the parameter at `Int` rather than at a variable `Int` sits above — so `def f(x: Int): x + "s"` is rejected with no call site, and moves back to the rejection cases. Its bounded twin is added alongside, as a case that is *not* caught. It is equally ill-typed and equally rejected at a call; `x <: Int` simply puts no base on the operand, so today's one-delivery-at-a-time narrowing has nothing to consume. That is a gap in reach rather than anything the exact/bounded split says about the program — measured, reading `x`'s requirements together with its `Int` bound rejects it too — and both the test and the design doc say so, so the pair is not misread as the split promising less of `<:`. --- src/ccl/design/type-inference.md | 3 +++ tests/type_check.rs | 38 +++++++++++++++++++++++--------- 2 files changed, 31 insertions(+), 10 deletions(-) diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index 1f926cc6..cdfd8189 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -774,6 +774,9 @@ The two coincide only where the value's type already *is* the annotation, leavin * **Width.** `x : {a: Int} = (a=1, b=2)` binds `x` at `{a: Int}`, so `x.b` is an error. `x <: {a: Int} = (a=1, b=2)` binds `x` at `{a: 1, b: 2}`, and `x.b` is `2`. * **Refinements.** A literal is typed by its own value ([A literal is refined by its own value](#a-literal-is-refined-by-its-own-value)), so `x : Int = 5` binds `x` at `Int` — the annotation is precisely what discards the singleton — while `x <: Int = 5` leaves it at `5`. Only the second still discharges `arr[x]`'s index-range obligation. +* **Delivery.** Trait narrowing consumes bases that *arrive* at an operand ([Delivery: the watch follows the edge](#delivery-the-watch-follows-the-edge)), and only the exact form puts one there — it binds at `Int`, while the bounded form binds at a variable that `Int` sits above. So `def f(x: Int): x + "s"` is rejected with no call site and `def f(x <: Int): x + "s"` is not, though both are ill-typed and both fail at the first call. + + This last one is a difference in *reach*, not in meaning, and it is the only bullet here that is: reading the requirements on a value together with its bounds — rather than one delivery at a time — catches the bounded program too, which is the residual gap [Typechecking a never-called definition](#typechecking-a-never-called-definition) already names and locates in the obligation machinery. Do not read it as the split saying that `x <: Int` promises less; what it promises is stated above, and this row is about which mechanism happens to notice. The refinement case is worth reading twice: the annotation is a bare `Int` and the forms still differ, because `5` is a strict subtype of `Int`. A "simple" annotation is no guarantee that the two agree — only a value that knows nothing beyond the annotation is. diff --git a/tests/type_check.rs b/tests/type_check.rs index fe74fd15..79da0578 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -635,6 +635,15 @@ fn dead_code(defs: &str) -> String { f = \a -> a.0 + a.foo f = 3 "#})] +// An *exact* annotation is a delivery, which is what brings this case back within +// reach: `x: Int` puts a base on the operand rather than a bound above it, so the +// obligation narrows to `{(Int, Int)}` and `"s"` empties it, with no call site +// needed. Its bounded twin below is equally ill-typed and is *not* caught here, and +// the difference is in the mechanism, not in the programs. +#[case::annotated_param(indoc! {r#" + def f(x: Int): + x + "s" +"#})] fn a_never_called_function_is_still_typechecked(#[case] defs: &str) { assert!( !infer_program_err(&dead_code(defs)).is_empty(), @@ -647,18 +656,27 @@ fn a_never_called_function_is_still_typechecked(#[case] defs: &str) { /// nothing, so a conflict that is only a trait conflict is not reached — see /// `src/ccl/design/type-inference.md`, "Typechecking a never-called definition". /// -/// Both bodies are rejected the moment they are called (`f(1)` on either names the -/// operand, its type, and what the position accepts), so this is about *when* the -/// conflict is found, not whether. What makes them unreachable here is that neither -/// asks any one delivery to be impossible: the first places two requirements on `a` -/// — `a + 1` fixes it at `Int`, `a + "s"` at `String` — each satisfiable alone and -/// jointly not, and the second sets a requirement against an annotation. Reading a -/// value's requirements together is what closes both, and that is a property of the -/// obligation machinery rather than of the discard walk. +/// The body is rejected the moment it is called (`f(1)` names the operand, its type, +/// and what the position accepts), so this is about *when* the conflict is found, not +/// whether. What makes it unreachable here is that no single delivery is impossible: +/// two requirements land on `a` — `a + 1` fixes it at `Int`, `a + "s"` at `String` — +/// each satisfiable alone and jointly not. Reading a value's requirements together is +/// what closes it, and that is a property of the obligation machinery rather than of +/// the discard walk. +/// +/// The bounded parameter pairs with the exact one in the previous test and is here +/// for the same reason as the case above it, not a different one: `x <: Int` bounds +/// the operand from above without putting a base on it, so nothing is delivered and +/// the obligation never narrows, while `x: Int` delivers and rejects. Both programs +/// are ill-typed and both are rejected at a call; what differs is only whether +/// today's narrowing has anything to consume. Reading `x`'s requirements together +/// alongside its `Int` bound closes this one too — measured, it is rejected once the +/// requirement sweep is in the same tree — so this is a gap in reach, not a +/// consequence of the exact/bounded split. #[rstest] #[case::conflicting_operand_types("f = \\a -> (a + 1, a + \"s\")")] -#[case::annotated_param(indoc! {r#" - def f(x: Int): +#[case::bounded_annotated_param(indoc! {r#" + def f(x <: Int): x + "s" "#})] fn a_never_called_function_whose_conflict_is_only_a_trait_conflict_is_not_reached( From 8e7d3ae1afaf9f8347427759a4b4d27af781d78d Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Thu, 13 Aug 2026 12:01:47 -0700 Subject: [PATCH 3/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`. The exact/bounded pairs are the ones this matters most for: the two spellings differ by a single token, so the programs they compare have to be readable side by side. --- docs/chl-spec.md | 4 +- src/ccl/design/type-inference.md | 22 +-- src/ccl/infer/context.rs | 6 +- src/ccl/lower/stmts.rs | 4 +- tests/type_check.rs | 229 ++++++++++++++++++++++++++----- 5 files changed, 210 insertions(+), 55 deletions(-) diff --git a/docs/chl-spec.md b/docs/chl-spec.md index 6cbc3246..ed789547 100644 --- a/docs/chl-spec.md +++ b/docs/chl-spec.md @@ -635,8 +635,8 @@ while `x <: Int = 5` leaves `x` at `5` (a bounded annotation only has to admit the value) — see [Two annotation forms: exact and bounded](#two-annotation-forms-exact-and-bounded). Any operation that computes a *new* value drops it, since it is a fact about one -value and not about the operation: `x + x` is an `Int`, and a mutable register -never takes it (a register is the sequence its writes produce, so no one write's +value and not about the operation: `x + x` is an `Int`, and a mutable variable +never takes it (a mutable variable is the sequence its writes produce, so no one write's value describes it). Unit is the exception with nothing to say: it has one inhabitant, so pinning it would add nothing to the base. diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index cdfd8189..c9059db2 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -789,7 +789,7 @@ Both kinds apply at both binder positions, `let` and function parameter, with on The bounded column is the *only* behaviour that existed before the split, at both positions: a binder annotation contributed one upper bound and nothing else, because `bind_annotation` is one-way (`inferred <: ann` — an annotation has to admit the value, not equal it). A parameter's type was therefore the **meet** of its annotation and whatever its body demanded, which is worth stating plainly because it is neither of the two readings one expects: in `def f(v <: {a: Int}): v.b`, the annotation admits the argument and the projection widens the demand, so `𝑣` ends up at `{a: Int, b: 𝑇}` and callers must supply both fields. That is still what the bounded form means; the split gave it its own spelling and gave `:` the exact reading. -Neither rule needs a mode test at its binder. A parameter binds at `normalize(annotation)`: exact normalizes to `𝑇` itself, bounded to a variable bounded by `𝑇`, and the old two-step (bind at a fresh variable, *then* reconcile against the annotation) is what made an exact annotation behave as neither reading — it contributed one upper bound among several instead of being the type. A `let` binds at the same normalization of its (completed) annotation, and two special cases fall out as consequences rather than tests: a **deref-copy** (`y: Int = x` off a register) binds at the annotation because that is what exact *means*, and a bare `_` completes to the initializer's type — so it stays a register, and the mutable-alias rule still rejects `y: _ = x`. +Neither rule needs a mode test at its binder. A parameter binds at `normalize(annotation)`: exact normalizes to `𝑇` itself, bounded to a variable bounded by `𝑇`, and the old two-step (bind at a fresh variable, *then* reconcile against the annotation) is what made an exact annotation behave as neither reading — it contributed one upper bound among several instead of being the type. A `let` binds at the same normalization of its (completed) annotation, and two special cases fall out as consequences rather than tests: a **deref-copy** (`y: Int = x` off a mutable variable) binds at the annotation because that is what exact *means*, and a bare `_` completes to the initializer's type — so it stays a mutable variable, and the mutable-alias rule still rejects `y: _ = x`. #### Below is a marker in a type slot, not a type @@ -815,9 +815,9 @@ An exact annotation may be partly unspecified — `x: List(_) = [1, 2, 3]`, or t The filling is a structural function on the two types, deliberately not a constraint: binding at a normalized annotation and relying on the one-way `rhs <: ann` edge to drive the annotation's fresh variables does *not* work — those variables are minted at the outer level, after the RHS's level has been popped, and escape inference unresolved. Shape disagreements need no handling here, because a `rhs` that cannot flow into `ann` at all is already an `AnnotationMismatch`. -#### A bound on a register bounds its value type +#### A bound on a mutable variable bounds its value type -`𝑥 <: Mut(𝑉) := 𝑒` declares a register whose **value type is inferred, subject to +`𝑥 <: Mut(𝑉) := 𝑒` declares a mutable variable whose **value type is inferred, subject to `<: 𝑉`** — the same declaration as `𝑥 <: 𝑉 := 𝑒`, and the same as writing no annotation whenever the inferred type already satisfies `𝑉`. Lowering applies the binder's mode to the value type it extracts from the annotation @@ -825,21 +825,21 @@ binder's mode to the value type it extracts from the annotation `Mut(Below(𝑉), 𝐷)` and the bound is consumed in the value position like any other. The value position is the only place the bound can go, and that is a fact about the -pipeline rather than about variance. A register binder's slot must stay structurally -a `History`: `as_register`, the deref coercion in `constrain`, `mut_elim`, and +pipeline rather than about variance. A mutable variable binder's slot must stay structurally +a `History`: `mut_value_type`, the deref coercion in `constrain`, `mut_elim`, and `transact_phase` all dispatch on that shape, and a variable standing for the whole -handle would skip a write's `value <: 𝑉` edge, so the register would never receive +handle would skip a write's `value <: 𝑉` edge, so the mutable variable would never receive its writes. The value position carries no such requirement — a variable there is the *ordinary* case, since an unannotated `x := 5` binds at `Mut(?v, ?d)` — and it is where a strict subtype can differ at all. -Distributing is also what makes the bound mean *bounded*. A register's value type is -invariant in **subtyping between two registers** — the call-site rule relating a -caller's register to a `Mut` parameter, where covariance would let a callee narrow a +Distributing is also what makes the bound mean *bounded*. A mutable variable's value type is +invariant in **subtyping between two mutable variables** — the call-site rule relating a +caller's mutable variable to a `Mut` parameter, where covariance would let a callee narrow a value the caller's declaration still promises. That is a different question from -bounding one register's own value, and treating them as the same made +bounding one mutable variable's own value, and treating them as the same made `x <: Mut(Int) := 5` bind at `Mut(Int)`: it discarded the singleton that the wholly -unannotated `x := 5` keeps — a register's value type is the join over its seed and +unannotated `x := 5` keeps — a mutable variable's value type is the join over its seed and every write, so a single contribution keeps its refinement and `x := 1` is a `Mut(1)`. The bound *lost* information rather than admitting it. diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs index 0642e5ce..3748ee8f 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -190,10 +190,10 @@ impl InferCtx { // consumed by the value position below. // // That is not merely where it happens to sit — it is the only place it - // can. A register binder's slot must stay structurally a `History`: - // `as_register`, the deref coercion, `mut_elim`, and `transact_phase` all + // can. A mutable variable binder's slot must stay structurally a `History`: + // `mut_value_type`, the deref coercion, `mut_elim`, and `transact_phase` all // dispatch on the shape, and a variable standing for the whole history - // would skip a write's `value <: V` edge, so the register would never + // would skip a write's `value <: V` edge, so the mutable variable would never // receive its writes. The value position has no such constraint — a // variable there is the ordinary case, since an unannotated `x := 5` binds // at `Mut(?v, ?d)` too — and it is where a strict subtype can differ at diff --git a/src/ccl/lower/stmts.rs b/src/ccl/lower/stmts.rs index 654eda50..39e08da2 100644 --- a/src/ccl/lower/stmts.rs +++ b/src/ccl/lower/stmts.rs @@ -963,7 +963,7 @@ pub(super) fn pre_register_txn_decls(stmts: &[Spanned], ctx: &mut Lower /// Whether a binder annotation is a pass-by-reference `Mut(…)` form. /// /// Reads the annotation's *type* only: the mode is orthogonal to whether the -/// binder names a register (`x <: Mut(V) := e` introduces one just as +/// binder names a mutable variable (`x <: Mut(V) := e` introduces one just as /// `x: Mut(V) := e` does). fn is_mut_annotation(annotation: &TypeAnnotation) -> bool { mut_annotation_parts(&annotation.ty).is_some() @@ -989,7 +989,7 @@ pub(super) fn lower_type_annotation(annotation: &TypeAnnotation) -> Result Type { diff --git a/tests/type_check.rs b/tests/type_check.rs index 79da0578..a221a194 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -991,9 +991,23 @@ fn test_def_param_annotation_enforced() { // The parameter binds *at* `Int` (exact), so the argument's singleton does not // flow through it — that erasure is what makes an annotated parameter a // monomorphization boundary (see `test_exact_param_shares_one_specialization`). - assert_eq!(infer_program("def g(a: Int):\n a\ng(1)"), int()); + assert_eq!( + infer_program(indoc! {r#" + def g(a: Int): + a + g(1) + "#}), + int() + ); // The bounded form keeps it: `a` is inferred, bounded above by `Int`. - assert_eq!(infer_program("def g(a <: Int):\n a\ng(1)"), int_lit(1)); + assert_eq!( + infer_program(indoc! {r#" + def g(a <: Int): + a + g(1) + "#}), + int_lit(1) + ); assert!(!infer_program_err("def g(a: Int):\n a\ng(\"x\")").is_empty()); // A `List(Int)` annotation enforces the element type through the annotation. assert_eq!( @@ -1014,7 +1028,11 @@ fn test_multiarg_def_param_annotation_enforced() { ); // Per-position modes inside the one tupled annotation: `a` exact, `b` bounded. assert_eq!( - infer_program("def g(a <: Int, b: String):\n a\ng(1, \"x\")"), + infer_program(indoc! {r#" + def g(a <: Int, b: String): + a + g(1, "x") + "#}), int_lit(1) ); // Wrong type on `a` is rejected. @@ -2030,12 +2048,36 @@ fn positional_and_named_projection_compose() { /// directly). The keying is what is at issue here, not the precision. #[test] fn brace_type_annotations_project_by_their_keying() { - assert_eq!(infer_program("t: {Int, Bool} = (1, True)\nt.0"), int()); - assert_eq!(infer_program("r: {a: Int} = (a=1)\nr.a"), int()); + assert_eq!( + infer_program(indoc! {r#" + t: {Int, Bool} = (1, True) + t.0 + "#}), + int() + ); + assert_eq!( + infer_program(indoc! {r#" + r: {a: Int} = (a=1) + r.a + "#}), + int() + ); // A *one*-element tuple type carries the trailing comma, like the `(e,)` term. - assert_eq!(infer_program("t: {Int,} = (1,)\nt.0"), int()); + assert_eq!( + infer_program(indoc! {r#" + t: {Int,} = (1,) + t.0 + "#}), + int() + ); // A one-*field* record type needs no comma — `a: Int` already marks the form. - assert_eq!(infer_program("r: {a: Int,} = (a=1)\nr.a"), int()); + assert_eq!( + infer_program(indoc! {r#" + r: {a: Int,} = (a=1) + r.a + "#}), + int() + ); } /// The empty product is `Unit`, and it is the *only* empty product: `{}` in an @@ -2609,10 +2651,20 @@ mod annotation_kinds { #[test] fn exact_narrows_record_width_and_bounded_does_not() { assert!( - !infer_program_err("x: {a: Int} = (a=1, b=2)\nx.b").is_empty(), + !infer_program_err(indoc! {r#" + x: {a: Int} = (a=1, b=2) + x.b + "#}) + .is_empty(), "an exact annotation is the binder's type, so `b` is not reachable" ); - assert_eq!(infer_program("x <: {a: Int} = (a=1, b=2)\nx.b"), int_lit(2)); + assert_eq!( + infer_program(indoc! {r#" + x <: {a: Int} = (a=1, b=2) + x.b + "#}), + int_lit(2) + ); } /// Same at a parameter, which is the asymmetry that motivated the split: the @@ -2620,11 +2672,20 @@ mod annotation_kinds { #[test] fn the_two_binder_positions_agree() { assert!( - !infer_program_err("def f(v: {a: Int}):\n v.b\nf((a=1, b=2))").is_empty(), + !infer_program_err(indoc! {r#" + def f(v: {a: Int}): + v.b + f((a=1, b=2)) + "#}) + .is_empty(), "an exact parameter is the annotation, so `v.b` is not typeable" ); assert_eq!( - infer_program("def f(v <: {a: Int}):\n v.b\nf((a=1, b=2))"), + infer_program(indoc! {r#" + def f(v <: {a: Int}): + v.b + f((a=1, b=2)) + "#}), int_lit(2) ); } @@ -2639,8 +2700,20 @@ mod annotation_kinds { /// here yet. #[test] fn only_bounded_keeps_a_literals_singleton() { - assert_eq!(infer_program("i: Int = 0\ni"), int()); - assert_eq!(infer_program("i <: Int = 0\ni"), int_lit(0)); + assert_eq!( + infer_program(indoc! {r#" + i: Int = 0 + i + "#}), + int() + ); + assert_eq!( + infer_program(indoc! {r#" + i <: Int = 0 + i + "#}), + int_lit(0) + ); } /// An unspecified position declares nothing and is completed from the @@ -2648,11 +2721,25 @@ mod annotation_kinds { /// nested inside a compound annotation. #[test] fn an_unspecified_position_is_completed_from_the_initializer() { - assert_eq!(infer_program("x: _ = 2\nx"), infer_program("x = 2\nx")); - assert_eq!(infer_program("x: _ = 2\nx"), int_lit(2)); + let unspecified = indoc! {r#" + x: _ = 2 + x + "#}; + let bare = indoc! {r#" + x = 2 + x + "#}; + assert_eq!(infer_program(unspecified), infer_program(bare)); + assert_eq!(infer_program(unspecified), int_lit(2)); // `List(_)` completes its element type rather than leaving a variable that // nothing resolves. - assert_eq!(infer_program("x: List(_) = [1, 2, 3]\nsum(x)"), int()); + assert_eq!( + infer_program(indoc! {r#" + x: List(_) = [1, 2, 3] + sum(x) + "#}), + int() + ); } /// An exact parameter annotation is a **monomorphization boundary**: it binds @@ -2671,7 +2758,15 @@ mod annotation_kinds { infer(&mut expr, &mut TypeInferenceContext::new()).expect("inference failed"); symbolic(&expr).matches("let __mono").count() } - let body = "\n v + 1\n\na = f(1)\nb = f(2)\na\n"; + let body = indoc! {r#" + + v + 1 + + a = f(1) + b = f(2) + a + + "#}; assert_eq!( clones(&format!("def f(v <: Int):{body}")), 2, @@ -2689,20 +2784,28 @@ mod annotation_kinds { // annotation, same literal — so a split here would be two clones of // identical code. assert_eq!( - clones("def f(v: Int):\n v + 1\nf(1) + f(1)"), + clones(indoc! {r#" + def f(v: Int): + v + 1 + f(1) + f(1) + "#}), 1, "which operand slot a use lands in is not information about the use" ); // The bounded form still splits under the same consumer: there the argument // reaches the *domain*, which is a real difference between the clones. assert_eq!( - clones("def f(v <: Int):\n v + 1\nf(1) + f(2)"), + clones(indoc! {r#" + def f(v <: Int): + v + 1 + f(1) + f(2) + "#}), 2, "a bounded param still splits per argument, operator consumer or not" ); } - /// A binder's mode applies to a register's **value** type, so `a <: Mut(V)` and + /// A binder's mode applies to a mutable variable's **value** type, so `a <: Mut(V)` and /// `a <: V` are the same declaration — and both agree with writing no annotation /// at all, since a bound the inferred type already satisfies admits it rather /// than replacing it. @@ -2712,37 +2815,78 @@ mod annotation_kinds { /// form discarded the singleton that the unannotated form keeps — a bound that /// lost information. #[test] - fn a_bound_on_a_register_bounds_its_value_type() { - // Compared by register *value* type. Each program ends in a bare read, and a - // tail denotes the register's *value*, so the program type is that value type + fn a_bound_on_a_mut_var_bounds_its_value_type() { + // Compared by mutable variable *value* type. Each program ends in a bare read, and a + // tail denotes the mutable variable's *value*, so the program type is that value type // directly — which also keeps the per-run domain variable, whose id differs // every time, out of the comparison. - let register_value = |code: &str| { + let mut_value = |code: &str| { let ty = infer_program(code); assert!( - ty.as_register().is_none(), - "a tail read denotes the register's value, got the handle {ty}" + ty.mut_value_type().is_none(), + "a tail read denotes the mutable variable's value, got the handle {ty}" ); ty }; // No writes, so the value type is the seed's — the bound admits `5`. - let bare = register_value("a := 5\na"); - assert_eq!(register_value("a <: Mut(Int) := 5\na"), bare); - assert_eq!(register_value("a <: Int := 5\na"), bare); + let bare = mut_value(indoc! {r#" + a := 5 + a + "#}); + assert_eq!( + mut_value(indoc! {r#" + a <: Mut(Int) := 5 + a + "#}), + bare + ); + assert_eq!( + mut_value(indoc! {r#" + a <: Int := 5 + a + "#}), + bare + ); // The exact form is what discards the singleton. - assert_eq!(register_value("a: Mut(Int) := 5\na"), int()); - assert_ne!(register_value("a <: Mut(Int) := 5\na"), int()); + assert_eq!( + mut_value(indoc! {r#" + a: Mut(Int) := 5 + a + "#}), + int() + ); + assert_ne!( + mut_value(indoc! {r#" + a <: Mut(Int) := 5 + a + "#}), + int() + ); // With a write, the value type is the join over seed and writes, so both // modes land on `Int` — the bound is satisfied, not doing the widening. - assert_eq!(register_value("a <: Mut(Int) := 0\na += 1\na"), int()); + assert_eq!( + mut_value(indoc! {r#" + a <: Mut(Int) := 0 + a += 1 + a + "#}), + int() + ); // And it is still a *declaration*, so the deref-copy below it is a read. - assert_eq!(infer_program("a <: Mut(Int) := 0\nb: Int = a\nb"), int()); + assert_eq!( + infer_program(indoc! {r#" + a <: Mut(Int) := 0 + b: Int = a + b + "#}), + int() + ); } - /// The bound is a real obligation on a bounded register, discharged against both + /// The bound is a real obligation on a bounded mutable variable, discharged against both /// contributions to its value type: the seed and every write. #[test] - fn a_bounded_registers_bound_constrains_seed_and_writes() { + fn a_bounded_mut_vars_bound_constrains_seed_and_writes() { let rejects = |code: &str, needle: &str| { let errs = infer_program_err(code); let rendered = format!("{errs:?}"); @@ -2751,9 +2895,20 @@ mod annotation_kinds { "expected an error mentioning {needle:?}, got: {rendered}" ); }; - rejects("a <: Mut(Int) := \"s\"\na", "initializer of mutable `a`"); rejects( - "a <: Mut(Int) := 0\nfor i in [1, 2]:\n a := \"s\"\na", + indoc! {r#" + a <: Mut(Int) := "s" + a + "#}, + "initializer of mutable `a`", + ); + rejects( + indoc! {r#" + a <: Mut(Int) := 0 + for i in [1, 2]: + a := "s" + a + "#}, "write to mutable variable `a`", ); } From f1a2bfbccee0a602ed64350de3cc6e36f22eeb74 Mon Sep 17 00:00:00 2001 From: Daniel Mills Date: Fri, 14 Aug 2026 15:51:49 -0700 Subject: [PATCH 4/4] =?UTF-8?q?Review:=20an=20annotation=20on=20a=20`:=3D`?= =?UTF-8?q?=20binder=20is=20exact=20and=20is=20a=20`Mut(=E2=80=A6)`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Type::History` is invariant in both payloads — a mutable variable is read *and* written through the same binder, and `constrain` relates two histories of the same kind in both directions. A `:=` binder's type is a `Mut(V, D)`. Together those rule out the two annotated spellings this branch had been accepting, and both were being accepted by reinterpretation rather than by meaning what they say: - `x: V := e` names the value type while the binder is at `Mut(V, D)`, so reading a bare `V` there made `:` mean something at a `:=` binder that it means at no other binder — precisely the exactness this branch introduced everywhere else. - `x <: Mut(V) := e` claims nothing `:` does not, since under invariance the only type below `Mut(V, D)` is `Mut(V, D)`. It was accepted by *distributing* the bound into the value position (`Mut(BoundedHole(V), D)`), which is a different claim from the one written. Both are now rejected, sharing one diagnostic because they share one remedy. The invariance argument does not depend on the binder being a `:=`, so a bounded pass-by-reference parameter goes too: a `Mut(…)` annotation is exact wherever it is written. That retires the machinery distribution needed. `apply_annotation_mode` existed only to push a binder's mode through the value/domain split and folds back into `lower_type_annotation`; `normalize_annotation`'s bound-wraps-a-history arm keeps its assertion but loses the essay justifying the value position, which is no longer a position anything can reach. The cost is that "a mutable whose value type is inferred under a ceiling" has no spelling. That is the honest position rather than a gap: under invariance it is not a bound on the binder's type at all, and a bound in the value position would need `<:` inside a type literal, which does not exist. Recorded as `[Open]` in the spec so the option stays open. `Below` also becomes `BoundedHole` throughout — pithy but ambiguous against the many ordering senses of "below", where `BoundedHole` says what the marker is: a `Hole` with a ceiling. --- docs/chl-spec.md | 95 ++++++++++------- src/ccl/ccl_utils.rs | 2 +- src/ccl/design/type-inference.md | 86 ++++++++-------- src/ccl/infer/api.rs | 25 ++--- src/ccl/infer/context.rs | 33 +++--- src/ccl/infer/emit.rs | 6 +- src/ccl/infer/solve.rs | 8 +- src/ccl/infer/solver/compact.rs | 8 +- src/ccl/infer/solver/constrain.rs | 8 +- src/ccl/infer/solver/mod.rs | 2 +- src/ccl/infer/solver/scheme.rs | 8 +- src/ccl/infer/solver/spec_key.rs | 8 +- src/ccl/infer/typing.rs | 2 +- src/ccl/lower/functions.rs | 21 +++- src/ccl/lower/stmts.rs | 124 ++++++++++++++++------- src/ccl/subst.rs | 12 +-- src/ccl/ty.rs | 16 +-- src/chl_parser/ast.rs | 2 +- tests/compilation_pipeline/mutability.rs | 70 +++++++++---- tests/type_check.rs | 63 ++++-------- 20 files changed, 355 insertions(+), 244 deletions(-) diff --git a/docs/chl-spec.md b/docs/chl-spec.md index ed789547..ca4b7124 100644 --- a/docs/chl-spec.md +++ b/docs/chl-spec.md @@ -1416,9 +1416,9 @@ rest of that iteration and gone at the next. The converse also holds: a mutable variable must be introduced **before** the loop that accumulates it. A `:=` inside a loop body whose target is not an already-declared accumulator is a lowering error, at every spelling — -`y := 0`, `y: Int := 0`, and `y: Mut(Int) := 0` alike, since whether an -introduction carries a type annotation says nothing about whether it -introduces a mutable variable. A mutable variable scoped to one iteration would need +`y := 0`, `y: Mut(Int) := 0`, and `y: Mut(Int, Txn) := 0` alike, since +whether an introduction carries a type annotation says nothing about +whether it introduces a mutable variable. A mutable variable scoped to one iteration would need the loop's own iteration extent as its sequencing domain, which is the nested-recurrence case below: @@ -1657,18 +1657,21 @@ element `{T,}`), record type `{f: T}`, variant type An annotation at a binder answers one of two questions, and the two have different spellings because the answers differ. -> **Note.** The *distinction* below is implemented and pinned by tests — -> that a binder can either fix its type or bound it, and what each means -> at every binder form. The **spelling** is **[Open]**: `:` versus `<:` -> is not a syntax we are satisfied with, and it may change without the -> semantics changing. Two things make it unsatisfying. `<:` reads as a -> type operator but describes a *binder*, which is why it cannot be -> written in a nested position — a restriction that falls out of the -> implementation rather than out of anything a reader would expect from -> the notation. And the more common intent is arguably the bounded one, -> yet it carries the heavier spelling. Read the semantics as settled and -> the two tokens as provisional; code written against them may need a -> mechanical rename. +> **Note — why these two spellings.** `<:` relates two *types* everywhere +> else, and here it sits between a term and a type. The capitalization +> rule (§6.1) is what makes that unambiguous rather than a pun: a +> lowercase head means the left side is a term, so `a <: T` reads "`a` has +> a type that is a subtype of `T`", while `A <: T` reads "`A` is a subtype +> of `T`". Which reading applies is settled by the case of the name, not +> by the operator. +> +> Exact gets the lighter spelling because it is the safer default, not +> because it is the more frequent intent. An annotation is written where +> the type is *not* obvious or where a contract is being fixed, and in +> both of those cases the more precise reading is the one to have by +> default. `<:` is then a deliberate opt-in: it loosens the contract and +> accepts inference whose result is harder to predict from the annotation +> alone. `x: T` is **exact**: the binder's type *is* `T`. The initializer (or, at a parameter, the argument) must be a subtype of `T`, and nothing @@ -1681,8 +1684,12 @@ constrains what may reach the binder. Both forms are accepted wherever a binder is introduced — an assignment (`x: T = e`, `x <: T = e`), a mutable introduction (`x: Mut(V) := e`), and a `def` parameter — and mean the same thing in -each. `<:` is **not** written in nested positions: it describes a -binder, not a type, so `{a <: Int}` is not a type. +each. `<:` does not appear **inside a type literal**: it says how an +annotation is read, and what it annotates is a term, so `{a <: Int}` is +not a record type. That is a restriction on type literals, not a claim +that a binder is the only place an annotation can go — an inline +annotation on an expression would carry both modes for the same reason a +binder does. The two coincide only when the value's type already **is** the annotation — when there is nothing for the annotation to discard. They @@ -1691,8 +1698,8 @@ more often than it sounds, because a CHL type carries more than a base: - **Width.** `x: {a: Int} = (a=1, b=2)` binds `x` at `{a: Int}`, so `x.b` is an error — the annotation is what discards the field. - `x <: {a: Int} = (a=1, b=2)` binds `x` at `{a: 1, b: 2}`, and `x.b` - is `2`. + `x <: {a: Int} = (a=1, b=2)` binds `x` at the record's own type, which + still has both fields, so `x.b` is `2`. - **Literal singletons** (§3.1). `i: Int = 0` binds `i` at `Int`; `i <: Int = 0` leaves it at `0`. Only the second still carries the fact a totality proof needs, so an exact annotation on an index @@ -1704,20 +1711,35 @@ a strict subtype of `Int`, so there is something to discard. What makes the forms coincide is the *value* knowing nothing beyond what the annotation says. -A `_` position **declares nothing** and is completed from the -initializer, so `x: _ = e` means exactly `x = e`. That holds nested -too: `x: List(_) = [1, 2, 3]` binds `x` at `List(Int)`. Consequently -`_` does not suppress the mutable-alias rule (§8.1): `b: _ = a` off a -mutable `a` is the same error as a bare `b = a`. - -On a mutable introduction the mode applies to the **value type**, which -is what the annotation names: `x <: Mut(V) := e` declares a mutable -whose value type is inferred subject to `<: V`, and is the same -declaration as `x <: V := e`. So `x <: Mut(Int) := 5` binds the value at -`5` — as the unannotated `x := 5` does — while `x: Mut(Int) := 5` binds -it at `Int`. The bound still constrains every contribution to the value: +A mutable introduction takes only the **exact** form, and only a +`Mut(…)`: `x: Mut(V) := e` and `x: Mut(V, Txn) := e`. A `:=` binder's +type *is* a `Mut(V, D)`, and both of the other spellings would have to +be reinterpreted to mean anything: + +- `x: V := e` names the value type, not the binder's. The binder is at + `Mut(V, D)`, so reading a bare `V` there would make `:` mean + something at a `:=` binder that it means at no other. +- `x <: Mut(V) := e` claims nothing the exact form does not. `Mut` is + **invariant** in its value type — a mutable variable is both read and + written through the same binder — so the only type below `Mut(V, D)` + is `Mut(V, D)`. + +Both are rejected rather than reinterpreted. As everywhere else, the +exact annotation *is* the type: `x: Mut(Int) := 5` binds the value at +`Int`, discarding the seed's singleton, while the unannotated `x := 5` +keeps it. The annotation constrains every contribution to the value — the seed and each write. +The same invariance makes a `Mut(…)` annotation exact wherever it is +written, so a `def` parameter takes `c: Mut(V)` and not `c <: Mut(V)`. + +> **[Open]** — a mutable whose *value* type is inferred under a ceiling +> has no spelling. Under invariance that is not a bound on the binder's +> type at all, so it would need a bound in the value position +> (`Mut(<: V)`, say) — and `<:` does not appear inside a type literal. +> Nothing needs it today; the rejection above is what keeps the option +> open. + > **Note.** An exact parameter annotation also fixes how many times > the function is compiled. A bounded or absent one leaves the > parameter's type open, so each call site's argument type — down to @@ -2101,12 +2123,13 @@ merge law (§8.4): a mutable variable is *last-write-wins*, a feed is A variable is mutable **by the operator that introduces it**. `:=` both introduces and writes a mutable variable; plain `=` is an immutable -binding and *never* mutates (§4.3). The `Mut(…)` annotation is optional — -it is `:=`, not the annotation, that makes a variable mutable. +binding and *never* mutates (§4.3). The annotation is optional — it is +`:=`, not the annotation, that makes a variable mutable — but a written +one is a `Mut(…)`, exactly, because that is the binder's type (§6.1). ```python cnt := 0 # loop accumulator; value type and domain inferred -cnt: Mut(Int) := 0 # same, value type spelled explicitly +cnt: Mut(Int) := 0 # value type spelled exactly, so `cnt` is `Int`, not `0` balance: Mut(Int, Txn) := 0 # transactional mutable variable over the commit order ``` @@ -2116,7 +2139,9 @@ balance: Mut(Int, Txn) := 0 # transactional mutable variable over the commit or `+=` applied to a name that is *not* mutable is a **type error**, not a silent rebind — this is the rule that makes "declare it with `:=`" a real discipline. -- `Mut(V)` / `Mut(V, D)` — the optional mutability annotation (§6.2). `V` +- `Mut(V)` / `Mut(V, D)` — the optional mutability annotation (§6.2), and + the only shape one can take: a bare `cnt: Int := 0` is rejected, since + the binder's type is `Mut(Int, D)` (§6.1). `V` is the value type; `D` is the sequencing domain, inferred as the writing loop's domain when omitted or written `_`. **`Txn` is never inferred** — sharing a variable across concurrent writers or endpoints is a semantic diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs index 380d5913..4f2e13f7 100644 --- a/src/ccl/ccl_utils.rs +++ b/src/ccl/ccl_utils.rs @@ -693,7 +693,7 @@ pub(crate) fn strip_refinements(ty: &Type) -> Type { match ty { // Annotation-position only, and structural: keep the wrapper and strip // inside it, so a bounded annotation's bound is stripped like any other. - Type::Below(t) => Type::Below(Box::new(strip_refinements(t))), + Type::BoundedHole(t) => Type::BoundedHole(Box::new(strip_refinements(t))), Type::Refinement(base, _) => strip_refinements(base), Type::Fun { domain, codomain, .. diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index c9059db2..b86c64f3 100644 --- a/src/ccl/design/type-inference.md +++ b/src/ccl/design/type-inference.md @@ -125,7 +125,7 @@ def identity(x): **Implemented today:** * **Let-polymorphism (functions).** A `let` whose RHS is a *function definition* is generalized: the RHS is typed one level deeper, generalized into a `PolyScheme` at the binding site, and instantiated freshly per use. Because Cambra targets fully-monomorphized output, generalization is paired with **monomorphization**, integrated into the coalesce walk (`infer::specialize_use`): a use of a generalized binding is specialized at first visit — clone + `freshen_expr_type_slots`, a two-way pin against the use's *live* instantiation type, and a re-entrant coalesce of the clone — and the binding's `let` rebuilds itself as the chain of demanded specializations. Specialization is keyed on the use's **instantiation identity** (a `SpecKey`, not a resolved type — see [Keying a specialization](#keying-a-specialization)), so uses that instantiate the definition identically **share** one definition. So `def f(x): x == x; f(1); f("foo")` type-checks and runs, a generator used at two element types compiles to two cached specializations (see F2), and a generalized UDF used only inside *another* generalized definition (poly-calls-poly) specializes by plain recursion — its use becomes concrete inside each wrapper clone's re-entrant walk. Levels are live (extrude fires on a genuine level mismatch). -* **Two binder-annotation forms.** Exact `𝑥 : 𝑇` fixes the binder's type; bounded `𝑥 <: 𝑇` infers it under an upper bound. Both apply at `let` and at a function parameter, carried by `Type::Below` in annotation position and erased by `normalize_annotation`. See [Annotation kinds: exact and bounded](#annotation-kinds-exact-and-bounded). +* **Two binder-annotation forms.** Exact `𝑥 : 𝑇` fixes the binder's type; bounded `𝑥 <: 𝑇` infers it under an upper bound. Both apply at `let` and at a function parameter, carried by `Type::BoundedHole` in annotation position and erased by `normalize_annotation`. See [Annotation kinds: exact and bounded](#annotation-kinds-exact-and-bounded). * **Tagged variants.** The dual of records, natively supporting sum types and pattern-match exhaustiveness inside the structural solver (see §4). Both named (`.Tag(...)`) and positional (`++`-style) sums are handled. * **Lattice-carried refinements.** Refinements ride the lattice natively (compared by structural predicate equality) rather than being stitched on by a post-pass; see §4 and [`crate::ccl::infer::solver`]'s `# Refinements`. * **Dependent refinements (Pi types).** Refinement predicates may close over an outer binder; `Type::Fun` carries an optional Pi binder, the solver derives binder correspondences when constraining function types, and dependent application discharges the binder to its argument at coalesce. Group-by lookup `groupby(xs, key)(𝑘₀)` types as `{𝑖 | 𝑖 ▷ xs ▷ key == 𝑘₀} ⇒ 𝑉`. See §4.5. @@ -772,7 +772,7 @@ An annotation at a binder answers one of two different questions, and CHL spells The two coincide only where the value's type already *is* the annotation, leaving nothing to discard. They differ wherever the value's type is a **strict** subtype of it — and the annotation's own shape does not decide that, because a Cambra type carries more than a base: -* **Width.** `x : {a: Int} = (a=1, b=2)` binds `x` at `{a: Int}`, so `x.b` is an error. `x <: {a: Int} = (a=1, b=2)` binds `x` at `{a: 1, b: 2}`, and `x.b` is `2`. +* **Width.** `x : {a: Int} = (a=1, b=2)` binds `x` at `{a: Int}`, so `x.b` is an error. `x <: {a: Int} = (a=1, b=2)` binds `x` at the record's own type, which still has both fields, so `x.b` is `2`. * **Refinements.** A literal is typed by its own value ([A literal is refined by its own value](#a-literal-is-refined-by-its-own-value)), so `x : Int = 5` binds `x` at `Int` — the annotation is precisely what discards the singleton — while `x <: Int = 5` leaves it at `5`. Only the second still discharges `arr[x]`'s index-range obligation. * **Delivery.** Trait narrowing consumes bases that *arrive* at an operand ([Delivery: the watch follows the edge](#delivery-the-watch-follows-the-edge)), and only the exact form puts one there — it binds at `Int`, while the bounded form binds at a variable that `Int` sits above. So `def f(x: Int): x + "s"` is rejected with no call site and `def f(x <: Int): x + "s"` is not, though both are ill-typed and both fail at the first call. @@ -780,7 +780,7 @@ The two coincide only where the value's type already *is* the annotation, leavin The refinement case is worth reading twice: the annotation is a bare `Int` and the forms still differ, because `5` is a strict subtype of `Int`. A "simple" annotation is no guarantee that the two agree — only a value that knows nothing beyond the annotation is. -Both kinds apply at both binder positions, `let` and function parameter, with one rule each. The *distinction* is settled and implemented; the two **spellings** are provisional, and the spec records them as `[Open]` ([chl-spec.md](../../../docs/chl-spec.md), "Two annotation forms: exact and bounded"). Nothing below depends on which tokens win: the mode is a two-valued property of a binder that lowering reads off the surface and turns into `Below`-or-not, so a respelling is a parser change. +Both kinds apply at both binder positions, `let` and function parameter, with one rule each. The distinction and the two spellings are both settled; the spec states them and gives the reasoning for the tokens ([chl-spec.md](../../../docs/chl-spec.md), "Two annotation forms: exact and bounded"). Nothing below depends on which tokens they are: the mode is a two-valued property of a binder that lowering reads off the surface and turns into `BoundedHole`-or-not, so the surface and the representation are independent. | | `𝑥 : 𝑇` (exact) | `𝑥 <: 𝑇` (bounded) | |---|---|---| @@ -789,25 +789,25 @@ Both kinds apply at both binder positions, `let` and function parameter, with on The bounded column is the *only* behaviour that existed before the split, at both positions: a binder annotation contributed one upper bound and nothing else, because `bind_annotation` is one-way (`inferred <: ann` — an annotation has to admit the value, not equal it). A parameter's type was therefore the **meet** of its annotation and whatever its body demanded, which is worth stating plainly because it is neither of the two readings one expects: in `def f(v <: {a: Int}): v.b`, the annotation admits the argument and the projection widens the demand, so `𝑣` ends up at `{a: Int, b: 𝑇}` and callers must supply both fields. That is still what the bounded form means; the split gave it its own spelling and gave `:` the exact reading. -Neither rule needs a mode test at its binder. A parameter binds at `normalize(annotation)`: exact normalizes to `𝑇` itself, bounded to a variable bounded by `𝑇`, and the old two-step (bind at a fresh variable, *then* reconcile against the annotation) is what made an exact annotation behave as neither reading — it contributed one upper bound among several instead of being the type. A `let` binds at the same normalization of its (completed) annotation, and two special cases fall out as consequences rather than tests: a **deref-copy** (`y: Int = x` off a mutable variable) binds at the annotation because that is what exact *means*, and a bare `_` completes to the initializer's type — so it stays a mutable variable, and the mutable-alias rule still rejects `y: _ = x`. +Neither rule needs a mode test at its binder. A parameter binds at `normalize(annotation)`: exact normalizes to `𝑇` itself, bounded to a variable bounded by `𝑇`, and the old two-step (bind at a fresh variable, *then* reconcile against the annotation) is what made an exact annotation behave as neither reading — it contributed one upper bound among several instead of being the type. A `let` binds at the same normalization of its (completed) annotation, and two special cases fall out as consequences rather than tests: a **deref-copy** (`y: Int = x` off a mutable variable) binds at the annotation because that is what exact *means*, and a bare `_` completes to the initializer's type, which for a mutable-variable initializer is the *value* it reads — so `y: _ = x` binds exactly where `y = x` does, and writing through `y` is rejected the same way. -#### Below is a marker in a type slot, not a type +#### BoundedHole is a marker in a type slot, not a type -The bounded form is represented by a `Type::Below(𝑇)`, which `normalize_annotation` erases into a fresh variable carrying `𝑇` as an upper bound. It is the same kind of object as `Type::Hole` one rung up: `Hole` is the unbounded case, and the two compose in exactly the positions where a compound annotation is partly specified. +The bounded form is represented by a `Type::BoundedHole(𝑇)`, which `normalize_annotation` erases into a fresh variable carrying `𝑇` as an upper bound. It is the same kind of object as `Type::Hole` one rung up: `Hole` is the unbounded case, and the two compose in exactly the positions where a compound annotation is partly specified. -Neither is a type, and that is the first thing to know about `Below`. `Hole`, `Infer`, and `Below` all inhabit the `Type` enum because *annotation and binder positions are typed positions*, not because they denote anything: `Below(𝑇)` is not "the type of values below `𝑇`" — no such type exists, since a bound picks out no set of values on its own. It records an obligation for inference to discharge, and inference discharges it by minting a variable and giving it `𝑇` as an upper bound; the bound then lives where bounds belong, on a variable in the constraint graph. +Neither is a type, and that is the first thing to know about `BoundedHole`. `Hole`, `Infer`, and `BoundedHole` all inhabit the `Type` enum because *annotation and binder positions are typed positions*, not because they denote anything: `BoundedHole(𝑇)` is not "the type of values below `𝑇`" — no such type exists, since a bound picks out no set of values on its own. It records an obligation for inference to discharge, and inference discharges it by minting a variable and giving it `𝑇` as an upper bound; the bound then lives where bounds belong, on a variable in the constraint graph. -The consequence is that no *typing* rule may take a `Below`. There is nothing to subtype against, nothing to narrow, nothing to compact — the solver asserts this rather than inventing a rule (`constrain::extrude`, `compact`). Only the structural walks that rewrite every slot uniformly — substitution, free-variable collection, refinement stripping — pass through one, and they do so because they are indifferent to what a slot means. +The consequence is that no *typing* rule may take a `BoundedHole`. There is nothing to subtype against, nothing to narrow, nothing to compact — the solver asserts this rather than inventing a rule (`constrain::extrude`, `compact`). Only the structural walks that rewrite every slot uniformly — substitution, free-variable collection, refinement stripping — pass through one, and they do so because they are indifferent to what a slot means. -Putting the bound *in the type* rather than beside it is forced by the **multi-parameter encoding**, not chosen for symmetry. A `def` with more than one parameter uncurries to a single tuple parameter whose annotation is one `Type::Tuple`, with `Hole` at each unannotated position (`lower::functions::uncurry_params`). So `def f(x: 𝐴, y <: 𝐵, z)` has to express three distinct annotation modes *inside one type*, and `Tuple([𝐴, Below(𝐵), Hole])` does it with no new plumbing. Carrying the mode alongside the type instead would need a mode *tree* mirroring the type's shape, which is this variant in a worse spelling. +Putting the bound *in the type* rather than beside it is forced by the **multi-parameter encoding**, not chosen for symmetry. A `def` with more than one parameter uncurries to a single tuple parameter whose annotation is one `Type::Tuple`, with `Hole` at each unannotated position (`lower::functions::uncurry_params`). So `def f(x: 𝐴, y <: 𝐵, z)` has to express three distinct annotation modes *inside one type*, and `Tuple([𝐴, BoundedHole(𝐵), Hole])` does it with no new plumbing. Carrying the mode alongside the type instead would need a mode *tree* mirroring the type's shape, which is this variant in a worse spelling. -#### Below cannot outlive inference +#### BoundedHole cannot outlive inference -`Below` is inference's to erase: Pass 1 replaces it with an `Infer` variable, and nothing downstream can observe one — not by convention but because **the slot it would live in does not survive inference at all**. See [The binder slot, and why annotations do not outlive inference](#the-binder-slot-and-why-annotations-do-not-outlive-inference); the bounded form needs no lifecycle rule of its own. +`BoundedHole` is inference's to erase: Pass 1 replaces it with an `Infer` variable, and nothing downstream can observe one — not by convention but because **the slot it would live in does not survive inference at all**. See [The binder slot, and why annotations do not outlive inference](#the-binder-slot-and-why-annotations-do-not-outlive-inference); the bounded form needs no lifecycle rule of its own. -That the slot does not survive is what makes the guarantee structural, and following `Hole`'s precedent instead would *not* have sufficed. `Hole`'s discipline is erasure plus a check on `ty` slots (`UnresolvedHole`) — which leaves annotation slots covered by neither, so an un-erased marker can sit in one to the end of inference whenever a compound annotation is partly unspecified. That is survivable for `Hole`, which means "unspecified" and is read as such; it is not survivable for `Below`, which carries a *bound* that something must discharge. A marker whose whole content is a constraint cannot be left somewhere nothing looks. +That the slot does not survive is what makes the guarantee structural, and following `Hole`'s precedent instead would *not* have sufficed. `Hole`'s discipline is erasure plus a check on `ty` slots (`UnresolvedHole`) — which leaves annotation slots covered by neither, so an un-erased marker can sit in one to the end of inference whenever a compound annotation is partly unspecified. That is survivable for `Hole`, which means "unspecified" and is read as such; it is not survivable for `BoundedHole`, which carries a *bound* that something must discharge. A marker whose whole content is a constraint cannot be left somewhere nothing looks. -The remaining backstop is therefore narrow: a binder `ty` is the only slot a `Below` could reach, and `collect_type_errors` reports `UnresolvedBelow` there. Nothing is expected to trip it — a `Below` reaching the solver un-normalized fails earlier, since there is no rule for constraining against one. +The remaining backstop is therefore narrow: a binder `ty` is the only slot a `BoundedHole` could reach, and `collect_type_errors` reports `UnresolvedBoundedHole` there. Nothing is expected to trip it — a `BoundedHole` reaching the solver un-normalized fails earlier, since there is no rule for constraining against one. #### A Hole inside an exact annotation is still inferred @@ -815,33 +815,37 @@ An exact annotation may be partly unspecified — `x: List(_) = [1, 2, 3]`, or t The filling is a structural function on the two types, deliberately not a constraint: binding at a normalized annotation and relying on the one-way `rhs <: ann` edge to drive the annotation's fresh variables does *not* work — those variables are minted at the outer level, after the RHS's level has been popped, and escape inference unresolved. Shape disagreements need no handling here, because a `rhs` that cannot flow into `ann` at all is already an `AnnotationMismatch`. -#### A bound on a mutable variable bounds its value type - -`𝑥 <: Mut(𝑉) := 𝑒` declares a mutable variable whose **value type is inferred, subject to -`<: 𝑉`** — the same declaration as `𝑥 <: 𝑉 := 𝑒`, and the same as writing no -annotation whenever the inferred type already satisfies `𝑉`. Lowering applies the -binder's mode to the value type it extracts from the annotation -(`lower::stmts::apply_annotation_mode`), so a bounded register arrives as -`Mut(Below(𝑉), 𝐷)` and the bound is consumed in the value position like any other. - -The value position is the only place the bound can go, and that is a fact about the -pipeline rather than about variance. A mutable variable binder's slot must stay structurally -a `History`: `mut_value_type`, the deref coercion in `constrain`, `mut_elim`, and -`transact_phase` all dispatch on that shape, and a variable standing for the whole -handle would skip a write's `value <: 𝑉` edge, so the mutable variable would never receive -its writes. The value position carries no such requirement — a variable there is the -*ordinary* case, since an unannotated `x := 5` binds at `Mut(?v, ?d)` — and it is -where a strict subtype can differ at all. - -Distributing is also what makes the bound mean *bounded*. A mutable variable's value type is -invariant in **subtyping between two mutable variables** — the call-site rule relating a -caller's mutable variable to a `Mut` parameter, where covariance would let a callee narrow a -value the caller's declaration still promises. That is a different question from -bounding one mutable variable's own value, and treating them as the same made -`x <: Mut(Int) := 5` bind at `Mut(Int)`: it discarded the singleton that the wholly -unannotated `x := 5` keeps — a mutable variable's value type is the join over its seed and -every write, so a single contribution keeps its refinement and `x := 1` is a -`Mut(1)`. The bound *lost* information rather than admitting it. +#### A `Mut(…)` annotation is exact + +`Type::History` is **invariant in both payloads**: `constrain` relates two histories of +the same kind in both directions, because a mutable variable is read *and* written +through the same binder. A `:=` binder's type is a `Mut(𝑉, 𝐷)`, and those two facts +together rule out both of the spellings a mutable introduction does not accept. Lowering +rejects them (`lower::stmts::check_mut_decl_annotation`) rather than reinterpreting them: + +* `𝑥 <: Mut(𝑉) := 𝑒` — under invariance the only type below `Mut(𝑉, 𝐷)` is `Mut(𝑉, 𝐷)`, + so the bound admits exactly the annotation and `<:` claims nothing `:` does not. +* `𝑥 : 𝑉 := 𝑒` — a plain value type names the wrong thing. The binder is at `Mut(𝑉, 𝐷)`, + so reading a bare `𝑉` there would make `:` mean something at a `:=` binder that it + means at no other. + +The invariance argument does not depend on the binder being a `:=`, so it rejects a +bounded pass-by-reference parameter too (`lower::functions::mut_param_history_type`): +a `Mut(…)` annotation is exact wherever it is written. + +The consequence for the representation is that a `BoundedHole` never wraps a history, +which `normalize_annotation` asserts. That is worth stating, because the alternative is +representable and tempting: **distributing** the bound into the value position, as +`Mut(BoundedHole(𝑉), 𝐷)`. A mutable variable binder's slot must stay structurally a +`History` — `mut_value_type`, the deref coercion in `constrain`, `mut_elim`, and +`transact_phase` all dispatch on that shape, and a variable standing for the whole handle +would skip a write's `value <: 𝑉` edge — so the value position is the only slot a bound +*could* occupy. But that is a fact about the pipeline, not about what `<: Mut(𝑉)` +denotes; distributing silently re-points the bound at a type other than the one written. +Rejecting leaves "a mutable whose value type is inferred under a ceiling" with no +spelling, which is the honest position: under invariance it is not a bound on the +binder's type at all, and no surface syntax puts a bound in a nested position (see +[chl-spec.md](../../../docs/chl-spec.md), "Two annotation forms: exact and bounded"). #### Exact annotations bound monomorphization @@ -858,7 +862,7 @@ Two caveats keep that from being a blanket guarantee. First, the win is confined There is no conversion *into* a solver type — the solver consumes `ccl::Type` as-is. The only adjustment Pass 1 makes is `normalize_annotation`, which readies a user annotation / expected type for constraint solving: * **Holes (`Type::Hole`):** become fresh `Type::Infer` variables at the current level. -* **Bounds (`Type::Below(𝑇)`):** become fresh `Type::Infer` variables at the current level, carrying `𝑇` as an upper bound — `Hole` with a ceiling (see [Annotation kinds: exact and bounded](#annotation-kinds-exact-and-bounded)). +* **Bounds (`Type::BoundedHole(𝑇)`):** become fresh `Type::Infer` variables at the current level, carrying `𝑇` as an upper bound — `Hole` with a ceiling (see [Annotation kinds: exact and bounded](#annotation-kinds-exact-and-bounded)). * **Refinements:** are **kept** (recursing to normalize the inner) — they ride the lattice natively (above). A `Refinement(Hole, r)` source annotation thus becomes `Refinement(?fresh, r)`. * **Everything else** — including existing `Type::Infer` vars, `Tuple`/`Record` products, and `Type::Variant` sums — is kept verbatim and handled by the solver's structural constraint rules. Tuples and records are width-subtyped positionally/by name; variants are admissible at both polarities (the dual of records), so they need no fresh-var indirection. diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index 10121c07..77446c6c 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -346,12 +346,12 @@ pub enum InferError { /// Display label for the message (see the type docs — not the location). at: String, }, - /// A [`Type::Below`] bounded-annotation marker survived past inference. + /// A [`Type::BoundedHole`] bounded-annotation marker survived past inference. /// /// Like [`InferError::UnresolvedHole`], a compiler bug rather than a - /// user-facing error: `normalize_annotation` erases every `Below` it is handed, + /// user-facing error: `normalize_annotation` erases every `BoundedHole` it is handed, /// so a survivor means a slot inference never normalized. - UnresolvedBelow { + UnresolvedBoundedHole { /// Display label for the message (see the type docs — not the location). at: String, }, @@ -675,7 +675,7 @@ impl std::fmt::Debug for InferError { InferError::UnresolvedHole { at } => { write!(f, "Unresolved type hole in expression: {at}") } - InferError::UnresolvedBelow { at } => { + InferError::UnresolvedBoundedHole { at } => { write!(f, "Unresolved bounded annotation `<:` in expression: {at}") } InferError::UnresolvedInfer { id, at } => { @@ -1046,7 +1046,7 @@ fn collect_type_errors( // A bounded annotation inference never normalized. Reported at every // strictness, exactly like `Hole`: both are lowering markers whose whole // contract is that inference consumes them. - Type::Below(_) => errors.push(InferError::UnresolvedBelow { + Type::BoundedHole(_) => errors.push(InferError::UnresolvedBoundedHole { at: context_sym.to_string(), }), Type::Infer(var) => { @@ -2617,7 +2617,7 @@ mod tests { use; got {exact:?}" ); - let bounded = param_annotation(Type::Below(Box::new(Type::Base(BaseType::Int)))); + let bounded = param_annotation(Type::BoundedHole(Box::new(Type::Base(BaseType::Int)))); assert!( bounded .iter() @@ -2949,19 +2949,20 @@ mod tests { assert_eq!(check_fully_typed(&expr), Ok(())); } - /// A `Type::Below` surviving inference fails with `UnresolvedBelow`. + /// A `Type::BoundedHole` surviving inference fails with `UnresolvedBoundedHole`. /// /// A backstop, like `UnresolvedHole`: `normalize_annotation` erases every - /// `Below` it is handed, and a bounded annotation that somehow reaches the + /// `BoundedHole` it is handed, and a bounded annotation that somehow reaches the /// solver un-normalized is rejected earlier (nothing can be constrained against - /// a `Below`, so it surfaces as an `AnnotationMismatch`). This pins the check + /// a `BoundedHole`, so it surfaces as an `AnnotationMismatch`). This pins the check /// itself, which the pipeline therefore cannot reach. #[test] - fn test_check_fully_typed_below_survivor() { - let expr = Expr::lit(Lit::Int(1)).with_ty(Type::Below(Box::new(Type::Base(BaseType::Int)))); + fn test_check_fully_typed_bounded_hole_survivor() { + let expr = + Expr::lit(Lit::Int(1)).with_ty(Type::BoundedHole(Box::new(Type::Base(BaseType::Int)))); assert_eq!( check_fully_typed(&expr), - Err(vec![InferError::UnresolvedBelow { at: "1".into() }]) + Err(vec![InferError::UnresolvedBoundedHole { at: "1".into() }]) ); } diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs index 3748ee8f..dd4d35d2 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -181,31 +181,24 @@ impl InferCtx { .clone(), // A bounded annotation `𝑥 <: 𝑇` means "infer this, subject to `<: 𝑇`" // → the same fresh variable, carrying `𝑇` as an upper bound. This is - // the *only* place `Below` is consumed; every other pass either + // the *only* place `BoundedHole` is consumed; every other pass either // rewrites through it structurally or treats it as unreachable. // - // A bound never wraps a **history**: lowering applies a binder's mode to - // the history's *value* type (`lower::stmts::apply_annotation_mode`), so - // `x <: Mut(V) := e` arrives as `Mut(Below(V), D)` and the `Below` is - // consumed by the value position below. - // - // That is not merely where it happens to sit — it is the only place it - // can. A mutable variable binder's slot must stay structurally a `History`: - // `mut_value_type`, the deref coercion, `mut_elim`, and `transact_phase` all - // dispatch on the shape, and a variable standing for the whole history - // would skip a write's `value <: V` edge, so the mutable variable would never - // receive its writes. The value position has no such constraint — a - // variable there is the ordinary case, since an unannotated `x := 5` binds - // at `Mut(?v, ?d)` too — and it is where a strict subtype can differ at - // all. A wrapper here means a lowering path built a history without - // routing its annotation through the mode. - Type::Below(bound) if bound.is_handle() => { + // A bound never wraps a **history**, and there is nothing this arm could + // do if one arrived: [`Type::History`] is invariant in both payloads, so + // `<: Mut(V, D)` admits exactly `Mut(V, D)` and a variable bounded by it + // would only lose the shape that `mut_value_type`, the deref coercion, + // `mut_elim`, and `transact_phase` all dispatch on. Lowering rejects the + // spelling outright (`lower::stmts::check_mut_decl_annotation`), so a + // wrapper here means a `Mut` annotation reached a binder without passing + // that check. + Type::BoundedHole(bound) if bound.is_handle() => { unreachable!( - "a bounded annotation wraps a history ({bound}); lowering applies \ - the binder's mode to the history's value type instead" + "a bounded annotation wraps a history ({bound}); `<:` on a `Mut(…)` \ + annotation is rejected at lowering" ) } - Type::Below(bound) => { + Type::BoundedHole(bound) => { let v = fresh_var(self.level); let bound = self.normalize_annotation(bound); // A **local** cache, not `self.cache`: this method takes `&self`, diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index 3c6af0a7..47e59276 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -318,9 +318,9 @@ fn stamp_kind_from(target: &mut Type, reference: &Type) { fn emit_annotation_predicates(ty: &mut Type, ctx: &mut InferCtx) -> Result<(), LocatedInferError> { match ty { // Runs *before* `normalize_annotation`, so a bounded annotation is still a - // `Below` here: recurse into the bound, or a predicate written inside one + // `BoundedHole` here: recurse into the bound, or a predicate written inside one // (`x <: {Int | p}`) never gets typed. - Type::Below(bound) => emit_annotation_predicates(bound, ctx), + Type::BoundedHole(bound) => emit_annotation_predicates(bound, ctx), Type::Refinement(inner, r) => { // The annotation's refinement is bare over REFINEMENT_BINDER, just // like a cast target's — bind the element over the refined base and @@ -1234,7 +1234,7 @@ pub(super) fn emit_let( // history, which is what makes it mean exactly `y = x`. Some(ann) => { let declared = match ann { - Type::Below(_) => ann.clone(), + Type::BoundedHole(_) => ann.clone(), _ => complete_annotation(ann, &bound_ty), }; ctx.bind_annotation(&bound_ty, &declared)? diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index 54a840d8..d66715d2 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1325,11 +1325,13 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) { /// uses `TermMemo` instead (`emit_bare_predicate`). fn coalesce_type_predicates(ty: &mut Type, level: Level, ctx: &mut CoalesceCtx) { match ty { - // `Below` is a *pre-inference* annotation marker: `normalize_annotation` + // `BoundedHole` is a *pre-inference* annotation marker: `normalize_annotation` // erases it into a bounded variable before any constraint is emitted, so // the solver never sees one. - Type::Below(_) => { - unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + Type::BoundedHole(_) => { + unreachable!( + "Type::BoundedHole reached the solver; `normalize_annotation` must erase it" + ) } Type::Refinement(inner, r) => { // A handle clone, so `ctx` stays freely borrowable for the rebuild — diff --git a/src/ccl/infer/solver/compact.rs b/src/ccl/infer/solver/compact.rs index 31a787b0..80bdaefe 100644 --- a/src/ccl/infer/solver/compact.rs +++ b/src/ccl/infer/solver/compact.rs @@ -590,9 +590,11 @@ fn compact_go( ) -> CompactType { match ty { // Not a type — an annotation-position obligation, erased by - // `normalize_annotation` before any constraint is emitted (see `Type::Below`). - Type::Below(_) => { - unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + // `normalize_annotation` before any constraint is emitted (see `Type::BoundedHole`). + Type::BoundedHole(_) => { + unreachable!( + "Type::BoundedHole reached the solver; `normalize_annotation` must erase it" + ) } // Atomic types contribute a single atom. A term substitution never // touches an atom, so `subst_acc` is irrelevant here. diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index 16883af2..5a4d6aaa 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -986,9 +986,11 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac } match ty { // Not a type — an annotation-position obligation, erased by - // `normalize_annotation` before any constraint is emitted (see `Type::Below`). - Type::Below(_) => { - unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + // `normalize_annotation` before any constraint is emitted (see `Type::BoundedHole`). + Type::BoundedHole(_) => { + unreachable!( + "Type::BoundedHole reached the solver; `normalize_annotation` must erase it" + ) } Type::Base(_) | Type::UIntRange(_) diff --git a/src/ccl/infer/solver/mod.rs b/src/ccl/infer/solver/mod.rs index 0228c5dd..5a11a6f1 100644 --- a/src/ccl/infer/solver/mod.rs +++ b/src/ccl/infer/solver/mod.rs @@ -72,7 +72,7 @@ pub fn type_level(ty: &Type) -> Level { // A bounded annotation's level is its bound's: the variable it becomes is // minted at the *use* level by `normalize_annotation`, so the bound is all // there is to report here. - Type::Below(t) => type_level(t), + Type::BoundedHole(t) => type_level(t), Type::Fun { domain: d, codomain: c, diff --git a/src/ccl/infer/solver/scheme.rs b/src/ccl/infer/solver/scheme.rs index 8740db85..9db56a63 100644 --- a/src/ccl/infer/solver/scheme.rs +++ b/src/ccl/infer/solver/scheme.rs @@ -235,11 +235,13 @@ pub fn freshen_above( return ty.clone(); } match ty { - // `Below` is a *pre-inference* annotation marker: `normalize_annotation` + // `BoundedHole` is a *pre-inference* annotation marker: `normalize_annotation` // erases it into a bounded variable before any constraint is emitted, so // the solver never sees one. - Type::Below(_) => { - unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + Type::BoundedHole(_) => { + unreachable!( + "Type::BoundedHole reached the solver; `normalize_annotation` must erase it" + ) } Type::Base(_) | Type::UIntRange(_) diff --git a/src/ccl/infer/solver/spec_key.rs b/src/ccl/infer/solver/spec_key.rs index acf93d47..b0de6417 100644 --- a/src/ccl/infer/solver/spec_key.rs +++ b/src/ccl/infer/solver/spec_key.rs @@ -343,11 +343,13 @@ pub fn spec_key(ty: &Type) -> SpecKey { fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView { match ty { - // `Below` is a *pre-inference* annotation marker: `normalize_annotation` + // `BoundedHole` is a *pre-inference* annotation marker: `normalize_annotation` // erases it into a bounded variable before any constraint is emitted, so // the solver never sees one. - Type::Below(_) => { - unreachable!("Type::Below reached the solver; `normalize_annotation` must erase it") + Type::BoundedHole(_) => { + unreachable!( + "Type::BoundedHole reached the solver; `normalize_annotation` must erase it" + ) } Type::Base(_) | Type::UIntRange(_) diff --git a/src/ccl/infer/typing.rs b/src/ccl/infer/typing.rs index 74b524b2..ec8dcb7f 100644 --- a/src/ccl/infer/typing.rs +++ b/src/ccl/infer/typing.rs @@ -162,7 +162,7 @@ pub(super) trait Typing { /// for the two forms this obligation serves. /// /// **Returns the normalized annotation**, because normalizing is not - /// idempotent: a `Hole` or a [`Type::Below`] mints a fresh variable each time, + /// idempotent: a `Hole` or a [`Type::BoundedHole`] mints a fresh variable each time, /// so a caller that both reconciles against an annotation and binds at it must /// use one normalization for both or it relates two unrelated variables. fn bind_annotation(&mut self, inferred: &Type, ann: &Type) -> Result; diff --git a/src/ccl/lower/functions.rs b/src/ccl/lower/functions.rs index 215fb1fe..20f4ba31 100644 --- a/src/ccl/lower/functions.rs +++ b/src/ccl/lower/functions.rs @@ -9,7 +9,7 @@ use std::collections::HashSet; use super::*; use crate::{ ccl::{Expr, Name, Type, TypedExprNode}, - chl_parser::ast::{Param, Span, Spanned}, + chl_parser::ast::{AnnotationMode, Param, Span, Spanned}, }; /// If `param` is annotated `Mut(…)` (a pass-by-reference mutable-variable parameter), @@ -28,11 +28,24 @@ use crate::{ fn mut_param_history_type(param: &Param) -> Option> { let annotation = param.annotation.as_ref()?; match mut_annotation_parts(&annotation.ty) { - // The mode rides the *value* type, as at a `:=` introduction: a bounded - // `def f(v <: Mut(V))` infers the parameter's value type under `<: V`. + // A `Mut(…)` annotation is exact wherever it is written, for the reason it is + // exact at a `:=` introduction: [`Type::History`] is invariant in both + // payloads, so `<: Mut(V)` admits exactly `Mut(V, D)` and says nothing `:` + // does not (`lower::stmts::check_mut_decl_annotation`). + Some(Ok(_)) if annotation.mode == AnnotationMode::Bounded => { + Some(Err(LoweringError::unsupported( + param.name_span, + format!( + "`{} <: Mut(…)` bounds a mutable parameter by its own type: `Mut` is \ + invariant in its value type, so `<:` claims nothing `:` does not. \ + Write `{}: Mut(…)`", + param.name, param.name + ), + ))) + } Some(Ok((value, is_txn))) => Some(Ok(( Type::History { - value: Box::new(apply_annotation_mode(annotation.mode, value)), + value: Box::new(value), domain: Box::new(Type::Hole), kind: crate::ccl::HistoryKind::Overwrite, }, diff --git a/src/ccl/lower/stmts.rs b/src/ccl/lower/stmts.rs index 39e08da2..11bd5f51 100644 --- a/src/ccl/lower/stmts.rs +++ b/src/ccl/lower/stmts.rs @@ -578,24 +578,15 @@ pub(super) fn lower_middle_stmt( } // Otherwise this is an *introduction*. Resolve the optional // annotation to `(value type, transactional?)`: - // (none) → induction accumulator, value type inferred - // `x: Mut(V) := e` → induction accumulator at value type `V` - // `x: Mut(V, Txn)` → transactional mutable variable at value type `V` - // `x: T := e` → induction accumulator at value type `T` - // `x <: T := e` → value type inferred, bounded above by `T` + // (none) → induction accumulator, value type inferred + // `x: Mut(V) := e` → induction accumulator at value type `V` + // `x: Mut(V, Txn) := e` → transactional mutable variable at value type `V` // - // In every annotated case the mode applies to the *value* type, which is - // what the annotation names: `Mut(V)` contributes `V` and the domain is - // decided below, so `x <: Mut(V) := e` and `x <: V := e` agree. + // Those are the only forms: an annotation on a `:=` binder is exact and + // is a `Mut(…)` (`check_mut_decl_annotation`). let (value_ty, is_txn) = match annotation { None => (Type::Hole, false), - Some(ann) => match mut_annotation_parts(&ann.ty) { - Some(parts) => { - let (value, is_txn) = parts?; - (apply_annotation_mode(ann.mode, value), is_txn) - } - None => (lower_type_annotation(ann)?, false), - }, + Some(ann) => check_mut_decl_annotation(&name, ann, stmt.span)?, }; // Stamp the binding `Mut(V, D)` (so inference binds `x` at `Mut` and // its references deref to `V`). `D = Txn` for a transactional mutable variable @@ -848,6 +839,77 @@ pub(super) fn check_mut_write_context( Ok(()) } +/// Resolve the annotation on a `:=` **introduction** to `(value type, transactional?)`, +/// rejecting the two forms that would have to be reinterpreted to be accepted. +/// +/// A `:=` binder's type *is* a `Mut(V, D)`, so that is what an annotation on one +/// names. Two consequences, and the rule is their conjunction — **an annotation on +/// a `:=` binder is exact and is a `Mut(…)`**: +/// +/// - A plain value type names the wrong thing. `x: Int := e` binds `x` at +/// `Mut(Int, D)`, not at `Int`, so reading it as the value type would make `:` +/// mean something here it means nowhere else. +/// - `<:` claims nothing `:` does not. [`Type::History`] is invariant in both +/// payloads (`solver::constrain`), so the only type below `Mut(V, D)` is +/// `Mut(V, D)`. +/// +/// Both are rejected rather than reinterpreted, and both have the same remedy, so +/// they share one diagnostic. This leaves "a mutable whose value type is inferred +/// under a ceiling" unspellable, which is the honest position: under invariance it +/// is not a bound on the binder's type at all, and no syntax for a bound in the +/// *value* position exists (`<:` does not appear inside a type literal — see +/// `docs/chl-spec.md`, "Two annotation forms: exact and bounded"). +pub(super) fn check_mut_decl_annotation( + name: &str, + ann: &TypeAnnotation, + span: Span, +) -> Result<(Type, bool), LoweringError> { + let parts = mut_annotation_parts(&ann.ty).transpose()?; + if let (AnnotationMode::Exact, Some(parts)) = (ann.mode, parts.clone()) { + return Ok(parts); + } + // Not accepted. Render what was written — lowering a non-`Mut` annotation + // here so an annotation that is not a type at all reports *that* instead. + let (value, is_txn, is_mut) = match parts { + Some((value, is_txn)) => (value, is_txn, true), + None => (lower_type_expr(&ann.ty)?, false, false), + }; + let op = match ann.mode { + AnnotationMode::Exact => ":", + AnnotationMode::Bounded => "<:", + }; + let written = if is_mut { + format!("{}", MutForm(&value, is_txn)) + } else { + value.to_string() + }; + let remedy = MutForm(&value, is_txn); + Err(LoweringError::unsupported( + span, + format!( + "`{name} {op} {written} := …` is not a valid mutable-variable annotation: a \ + `:=` binder's type is `Mut(V, D)`, and `Mut` is invariant in `V`, so the \ + annotation names the whole variable and is always exact. Write \ + `{name}: {remedy} := init`, or drop the annotation to infer the value type \ + (`{name} := init`)" + ), + )) +} + +/// Renders a value type back as the `Mut(…)` annotation that declares it. +struct MutForm<'a>(&'a Type, bool); + +impl std::fmt::Display for MutForm<'_> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let Self(value, is_txn) = self; + if *is_txn { + write!(f, "Mut({value}, Txn)") + } else { + write!(f, "Mut({value})") + } + } +} + /// If `annotation` is a `Mut(…)` form, extract its declared *value* type and /// whether it is **transactional** (`Mut(V, Txn)`). /// @@ -962,41 +1024,29 @@ pub(super) fn pre_register_txn_decls(stmts: &[Spanned], ctx: &mut Lower /// Whether a binder annotation is a pass-by-reference `Mut(…)` form. /// -/// Reads the annotation's *type* only: the mode is orthogonal to whether the -/// binder names a mutable variable (`x <: Mut(V) := e` introduces one just as -/// `x: Mut(V) := e` does). +/// Reads the annotation's *type* only. This runs during pre-registration, before +/// the mode is validated, so a bounded `Mut(…)` still answers `true` here and is +/// rejected where the parameter is lowered +/// (`lower::functions::mut_param_history_type`) — registering it either way is +/// harmless, since the rejection is what the program sees. fn is_mut_annotation(annotation: &TypeAnnotation) -> bool { mut_annotation_parts(&annotation.ty).is_some() } /// Lower a binder's type annotation, applying its [`AnnotationMode`]. /// -/// `x: T` lowers to `T`; `x <: T` lowers to [`Type::Below`], the marker +/// `x: T` lowers to `T`; `x <: T` lowers to [`Type::BoundedHole`], the marker /// `normalize_annotation` turns into an inference variable bounded above by `T`. /// The mode is a property of the *binder*, not of a type: `<:` is grammatical only /// where a binder is introduced, so nested positions inside `T` are always exact /// and [`lower_type_expr`] needs no mode parameter. (Design: /// `src/ccl/design/type-inference.md`, "Annotation kinds: exact and bounded".) pub(super) fn lower_type_annotation(annotation: &TypeAnnotation) -> Result { - Ok(apply_annotation_mode( - annotation.mode, - lower_type_expr(&annotation.ty)?, - )) -} - -/// Wrap a lowered annotation type in its binder's mode. -/// -/// Separate from [`lower_type_annotation`] because a `Mut(…)` annotation is not -/// lowered as one type: `mut_annotation_parts` splits it into a *value* type and a -/// domain, and the binder's mode belongs to the value — `x <: Mut(V) := e` bounds -/// the mutable variable's value type, exactly as `x <: V := e` does. Applying the mode in -/// one place is what keeps those two spellings from disagreeing, which is how the -/// `Mut` form came to silently drop its mode and read as exact. -pub(super) fn apply_annotation_mode(mode: AnnotationMode, ty: Type) -> Type { - match mode { + let ty = lower_type_expr(&annotation.ty)?; + Ok(match annotation.mode { AnnotationMode::Exact => ty, - AnnotationMode::Bounded => Type::Below(Box::new(ty)), - } + AnnotationMode::Bounded => Type::BoundedHole(Box::new(ty)), + }) } /// Lower a CHL type *expression* to a CCL [`Type`]. diff --git a/src/ccl/subst.rs b/src/ccl/subst.rs index 79b16d65..e023580f 100644 --- a/src/ccl/subst.rs +++ b/src/ccl/subst.rs @@ -756,7 +756,7 @@ impl Subst { fn rewrite_type_go(&self, ty: &mut Type, memo: &PredMemo) { match ty { - Type::Below(t) => self.rewrite_type_go(t, memo), + Type::BoundedHole(t) => self.rewrite_type_go(t, memo), Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) @@ -976,7 +976,7 @@ impl Subst { fn apply_type_inner(&self, ty: &Type) -> Type { match ty { - Type::Below(t) => Type::Below(Box::new(self.apply_type_inner(t))), + Type::BoundedHole(t) => Type::BoundedHole(Box::new(self.apply_type_inner(t))), Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) @@ -1107,9 +1107,9 @@ pub fn type_contains_infer(ty: &Type) -> bool { Type::Variant(tags) => tags.iter().any(|(_, t)| type_contains_infer(t)), Type::Refinement(base, _) => type_contains_infer(base), // Annotation position only, and normalized away before solving. Answering - // for the bounded type is the honest reading of the question; a `Below` that - // reaches here at all is reported as `UnresolvedBelow`, not by this test. - Type::Below(t) => type_contains_infer(t), + // for the bounded type is the honest reading of the question; a `BoundedHole` that + // reaches here at all is reported as `UnresolvedBoundedHole`, not by this test. + Type::BoundedHole(t) => type_contains_infer(t), } } @@ -1143,7 +1143,7 @@ fn collect_type_fv( // A bounded annotation binds nothing, so its bound's free variables are // free in it — a name referenced only from inside an annotation is still // referenced. - Type::Below(t) => collect_type_fv(t, bound, visited, out), + Type::BoundedHole(t) => collect_type_fv(t, bound, visited, out), Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index 40fe9c4c..7b9d7cfc 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -483,7 +483,7 @@ pub fn reset_kind_var_counter() { /// | Variant | Owner | Meaning | Must be eliminated by | /// |---|---|---|---| /// | `Hole` | Lowering | "This slot needs a type; not yet known" | End of inference (compiler bug if survives — flagged as `UnresolvedHole`) | -/// | `Below(𝑇)` | Lowering | "A bounded annotation `𝑥 <: 𝑇`: infer this, subject to `<: 𝑇`" — an obligation, not a shape | Pass 1's `normalize_annotation` (flagged as `UnresolvedBelow` if it survives) | +/// | `BoundedHole(𝑇)` | Lowering | "A bounded annotation `𝑥 <: 𝑇`: infer this, subject to `<: 𝑇`" — an obligation, not a shape | Pass 1's `normalize_annotation` (flagged as `UnresolvedBoundedHole` if it survives) | /// | `Infer(id)` | Type checker only | "Inference variable N from the coalesce pass" | End of inference for any type reachable from the program's root output (flagged as `UnresolvedInfer` by `collect_type_errors`); an induction accumulator's *domain* is necessarily `Infer` until the unified phase resolves it (see `Strictness::PreDesugar`) | /// | `History` (`kind: Overwrite`) | Type checker only | "Mutable variable: a `value` cell tracked over a `domain` (loop index or transaction time)" | the unified phase (`transact_phase` / `mut_elim`, which runs *before* `channelize`; a survivor downstream is a compiler bug) | /// | `History` (`kind: Feed`) | Type checker only | "Feed channel `domain ⇒ value`: the defer binding's post-desugar stream type" | `channelize` (which runs after inference; a survivor downstream is a compiler bug) | @@ -582,7 +582,7 @@ pub enum Type { /// **This is not a type.** Like [`Hole`](Self::Hole) and [`Infer`](Self::Infer) /// it denotes no set of values — it is a *slot* inhabiting the `Type` enum /// because annotations are typed positions, and it states an obligation for - /// inference rather than a shape. `Below(𝑇)` is not "the type of values below + /// inference rather than a shape. `BoundedHole(𝑇)` is not "the type of values below /// `𝑇`": there is no such type, which is why nothing may subtype against one, /// narrow against one, or compact one. The solver has no rule for it and asserts /// so (`constrain::extrude`, `compact`); only the @@ -594,10 +594,10 @@ pub enum Type { /// occupies do not survive inference at all /// (`infer::api::debug_assert_annotations_cleared`), so a binder `ty` is the /// only place a survivor could hide — flagged there by `collect_type_errors` - /// as [`InferError::UnresolvedBelow`](crate::ccl::infer::InferError::UnresolvedBelow). + /// as [`InferError::UnresolvedBoundedHole`](crate::ccl::infer::InferError::UnresolvedBoundedHole). /// /// See `src/ccl/design/type-inference.md`, "Annotation kinds: exact and bounded". - Below(Box), + BoundedHole(Box), /// Unresolved type variable, identified by a unique [`crate::ccl::InferVarId`]. /// /// Created during inference by the inference pass @@ -779,7 +779,7 @@ impl fmt::Display for Type { Type::Base(b) => write!(f, "{}", b.keyword()), // `n == 0` means an empty range (e.g. the domain of `[]`); render // it as `∅` instead of computing `n - 1` and underflowing. - Type::Below(t) => write!(f, "<:{t}"), + Type::BoundedHole(t) => write!(f, "<:{t}"), Type::UIntRange(0) => write!(f, "∅"), Type::UIntRange(n) => write!(f, "[0, {}]", n - 1), // The arrow reflects the resolved `kind`: `⇒` for a compute @@ -1101,7 +1101,7 @@ impl Type { domain: Box::new(domain.without_pi_names()), codomain: Box::new(codomain.without_pi_names()), }, - Type::Below(t) => Type::Below(Box::new(t.without_pi_names())), + Type::BoundedHole(t) => Type::BoundedHole(Box::new(t.without_pi_names())), Type::Tuple(ts) => Type::Tuple(ts.iter().map(|t| t.without_pi_names()).collect()), Type::Record(fs) => Type::Record( fs.iter() @@ -1171,7 +1171,7 @@ impl Type { // A bounded annotation's bound is an ordinary child type — a pass // that rewrites types (uniquify's α-renaming, `subst`) must reach // inside it exactly as it reaches inside a `Refinement`. - Type::Below(t) => f(t), + Type::BoundedHole(t) => f(t), Type::Fun { domain, codomain, .. } => { @@ -1217,7 +1217,7 @@ impl Type { // A bounded annotation's bound is an ordinary child type — a pass // that rewrites types (uniquify's α-renaming, `subst`) must reach // inside it exactly as it reaches inside a `Refinement`. - Type::Below(t) => f(t), + Type::BoundedHole(t) => f(t), Type::Fun { domain, codomain, .. } => { diff --git a/src/chl_parser/ast.rs b/src/chl_parser/ast.rs index fbaf1e16..e0058cd0 100644 --- a/src/chl_parser/ast.rs +++ b/src/chl_parser/ast.rs @@ -274,7 +274,7 @@ pub struct Param { /// /// The two spellings differ only in the mode; the type expression is parsed /// identically. Lowering turns [`AnnotationMode::Bounded`] into a -/// [`crate::ccl::Type::Below`] wrapper and leaves `Exact` bare. +/// [`crate::ccl::Type::BoundedHole`] wrapper and leaves `Exact` bare. #[derive(Debug, Clone, PartialEq)] pub struct TypeAnnotation { pub mode: AnnotationMode, diff --git a/tests/compilation_pipeline/mutability.rs b/tests/compilation_pipeline/mutability.rs index 3f053350..26a51b79 100644 --- a/tests/compilation_pipeline/mutability.rs +++ b/tests/compilation_pipeline/mutability.rs @@ -639,7 +639,8 @@ fn mut_annotation_with_non_txn_domain_rejected() { /// annotation says nothing about whether it introduces a mutable variable. Gating on the /// annotation instead accepted the bare `y := 0` — which then fell back to a /// per-iteration shadowing `let`, silently discarding each update at the iteration -/// boundary, the very thing `:=` exists to avoid. +/// boundary, the very thing `:=` exists to avoid. (The spellings are the ones a +/// `:=` binder accepts at all — see `mut_decl_annotation_is_exact_and_is_a_mut`.) #[rstest] #[case::annotated_mut(indoc! {r#" t := 0 @@ -648,13 +649,6 @@ fn mut_annotation_with_non_txn_domain_rejected() { t += y t "#})] -#[case::annotated_value(indoc! {r#" - t := 0 - for i in [1, 2, 3]: - y: Int := i - t += y - t -"#})] #[case::bare(indoc! {r#" t := 0 for i in [1, 2, 3]: @@ -662,17 +656,10 @@ fn mut_annotation_with_non_txn_domain_rejected() { t += y t "#})] -#[case::bounded_mut(indoc! {r#" +#[case::annotated_txn(indoc! {r#" t := 0 for i in [1, 2, 3]: - y <: Mut(Int) := i - t += y - t -"#})] -#[case::bounded_value(indoc! {r#" - t := 0 - for i in [1, 2, 3]: - y <: Int := i + y: Mut(Int, Txn) := i t += y t "#})] @@ -680,6 +667,55 @@ fn register_declared_inside_loop_rejected(#[case] code: &str) { expect_compile_error(code, "introduced inside a for-loop body"); } +/// An annotation on a `:=` binder is **exact** and is a **`Mut(…)`**. Both halves +/// are rejections rather than reinterpretations, and they share one diagnostic +/// because they share one remedy. +/// +/// A plain value type names the wrong thing — `y: Int := 0` binds `y` at +/// `Mut(Int, D)`, not at `Int`, so reading the annotation as the value type would +/// make `:` mean something at a `:=` binder that it means at no other. And `<:` +/// claims nothing `:` does not: `Type::History` is invariant in both payloads, so +/// the only type below `Mut(V, D)` is `Mut(V, D)` itself. +#[rstest] +#[case::bare_value_exact("y: Int := 0\ny")] +#[case::bare_value_bounded("y <: Int := 0\ny")] +#[case::mut_bounded("y <: Mut(Int) := 0\ny")] +#[case::mut_txn_bounded("y <: Mut(Int, Txn) := 0\ny")] +fn mut_decl_annotation_is_exact_and_is_a_mut(#[case] code: &str) { + expect_compile_error(code, "is not a valid mutable-variable annotation"); +} + +/// The remedy the diagnostic names is the one that compiles, in both the plain and +/// the transactional case — the rejection is not hiding a second problem. +#[test] +fn the_exact_mut_spelling_the_diagnostic_names_compiles() { + check_scalar( + indoc! {r#" + y: Mut(Int) := 0 + y += 5 + y + "#}, + cambra::interpreter::Value::Int(5), + ); +} + +/// A `Mut(…)` annotation is exact wherever it is written, so the same invariance +/// argument rejects a bounded pass-by-reference parameter. +#[test] +fn a_bounded_mut_param_is_rejected() { + expect_compile_error( + indoc! {r#" + def bump(c <: Mut(Int)): + c := c + 1 + cnt: Mut(Int) := 0 + for i in [1, 2, 3]: + bump(cnt) + cnt + "#}, + "invariant in its value type", + ); +} + /// `op=` inside a for-loop body is a **mutable write**, so a target that is not a /// mutable variable declared before the loop is a type error rather than a rebind — /// the spec's *"a `+=` to an immutable binding is a type error, not a silent diff --git a/tests/type_check.rs b/tests/type_check.rs index a221a194..9197ec96 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -2805,17 +2805,15 @@ mod annotation_kinds { ); } - /// A binder's mode applies to a mutable variable's **value** type, so `a <: Mut(V)` and - /// `a <: V` are the same declaration — and both agree with writing no annotation - /// at all, since a bound the inferred type already satisfies admits it rather - /// than replacing it. + /// The one annotated spelling a `:=` binder accepts is exact and is a `Mut(…)`, + /// and it means at a mutable variable what it means at any other binder: the + /// annotation *is* the type, so it discards what the value knew beyond it. /// - /// The `Mut(…)` spelling used to read as *exact*: lowering split the annotation - /// into a value type and a domain and dropped the mode on the way, so the bounded - /// form discarded the singleton that the unannotated form keeps — a bound that - /// lost information. + /// `a: Mut(Int) := 5` therefore binds the value at `Int`, while the unannotated + /// `a := 5` keeps the seed's singleton. The rejected spellings are covered by + /// `mut_decl_annotation_is_exact_and_is_a_mut` (they fail at lowering). #[test] - fn a_bound_on_a_mut_var_bounds_its_value_type() { + fn an_exact_mut_annotation_discards_the_seeds_singleton() { // Compared by mutable variable *value* type. Each program ends in a bare read, and a // tail denotes the mutable variable's *value*, so the program type is that value type // directly — which also keeps the per-run domain variable, whose id differs @@ -2828,26 +2826,14 @@ mod annotation_kinds { ); ty }; - // No writes, so the value type is the seed's — the bound admits `5`. - let bare = mut_value(indoc! {r#" - a := 5 - a - "#}); - assert_eq!( - mut_value(indoc! {r#" - a <: Mut(Int) := 5 - a - "#}), - bare - ); - assert_eq!( + // No writes, so the unannotated value type is the seed's singleton. + assert_ne!( mut_value(indoc! {r#" - a <: Int := 5 + a := 5 a "#}), - bare + int() ); - // The exact form is what discards the singleton. assert_eq!( mut_value(indoc! {r#" a: Mut(Int) := 5 @@ -2855,27 +2841,20 @@ mod annotation_kinds { "#}), int() ); - assert_ne!( - mut_value(indoc! {r#" - a <: Mut(Int) := 5 - a - "#}), - int() - ); - // With a write, the value type is the join over seed and writes, so both - // modes land on `Int` — the bound is satisfied, not doing the widening. + // With a write, the value type is the join over seed and writes, so the + // unannotated form lands on `Int` too — the annotation is not what widens it. assert_eq!( mut_value(indoc! {r#" - a <: Mut(Int) := 0 + a := 0 a += 1 a "#}), int() ); - // And it is still a *declaration*, so the deref-copy below it is a read. + // It is still a *declaration*, so the deref-copy below it is a read. assert_eq!( infer_program(indoc! {r#" - a <: Mut(Int) := 0 + a: Mut(Int) := 0 b: Int = a b "#}), @@ -2883,10 +2862,10 @@ mod annotation_kinds { ); } - /// The bound is a real obligation on a bounded mutable variable, discharged against both - /// contributions to its value type: the seed and every write. + /// The exact annotation is a real obligation on the mutable variable, discharged + /// against both contributions to its value type: the seed and every write. #[test] - fn a_bounded_mut_vars_bound_constrains_seed_and_writes() { + fn a_mut_vars_annotation_constrains_seed_and_writes() { let rejects = |code: &str, needle: &str| { let errs = infer_program_err(code); let rendered = format!("{errs:?}"); @@ -2897,14 +2876,14 @@ mod annotation_kinds { }; rejects( indoc! {r#" - a <: Mut(Int) := "s" + a: Mut(Int) := "s" a "#}, "initializer of mutable `a`", ); rejects( indoc! {r#" - a <: Mut(Int) := 0 + a: Mut(Int) := 0 for i in [1, 2]: a := "s" a