Type system

This document specifies Hale's type system: what types exist, how they relate, what the compiler verifies. Where the grammar (grammar.ebnf) tells you what's…

Reference material, synced from the compiler repo’s spec/. The guide is the gentler path in.

This document specifies Hale’s type system: what types exist, how they relate, what the compiler verifies. Where the grammar (grammar.ebnf) tells you what’s syntactically valid, this document tells you what’s meaningfully valid.

FnPtr (m80): First-class function values, type-spelled fn(T1, T2) -> R (or fn(T1, T2) for void-returning). LLVM lowering is ptr (raw fn pointer); calls go through build_indirect_call with an LLVM FunctionType synthesized from the FnPtr’s args/ret at the call site. The implicit __caller_arena: ptr first param of every user fn (m49 calling convention) is also expected on the FnPtr’s call ABI — indirect calls prepend it before user-visible args. See stdlib/io_tcp.hl for the canonical use: Listener.on_connection: fn(std::io::tcp::Stream).

FFI-portable subset (Stage-1 FFI): the primitive type set above carries an additional axis of distinction at the @ffi("c") boundary: which types have a stable C-ABI mapping. Int / Float / Bool / Duration / Time / String / Bytes / BytesView / StringView may appear in @ffi parameter and return positions; Decimal / Uint are typecheck-rejected (platform-variable ABI or Hale-internal). See spec/ffi.md for the full marshalling table and the lifetime contract.

Beside the primitives, a program declares the unit dialect’s scalar types. spec/units.md is their whole contract (the declarations, the laws, the algebra, the conversions and their policies, printing and the wire); what the type system holds of them is this. Each is a nominal named type, not a new primitive: the name survives resolution, two of them never unify, and each is represented as an Int.

An expression’s quantity or point type carries its denomination, and one no declaration names is a synthesized type, keyed by its quantity and its denomination as a monomorph is by its arguments, and displayed Money in 1/10000 cent (spec/units.md § Synthesized denominations). Duration and Time are a quantity and a point declared by the stdlib, which keep their own representation class (the table above).

A struct declares each field once, and an enum declares each variant once. A second declaration of a name already declared in the same type is a type error at the second, naming the first:

main.hl:4:5: type error: field `a` is already declared in type `T`;
a name is one slot, so declare it once
main.hl:2:5: the first declaration

The same rule holds for a locus’s or a perspective’s params, for the named members of a contract, and for an interface’s methods. Before it, the second declaration passed hale check and one of the two won the slot, with nothing in the source to say which — while the json codecs and a surface’s description assume one slot per name.

let b = <place>; where the place holds a struct — a field of self or of a child, a local, an element — binds a copy: a fresh struct in the frame’s own region (a method’s scratch; the caller’s arena for a binding the fn hands back), its String and Bytes fields cloned, nested structs copied the same way, locus handles left as handles. The binding then follows nothing: replacing the source (self.row = Row { }) leaves b as it was read, and writing through the binding (let mut c = self.row; c.n = 9;) leaves the source untouched. A literal or a call result is fresh already and is bound as it is. Assignment reads the same way (GH #992): b = <place> on a struct local, and arr[i] = <place> or b.inner = <place> under one, store a copy. And a write through a local never reaches another (GH #993): a copy may share an unchanged String with its source, so a String or Bytes field under a local root is replaced, never overwritten in place — only a locus’s own storage takes the in-place path. This finishes for structs the single-owner rule spec/memory.md states for String and Bytes stores (2026-09-22; before it the binding was a view of the storage, and an acknowledgement body read after the proposal field was cleared came back empty). A deliberate view has no spelling yet; read the field again when the current value is wanted.

type Name = Type; declares an alias: a second spelling of an existing type.

type Thing = Int;
type Row2  = Row;
type Names = Vec<String>;
type Span  = (Int, Int);

An alias is transparent, not nominal. It is replaced by its target wherever a type is written, so the alias and its target are the same type — they unify in both directions, share every field, and dispatch to the same methods:

type Thing = Int;

fn bump(t: Thing) -> Thing { return t + 1; }

fn main() {
    let t: Thing = 3;      // an Int
    let u: Int = bump(t);  // and back, with no conversion
}

The consequences are all one rule:

• Structural, never nominal. An alias declares no type of its own, so nothing attaches to the alias name. type Held = Holder; names the locus Holder; held.method() is Holder’s method. There is no way to give an alias behaviour its target does not have — for a distinct type with its own methods, declare a locus or a struct.

• Transparent in every type position: let ascriptions, struct fields, params, function parameters and return types, capacity cell types (the form’s indexed_by resolves to the target’s field), generic arguments, and nested shapes ([Row2; 2], (Thing, Thing)).

• An alias chains. type A = B; type B = Int; makes A an Int. A chain that returns to a name it already visited names nothing and is a type error:

  main.hl:1:1: type error: type alias `A` is cyclic — an alias
  chain must end at a declared type

  A chain that ends at a bare name nothing declares is refused the same way, at the target rather than at every use of the alias (see “Bare type names” below).

• Transparent in construction too. A struct, locus or perspective literal, and an enum-variant path, may be spelled with the alias name: with type Row2 = Row;, Row2 { id: 1 } builds a Row, and with type C2 = Color;, C2::Red is Color::Red — both where a variant is constructed and where it is matched. Construction resolves the name through the alias chain to the declaration it ends at, so the value’s type, its fields and its methods are the target’s; the alias adds nothing and forgives nothing (a field the target does not declare is still an error). A literal whose alias target is not a declaration is still refused — nothing is constructible from type Thing = Int; or type TwoRows = [Row; 2];:

  main.hl:5:13: type error: `Thing` is not a struct type

• The alias form takes no generic parameters. type Twin<T> = Pair<T>; is not supported — the alias target must be a concrete type expression (which may itself be a generic instantiation, as type Names = Vec<String>; is). The parser refuses the parameter list, at the <:

  main.hl:1:10: parse error: generic type aliases are not
  supported; write the concrete alias `type Name = Pair<Int>;`

Rich<T>, Chunked<T>, Recognition<T> are language-native generic constructors. The compiler recognizes them and selects allocator + implementation strategy based on which projection- class wrapper a value carries (per memory.md).

The constraint <T: ProjectionClass> (per F.2) is a built-in “any-of-three” constraint: T must instantiate to Rich<U>, Chunked<U>, or Recognition<U> for some U. No trait system required.

fn process<P: ProjectionClass, T>(input: P<T>) -> P<U> { ... }

The compiler monomorphizes per concrete P instantiation.

A locus L { ... } declaration introduces a locus type L. Locus types have:

• A set of params (name, type, default value or : inferred); these are also the locus’s mutable state (per F.3 / §3 in decisions).
• Optional contract (expose / consume entries).
• Optional capacity slots (F.22 — pool X of T; / heap Y of T; declarations naming slots 1..N beyond the implicit slot 0 / Arena).
• Optional lifecycle methods (birth, accept, run, drain, dissolve, on_failure).
• Optional mode declarations (bulk, harmonic, resolution).
• Optional bus interface (subscribe, publish).
• Optional closure tests.
• Optional member fns.

Instantiating a locus type produces a locus handle of that type, allocated as a region within the enclosing scope (per memory.md).

A locus body may not declare a type. type X { ... } is a top-level declaration only (see grammar.ebnf: type_decl is a top_decl, not a locus_member), and a type inside a locus body is a type error at the type keyword:

main.hl:2:5: type error: `type Pair` is declared inside locus
`Holder`: `type` is a top-level declaration, not a locus member.
Move it above the locus — a top-level `type` is in scope
everywhere in the seed, including inside every locus.

A top-level type is the supported spelling and loses nothing: it is in scope inside every locus of the seed, so a locus that wants a record of its own declares it above itself and uses it unqualified. A locus-level type had no reading at all before this rule — the resolver registers no member type, so the name it introduced was invisible everywhere, including inside the locus that declared it.

Before this rule, the parser accepted the member and the checker ignored it, so such a program passed hale check and then failed in the backend with locus L member kind not yet lowered to codegen — a program the gate accepted that could not be built (GH #756, the sibling of the member const).

A locus body may not declare a const. const NAME: T = value; is a top-level declaration only (see grammar.ebnf: const_decl is a top_decl, not a locus_member), and a const inside a locus body is a type error at the const keyword:

main.hl:2:5: type error: `const limit` is declared inside locus
`Holder`: `const` is a top-level declaration, not a locus
member. Move it above the locus — a top-level `const` is in
scope inside every locus of the seed — or, if each instance
should carry its own, make it a params field with a default
(`params { limit: ... = ...; }`).

The two spellings the diagnostic names are the supported ones: a top-level const is in scope inside every locus of the seed (one value, shared, compile-time), and a params field with a default gives each instance its own copy (self.name). A locus-level const is neither — it is not per-instance state, so it is not reachable as self.name, and it had no settled spelling for the other two readings (L::name from outside, bare name inside).

Before this rule, the parser accepted the member and the checker typechecked its value, so such a program passed hale check and then failed in the backend with locus L member kind not yet lowered to codegen — a program the gate accepted that could not be built (GH #747).

Every locus type also carries three synthetic members the compiler injects, readable by name from any method body:

self.<name> resolves the synthetic member before any member the locus declares, so these three names are reserved: a params field, member fn, or capacity slot spelled children, k_max, or draining is a type error at its declaration, naming the synthetic member it collides with and suggesting a rename. The rule is unconditional — it holds for a locus that accepts no child type as much as for one that does, because the synthetic member is resolved in both.

The reservation is per-locus-namespace, not per-spelling: a type’s struct field may be named children (types carry no synthetic members), and so may a local binding or a fn parameter.

Cell<T> is the value type returned by acquire() (Pool slots) and alloc() (Heap slots), and accepted by release(c) / free(c). It is not user-spellable in source — there is no let x: Cell<Int> = ...; syntax. The type appears only at typecheck and codegen.

A perspective P { ... } declaration introduces a contract type P — a set of bodyless fn signatures (optionally a bus { subscribe/publish ... } surface) that form a stable ABI boundary. Holders program against the slot type perspective(P) — never a concrete impl — and dispatch through a single program-global, live-rebindable slot. A locus L : serves P provides the contract and can be swapped in behind the slot at pointer-flip cost via reperspective. An optional stable_when { ... } predicate feeds the (aspirational) transport-driven hot-load path. See semantics.md § Perspectives for the full model (contract / serves / slot / live swap).

An interface I { fn ...; ... } declaration introduces a structural interface type I — a named set of method signatures. A locus L satisfies I iff for every method in I, L declares a method with the same name, the same arity, compatible param types, and a compatible return type. Satisfaction is implicit: there is no impl I for L declaration.

Interface types appear in fn parameter positions:

fn render(sink: Sink) {
    sink.line("hello");
}

The structural-impl check fires at every call site where a fn declares an interface-typed param: missing-method, arity- mismatch, param-type, or return-type mismatches all produce typed diagnostics at typecheck time.

Fallible methods (GH #732). An interface method may declare fallible(E) after its return type, as a fn does:

interface Store {
    fn put(k: String) -> Int fallible(StoreError);
}

A call through the interface is a fallible call: or <fallback>, or handler(err), or raise and or discard apply as on a direct call, and a call that does not address the error is rejected. Which methods satisfy one:

• An infallible method satisfies a fallible interface method; a call through the interface then always takes the success path.
• A fallible method does not satisfy an infallible interface method.
• The error types must be the same type; there is no subtyping of error payloads.

A mismatch is a check-time error naming both signatures. An imported interface keeps its methods’ error types and enforces them the same way. The vtable slot of a fallible interface method holds a callee with the fallible locus-method ABI (i1 return, out_val / out_err slots); for an infallible method, the compiler puts a small adapter with that ABI in front of it.

v0.1 scope (Phase A + Phase B). Interface declarations parse, register, and the typechecker enforces the structural rule (Phase A, shipped 2026-05-10). Codegen vtable dispatch (Phase B) is shipped 2026-05-11. Interface values are fat pointers {data, vtable} allocated in the current arena; the data slot holds the underlying locus pointer (same single-ptr ABI as LocusRef) and the vtable slot holds a per-(locus, interface) static global of fn pointers indexed by interface- method declaration order. A locus flowing into an interface slot coerces at the call site; method calls on an interface value lower as indirect calls through vtable[i] with the data pointer passed as the implicit self arg.

Interface values are usable as fn parameters, fn returns, locus param / field values, and @form(vec) cell elements. Method-call receivers, polymorphic return through control flow, and pass-through aliasing (the original instantiator’s binding and the returned binding refer to the same underlying locus) all work end-to-end. The std::text::Sink stdlib migration (split Sink into StdoutSink / StringSink / FileSink loci behind one Sink interface) shipped 2026-05-11; see spec/stdlib.md and crates/hale-codegen/tests/sink_polymorphism.rs.

The implicit LocusRef → Interface coercion fires at the following positions:

• Free-fn arguments. fn render(s: Sink) accepts any LocusRef of a locus satisfying Sink.
• Locus-method arguments. fn add(t: Tower) on a Registry locus accepts the same coerce (added 2026-05-18).
• Returns. return r; from a fn declared -> Sink builds the fat pointer at the return site.
• type field initializers. TowerEntry { t: r } where field t is interface-typed coerces the LocusRef r (added 2026-05-18).
• Locus params / field initializers. Same shape as above for locus param defaults and locus L { params { t: Tower; } } slots.
• An interface VALUE into a field of the same interface (GH #730, 2026-09-22). Attempt { performer: self.performer } where both are Performer: identity, no structural check, no fat-pointer rebuild from a locus. The holder stores its own {data, vtable} pair and owns nothing — the impl is a borrow, exactly as a name in a field initialiser is (F.39) and as the assignment form self.f = handle has been since GH #967. The impl must outlive the holder; that is the same contract every borrowed handle carries, and the checker’s lifetime pass for it is #730’s remaining work. A value of a different interface is still refused.
• @form(vec) cell push. A Registry @form(vec) of Tower accepts pushes of any satisfying LocusRef.
• or <substitute> fallback expressions. When a fallible has success type Interface(I), an or fallback expression of LocusRef type satisfying I coerces (added 2026-05-18). E.g. lookup(...) or Hello { } where lookup returns Greeter fallible(...).
• let-binding ascription with composite type (G20). let arr: [Greeter; 2] = [Hi {}, Hey {}]; coerces each element through the ascription’s element type; same shape for let pair: (Greeter, Greeter) = (Hi {}, Hey {}); and let arr: [Greeter; 3] = [Hi {}; 3];. The codegen routes the RHS through lower_expr_into(expr, hint) so the composite-element coerce fires per position. The single- element let-ascription case is still permissive-via-Unknown (interface names resolve to Ty::Unknown at typecheck per collect_known_names); composite-element coercion picks up where the single case’s implicit handling leaves off.

The return path uses two cooperating mechanisms: at the return site, an implicit locus → interface coercion builds the fat pointer, and the locus-instantiation routing extension (the same m90 shape that handles -> LocusRef(L) returns) routes any instantiation of a satisfying locus inside an -> Interface(I) fn body to the program-lifetime payload arena. The fat-pointer struct itself is then deep-copied into the caller’s arena by emit_return_value_deep_copy. Single-element coverage is in crates/hale-codegen/tests/interface_return.rs.

Composite-construction coercion (G20). Interface elements inside fixed-size arrays, array-repeat literals, and tuples are now coerced at the construction site when the destination type is known. The let-RHS with a composite ascription is the wired entry point:

let arr:  [Greeter; 2]    = [Hi { }, Hey { }];
let arr3: [Greeter; 3]    = [Hi { }; 3];
let pair: (Greeter, Greeter) = (Hi { }, Hey { });

The codegen propagates the ascription’s element type through lower_expr_into(expr, hint) so per-position coerce_to_interface fires before the array’s “mixes element types” check would otherwise reject heterogeneous LocusRefs. Tests live in crates/hale-codegen/tests/interface_in_composites.rs.

Once the let-RHS coerces, the array’s static type is already Array<Interface, N> (or the tuple’s positional types are Interface), so flowing it to fn-args, struct fields, or return positions of the same type goes through plain type matching — no further coercion is needed at the consumer side.

Still deferred: locus-routing across nested return positions — a fn declared -> [Greeter; N] instantiating loci inline in its return expression still aliases the fn’s stack frame. Closing that needs the m90 routing extension to fire on nested locus instantiations inside composite returns, the same gap that governs tuple-of-LocusRef escape today.

F.11 child acceptance (accept(c: ConcreteLocus) { ... }) is intentionally NOT in the coerce list above. The child-accept mechanism keys dispatch by exact concrete locus name across substrate sites — accept fn signature, the self.children storage layout, and the parent’s accept-dispatch table — so accept(c: Iface) is a multi-system change, not a coercion wire-up. Single-accept-type per parent is the v1 design.

Interfaces have no default methods at v0; the body is signature- only. No interface inheritance, no multi-interface bounds on generics, no interface equality. F.21 sketches a paired substrate-aware (cascading-dimension) interface form for the n-dim growth case; not implemented at v0.

Lotus is invariant at the type level — no implicit subtyping. A Rich<int> is not assignable to a Chunked<int> even though both wrap int; explicit conversion required.

Exception: contract-graded subtyping (next section).

A single documented one-way widening fires at the following surfaces:

• let-binding type ascription: let nf: Float = self.n; where self.n: Int widens n to a Float at the binding site (codegen sitofp).
• fn-arg coercion: when a parameter is typed Float and the call-site argument is typed Int, the argument widens at the call site. Same rule applies to user-declared fns and to stdlib path-calls (std::math::sqrt(n) with n: Int works without 2.0 literals).
• binary-op promotion (B13 / G30): when exactly one side of a numeric binop is Int and the other Float, the Int side widens to Float and the op produces Float. Same rule covers comparison ops (<, >=, ==) so i < 0.5 typechecks. Symmetric — either side can be the one that widens.
• user-type field init: assigning an Int value into a Float-typed struct field at literal-init time widens at the store, mirroring fn-arg coercion. Lets a config bundle declare timeout: Float and accept an Int from the caller without sprinkling Float(n) casts.
• return: a fn or method declared -> Float that returns an Int — return n; or a block-tail n — widens it at the return, mirroring fn-arg coercion. A fallible fn’s success return does not widen: return n; in a -> Float fallible(E) fn is refused.

The widening is strictly one-way. Float → Int narrowing remains explicit (round + cast). Decimal never participates in implicit cross-type conversion. Only an Int widens: a quantity (5ms is a Duration, spec/units.md) or a range type is not one, so let f: Float = 5ms; is refused. The five surfaces are the whole list: a locus param’s default and a locus literal’s param override (Worker { rate: 3 }) take a Float. The rule was added 2026-05-11 as part of the float-surface-gaps friction-log resolution; see F.23 in spec/decisions.md and the Phase 2c entry in spec/stdlib.md.

Where the implicit widening above does not apply — most often a Float → Int narrowing, or an Int → Float conversion needed in the middle of an expression rather than at one of the coercion surfaces — there are two explicit forms, both round-toward-zero for the narrowing direction (LLVM fptosi / sitofp):

• The Int(x) / Float(x) casts — the idiomatic in-language form. Int(f) narrows a Float to an Int (truncates toward zero); the cast is opt-in, so there is no silent Float → Int. Float(i) widens an Int to a Float (sitofp). Each is the identity on its own type, and rejects any other argument type. They are the only two numeric casts: there is no String(x), Bool(x), Bytes(x) or Decimal(x) — those names are types. Duration(x) and Time(x) are the unit dialect’s conversions of a value of the time component (spec/units.md § Conversions), never of an Int (n * 1ns makes a count a Duration). Rendering is to_string(x), and reading a value back out of text is std::str::parse_*.
• std::math::int_to_float(i: Int) -> Float and std::math::float_to_int(f: Float) -> Int (WS3.1) — the named-function spelling, callable in any expression position. Semantically identical to the casts (sitofp / fptosi, round-toward-zero); provided so numeric code does not have to round-trip through ASCII (to_string + parse_*) and so the conversions sit alongside the other std::math numeric primitives. An already-correct-typed argument passes through unchanged.
• std::math::round(f: Float) -> Int and std::math::trunc(f: Float) -> Int — the Float→Int conversions that round at a chosen mode. trunc is round- toward-zero (an alias of float_to_int); round is round- half-away-from-zero (3.7 → 4, 2.5 → 3, -2.5 → -3), computed as fptosi(f + copysign(0.5, f)) via a compare/select half-shift (no llvm.round intrinsic, so the path needs no libm libcall — it lowers host-free on wasm32). round is the spelling numeric code wants when building an integer field from a Float quantity; Int(f) / float_to_int / trunc all truncate.

When parent declares consume X: T and child declares expose X: T, the compiler requires:

• X is the same name in both.
• The child’s type for X is a subtype of (or equal to) the parent’s expected type.

For v0, “subtype” is just type equality. Future versions may admit covariant / contravariant relationships; v0 is invariant.

This is the F.8 commitment expressed as a typing rule.

Per F.14: any function injected by L into its arena that satisfies a contract entry must return the contract’s typed surface. The compiler verifies, for each contract expose X: T declaration:

• L has either (a) a param named X of type T, OR (b) a fn returning T named X (or an annotated impl), OR both.
• Multiple impls (the projection-class-specific case) are permitted; all must return T.

Default-implementation rule: if no fn is annotated, the param named X is the default implementation (read field directly).

Per F.E (design-rationale): bindings are immutable by default. let x = 0; produces an immutable binding. let mut x = 0; produces a mutable binding; reassignment permitted.

Mutability is a per-binding property, not a per-type property. There’s no Mut<T>; the binding either is or isn’t mut.

For params / locus state, the implicit rule is that fields are mutable through self.x = ... (per F.3). The locus’s state is the locus’s mutable bundle.

Reassigning a locus-typed field is a lifecycle transition. A field that holds a child locus (params { conn: WsClient = WsClient { … }; }) can be whole-value reassigned from a member fn (self.conn = WsClient { … }). Because a locus is not a plain value — it owns a region and possibly @ffi-acquired resources — this is lowered as dissolve-the-old + construct-the-new, not a pointer store: the previous instance is reclaimed (its drain / dissolve run, releasing its resources) and the new instance is constructed into the owning locus’s arena, owned by the field (so the parent’s dissolve cascade reclaims it). The field always points at a fully-live instance. (Before this rule the new instance was a scope-bound temporary dissolved at the method’s exit — a use-after-free; see WS1#4.) For “same instance, reconfigure,” prefer in-place mutation (self.conn.url = …), which keeps the locus’s identity and resources and is cheaper. v1 limitation: the reassigned instance inherits the owner’s pool; reassigning a field with an explicit non-default placement does not re-apply that placement.

Per F.1 / F.3: the compiler computes k_max = B / [(1 - phi) * c + phi * sigma] from the locus’s declared params. This determines the maximum coordinatees an accept() can attach.

If params are constants (compile-time-known), k_max is a compile-time integer. The compiler may reject accept call sites that statically exceed k_max. (For dynamic params, the runtime checks at each accept; exceeding k_max raises a typed KMaxExceeded failure handled by the parent’s on_failure.)

Types are pure data, so they cannot hold a @form(vec) (a locus). bounded[T; N] is the type-level collection: a fixed-capacity counted buffer laid out inline as { i64 len, [N x T] } — the capacity is part of the type (K made value-level, the F.22 philosophy). Works in type fields and locus params.

Operations are GRAMMAR INTRINSICS (like len(s)), not methods, so the types-have-no-methods axiom holds:

push(f, x)       -> ()  fallible(CapacityError)  // full = error;
                                                 // displacement policy
                                                 // lives in the or-arm
at(f, i)         -> T   fallible(IndexError)
set(f, i, x)     -> ()  fallible(IndexError)     // overwrite live slot
count(f)         -> Int
clear(f)                                          // len = 0
truncate(f, n)   -> Int                           // len = clamp; returns it
for x in f { }                                    // iterate live slots
f.get(i)         -> T   fallible(IndexError)      // = at(f, i); see below

get is the one operation in method position, and the same is true of [T; N]. Element chains rewrite to a loop that fetches through the source’s get, so answering that name is what makes a form chainable at all — without it, f.filter(…).count() failed with “no field get” and the type-level collections could not anchor a chain. It is identical to at in signature and semantics (on bounded it is at, bounded by the live count rather than the capacity); at remains the idiomatic spelling for a direct index.

The six free-fn-shaped names are NOT reserved. They dispatch on the first argument’s type, so a program may declare a free fn of any of them, and a declaration whose first parameter is the receiver’s own bounded[T; N] shadows the intrinsic for that receiver type — checker and codegen alike. See tokens.md § Built-in identifiers for the exact rule. f.get(i) is unaffected: method position is not the free-fn namespace.

Semantics:

• Fields auto-initialize EMPTY. Literal init and whole-field assignment are rejected — the intrinsics are the only mutation surface. Whole-STRUCT copies carry elements + count by construction (the storage is inline).
• Scalar elements (Int/Float/Bool/Decimal/Duration) are flat under zero_copy and travel the bus as raw bytes. Pointer-shaped elements (String/Bytes/struct) work in-process — push/set arena-anchor the element into the receiver’s owning arena — but are rejected in cross-process bus payloads (post-v1 polish).
• Drop-front/FIFO is the shift-left idiom: set live slots down, then truncate.
• CapacityError { cap: Int; count: Int } and the shared IndexError are the injected error shapes.
• The unbounded-alloc analysis treats bounded fields as bounded by construction. @form(vec) remains the unbounded, locus-owned collection: unbounded data lives on a locus; bounded data can live in a type.

Generic type-expr ↔ monomorph unification: a generic instantiation type-expr (Box<Int>) resolves at typecheck to its mangled monomorph name (Box_Int) — the same name codegen synthesizes and that Box_Int { ... } literals produce — so declarations and literals unify, and a Box_String literal in a Box<Int> slot is a caught mismatch. Monomorph literal fields validate against the template with the type args substituted, and field reads on monomorph values type as the substituted field.

A declared type parameter shadows a same-named top-level declaration or alias throughout its template’s signatures, fields and body annotations. Before specialization it remains unbound; a global name cannot supply its type or create an apparent concrete monomorph.

Generic loci monomorphize the same way. locus Cache<K, V> is a template; Cache<Int, String> names the monomorph Cache_Int_String, whose params are the template’s with the arguments substituted. A field read on a monomorph locus value (c.cap) types as the substituted param, exactly as a monomorph struct’s field read does.

Generic function calls inside a generic locus are typed for each concrete locus monomorph. A call on self.value, or on a local bound to that field, uses the substituted field type. The checked call rows retain their source body and call identities; lowering selects the row for that locus’s arguments. Params defaults use their declaring locus’s specialization even when construction happens inside another generic function or locus. Specializations discovered in these bodies are checked in turn.

Omitted function and method defaults are typed at each invocation in the caller’s scope. Their generic call rows retain the default’s source site and distinguish the invocation path and the caller’s specialization. The same default can therefore use Int in one caller and String in another. Lowering reads the corresponding checked row; supplied arguments do not evaluate the default.

Where the arguments come from. A struct / locus literal spelled with the template name (Box { value: 1 }, Cache { cap: 2 }) carries no type arguments of its own; it takes them from the declared type at the site. The sites that declare one are:

• a let ascription — let c: Cache<Int, String> = Cache { cap: 2 };
• a declared return type — fn make() -> Box<Int> { return Box { value: 4 }; }
• a declared field or param, at its DEFAULT — params { b: Box<Int> = Box { value: 0 }; }
• a declared field of a data type, at a literal’s init — Outer { inner: Box { value: 9 } }

At a let ascription, a transparent alias of the whole instantiation supplies the same arguments: type IntBox = Box<Int>; permits let b: IntBox = Box { value: 1 };. Imported template paths resolve through their import aliases before specialization. Different aliases for one imported template retain the same declaration identity; each construction carries its own concrete arguments and child layouts.

Anywhere else — an un-annotated let, a literal in statement position — the arguments cannot be recovered, and the literal is a type error naming the template and the annotation to write. There is no inference from a literal’s field values back to the parameters.

A generic instantiation’s argument COUNT must equal the template’s parameter count: Box<Int, String> on type Box<T> is a type error at the annotation.

The mangled monomorph name is spellable for a generic TYPE (Box_Int { value: 1 }, and through an alias — type IntBox = Box<Int>; IntBox { ... }). It is not spellable for a generic LOCUS: Cache_Int_String { cap: 2 } is a type error pointing at the template spelling.

Generic params are declared with angle brackets:

fn map<T, U>(xs: [T], f: fn(T) -> U) -> [U] { ... }
type Stack<T> { items: [T]; }
locus Cache<K, V> { params { cap: Int = 1; } }

The constraint syntax <T: Constraint> admits:

• ProjectionClass (built-in any-of-three; F.2)
• A specific projection class: Rich, Chunked, Recognition
• Concrete types: <T: int> is illegal (use the type directly); <T: SomeStruct> is also illegal (no trait system in v0)

V0 supports only projection-class constraints. Future versions may add traits.

Monomorphization: the compiler emits one machine-code instance per concrete generic instantiation (per F.1 commitment to runtime perf over compile-time perf). Compile times grow with generic surface; runtime is full-speed.

A monomorph has to be NAMED before it can be declared — Box<Int> is lowered as Box_Int — so each argument must contribute a token to that name. The primitive vocabulary is:

Int  Float  Bool  String  Duration  Decimal  Time
Bytes  BytesView  BytesMut  StringView

Uint is the one primitive that may NOT be a generic argument: it is parser-recognized with no codegen representation in any storage position (see the table at the top of this document), so there is no monomorph to name. hale check refuses the instantiation at the argument’s span and names the supported set:

main.hl:6:12: type error: `Uint` cannot be a generic argument: no
monomorph name exists for it (supported: Int / Float / Bool /
String / Duration / Decimal / Time / Bytes / BytesView / BytesMut
/ StringView)

A non-primitive argument is a single-segment named type (a user type, or another generic instantiation, which mangles recursively). An array, tuple, bounded[T; N] or function type as an argument is refused at lowering; a qualified path is rewritten to a single segment by the import renames before the mangler sees it, which is why the checker’s rule above is confined to primitives — the only argument form whose answer is the same in both layers.

The type of let x = expr; is inferred from expr. Explicit annotation let x: T = expr; overrides inference; if expr’s type is incompatible with T, compile error.

If a fn omits -> T, the return type defaults to () (unit). Explicit -> T is required for any non-unit return.

Params must declare types explicitly. params { x: Int = 0; } is the full form. (Inference of param types from defaults is not supported in v0; explicit is preferred for the inferred-vs- = default distinction.)

Three init shapes:

• name: T = expr; — default. Used when the caller omits the field; evaluated in the caller’s scope at instantiation time.

• name: T; — required. The caller MUST supply the field at the locus literal site; instantiation without it is a compile error. Use for fields where no sensible default exists (e.g. Server { handler: ... } where the handler is the whole reason the locus exists).

  Exception (B7 / G19): if T is a user-defined type (struct) and every field of T has a declared default, the compiler synthesizes T { } as the param’s default. So params { cfg: Cfg; } against type Cfg { host: String = "localhost"; port: Int = 8080; } works without = Cfg { } spelled out. Required-shape is preserved when any field on T lacks a default.

• name: T : inferred; — F.3 inference path; compiler / runtime determines the value.

T may be another locus (B10 / G24). A param typed as a locus name (params { db: DB; }) stores a LocusRef — a single-pointer borrow. The param-holding locus does not own the referenced locus; the caller keeps it alive. Cross-decl declaration order doesn’t matter: a forward reference (User { db: DB; } declared above locus DB { ... }) resolves via the codegen-side pending_locus_names pre-pass.

Reading through the borrow (self.db.name, self.db.draining) goes through the same field-access lowering as any other LocusRef receiver. Synthetic fields (self.db.k_max, self.db.draining) work on non-self receivers too (B14 / G31).

A locus may not contain itself by value (GH #813). A param default that constructs the locus it belongs to — directly, or around a cycle through other loci — is an error at the param (“param next of Node defaults to a Node; a locus cannot contain itself by value”). Every instance the default builds needs another, and no call site can end the chain: Node { next: ... } needs a Node to hand over, and building one asks the same question again. The rule is over locus LITERALS in a default, anywhere in it — inside an if or match arm or a block’s statements too, since every branch is lowered — and a literal’s own supplied fields count: a default that spells out every param of the locus it builds expands no default of its own and is not a cycle.

A call that builds one counts (GH #870). next: Node = make() with fn make() -> Node { return Node { }; } is the same ring spelled through a function, and the same error at the param (“param next of Node defaults to make(), which builds a fresh Node; a locus cannot contain itself by value”). Lowering a call emits a call rather than inlining the callee, so that program used to compile and then overflow its own stack at run time instead — every Node make builds leaves ITS next to the same default, which calls make again. A fn counts when every value it hands back is freshly built: a literal of its declared locus, a call to another such fn, or a local binding of either — the binding the returned name resolves to, so an inner let that reuses the name does not hide it (GH #1140) — including through an if, a match or a block whose every arm is one of those (return if c { Node { } } else { make() };), the set lowering reads too. A call the compiler cannot see as fresh is not an edge and stays accepted — an accessor handing back a locus somebody else owns (next: Node = registry.head()), a method, a std:: or cross-seed path, a carrier with an arm that is none of those. That program may still recurse at run time; @no_recursion is the contract for unbounded recursion, and this rule only reports the rings it can prove.

A cycle whose loci live in different files of one seed is reported when the seed is checked together, since a single file holds no declaration for its sibling’s types. The test harness’s build, which skips the rest of the check, judges this rule too, so lowering keeps no guard of its own (F.40 phase 3, C7).

Per F.3: a param declared : inferred (instead of = value) indicates the compiler / runtime determines the value, not the author. The compiler treats:

• Hand-declared = value → prior, fixed at compile time.
• : inferred → unknown; resolved at compile time if possible (constant propagation), at runtime otherwise (via the perspective-stability machinery).

Typing-wise, inferred params have the declared type; they’re just not bound to a value at declaration time.

Functions are first-class values. fn(A, B) -> C is a type; function literals can be assigned, passed, returned.

A locus’s fn member can be a method (takes self) or a free function within the locus’s scope. Lifecycle methods (birth, accept, etc.) are not regular fns — they have their own syntax and don’t take self (it’s implicit).

A call whose callee is a bare identifier must name something: a local binding (a fn pointer), a free fn, a generic fn, or one of the builtins the compiler answers itself. That set is exactly:

(sum(x) and prod(x) are accumulator vocabulary too, but the parser gives them their own syntax rather than a call, so they are never a bare callee. __fmt, the desugaring of f"{x:spec}", is the compiler’s own and is not written by hand.)

In a whole program — every import resolved, which is every command’s: hale check on a seed (<directory>, what the organization’s gate runs) or on one file, every command that compiles (hale build / hale run / hale test / hale replay compile exactly what they bundle) and hale lsp — any other bare callee is a type error — call to X: no free fn, generic fn or fn-pointer binding with that name is in scope, with a did-you-mean over the program’s fns. The rule holds wherever the call stands: a statement, an operand, a condition, a fn or method body, a lifecycle hook, a bus handler, a params default, a const initializer. Only a partial program a library caller assembles (a styleguide snippet, a test harness’s fragment) keeps the permissive reading (dna/FRICTION.md F.18).

hale check <file> loads that file and what its own imports reach, never the other files of its directory — exactly what hale build <file> loads — so a fn only a sibling file defines is unbound in the program both commands see, and both refuse the call. Until 2026-10-11 the file target kept a permissive reading for a sibling’s fn, so hale check f.hl accepted a call to a fn nobody wrote that hale build f.hl refused. A multi-file seed is checked as the seed: hale check <directory>. When a file target is refused for a name nothing binds and other .hl files sit beside it, the check says so after its diagnostics (not under --json, whose stream carries the records alone):

main.hl:1:21: type error: call to `sib_helper`: no free fn, generic fn or fn-pointer binding with that name is in scope
note: `main.hl` was checked alone, as `hale build` builds it; the 1 other .hl file(s) beside it are not loaded, so a name only they declare is unbound here — `hale check .` checks the whole seed

The rule was on for the seed check alone until GH #911 B1, so the build path let the call through to codegen, which refused it as unsupported in codegen v0: call to X: … — from a layer below the one that had just approved the program, with no file, line or caret, and a did-you-mean drawn from compiler-internal symbols. The two layers gave two answers to one question; they now give the located one.

The list is a contract in both directions, and neither is optional.

A name the compiler answers must be exempt from the rule. A builtin the rule does not know about turns the admission gate into a refusal of correct code — hale check red, hale run fine — which is strictly worse than the late diagnostic the rule exists to replace (GH #779).

A name the rule exempts must be one the compiler answers. An exemption for a name nothing lowers is the divergence the rule was written to remove, moved inside the rule: hale check accepts the call, and hale build refuses it at lowering, without a source location. The list is therefore exactly the set above and carries no aspirational entries — a name is on it when codegen dispatches it, not when it looks like it should (GH #800). The compiler tests both directions over its whole program corpus rather than trusting the list.

The value builtins have types, and the checker and the compiler read them from one signature table:

A call over operands outside its row is typed as unknown: the checker names no type for it, and the compiler refuses it where it lowers it. So first(len(s)) instantiates first<Int>, and let n: String = len(s) is a type error at the let.

The same rule holds in value position. A bare identifier must name something in scope: a local binding, a fn param, a match-arm binder, the implicit err of an or handler, a chain’s it / idx, a top-level const, or a top-level declaration (fn, locus, type, perspective, interface; a topic resolves and is then refused by its own rule — it addresses a channel, it is not a value). In a whole program — every import resolved, which is hale check on a seed or a file, every build (hale build / hale run / hale test compile exactly what they bundle) and hale lsp, which loads the whole seed as hale check <dir> does, imports followed, and typechecks it only once every member has read and parsed — any other bare identifier is a type error at its own span: unknown identifier X: no binding, param, const or declaration with that name is in scope, with a did-you-mean over the locals in scope and then the program’s top-level names.

Before this, an identifier that bound nothing typed as Unknown, which is permissive everywhere, so a one-character typo passed check and verify and failed in the backend as unknown identifier with no source location.

One file of a multi-file seed, checked alone (hale check <file>), is held to the rule as its build is: a const only a sibling file declares is unbound in the program the file target loads, and the check refuses the read with the note above. (It kept a permissive reading until 2026-10-11, which hale build <file> never had.)

A name a block of the same body bound and released — if take { let x = 1; } return x; — is the block’s (§ “Dissolve timing rules” in spec/semantics.md), so the refusal says so: unknown identifier x: … it was bound in a block that has ended, and a block's binding is the block's (GH #1139).

A bare unknown CALLEE reports the call diagnostic above and not this one — one mistake, one message (GH #721).

And the same rule holds in TYPE position. A bare name written where a type is expected must name a declaration: a primitive, a type (struct, enum or alias), a locus, an interface, a perspective, a generic parameter of the declaration being checked, or one of the types the compiler synthesizes for its own channels (IoError, ParseError, CryptoError, IndexError, KeyError, EmptyError, CapacityError, BusUnmatchedKey, ClosureViolation). In a whole program — the same set of callers as above — any other bare name is a type error at its own span:

main.hl:1:16: type error: unknown type `int`: no type, enum, locus,
interface or alias with that name is declared — did you mean `Int`?

The rule holds in every annotation position: a fn parameter and return, a fallible(E) payload, a struct field, an enum variant’s payload, an alias target, a const ascription, a locus params field, a capacity cell type, a lifecycle / mode / on_failure parameter, and a let ascription — including inside the compound forms, so the name in [Row; 4], (Int, Row), bounded[Row; 8], fn(Row) -> Row and Rich<Row> is checked as well.

Before this, an unresolvable bare type name resolved to Unknown, which is permissive everywhere, so fn helper() -> int typechecked and then failed in the backend as unknown type name 'int' in signature — no location, and the annotation had silenced every check that would have used it (GH #877).

A QUALIFIED name (lib::Thing, std::text::Sink) is NOT subject to this rule. It resolves against the bundle’s import-rename table, which only a caller that merged the imported seeds has, so a tool holding one seed without them keeps the permissive reading for paths (GH #803 / #833). One file of a multi-file seed, checked alone, does not: it loads what its build loads, so a type only a sibling declares is refused by both.

For two contracts C1 and C2, C1 ⊆ C2 iff every entry in C1 has a matching (compatible) entry in C2. This is used for:

• Parent-child compatibility: parent’s consume ⊆ child’s expose.
• Locus-type substitutability: when a child locus type is expected, any locus type with a compatible expose-surface may substitute.

Per F.6 / F.11 / memory.md: cross-locus references at the type level are limited to the contract’s typed surface. Specifically:

• A reference to a coordinatee accessible only via self.children[i].x where x is in the contract.
• Sibling references: not typeable. No syntax exists for reaching from one sibling to another; if attempted via manual pointer construction, the compiler rejects on region-lifetime grounds.
• Grandparent references from a child: not typeable. Failure flows through bubble; intent flows through the parent.

This makes the framework’s vertical-only commitment a type-system invariant, not just a convention.

A locus’s methods may be invoked only on the OS thread that owns the locus’s placement’s pool. Cross-pool direct calls are typecheck errors; cross-pool coordination goes through the bus.

The invariant is enforced via a static call-graph walk over the placement table (the placement family: one row per static instance, seeded from the main locus’s placement { } entries):

1. Each main-locus params field has a pool — explicit (placement { field: cooperative(pool = X); } or placement { field: pinned; }) or default (cooperative(pool = main)).
2. Each nested locus inherits its containing tower’s pool (see spec/semantics.md § “Nested instantiation”). Methods on a nested locus run on the parent’s pool’s thread.
3. For a method-call expression self.field.foo(args), the caller is each instance of the enclosing locus, on its own pool, and the receiver’s pool is the pool of that instance’s field instance: the enclosing locus’s own placement { } entry for field if it names one (e.g. a db: pinned field on the main locus), otherwise the field co-locates with its owner (the caller’s pool). A field that holds an instance built elsewhere (App { w: held }) runs in its holder’s pool whatever an entry names for it; such an entry is refused (GH #890). The pool is a property of the instance, not the field’s type — the same locus type used as a field in two loci on two pools is two independent instances, one per owner, each single-pool. A field is a receiver however its type is written: a single name, a qualified path (std::log::Logger), an alias, or a contract the field’s literal implements, named in the diagnostic by the locus it realizes. An enclosing locus the table holds no static instance of (one built only inside a method body, or one held through a parameter) is not judged: its pool is unknown, never assumed to be main.
4. If the receiver instance’s pool differs from the caller’s pool, the call is rejected with a diagnostic naming both pools and pointing at the placement { } entries that picked them.
5. Bus sends (Topic <- v; / "subj" <- v;) are unrestricted — the runtime’s cross-thread dispatch (m28b condvar+memcpy) handles the boundary safely.

The invariant is the substrate enforcement that makes M:N cooperative pools safe. Without it, multi-pool deployments would silently race on locus arenas (unsynchronized bump allocators by design). The typecheck happens once per main locus (the placement-bearing locus is unique per binary), so the rule applies at binary compile time rather than at every library typecheck.

Interaction with LocusRef borrows. A locus param of type LocusRef(L) carries a borrow of an L — but the borrow’s pool is the locus’s own placement, not the borrower’s placement. So self.db.query(...) where self.db: DB and the DB instance is on pool db_pool is a cross-pool call from any non-db_pool thread, and routed through the bus. This is the “vertical-only flow” rule generalized to cooperative pools: cross-pool access is the same shape as sibling access — bus only.

Interaction with builtins / stdlib. Free functions and stdlib path-calls (std::io::fs::read_file, std::str::*, etc.) are pool-neutral — they run on whichever thread calls them. Their arena routing through lotus_current_caller_arena TLS handles the per-thread isolation. The single-threaded- method invariant applies only to locus member functions, which are what carry per-locus arena state.

Interaction with @form(...) loci. A locus declared with a @form(...) annotation (@form(hashmap), @form(vec), @form(ring_buffer)) is single-pool by default — its methods participate in the same single- threaded-method invariant as any other locus. Plain @form(...) cells have no runtime synchronization; concurrent writers from different pools corrupt the underlying structure.

Cross-pool access is opt-in via the sync = kwarg on the form annotation:

When a locus carries a recognized sync discipline, cross- pool method calls into it are accepted without diagnostic — the substrate’s chosen discipline carries the safety contract. Plain @form(...) (no sync kwarg) gets the same cross-pool diagnostic as any other locus, extended with an upgrade-path hint naming the sync kwargs.

Because a form field’s pool is its instance’s (rule 3 above), two loci that each hold their own @form field of the same type on different pools are two separate, single-threaded structures — each accessed only by its owner’s pool. Neither is a cross-pool access, so neither is flagged, and neither needs a sync discipline (there is no sharing to synchronize). The diagnostic fires only on a genuine cross-pool access — reaching one instance from a pool other than the one it lives on, e.g. a form field explicitly placed off its owner. (This is why two same-type form instances on two pools do not require byte-identical twin types.)

Concrete shape: a Registry @form(hashmap, sync = striped) of Counter indexed_by name shared across producer pools (gateway loci incrementing counters) and a consumer pool (MetricsEndpoint rendering Prometheus text) typechecks clean. Without the sync = striped, every cross-pool self.registry.counter(...) would be rejected.

Non-form receiver loci have no sync discipline available; cross-pool coordination must go through the bus.

Inference. F.32-1∞ adds a closed-world inference pass that picks a sync default per form-bearing locus type from the pool-propagation graph. The explicit annotation always overrides; the inferred pick is shown via a compile-time diagnostic at the decl site. See notes/f32-cache-aware-delivery-plan.md § F.32-1∞.

History. Commit 3ec6391 (2026-05-24, first cut) admitted any @form(...) locus into the cross-pool-safe set unconditionally, on the strength of a not-yet-shipped “form ABI serializes” claim. Bench-prep for F.32-1 surfaced that the runtime had no synchronization on the form paths; F.32-0 (this section’s current state) scopes the exemption to explicit opt-in via sync = X. See notes/f32-cache-aware-delivery-plan.md § F.32-0.

A closure name { left ~~ right within tolerance; ... } declaration types as:

• left and right must be expressions of compatible numeric types (integer or numeric).
• tolerance must be a non-negative numeric expression.
• The compiler verifies left/right resolve in the closure’s scope (which is the locus’s scope; self.x is permitted, member fns may be called).
• For epoch tick / epoch duration(d) / epoch dissolve / epoch birth / epoch explicit, the runtime evaluates the closure at the appropriate event boundary.

A closure failure at evaluation produces a typed ClosureViolation event (per F.9), not a generic error.

A function declared -> T fallible(E) produces a value of type T fallible(E) at every call site. This type cannot be used where a plain T is expected — the caller MUST address the error before the value is consumable. See spec/design-rationale.md for the design rationale.

Declaration sites are restricted by the two-channel rule (see spec/semantics.md § “Fallible call semantics” § “Where each channel lives”). fallible(E) may be declared on:

• Free fns.
• Stdlib-synthesized methods over @form(...) containers (@form(vec).get / .pop, @form(hashmap).get / .remove / .key_at / .entry_at, @form(ring_buffer).pop).
• User-declared fn member fns on a locus (open-question #24, shipped 2026-05-25). Heap-bearing success and err payload types are supported via the same TLS caller-arena snapshot non-fallible heap-returning locus methods use.
• Interface method signatures (GH #732) — see § “Interface types (F.20)” for which methods satisfy one.

fallible(E) is rejected on substrate-facing surfaces that have no caller frame to address the error channel:

• Lifecycle methods (birth / run / accept / drain / dissolve / on_failure). Physically rejected at the AST level — LifecycleDecl doesn’t carry a fallible field.
• Mode methods (bulk / harmonic / resolution). Same shape as lifecycle: AST doesn’t carry a fallible field.
• Closure assertions. Substrate evaluates the assertion at the epoch boundary; no caller frame exists in the expression.
• Bus-subscribed handlers. A fn that’s declared fallible(E) may not also be referenced by a bus subscribe ... as <fn> declaration. Bus dispatch has no return path. Rejected at the subscribe site, not the fn decl (one fn may be referenced by zero subscriptions; the subscription is what fails to typecheck). A subscribed handler MAY declare a return type (GH #1106): bus dispatch ignores the value. A reply to a caller is a served rpc row’s response (spec/api.md § Surfaces and their rows), not a bus handler’s return.

The narrowing from “no fallible on locus methods” to “substrate-facing surfaces only” preserves the two-channel separation (structural failures still flow vertically via closure violations + on_failure) while removing the friction that made devs extract free fns just to get a value- error channel back. The typechecker emits the diagnostic at the offending site (locus member decl for lifecycle / mode; subscribe site for bus-handler-fallible conflict).

The checker represents fallible returns as a wrapper around the underlying success type:

Only an or addresses a Ty::Fallible: it must be unwrapped at the immediate call site, as the operand of an or (or an or’s handler, below). Anywhere else the call is bare, and the bare_fallible law reports it with one error naming the callee and its payload (spec/semantics.md § “A bare fallible call is an error”), at:

• let v = f(); with f fallible
• let v: T = f(); with f fallible (typed binding)
• f(); as an expression statement
• g(f()) — fallible passed as an argument
• match f() { .. } — a match does not handle it
• operand, assignment, return, condition positions

The checker types a bare fallible value as its success type T, so the position reports no type mismatch beside the law’s error.

<expr> or raise : Propagate the error one frame up the static call stack. Evaluates the inner; on FallibleErr payload, re-enters the fallible-return shape of the enclosing fallible(E) fn (the error climbs the call stack until a frame addresses it). The value-error channel is value-level and orthogonal to the closure-violation channel; the bubble / on_failure machinery is not entered by default. (An application may later promote a value error to a closure violation explicitly; no such syntax exists in v1.) On success, passes the inner value through. The resulting expression’s type is the success type T.

Past every enclosing fallible(E) frame — at the implicit main locus’s root boundary — the runtime panics via lotus_root_panic. See spec/semantics.md § “Process exit” for the boundary semantics.

<expr> or <fallback> : Substitute a fallback value of type T. On failure, evaluates the fallback expression with err implicitly bound to the payload (typed as E). On success, passes through. Fallback type must be assignable to T. The fallback may itself be a call (or handler(err)), making err a regular expression-position binding inside the fallback.

Fallible handlers: the handler may itself be fallible(E2). Its success value substitutes; its FAILURE propagates through the ENCLOSING fn’s error path — implicit or raise, sugar for the already-legal nested spelling call() or (handler(err) or raise). E2 must be assignable to the enclosing fn’s declared payload (“handler’s failure has nowhere to go” / “propagated payload must match” otherwise). The implicit or raise applies where lowering supports it, a limitation to lift rather than a rule: a fn the program declares (not a generic one), an imported or bundled stdlib fn written as Hale, and a locus member fn called on self, a local or a field of self. Any other fallible handler (a stdlib path-call, a generic fn, an interface’s or a perspective’s method, an @form-synthesized or an array’s method) is refused with the explicit nested spelling to write instead. In statement position the substituted value is discarded, so the handler’s success type needn’t match the call’s.

The fallback may be a { block } — or { … }, with err in scope — for multi-statement recovery. Two cases:

• A block that always diverges (return / fail on every path) produces no substitute value, so it imposes no constraint on T and is accepted for any success type — let s = read_file(p) or { return "fallback"; }; where the fallible’s success type is String, Bytes, a struct, etc. (It disposes like or raise: the err branch is closed and only the success value reaches the continuation.)
• A non-diverging block substitutes its tail expression as the fallback value, whose type must be assignable to T: let s = read_file(p) or { log(err); "default" };.

On a Unit-success fallible (() fallible(E), e.g. std::io::fs::write_file), or { block } runs the block for effect — including in statement position: write_file(p, s) or { println("failed"); }; — the same as or raise / or discard there.

The or operator is right-associative: a() or b() or raise parses as a() or (b() or raise), so each level disposes one fallible in turn until a non-fallible value remains.

A value-returning fn or locus method whose body may violate (spec/semantics.md § “A value-returning method that may violate is fallible”: a violate statement in its own body, or a call to a value-returning fn that may violate and is not fallible) is declared -> T fallible(ClosureViolation). The checker refuses it otherwise, at the fn’s name: “`P.take` returns a value and may violate (`violate exhausted`): declare it `fallible(ClosureViolation)`; its callers then say what happens when the locus fails”. A fn has one error type, so one that may violate declared fallible(E) with any other E is refused too. Lifecycle bodies, bus handlers and fn main are exempt; a fn returning nothing that may violate is warned about rather than refused.

The violation is the call’s failure. The caller’s or runs, and the err an or handler(err), an or { … } or an or fail sees is typed ClosureViolation (err.locus, err.closure, err.diff), the record the owner’s on_failure received; at a stdlib method’s call (BytesBuilder.snapshot and finish, the stdlib’s two) as at a program’s own.

fail <expr>; is only valid inside a fallible fn body. It evaluates <expr>, requires the result type to match the fn’s declared payload type E, and exits via the error path (the caller sees a FallibleErr value).

The payload E is an ordinary type expression — usually a small user-defined record (type ParseError { ... }) or a stdlib- synthesized type. The runtime / typechecker does NOT impose a common base — there is no Error trait, no impl Error for ParseError. Failure is a single anonymous fact; the payload is just a value tagged onto the failure for diagnostic purposes.

Across an API boundary the payload is a contract: a fallible(E) handler that a surface row names (spec/api.md § Surfaces and their rows) has E as the row’s error type, hashed into the surface’s digest, described as the member’s error schema and carried to the caller as the handler error outcome (422 over HTTP, {"ok": false, "error": E} over the Unix socket; spec/api.md § Outcomes), encoded by the exposure’s codec like the response.

The resolver injects four fallible-payload types into the top scope so user code can name them in fallible(...) markers and or substitute clauses. All are idempotent — a user-declared type with the same name wins.

The IoError payload is the unified shape for the fallible I/O surface — see spec/stdlib.md § “IoError” for the errno → kind tag taxonomy.

role NAME; at top level declares a role: authorization vocabulary, the way group declares claim vocabulary and effect declares an effect class. A role is a name the deployment maps to principals; the program never says who holds it. role NAME includes A, B; is the hierarchy: whoever holds NAME holds A and B, and whatever they include, transitively. Composition is grant-only and union-only (the constitutions rule): includes can only widen what a holder may do, so a cycle says nothing and is an error, and a name declared twice is an error rather than a merge. A role an includes names must be declared; no role is implicit (owner is a role only a program that declares it has). Role names are deployment vocabulary (the keys of [environments.<env>.roles], the word a refusal names) and are never mangled: an imported seed’s role x; and the entrypoint’s are one x, and declaring it in both is the duplicate error.

A role is named by a requirement: a surface row’s requires: [R, …] (rpc Orders::cancel requires: [operator];, or @rpc(requires: [R]) on the handler) or a hub binding’s requires: (spec/api.md § Surfaces and their rows, § Streams). R must be declared (surface law 4). The requirement is a property of the surface row, never of the handler, so one handler shared by two surfaces meets each surface’s; it is a boundary check, named so, and says nothing about the program’s own call paths; who holds the role is the serve site’s role source (spec/api.md § Identity sources).

@gated(role: R), which gated a subscribed handler, an expose member or a publish through the retired api binding, is refused by the parser with the replacement (requires on an rpc row, spec/api.md).

Recovery primitives (restart, restart_in_place, quarantine, reorganize, bubble, dissolve, drain) are statement-level keywords (per precedence.md); they don’t have types in the value sense. They take a locus handle or error value as argument:

restart(child);
restart(child) for 3;
quarantine(child);
bubble(err);

The compiler verifies the argument is a valid handle / error in the current scope.

F.32-2 ships a compile-time working-set estimator that projects each user-declared locus’s approximate byte cost and compares against a cache-tier budget. The estimator runs post-typecheck, pre-codegen; it doesn’t change codegen output and emits diagnostics rather than changing program behavior.

Estimator formula (per-locus, in bytes):

working_set(L) =
    sizeof(L's struct)                              [arena + user fields with alignment padding]
  + sum(slot in L's capacity slots) cap × cell_stride
  + sum(child in L's params if locus-typed) working_set(child)

Cache-tier budgets are read from /sys/devices/system/cpu/cpu0/cache/index{0,2,3}/size on Linux at first probe (cached for the build’s lifetime); static fallbacks 32 KB / 512 KB / 8 MB apply on non-Linux or when sysfs is unavailable. See hale_types::working_set for the engine.

Per-locus annotation (F.32-2 v0.2):

@locality(L1) / @locality(L2) / @locality(L3) declare a per-locus cache-tier expectation. @locality(any) explicitly opts the locus out of any global gate. The annotation stacks with @form(...) in either order:

@form(hashmap, sync = lockfree, cap = 64)
@locality(L2)
locus Registry {
    capacity { pool entries of Entry indexed_by k; }
}

The grammar surface is in grammar.ebnf § locality_annotation.

Build-flag surface (CLI, on hale build):

Effective budget precedence (per locus):

1. @locality(L1|L2|L3) annotation → that tier (hard contract; evaluated regardless of CLI flag).
2. @locality(any) annotation → no budget (opts out even under --target-cache).
3. No annotation → falls through to --target-cache global tier (or no budget when the flag isn’t set).

--strict controls warnings vs errors uniformly across both sources. The diagnostic names which source applied (per the BudgetSource::label() “@locality” / “–target-cache” attribution).

Estimator approximations (deliberately imprecise; see the working_set module doc for the full list):

• params { } field layout uses alignment-correct accumulation (each field rounded up to its natural alignment; struct rounded up to max field alignment). Was packed-layout in v0.1; v0.2 adds the padding.
• Arena overhead modeled as a flat 64-byte budget for synthetic headers.
• Heap-managed primitives (String / Bytes / *View) count as 16 bytes (ptr + len); the heap buffer’s contents are not counted (lives in the locus’s arena).
• Per-method scratch high-water mark — not modeled. The scratch arena is destroyed at method exit, so contents are transient, not resident.
• Unbounded-cap capacity slots (no cap = N on the form) surface in WorkingSetEstimate::unbounded_slots rather than contributing zero silently.

Forward-looking / deferred items for this area now live in the decision log — see decisions.md § Deferred & future work.

Where each typing rule lives in the compiler pipeline:

• Parse + AST construction: grammar.ebnf rules.
• Name resolution: identifier scopes, qualified-name lookup.
• Type inference: let-binding types, fn return types when explicit -> T omitted.
• Type checking: assignment compatibility, function call signature, generic instantiation, projection-class constraints.
• Locus-shape checking: contract compatibility (F.8 / F.14), k_max bounds (F.1 / runtime-checked when dynamic), mode signature consistency, lifecycle method signatures.
• Region-lifetime checking (compile-time): no escape from shorter-lived to longer-lived scope; no sibling references.
• Closure-cycle existence check: closure assertions reference defined values in the closure’s scope.

The Phase 1 compiler in Rust implements these checks; the Phase 6 self-hosted compiler ports them.