diff --git a/docs/chl-spec.md b/docs/chl-spec.md index e4160de7..ca4b7124 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 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. > **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 @@ -1406,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: @@ -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,103 @@ 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 — 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 +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. `<:` 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 +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 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 + 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 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 +> *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.) @@ -2015,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 ``` @@ -2030,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 b5727136..4f2e13f7 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::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 3584cfd7..b86c64f3 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::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. @@ -761,11 +762,107 @@ 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 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. + + 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. + +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) | +|---|---|---| +| `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 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. + +#### BoundedHole is a marker in a type slot, not a type + +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 `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 `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([𝐴, 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. + +#### BoundedHole cannot outlive inference + +`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 `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 `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 + +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 `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 + +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::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 7db70c4b..77446c6c 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::BoundedHole`] bounded-annotation marker survived past inference. + /// + /// Like [`InferError::UnresolvedHole`], a compiler bug rather than a + /// user-facing error: `normalize_annotation` erases every `BoundedHole` it is handed, + /// so a survivor means a slot inference never normalized. + UnresolvedBoundedHole { + /// 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::UnresolvedBoundedHole { 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::BoundedHole(_) => errors.push(InferError::UnresolvedBoundedHole { + 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::BoundedHole(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,23 @@ mod tests { assert_eq!(check_fully_typed(&expr), Ok(())); } + /// A `Type::BoundedHole` surviving inference fails with `UnresolvedBoundedHole`. + /// + /// A backstop, like `UnresolvedHole`: `normalize_annotation` erases every + /// `BoundedHole` it is handed, and a bounded annotation that somehow reaches the + /// solver un-normalized is rejected earlier (nothing can be constrained against + /// 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_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::UnresolvedBoundedHole { 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..dd4d35d2 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -179,6 +179,40 @@ 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 `BoundedHole` is consumed; every other pass either + // rewrites through it structurally or treats it as unreachable. + // + // 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}); `<:` on a `Mut(…)` \ + annotation is rejected at lowering" + ) + } + 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`, + // 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 +429,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 +463,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..47e59276 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 + // `BoundedHole` here: recurse into the bound, or a predicate written inside one + // (`x <: {Int | p}`) never gets typed. + 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 @@ -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::BoundedHole(_) => 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..d66715d2 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1325,6 +1325,14 @@ 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 { + // `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::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 — // 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..80bdaefe 100644 --- a/src/ccl/infer/solver/compact.rs +++ b/src/ccl/infer/solver/compact.rs @@ -589,6 +589,13 @@ 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::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. Type::Base(_) diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index 6a8f9518..5a4d6aaa 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -985,6 +985,13 @@ 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::BoundedHole`). + Type::BoundedHole(_) => { + unreachable!( + "Type::BoundedHole 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..5a11a6f1 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::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 0a1a8298..9db56a63 100644 --- a/src/ccl/infer/solver/scheme.rs +++ b/src/ccl/infer/solver/scheme.rs @@ -235,6 +235,14 @@ pub fn freshen_above( return ty.clone(); } match ty { + // `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::BoundedHole(_) => { + unreachable!( + "Type::BoundedHole 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..b0de6417 100644 --- a/src/ccl/infer/solver/spec_key.rs +++ b/src/ccl/infer/solver/spec_key.rs @@ -343,6 +343,14 @@ pub fn spec_key(ty: &Type) -> SpecKey { fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView { match ty { + // `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::BoundedHole(_) => { + unreachable!( + "Type::BoundedHole 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..ec8dcb7f 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::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; /// 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..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), @@ -27,7 +27,22 @@ 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) { + // 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(value), 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..11bd5f51 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 @@ -576,16 +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` + // (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` + // + // 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) { - Some(parts) => parts?, - 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 @@ -838,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)`). /// @@ -864,9 +936,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 +996,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 +1022,34 @@ 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. 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::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 { + let ty = lower_type_expr(&annotation.ty)?; + Ok(match annotation.mode { + AnnotationMode::Exact => ty, + AnnotationMode::Bounded => Type::BoundedHole(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 +1065,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 +1083,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 +1171,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..e023580f 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::BoundedHole(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::BoundedHole(t) => Type::BoundedHole(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 `BoundedHole` that + // reaches here at all is reported as `UnresolvedBoundedHole`, not by this test. + Type::BoundedHole(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::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 a914316a..7b9d7cfc 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`) | +/// | `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) | @@ -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. `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 + /// *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::UnresolvedBoundedHole`](crate::ccl::infer::InferError::UnresolvedBoundedHole). + /// + /// See `src/ccl/design/type-inference.md`, "Annotation kinds: exact and bounded". + BoundedHole(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::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 @@ -1071,6 +1101,7 @@ impl Type { domain: Box::new(domain.without_pi_names()), codomain: Box::new(codomain.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() @@ -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::BoundedHole(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::BoundedHole(t) => f(t), Type::Fun { domain, codomain, .. } => { diff --git a/src/chl_parser/ast.rs b/src/chl_parser/ast.rs index f33f2671..e0058cd0 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::BoundedHole`] 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..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,24 +649,73 @@ fn mut_annotation_with_non_txn_domain_rejected() { t += y t "#})] -#[case::annotated_value(indoc! {r#" +#[case::bare(indoc! {r#" t := 0 for i in [1, 2, 3]: - y: Int := i + y := i t += y t "#})] -#[case::bare(indoc! {r#" +#[case::annotated_txn(indoc! {r#" t := 0 for i in [1, 2, 3]: - y := i + y: Mut(Int, Txn) := i t += y t "#})] -fn mut_var_declared_inside_loop_rejected(#[case] code: &str) { +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 @@ -1220,17 +1270,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 +1292,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..9197ec96 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( @@ -970,7 +988,26 @@ 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(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(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!( @@ -987,6 +1024,15 @@ 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(indoc! {r#" + def g(a <: Int, b: String): + a + g(1, "x") + "#}), int_lit(1) ); // Wrong type on `a` is rejected. @@ -1098,14 +1144,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 +2041,43 @@ 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(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_lit(1)); + 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_lit(1)); + 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 @@ -2550,3 +2636,259 @@ 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(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(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 + /// two positions now read an annotation the same way. + #[test] + fn the_two_binder_positions_agree() { + assert!( + !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(indoc! {r#" + def f(v <: {a: Int}): + v.b + f((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(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 + /// 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() { + 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(indoc! {r#" + x: List(_) = [1, 2, 3] + sum(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 = indoc! {r#" + + v + 1 + + a = f(1) + b = f(2) + a + + "#}; + 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(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(indoc! {r#" + def f(v <: Int): + v + 1 + f(1) + f(2) + "#}), + 2, + "a bounded param still splits per argument, operator consumer or not" + ); + } + + /// 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. + /// + /// `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 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 + // every time, out of the comparison. + let mut_value = |code: &str| { + let ty = infer_program(code); + assert!( + ty.mut_value_type().is_none(), + "a tail read denotes the mutable variable's value, got the handle {ty}" + ); + ty + }; + // No writes, so the unannotated value type is the seed's singleton. + assert_ne!( + mut_value(indoc! {r#" + a := 5 + a + "#}), + int() + ); + assert_eq!( + mut_value(indoc! {r#" + a: Mut(Int) := 5 + a + "#}), + int() + ); + // 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 := 0 + a += 1 + a + "#}), + int() + ); + // It is still a *declaration*, so the deref-copy below it is a read. + assert_eq!( + infer_program(indoc! {r#" + a: Mut(Int) := 0 + b: Int = a + b + "#}), + int() + ); + } + + /// 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_mut_vars_annotation_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( + 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`", + ); + } +}