Type system

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.

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).

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.

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.
• @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.

The widening is strictly one-way. Float → Int narrowing remains explicit (round + cast). Decimal never participates in implicit cross-type conversion. 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.
• 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

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.

Generic params are declared with angle brackets:

fn map<T, U>(xs: [T], f: fn(T) -> U) -> [U] { ... }
type Stack<T> { items: [T]; }

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.

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).

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).

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 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 receiver’s pool is the pool of the field instance, inferred at the call site: 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). 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.
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.

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).

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:

A Ty::Fallible is not assignable to its success type. It must be unwrapped at the immediate call site. The checker emits error: error not addressed 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 a non-fallible-typed arg
• assignment, return, condition positions

<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). User free fns, imported-path fns, and locus member fns are classified; @form-synthesized methods and stdlib path-calls still need the explicit nested spelling. 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.

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.

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.

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);
quarantine(child) for 30s;
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.