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.

Primitive types

Type	Repr (v0 codegen)	Notes
Int	i64	Signed; default for integer literals
Uint	i64	Unsigned at the type level; codegen lowers as i64. Parser-recognized; full lowering pending a workload that exercises the unsigned-arithmetic distinction.
Float	f64	IEEE 754 double; default for float literals
Decimal<S>, Decimal	i128	Fixed point: an i128 mantissa at the scale S (mantissa × 10^-S), S an integer literal from 0 to 18 that is part of the type; plain Decimal is Decimal<9>, the same type (2026-10-12, § Decimal). Every scale is the one 16-byte, 16-aligned layout. Distinct from Float at the type level; suffix d on literals (1.50d). A literal holds no more places than the scale of the place it flows into (a check error at the literal otherwise, never a truncation); + - % are exact, * and / truncate toward zero at the scale; two scales never mix, and d.rescale(T) converts. Real arbitrary-precision deferred.
String	ptr (NUL-terminated)	UTF-8 bytes, C-style NUL-terminated. Single-pointer ABI to fit return-by-value through the m49 calling convention. Embedded NUL truncates — use Bytes for binary content. Allocated in the caller’s arena (or the lazy global payload arena for stdlib returns whose lifetime needs to outlive the call).
Bool	i1	true / false
Time	i64	Nanoseconds since the Unix epoch, UTC (GH #607, 2026-09-14). A literal is ISO-8601 between backticks — `2026-05-08T12:00:00Z`, an optional fraction of one to nine digits, an optional Z; an offset such as +01:00 is a compile error, never read as UTC, and so is a day past its month’s length (2099-02-30, 2100-02-29), never rolled into the next month — and is parsed at check time. Declared by the stdlib (type Time = point Duration;, GH #1076 U4, spec/units.md § The stdlib’s time catalogue): a point over Duration with no origin:, so the unit dialect’s algebra of points is its arithmetic: Time ± Duration → Time, Duration + Time → Time, Time − Time → Duration; anything else with a Time operand is refused, naming both. Orders and compares as an instant. to_string / println render ISO-8601, the fraction only when it is not zero. Before the epoch is negative, not an error. It holds 1677-09-21T00:12:43.145224192Z through 2262-04-11T23:47:16.854775807Z: a literal past either end is a check error at the literal, parse_time of one is its ParseError, and time_from_unix or Time ± Duration past either end is a runtime violation (spec/stdlib.md std::time), never a wrapped instant. On the wire and in a struct it is the same 8 bytes as Int; over FFI it is i64. std::time::current() reads the wall clock as one; iso8601, parse_time, unix, nanos, from_nanos, time_from_unix convert. Was a string-shaped placeholder until v0.20.0.
Duration	i64	Nanoseconds. Declared by the stdlib (type Duration = quantity Int in ns;, GH #1076 U4, spec/units.md § The stdlib’s time catalogue): a quantity of the time catalogue (ns us ms s min h day), whose literals are its units’ (5s, 100ms, 2min, 1day), each its count of nanoseconds. Arithmetic is the unit dialect’s algebra of quantities: Duration ± Duration → Duration; scalar scale Int * Duration (either order) produces Duration (the runtime-computed-delay shape, ms * 1ms); Duration / Duration → Int, the quotient of the two counts (1h / 1min is 60); Duration / Int → Duration, the integer division for a runtime divisor, and for an integer literal other than one a narrowing whose or says what becomes of the remainder (timeout / 2 or floor, or ceil, or <value>; a bare timeout / 2 is refused, U4’s second correction); Duration * Duration and % are refused, naming both. Keeps its representation: prints its nanoseconds (1500000000ns), tags a topic field u, is its own FFI class. d.in(u), d.split(u) and Duration(x) are the dialect’s conversions (spec/units.md § Conversions).
Bytes (m89)	ptr → [i64 len][u8 data[len]]	Binary-safe. Single-pointer ABI like String, but the underlying blob carries an explicit length prefix so embedded NUL bytes don’t truncate. len(b) reads the prefix. Distinct from String at the type level; the typechecker keeps them apart. Operations: std::io::fs::read_bytes (m89), Stream.send_bytes (m89), Stream.recv_bytes (Phase 2g; both fallible(IoError) since #209), std::bytes::at / std::bytes::slice / std::bytes::from_string (Phase 2g), std::str::from_bytes for the inverse direction (Phase 2g).
BytesView (F.30)	lotus_view_t { src: ptr, epoch: i64 } (16 bytes, by-value; SysV AMD64 returns in rax/rdx)	Non-owning view over a BytesBuilder’s buffer. Returned by BytesBuilder.view(). src is the builder pointer; epoch snapshots the builder’s mutation_epoch. The underlying Bytes-shaped data pointer (buf - 8) is recomputed at read time by lotus_bytes_view_data, so the view itself doesn’t allocate or carry the data pointer. Coerces implicitly to Bytes at function-argument READ positions (e.g. std::bytes::at(view, i), len(view), user-defined fallible-fn args, self/external/interface method args, monomorphized-generic args); codegen emits a call to lotus_bytes_view_data which checks the stamped epoch against the builder’s live epoch, panics on mismatch (F.30b mutation-while-view-live guard), and returns the recomputed data ptr on the OK path. Rejected at Bytes-typed storage sites — callers wanting owned storage must std::bytes::clone(view) for a deep-copy into the caller’s arena. Storage typed BytesView is allowed; a String / Bytes literal at a BytesView/StringView storage default is wrapped via lotus_view_from_static_data with epoch == LOTUS_VIEW_EPOCH_STATIC = -1 — the unpack helper sees the static sentinel and returns src directly without an epoch check (the literal lives in the global string table at program-lifetime, so there’s no source builder to check against). 2026-05-22 PM: ABI compacted from a 24-byte heap-allocated struct to this 16-byte by-value shape; no arena allocation per view() call.
StringView (F.30)	lotus_view_t { src: ptr, epoch: i64 } (16 bytes, by-value)	Non-owning view over a BytesBuilder’s NUL-terminated buffer. Returned by BytesBuilder.text_view(). Symmetric companion to BytesView: same layout, same epoch guard, same static sentinel. Coerces to String at read sites via lotus_str_view_data (which recomputes the C-string pointer as b->buf — the buf[len] == '\0' invariant maintained by every mutating op makes this well-formed); rejected at String-typed storage; std::str::clone(view) upgrades to owned.
BytesMut (#3)	raw {ptr, len} window (by-value; no [i64 len] prefix)	A non-owning raw writable/readable window — distinct from Bytes (which carries a length prefix the handle points into) because BytesMut is a bare {ptr, len} pair over memory owned elsewhere. Handed out by the zero-copy ring producer (Topic.write(max) { w => … } binds w: BytesMut over the reserved slot) and by std::io::MirrorRing (readable() / writable() return a BytesMut over the live / free region). Read it zero-copy with the _raw siblings of the binary-pack family (std::bytes::read_* / at / find_byte accept a BytesMut directly — length is the window length, not a prefix); write into it with the binary-pack writers (std::bytes::write_*). The window is valid only until the next ring commit / mirror advance — no epoch guard, so the lifetime discipline is the caller’s.

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 (any scale) / Uint are typecheck-rejected (platform-variable ABI or Hale-internal). See spec/ffi.md for the full marshalling table and the lifetime contract.

Float comparison

Float compares by IEEE 754. ==, <, <=, > and >= are the ordered comparisons: each is false when either operand is NaN, so nan == nan is false. != is the negation of == and is true when either operand is NaN — nan != nan and nan != 1.0 are both true (codegen fcmp une; until 2026-10-12 it lowered to the ordered fcmp one and answered both false). x != x is therefore the NaN test, the same one std::math::is_nan makes. The two zeros are equal (-0.0 == 0.0) and neither orders below the other; the infinities order beyond every finite value and equal themselves. A match arm on a Float literal is an == test, so it never matches a NaN scrutinee.

The value builtins follow IEEE 754-2019: min(a, b) / max(a, b) on Float are minimum / maximum — a NaN on either side makes the result NaN, and -0.0 orders below 0.0 (min(0.0, -0.0) is -0.0) — and abs(x) clears the sign bit (abs(-0.0) is 0.0, abs(nan) is NaN). They lower to llvm.minimum / llvm.maximum / llvm.fabs, inline on every target (f64.min / f64.max / f64.abs on wasm32), so none needs a libm symbol or host import.

Float text

A Float’s text (to_string(x), println(x), f"{x}", and what the api codec writes) is the shortest that reads back as the identical double, so parse_float(to_string(x)) == x for every finite x, a subnormal included: 0.1 + 0.2 is 0.30000000000000004, 99.999995 is 99.999995, 1.0 / 3.0 is 0.3333333333333333. Of two shortest texts equally near the double, it is the one ending in the even digit. The digits are laid out as C’s %.17g lays them: fixed point when the first digit’s decimal exponent is from -4 to 16, so an integral value has no point (100.0 is 100, 1234567.0 is 1234567), and otherwise one digit, the rest after a point, and a signed exponent of at least two digits (1e+17, 1e-05, 2.5e-300). Negative zero is -0, and NaN and the infinities are nan, inf and -inf. The text is the runtime’s own (lotus_fmt_float_shortest), not the C library’s, so a native and a wasm32 build print the same bytes. A format spec (f"{x:.2}") still rounds to its places.

Reading a decimal back (parse_float, and every Float a codec reads) is the runtime’s own exact reader too (lotus_read_decimal_exact): the nearest double to the decimal written, ties to the even one, from any number of digits, the same bits on every target. A text past the largest double (1e400), or a nonzero one that rounds to zero (1e-400), is refused; a subnormal (5e-324) reads as itself. A text that is no plain decimal (inf, nan) is read as before.

Decimal — the scale is part of the type

A Decimal<S> is a fixed-point number: an i128 mantissa m read as m × 10^-S. S, the scale, is an integer literal from 0 to 18 written in the type (Decimal<18>, Decimal<2>, Decimal<0>), and two scales are two types: they never unify, and nothing converts between them implicitly. Plain Decimal is Decimal<9>, the same type under either spelling, with the behaviour and the layout Decimal always had. Decimal<19> (or a scale that is not an integer literal) is a parse error at the scale: an i128 mantissa at scale 18 still holds twenty integer digits (about ±1.7 × 10²⁰), and 10^S is an Int, which the conversions multiply and divide by.

Layout. Every scale is the one i128 (16 bytes, align 16) in a struct field, a locus param, a bus payload and a return; the scale lives only in the type, so changing a field’s scale changes no offset. Decimal is not FFI-portable at any scale.

Literals. A Decimal literal (1.5d) has no scale of its own: it takes the scale of the place it flows into — a let ascription, a parameter, a struct field, a locus param or const ascription, a return or a fn body’s tail, the other operand of an arithmetic or comparison operator, the other argument of min / max, an array literal’s element type, a match’s scrutinee — and is Decimal<9> where nothing gives it one (let a = 1.5d;). So does an expression built only of such values: a negated literal, an arithmetic operator over two of them, a block, an if or a match whose every value is one (let y: Decimal<2> = match n { 1 -> 1.25d, _ -> 0.5d, };), an or over a std::str::parse_decimal / range_parse_decimal call whose fallback is one. An array, a tuple or a [v; N] literal holding a Decimal flows into its place element by element, its shape (length, arity) held first: a scale-less element takes the element’s scale whatever its neighbours are, and any other element is held to the element type ([a, 2.34d] into [Decimal<2>; 2], a a Decimal<2>, is two Decimal<2>s; [1.0d] is not a [Decimal; 2]). So does a bounded push, and a generic struct literal’s field of a parameter bound to a Decimal. An if or a match in expression position joins its arms as an operator joins its operands: a scale-less arm takes the scale the other arms have, and arms of two scales are mismatched. The literal must fit that scale: a nonzero digit past the scale’s last place, or a mantissa no i128 holds at it, is a check error at the literal (“Decimal literal 1.505d cannot be represented: a Decimal<2> has 2 fractional digits, and this one has a nonzero digit past them (it would be truncated); round it to 2 places, or give the place it flows into a wider scale”). Zeros past the last place are the same value and are accepted (1.500d is a Decimal<2>).

Arithmetic is within one scale. +, - and % are exact mantissa operations; * is (a × b) / 10^S and / is (a × 10^S) / b, each an integer division that drops the digits past the Sth place toward zero (1.0d / 3.0d is 0.333333333 at scale 9 and 0.333333333333333333 at 18; -1.0d / 3.0d is the negation; a product below one unit of the scale is 0), with no rounding and no diagnostic. The intermediate is the i128 itself up to scale 9, as Decimal always was, and wraps like Int arithmetic past it; above scale 9 the product and the scaled dividend are i256, so any two operands whose result an i128 holds compute exactly (an i128 intermediate at scale 18 overflows for operands as small as 14), and only a result past i128 wraps. Comparison orders the mantissas. Unary -, abs, min and max keep the scale. An operator, a binding, an argument or a return whose two Decimals have different scales is refused, naming both: “binary op: Decimal<18> and Decimal are different scales: a Decimal’s scale is part of its type, and two scales never mix; convert one explicitly (.rescale(18))”, “Decimal<18> is not Decimal: …”.

d.rescale(T) is the one conversion between scales, T an integer literal from 0 to 18, typed Decimal<T>:

• widening (T >= S) multiplies the mantissa by 10^(T-S) and is exact (a mantissa past i128 wraps, as * does);
• narrowing (T < S) divides by 10^(S-T), and a nonzero dropped digit is a remainder, so the call is fallible exactly as the unit dialect’s change of denomination is (spec/units.md § Conversions): its or says what becomes of the digits — or trunc (toward zero), or floor, or ceil, or half_up, or half_even round; or <value>, or raise, or handler(err) and or fail <payload> keep the exact quotient and take their path only when a dropped digit is nonzero, with an InexactError { kind, value, divisor } (kind is the target type, value the mantissa — the nearest Int — and divisor the power of ten). A bare narrowing rescale is refused: “.rescale(2) narrows Decimal<18> to Decimal<2>, dividing its mantissa by 10,000,000,000,000,000, and says nothing of the digits it drops: …”. or clamp / or wrap are a range’s policies and are refused here.

Printing. to_string, println and + with a String render the value at its scale with trailing zeros trimmed (12.50d prints 12.5 at every scale; 0.000000000000000001 at 18). The fixed-places surface is std::decimal::format(d, places) and an f-string precision ({d:.2}): exactly places fraction digits, rounded half-up away from zero, places clamped to 0..=S (there is no digit past the scale to print).

Parsing. std::str::parse_decimal(s) and range_parse_decimal(s, start, end) read at the scale of the place their result flows into (scale 9 where nothing gives one): let p: Decimal<18> = std::str::parse_decimal(s) or raise;. Text with a nonzero digit past that scale is the call’s ParseError, never a truncation; zeros past it are accepted.

On the wire. A bus payload carries the mantissa (16 bytes) and the scale is the topic’s type, so a field round-trips every digit its scale holds; a payload’s contract shape tags a Decimal<S> field d<S> for S other than 9 (d18; plain Decimal keeps d, spec/model.md § The shape of a type), so a publisher and a subscriber that disagree on a scale disagree on the contract. The JSON codec (T::to_json / T::from_json, the json: tag in spec/semantics.md) writes a Decimal<S> field as a JSON number with its exact digits and reads it back at the field’s scale; a number with a nonzero digit past the scale is the field’s wrong_type. An api surface’s codecs (JSON, protobuf) do not carry a Decimal at any scale (spec/api.md § Codecs): a row that names one is refused.

Units. A quantity, an identity and a range count an Int (spec/units.md), so quantity Decimal<18> in wei is refused as quantity Decimal in wei is (“a quantity counts an Int, and Decimal<18> is not one”).

Generics. Decimal<S> is a generic argument like any primitive: Box<Decimal<18>> is the monomorph Box_Decimal18 (plain Decimal keeps the token Decimal), and a literal in a field of a type parameter bound to Decimal<S> (let b: Box<Decimal<18>> = Box { value: 0.5d };) takes S.

Scalar types (GH #1076)

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.

Kind	Declared	As a type
Identity	type OrderId = distinct Int;, optionally { range: a..b; }	no arithmetic; compares within one; widens to nothing (Int(id), OrderId(n) convert)
Range	type Byte = Int { range: 0..256; }, or over an identity or a range	widens to its parent for free; narrowing into it is Byte(n) or …
Quantity	type Money = quantity Int in cent;, or a boundary denomination of one, type Ledger = quantity Int in cent { round: half_even; }	carries its denomination; converts by an exact factor
Point	type Price = point Tick;, optionally { origin: N UNIT; }	a position over its quantity

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

Compound types

Construct	Form	Notes
Slice / array	[T] or [T; N]	Dynamic or fixed-size
Bounded collection	bounded[T; N]	Fixed-capacity counted list, INLINE in its containing type/params ({ i64 len, [N x T] }). See § “bounded[T; N]” below.
Tuple	(A, B, C)	Fixed-size heterogeneous
Struct	type Foo { x: Int; y: Int = 0; }	Named record, a value: let b = a; copies (see § “A struct binding is a copy”). Each field can declare a default value (= expr); literals omitting a defaulted field fill it from the default at instantiation time, the default evaluated where the literal that leaves it is written. A default reads only its constants and the module’s items, never the literal’s scope (§ Locus params).
Enum	type Foo = enum { A, B(int) };	Tagged union (sum type). A constructor call carries the variant’s declared values: Foo::B(x) is checked for the count and each value’s type, a Decimal literal taking the field’s scale (“`Foo::B` value 0: expected `Int`, got `String`”). A payload-free enum is stored as its tag.
Set	type Inbound = Book | Trade;	Untagged union: each member is a declared struct or enum and is its own discriminant. A member’s value is the set’s where a set is expected; match names a member by its type. See § “Set types”.
Alias	type Thing = Int;	A second SPELLING of a type, not a new type. See § “Type aliases”.
Function	fn(A, B) -> C	First-class function values
Generic	Foo<T>	Parametric over type T

A variant may declare an error class before its name, @not_found Missing, one of @not_found, @conflict, @invalid, @forbidden and @unavailable; it is what a served member’s handler error of that variant is answered with (spec/api.md § Error classes), and any other word is a type error.

One name, one field (GH #1141)

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.

A struct binding is a copy (GH #713)

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 is fresh already and is bound as it is; so is a call’s result, unless the callee may hand back a place’s value (§ A local bound from a place is yours). A value read from a form’s cell (m.get(k) or d) is the reader’s in the same way: writing into it never changes the cell, though the compiler keeps its nested parts shared with the cell until a write could show (spec/forms.md § Reading a cell). 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.

Any binding of a place keeps its value

A String, Bytes, tuple, array or payload-enum value bound from a place — let s = self.f.s;, let (a, n) = self.pair;, a bare x = self.f.s, a match self.e { E::A(s) -> .. } payload, the array a for x in self.f.names walks — and a place passed straight to a call (self.take(self.f.s)) keep the value they were given, whatever replaces the place while they are live. So does a value carried out of a place by another expression: a match arm’s payload (let held = match self.e { E::A(s) -> s, E::B -> "", };), an if or block result, a tuple, array or record literal holding it, an or substitute, an enum constructor holding it. (A stdlib call’s result is built fresh, and a method’s copied out of its locus into the caller’s arena; a call that may hand back a part of an argument or a form cell’s read is a place’s value, § A local bound from a place is yours.) The compiler keeps these the place’s own pointer where it can, which costs nothing: it binds an owned copy only when a write that may replace the place comes between the binding and a use of it (or is the call it is passed to; an argument is passed by reference, so only a String or Bytes argument is copied — a record, tuple or array handed to a callee stays the caller’s, and what the callee writes through its parameter the caller sees — unless a later argument’s evaluation replaces its place, when it is copied whole: nothing is left to write through). An operand held while a later one is evaluated — an earlier argument of a call, a method’s receiver, a binary operator’s left side, an earlier field of a literal — is copied where it is evaluated when the later one may replace its place (take(match self.e { E::A(s) -> s, E::B -> "", }, self.reset())). Such a write is a store into the place’s field (self.f.s = .., self.f = .., through any root), a call whose callee writes it, transitively (a method of the locus its receiver’s type names, only that locus’s; a method through an interface or a perspective, any locus’s of the name; a method called on the field itself, as a form’s set), and anything that may run other code of the locus: a publish, yield and a stdlib call that parks on an async_io pool write what the program’s bus handlers write (a publish lowered as a direct call of its one subscriber’s handler writes what that handler writes), and a call the checker did not resolve — through a fn value (a local, a parameter, a field of fn type), of a name no declaration answers to, on a receiver it could not type — and a recovery statement may write anything. Every one of these questions is answered over the types the checker resolved (the ones it checks the program against: an alias, an imported seed’s lib::Kid, a qualified name and a fn-typed alias are what they name, whatever the spelling), never over a spelling resolved again; where the checker has no type for a value or no callee for a call, the binding is an owned copy. A field of a record the frame holds itself is never replaced under a binding of it (a write through a local root replaces the field’s pointer); a field read through a handle is — a value whose type is a locus, an interface or a perspective, however it is spelled (an alias, an imported seed’s lib::Kid, a binding’s declared type). A write inside a loop reaches a use anywhere in the loop when the variable was declared before the loop — a local declared outside and rebound inside (held = self.f.s; then a replacing call, read on the next iteration) included. Before this a String local held across a method that replaced its field read the block the replace retired, reused by the next allocation (spec/memory.md rules 6 and 7), and a same-length store into the field changed the local in place.

A local bound from a place is yours

Writing into a local bound from a place never changes the place, and writing into the place never changes the local (ruling of 2026-10-13). The local is any binding: a let or let mut, a bare =, a tuple let’s element, a match payload, a for element of an array, and a part of a local assigned from a place (h.arr = r.arr;, xs[0] = m.get(k) or d;); the place is a field (of self, a child, a record local, a parameter), an element, a local, a parameter, or a value carried out of one (a match or if result, a literal holding it, the result of a call that may hand it back). A call may hand back a place’s value when its callee returns a part of a parameter (fn get_in(r: R) -> In { return r.arr[0]; } returns the caller’s block uncopied), a form cell’s read (fn read() -> Rec { return self.m.get(1) or Rec { }; }), or what a callee that does returns — transitively, by which parameter. A callee the compiler cannot identify (a call through a fn value, a name nothing declares) may hand back a part of any argument its declared result type can be, hold or share a record, enum, array or tuple with (a Response handed back by fn(Context) -> Response is no part of the Context), and anything where that type is unknown; through a fn value that may be a method read as a value, also whatever that method’s receiver holds. A result declared a primitive or a handle never is one; a result fresh at its top level that holds such a value in a field (a returned struct literal around r.arr[0]) copies only when a write goes below that field. A free fn returning a field read through a handle parameter (fn arr_of(k: K) -> [In; 2] { return k.r.arr; }) hands back that locus’s storage, a place’s value; a locus’s method returning its own fields hands back a copy. A place’s value assigned into a part of a parameter (fn store(h: Holder, r: R) { h.arr = r.arr; }) is stored as a copy, so the caller’s two arguments never share a block. A cell’s read handed back through a call keeps its kind: passed straight to a callee that writes through it, it is copied where it is evaluated. A write into it is an assignment at any depth (a[0] = x, x.k = 1, b[i].inner.s = s) or a call that may write through its parameter.

let mut a = self.r.names;
a[0] = "x";                          // self.r.names is unchanged
match self.r.e { P::A(i) -> { i.k = 1; }, P::B -> { }, }   // so is the payload
for x in self.r.cells { x.k = 1; }   // and every element
let held = r.names;
r.names[0] = "y";                    // held[0] is what it was

How the compiler keeps this is its business, and it keeps reads free: the binding stays the place’s own block until a write into it, which copies the whole value into the frame first (copy on write, a flag per local set at each binding, so one copy serves every later write; a for element is copied at its first write in each iteration). A struct let or = of a place is a copy already (§ A struct binding is a copy); a struct literal holding a place’s value copies only the field written below (let mut l = R { a: self.a }; l.a[0] = x; copies a). A local handed to a call that may write through its parameter is bound as a copy, and so is a binding live across a write into the local’s or parameter’s value it was read from. Three shapes are not copies:

• the get-modify-store of a self field, let mut v = self.f; v.x[i] = y; self.f = v; — every binding of v reads that field, the store of v back into it follows the write on every path, nothing that may read the field (a read of it, a call of the program’s, a publish or yield) comes between, no other binding views it, and v is not used after. The store keeps the block the field already holds (spec/memory.md rule 6), so the write lands where the store would have put it;
• a parameter: an argument is passed by reference, and a callee that writes through its parameter (fn bump(r: R) { r.a[0] = 1; }) writes the caller’s value;
• a @form(vec) walk, for x in v.items, which visits the vec’s cells in place (spec/forms.md), and a value that is a locus handle.

Each copy is a site of the allocation survey (place-copy (<reason>): copy: written local bound from a place, copy: a local bound from a place is passed to a call that may write through its parameter, copy: what the local was read from is written while it is live), so it counts toward @budget(alloc_per_call = N) and the alloc effect, and the hot-path lint reports one in a loop, a bus handler or a @hot fn. A store’s own copy is one too: copy: a place's value stored into a part of a parameter (h.arr = r.arr), and copy: a value stored into a locus's field from outside its methods (§ A store into a locus’s field is the locus’s own), unless the slot or the value is an inline scalar. The latter is store-latest, as a method’s self.f = v is: a @hot fn’s error and a budget’s count, never a loop’s or a handler’s warning. A field of self handed to a call that may write through that parameter (poke(self.source)) is written there, as a store into it is, so a local or a literal’s part viewing it is copied first. A call through a parameter declared a fn returning a primitive (cb: fn(Int) -> Int) hands back a primitive, as a declared fn of that signature does. A bounded[T; N] local is not a first-class value and is not copied: a bounded intrinsic on one bound from a field still writes the field, and the element a push or a set stores through it is anchored where that field lives (the holding locus’s arena, for let mut dest = self.xs or a child’s field), as on the field itself; until 2026-10-17 it went to the current arena, so a method’s view of self.xs left the field holding Strings its scratch freed at return. Before this rule the write landed in the place’s block: let mut a = self.r.names; a[0] = x; changed the field.

Set types

A set type (GH #1530, 2026-10-17) is an untagged union: type Inbound = Book | Trade | Unknown;. Each member is a struct or an enum the program declares, and the member’s type is the discriminant, so nothing is named twice: no variant names a type that is already a name. A primitive, a list, a tuple or a function type is no member (a parse error: declare a struct that holds the value), nor is an alias of one; a set is no member of a set (name its members instead); a member is named once, and two members may not share the last segment of their names (a::Book and b::Book), since a pattern names a member by that alone.

A member’s value is the set’s wherever a set is expected: a return from a fn returning the set, an argument to a parameter of it, a let of its type, an assignment to a place of it and a field of it. Two sets may share a member; the place’s type says which set the value becomes. The arms of an if or a match whose values are different members are not joined into a set: give each arm the set’s type (a fn returning it).

match names each member by its type alone, binding the member’s value:

fn handle(m: Inbound) -> Outbound {
    return match m {
        Book(b) -> answer(b),
        Trade(t) -> fill(t),
        Unknown(u) -> reject(u.raw),
    };
}

A name that is no member of the scrutinee’s set is refused (“Side is not a member of the set Inbound, whose members are Book, Trade, Unknown”), and the match is exhaustive as an enum’s is: every member, or a _ arm. Name(_) matches a member without binding it; a bare Name is a binding, as everywhere.

Underneath, a set is an enum whose variants are its members, each named for its type and holding one value of it, and it costs what that enum costs: Inbound::Book(b) is the same value as b flowing into an Inbound, and both spellings are accepted. It prints as that enum does (Inbound::Book(Book { id: 7 })).

Type aliases

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>;`

Projection-class types

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.

Locus types

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 store into a locus’s field is the locus’s own

A store into a locus’s field from outside that locus’s methods is the locus’s own store, exactly as a method of it storing self.f = v (GH #1561). Such a store goes through a handle parameter (fn put(l: L, s: String) { l.name = s; }), a handle local (let l = L { }; l.name = s;), a child reached through a handle or through self (h.loc.name = s, self.loc.name = s in the parent’s method), or an element of an array of loci (ls[i].r.arr = r.arr). The locus that owns the field is the last one on the store’s path: loc in h.loc.name, the element in ls[i].r.arr.

• Owned. The value is copied into the owning locus’s storage (spec/memory.md rules 6 and 7) whatever spelled it: a place, an if, a match, a block, an or, a call, a concatenation. The locus and the caller never share a block afterwards, in either direction. A write into the locus (self.r.arr[0].k = 9, a same-length self.name = "ZZZ") never reaches the caller’s value, and a write into the caller’s value never reaches the locus. The copy lives as long as the locus that owns the field, whatever happens to the handle’s root (a child stored into through its parent outlives the parent).
• Retired. The value the store replaces is retired, and the store ends the way a method call on that locus does, at an activation boundary that makes the locus’s retired blocks reusable. A free fn that stores a fresh String into a long-lived locus 200 000 times stays at the same floor as the method form: 4.7 MB of resident memory for both.
• One pool. A store into the field of a locus that runs on another pool is refused at check, as the cross-pool method call is (§ Single-threaded-method invariant (F.31)). A store into an inline scalar slot (a number, a Bool, a Time, a payload-free enum) is one plain store with no arena work, and is not refused, as a cross-pool field read is not.
• A child replaced. A locus-typed field given a fresh locus literal (h.loc = L { … }) is the owner’s lifecycle reassign (§ Reassigning a locus-typed field is a lifecycle transition): the old child is reclaimed, the new one built as the owner’s field.

A store below a record held in a locus’s field (l.r.arr = v, l.c.s = s) is the same store, owned by that locus. The parameter-part rule (§ A local bound from a place is yours: h.arr = r.arr copies) is about a record the caller holds, not a locus, and adds no copy to a store through a handle: the store’s copy into the locus is the only one.

type is a top-level declaration

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 type cannot hold a locus

A type is plain data: it is copied by value and has no lifecycle, so it can neither own a locus nor keep one alive. A struct field, or an enum variant’s payload, whose type names a locus — the locus itself, an array, bounded[T; N] or tuple of it, or a stdlib locus (std::io::tcp::Stream) — is a type error at the field’s type:

main.hl:2:17: type error: `type Layer`: field `w` holds the locus `M`.
A `type` is plain data with no lifecycle: it is copied by value, so it
can neither own a locus nor keep one alive. Hold the locus in a locus
instead: make `Layer` a locus with a `params { ... }` field of type
`M`, or pass the `M` as a parameter where it is used.

A locus lives in a locus: a params field (the owner holds it for its life) or a parameter. An interface is not a locus here: a type may hold an interface-typed field, which is a handle (a fat pointer) rather than an owned locus.

Before this rule the checker accepted the field and the backend refused it with unknown type name in signature and no source location — a program the gate accepted that could not be built.

const is a top-level declaration

A const states its type, const LIMIT: Int = 100;, except where the initializer is a literal: const LIMIT = 100; takes the literal’s primitive type (Int, Float, Decimal, String, Bool, Bytes; a negated numeric literal too). Any other initializer without a type is a parse error at the initializer that says to write const NAME: T = …;.

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

Reserved member names

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

Name	Type	Meaning
children	[ChildType]	the accept’d-child collection (F.11); self.children.count / .is_empty summarize it
k_max	Float	the F.1 displacement bound computed from B / c / sigma / phi
draining	Bool	the F.27 drain flag, true once the locus is winding down

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.

Capacity-slot cell handles (F.22)

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.

Aspect	v1 behavior
LLVM repr	ptr — a typed pointer to T’s struct layout
Element type	The boxed inner type carries T from the slot’s of T declaration; Cell<Int> and Cell<Float> typecheck distinctly.
Validity surface	Round-trip only: a value can flow through let-bindings, get re-supplied to release / free, and live inside the locus body.
Forbidden ops	println, arithmetic, comparison, fn-return-boundary crossing. Printing a cell (println, print, to_string, an f-string) is a type error at the cell; the others reject with a focused build-time diagnostic.
Field access (v1.x-2)	Struct cells support cell.field reads and cell.field = v writes; lowers to struct GEP + load/store, and a read types as the record’s field. Primitive cells (Cell<Int> etc.) have no fields: c.foo is a type error at the field name.
Slot-of-origin tracking (v1.x-5)	Cell<T> carries both T AND the originating (locus, slot) pair. Releasing a cell into a different slot than it came from is a type error at the cell, naming the originating slot.

The checker follows a cell from the slot call that makes it (self.entries.acquire()) through the let bindings that hold it; those are the cells its rules see.

Perspective types

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

Interface types (F.20)

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.

An interface may also be the type of a locus’s accept and release param (accept(c: I)): the locus then accepts every locus satisfying I, by the same rule, resolved statically per concrete type, never through a vtable (semantics.md § Locus instantiation, “An interface accept”).

Inside the fn, the parameter’s local IS the interface: it offers exactly the interface’s methods, and nothing of the locus behind it. A field read (sink.path) or a method the interface does not declare (sink.flush()) is a check-time error naming the interface and its methods; a local bound from the parameter (let s = sink;) is the interface too (friction sweep 2026-10-12; until then the parameter typed as unknown, the check passed such a read and the build refused it). A fn or locus-method parameter has this typing; an interface- typed slot (a field, an array element, a let annotation) still accepts any satisfying locus.

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.

Type compatibility

Subtyping

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

Numeric coercion: Int → Float (Phase 2c)

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.

Explicit numeric conversions

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; a Decimal changes scale by d.rescale(T) (§ Decimal). 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.

Contract compatibility

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.

Three-way interface (F.14)

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

Mutability

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.

An assignment target names declared fields only. Each field of a place’s path (self.x, self.j.rec.p.a, r.ps[0].b, h.repo through a handle) is resolved as a read of it is: a field the record or the locus’s params does not declare is refused at the field with the read path’s diagnostic (“no field `record` on `Inner`”, with a near name when there is one), and the value is held to the field’s type. Until 2026-10-17 such a target checked clean and only the build refused it (“no field `record` on `self.j`”).

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. The same holds from outside the owner (h.loc = L { … } in a free fn, hs[i].loc = L { … }, GH #1561): the store is the owner’s, so the old child is reclaimed and the new one is built as the owner’s field, exactly as the owner’s own self.loc = L { … }. A field initializer of that literal may not read self in another locus’s method (it would read the owner); bind the value to a local first.

k_max as a typing rule

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

bounded[T; N] — fixed-capacity collections in types

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.

The element type is one a slot holds inline or by a pointer it anchors: a scalar (Int, Float, Bool, Decimal<S>, Duration, Time, an identity, a range or a quantity), an enum without payloads (its tag), String, Bytes or a struct. hale check refuses any other at the annotation, naming it: a tuple, an array, another bounded, an enum with payloads (a pointer to its cell, which the slots’ anchoring does not walk) or an interface (“`bounded[Shape; N]`: `Shape` is an enum with payloads, which a bounded buffer cannot hold inline … wrap the element in a struct”). Until 2026-10-13 the check admitted them and the build refused the element type with no file or line, and a payload-free enum, which lowers as a Bool does, was refused too.

Semantics:

• Fields auto-initialize EMPTY. Literal init is rejected — the intrinsics build a bounded value. Whole-STRUCT copies carry elements + count by construction (the storage is inline).
• A fn, a locus method or an interface method does not return a bounded (written, or through an alias): the check refuses the declaration (“`names` returns a `bounded[String; 4]`, and bounded[T; N] cannot be returned by value — it lives inline in its containing type …”), where the build refused it with no file or line until 2026-10-18. A record holding the bounded returns it.
• Its live count is count(x); len does not apply to a bounded (written or through an alias), and the check refuses it, pointing at count (“`len` does not apply to a `bounded[String; 4]`: a `bounded`’s live count is `count(x)`”), where the build refused it with no file or line until 2026-10-18.
• A bounded place (a field, a locus param) is assigned whole only from a value of its own type, bounded[T; N] with the same T and N: row.models = req.models copies the count and the live slots, and each pointer-shaped element is anchored in the place’s owner’s arena, as push anchors the one it adds (the holding locus’s arena, else the current one). It is a copy: a later intrinsic on either side does not reach the other. Any other value (an array literal, another element type or capacity) is refused at the assignment (“a `bounded[String; 4]` is assigned whole only from another `bounded[String; 4]` …”). A bounded local is not assigned whole: it is a view of the place it was bound from, and the assignment would anchor the elements in the frame rather than where that place lives (a locus’s field would hold blocks its method’s scratch frees), so the check refuses it and names the place to assign instead. Until 2026-10-17 every whole assignment was refused, with no ruling behind it but a lowering that had none, so a copy between two records’ fields was a push loop.
• Scalar elements (Int/Float/Bool/Decimal/Duration) are flat under zero_copy and travel the bus as raw bytes. A Time element is the i64 a Duration is and lowers inline the same way; it is not flat under zero_copy, as [Time; N] is not (semantics.md § Payload-shape compatibility). 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).
• A pointer-shaped element pushed or set into a bounded place under a parameter is kept in the frame that runs the call: a free fn allocates in its caller’s arena (a fn that takes a record is never scratch-local), a locus member in its own scratch. So a locus member doing it is refused at the intrinsic (“push of a `String` element into a bounded place under a parameter of a locus member …”), and a free fn doing it, directly or through a fn it hands the place to, is refused at a call that hands it a place the frame does not own: one under self or a bounded local viewing one (“`fill` stores pointer-shaped elements … this argument is a place in this locus’s arena …”). A call through a function value is the fn the value’s binding names (let f = fill;, a tuple let’s element of a tuple literal); a binding the body assigns (f = other;), a parameter of fn type or a computed callee names no one fn, and such a call is refused for any argument holding such a place. Names are bindings, not spellings: an inner let f names nothing after its block, and let r = r; is an owned copy, not the parameter. A generic fn is read as any other, its type parameters taken as any type (fail closed): a field path through one (fn fill<T>(r: T) { push(r.xs, s) }, or a local view of it, let dst = r.xs) may be such a place, so fill(self.row) is refused; a type parameter is the fn’s own, whatever global type shares its name. A record of the frame’s own, a copy of one, and a scalar element are sound; the shape that works for a locus’s field is to fill a local and store it whole (self.row = mine), which anchors the elements in the locus’s arena. The stdlib’s std::http::is_route writes its captures into ctx.params this way, so a context a locus holds is refused as its argument (2026-10-17: it was a use-after-free).
• 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.
• A wire map (2026-10-17): checks: bounded[Check; 16] indexed_by name; keys the list by its elements’ name. It is the same bounded list in the program (iterated, pushed, read by index); only the api codecs read the clause, which carry it as an object keyed by name (spec/api.md § Codecs). The clause has the @form(hashmap) slot clause’s spelling and rules: the field is a bounded[T; N], T a user-declared struct, and the named field a String field of it; any other shape is refused at the clause (`indexed_by` on `Health.checks`: key `Check.n` is a `Int`: a wire map's key is a `String` ...). Nothing keeps the keys distinct in the program; a duplicate key is refused when a payload is decoded, and an encoder writes what the list holds. indexed_by name -> status (2026-10-19) names the value of a map of values, each element crossing as its status alone. The element has the key and that field and no other, and the value is a scalar, a Time or a payload-free enum. Anything else is refused at the clause (`indexed_by` on `Health.checks`, its value `-> status`: `Check` has other fields (detail), ...).

Generics

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 that leaves them. Their generic call rows retain the default’s source site and distinguish the invocation path and the caller’s specialization. A default reads only its constants and the module’s items (§ Locus params), so every invocation types it alike. 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 } }
• the place of a plain assignment (=, not +=) — self.cfg = Cfg { n: 2 };, a local, a record’s field or an array’s element, by the place’s declared type

An array ([x, y] or [x; N]) or tuple literal at one of these sites hands each element the declared element type, so its template literals take that type’s arguments: let cs: [Cfg<Int>; 2] = [Cfg { n: 1 }, Cfg { n: 2 }];, let rs: [Cfg<Int>; 3] = [Cfg { n: 0 }; 3];, let t: (Cfg<Int>, String) = (Cfg { n: 1 }, "a");, and a param default of array type (params { cfgs: [Cfg<Int>; 2] = [Cfg { n: 1 }, Cfg { n: 2 }]; }).

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.

The literal’s fields are then typed as the instantiation’s: a field whose declared type mentions a parameter holds a value of the type the arguments make of it, so with b: Box<Int>, b = Box { value: "x" }; is a type error at "x" (type Box: field valueexpectsInt, got String``), wherever the literal stands. An Int widens into such a Float field of a data type, as into any data literal’s (F.23), never into a locus param’s.

Anywhere else — an un-annotated let (of the literal, or of an array or tuple literal holding it), 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; } }

Generic bounds

The constraint syntax <T: Bound> admits one bound, Numeric: the argument is Int, Float, a Decimal or a Duration (type Box<T: Numeric> { value: T; }, fn twice<T: Numeric>(x: T) -> T). hale check holds it where the template is instantiated — at the argument of a type annotation (Box<String>), and at the callee of a generic fn call whose arguments bind T to another type (an identity or a range included: it is a named argument) — and refuses any other bound name at the declaration (<T: Eq>, <T: SomeStruct>): there is no trait system. An argument that is itself a type parameter of the enclosing template is held where that template is instantiated.

main.hl:7:20: type error: generic type `Box`: `T` is bounded
`Numeric`, and `String` is not one of `Int`, `Float`, `Decimal` or
`Duration`

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.

What may be a generic argument

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

Decimal stands for every scale: Decimal<S>’s token is Decimal<S> without the brackets (Box<Decimal<18>> is Box_Decimal18), and plain Decimal’s (Decimal<9>) is Decimal.

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 identity or a range (spec/units.md) is one too, and lowers as its Int. A quantity or a point declared by the program is not: its unit lives in the checker’s rows for the places that name the type, and a generic body names T, so it would print and convert as the bare count. A generic fn call that would bind one is refused at the callee (“generic fn `id`: `T` would be `Money`, a quantity, and a generic body has no unit to print or convert one by”); the stdlib’s Duration and Time are primitives and bind. 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.

Type inference

let bindings

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.

Function return types

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

Locus params

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 where the locus is built, at instantiation time. A default reads only its own fields and constants, never the scope of the literal or call that leaves it. That holds for every default: a locus’s param, a record type’s field, a fn’s, method’s or hook’s param. Each name a default reads must be one of these:

  • a module-level item: a constant, a free fn (as a call or a value), a type, a variant, a locus;
  • a builtin, or a primitive’s conversion (Time(3ns));
  • a qualified path (no local is qualified);
  • a name the default binds itself (a block’s let, a match arm’s binding, an or handler’s err), where that binding is in scope: after its let and within its block, within its arm or handler. A read in a let’s own initializer, or after the block that bound it, is not the default’s. The checker answers each of these, typing the default once where it is declared with no binding in scope, as it types it wherever it is evaluated: a word after or is a narrowing’s policy (T(x) or clamp) only where the or narrows, and after any other fallible (parse_int(s) or clamp) it is a name like any other;
  • for a locus’s param only, an earlier param through self.<param>.

  Anything else is refused where the default is written (“a default reads only its own fields and constants; a is in the caller’s scope”): a caller’s local, a fn value bound there, an earlier parameter of the same fn. So is self in a record field’s or a fn’s, method’s or hook’s parameter default, where it would be the caller’s. A default that calls a fn leaving out a parameter, or builds a record leaving out a field, expands defaults held to the same rule where they are declared. Where a literal or call leaves a default out, a caller binding of a name the default reads (a let K beside const K) would be read in its place, so the check refuses that literal or call (“K here is the caller’s binding, …”): rename the binding or pass the value. A default publishes nothing: a <- (or a Topic.write) written in any default (a locus’s param, a record type’s field, a fn’s, method’s or hook’s param) is refused at the send, since the scope that evaluates it holds none of the declaration’s bus (“a publish in a default: …; publish from a hook or a method instead”). A method the default calls may publish. A record literal written in a default is held to every record literal’s rule: it writes each field that has no default of its own, and one that leaves such a field out is refused at the literal (“type T: missing field f”), in any default, by the check rather than the build.

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

inferred params

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.

Function types

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 function value is a free fn’s name read as a value (apply(dbl, 1)). A method is not one: it is called on its locus, and a fn(A) -> B value carries no locus, so self.dbl (or h.dbl, a perspective’s or an interface’s method) written anywhere but a call’s callee is a type error at the method’s name:

main.hl:3:33: type error: `.dbl` is a method of the locus `App`,
written as a value: a method is called on its locus (`….dbl(…)`),
and a `fn(…)` value carries none, so it is not one. Pass a free fn,
or call the method where the value is needed

A fallible(E) fn is not a value either, a program’s own, an imported seed’s (lib::parse) or the stdlib’s: its ABI returns the failure beside the value, and a fn(…) -> T value’s call reads a plain result, so there is no error channel to carry it through. Its name read as a value is a type error at the name that names a wrapper handling the error:

main.hl:4:27: type error: `parse` is `fallible(Oops)`, and a fn value
has no error channel: a call through it could not address the
failure. Wrap it in a fn that handles the error, `fn parse_or(a0:
String) -> Int { return parse(a0) or 0; }`, and pass that

A fn returning a locus is a value only when it builds every instance it returns — a fresh factory (spec/semantics.md § Dissolve timing rules): a call through a fn value hands its caller a fresh instance to own (a binding’s or a holder’s, else the frame’s temporary), so a fn that may hand back one it was given (fn id(w: W) -> W { return w; }) is a type error at its name:

main.hl:4:42: type error: `id` may hand back a `W` it did not build (one
it was given, or one another binding keeps), and a call through a fn
value hands its caller a fresh `W` to own: only a fn that builds every
`W` it returns may be taken as a value. Pass a fn that builds one, or
call `id` directly

A fn that hands back what a parameter of a fn type builds (fn via(f: fn() -> R) -> R { return f(); }) builds what it returns.

So every fn value returning a locus is a fresh factory, wherever it came from — a fn’s name, a call that returns one (let f = pick(); with fn pick() -> fn() -> W), an if, a loop variable over an array of them, a tuple pattern’s name — and a call through one is owned as a factory call is: by the binding it is bound to, by the field or the caller it is handed to, else by the frame, and a discarded one at the statement.

A fn handing back a tuple or an array with locus parts is a value under the same rule: only when it builds every locus part it returns (fn mk2() -> (W, Int) { return (W { }, 1); }), or hands back what a fn value it was handed builds, or a call of a fn that is one itself (fn mk3() -> (W, Int) { return mk2(); }, through any chain of such fns). The rule holds wherever a fn’s name is read as a value. A record’s field cannot hold such a fn value at all: a type holds no locus, not even in a fn type’s signature, so type R { f: fn() -> W = mkw; } is refused at fn() -> W, and so is a field or a variant typed by an alias of such a fn type (type Maker = fn() -> W;), through any chain of aliases.

A std:: fn is a value when the stdlib writes it in Hale: its body is merged into the program under its rename, so apply(std::url::encode, s) passes that fn as apply(dbl, 1) passes dbl, typed by its signature (a fallible one, std::hex::decode, is refused as above). A builtin the stdlib answers at a call (std::math::abs, std::str::upper) has no fn behind it, and its path in any position but a call’s callee is a type error at the path that names a wrapper:

main.hl:2:27: type error: `std::str::upper` is not a fn value: the
stdlib answers it at a call, and there is no fn behind it to pass.
Wrap it in a fn of your own, `fn upper_of(a0: String) -> String {
return std::str::upper(a0); }`, and pass that

Calls to bare names

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:

group	names
length and rendering	len, to_string
the numeric casts	Int, Float
the printers	print, println, eprint, eprintln
the numeric trio	abs, min, max
the string predicates	starts_with, contains
the bounded intrinsics	push, at, set, count, clear, truncate
accumulators, inside a closure assertion	count, mean
the explicit-epoch closure surface	check_closures

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

A binding declared as a fn value shadows a top-level fn, or a builtin (len, min, a bounded intrinsic, a printer), of the same name in a call, as it does wherever else the name is read. A binding is declared as a fn value when its declaration says so: a parameter or a let written with a fn(..) type, a let (or a tuple let‘s part) of a fn’s name or of another such binding, a for over an array literal of fns’ names, a match pattern’s binding of a variant’s value whose declared type is a fn(..) type (Op::Use(f) with Use(fn(Int) -> Int)). So fn apply(f: fn(Int) -> Int, x: Int) -> Int { return f(x); } beside a fn f calls the parameter, and { let helper = zero; helper() } calls zero.

A bare callee no such binding shadows names the fn or the builtin. A binding of a known type that is no fn leaves it so (let max = 10; max(1, 2) calls the builtin, max still reads 10). A binding whose declaration does not show it to be a fn value, while its type is one or is one the check cannot name (a tuple pattern’s binding, a value read from a field or a call), would read as the callee and is not: the check refuses the call, and the binding is given its type, or renamed. A call through a value that is no fn (let x = 3; x(2)) is refused at the callee.

A call the compiler writes into the user’s scope (an f-string’s to_string and __fmt, a from_json’s parser) is the compiler’s, whatever binding of the name is in scope. A qualified callee (lib::helper()) names the declaration. The check and the build read every call one way: the desugar sequence calls a shadowing binding as a value before either sees the program.

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:

call	operands	type
len(x)	a String or Bytes (or a view of either), a fixed-size array	Int
to_string(x)	a printable value	String
Int(x) / Float(x)	an Int or a Float	Int / Float
abs(x), min(a, b), max(a, b)	Int, Float, Duration or Decimal, one type throughout	the operands’ type
starts_with(s, p), contains(s, p)	two Strings	Bool

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.

Bare identifiers

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

Bare type names

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.

Contract subsumption

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.

Vertical-only flow as a typing rule

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.

Single-threaded-method invariant (F.31)

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.

   The receiver is the field instance however the call reaches it (GH #1561): below the field (self.h.w.m(), self.h.ws[i].m() — a nested instance, an element included, runs in its holder’s pool), through a local bound to it (let w = self.w; w.m()) or a for over its elements. The check is a dataflow over the body: each local carries what it may be (a cross-pool instance) and what it may hold (a tuple, array or record around one, a fresh locus literal whose params do), joined where control flow merges, iterated to a fixpoint over a loop (its condition included, at every iteration), with each block’s lets in a scope of their own (a shadowed binding keeps its own rebinds) and a block’s, if’s or match‘s value taken from its tail before its locals go out of scope; a part written (ws[0] = self.b) joins into its container, a field of self any member stores a handle into may be that handle wherever it is read, and an operand or fallback that may be skipped (&&, ||, or) is joined with the state that skipped it. A call carries its callee’s writes too: a helper that writes one argument into a part of another (fn install(ws: [W; 2], w: W) { ws[0] = w; }), or a method that writes an argument into its own field, leaves the caller’s container or field holding that argument’s handle, and so does a method that writes one of its own fields into an argument (that field of the receiver, per instance). A bounded-list push or set stores its value into the list (no form cell can be a locus); a stdlib fn may write an argument into another only when the other’s declared type can hold it; a call through a fn value, or one the check cannot see into, may write any argument into any other; a serve site (api::serve) writes none, its receivers being reached through the bus. A locus literal is one instance however many bindings copy its handle: what is written into it through one (let alias = h; alias.ws[0] = self.b;) is read through every other (h.ws[0]), and its params’ values are held by field. A method that stores into, or calls a method on, a locus one of its own fields holds (fn poke() { self.ws[0].name = s; }) is judged, on a receiver that is no field of self (a literal, a local or a parameter bound to one), on what that receiver’s field may hold: H { ws: [self.b, self.a] }.poke() is the store into self.b itself, as is the same call on a field of self a member stored that literal into, or through a local or helper inside the method (let w = self.ws[0]; w.name = s;, put(self.ws[0])); a method of a receiver whose locus type the check cannot tell (hs[0].poke()) is judged as every method of that name. A locus a helper builds and returns is one instance built at the call, holding what the helper’s held (let h = make(); let alias = h; share it), and one it was handed is still that instance. A callee the check has not yet summarized does nothing until it is, so the order fns are declared in never changes a verdict. A value whose type can hold no locus handle (a record of data, a String) carries none: reading one copies it. A value comes from a field of self (or below one), another local, a part of one (p.0, ws[1], n.w), a literal holding one, or a call: a fn or method by what its body may return (a parameter or a part of one, a field of self, or a value holding one — summarized per body, transitively; a fresh record of its own carries nothing, a fresh locus is the instance built at the call), a call through a fn value declared to return a locus type by any instance of that type (one on another pool is enough), and a stdlib call by its declared result, which carries an argument’s handle only when it can be or hold that argument’s type, a generic result included. (A method may not return a locus itself.) — and through a free fn handed it that calls a method on its parameter (fn poke(w: W) { w.m(); }, poke(self.w)), directly or by handing the parameter on to such a fn (by name, a fixpoint over the program’s free fns).

   A store into a field of the receiver instance is that locus’s own work, as a method call on it is (§ A store into a locus’s field is the locus’s own), and is rejected the same way when the pools differ, reached the same ways: a store down self.field (self.w.name = s, self.h.ws[i].name = s); a store through a local bound to self.field (let w = self.w; w.name = s;); and a call of a free fn that stores into a field of the parameter it is handed self.field at (put(self.w, s) with fn put(w: W, s: String) { w.name = s; }). The last includes a fn that hands that parameter on to such a fn, transitively. The diagnostic names the locus, both pools and the store, and suggests a method of that locus, reached through the bus. GH #1561: such a store copies the value into the receiver’s arena and retires what it replaces, which only the receiver’s own thread may do. A store whose slot is an inline scalar (a number, a Bool, a Time or Duration, a unit scalar, a payload-free enum, read from the declarations) is one plain store with no arena work, and is not rejected, as a cross-pool field read is not.

   Not followed, known: what a handler the runtime calls through a function pointer does (an std::http::Server handler, a serve site’s receivers: the site is the exposure it builds, and the handler runs on the server’s pool); a stdlib locus’s own methods, which are not summarized (a call on one may move any argument into any other and into the receiver, but what it stores into or calls on a locus it holds is not judged); the parameter effects of a method on a receiver whose locus type the check cannot tell; and a call through an interface. A locus’s params defaults are walked only for the hand-over rule below. Where the check cannot tell instances apart it takes them as one: every instance one literal (or one call of a helper that builds one) produces, and every free fn of one name, so it may refuse a store into an instance that never holds the handle another one does.

   One instance is never shared across pools (GH #1566). A locus that holds an instance in a field reaches it as its own, on its own thread, so handing it an instance that runs on another pool makes one instance two threads write. Such a hand-over is refused where it is made: a locus literal’s param, a store into a locus’s field (or an element or part below one), or a call of a helper that does either with an argument — whenever the value may be an existing instance (a field of another instance, or a value reached from one, through locals, blocks, parameters, returns and aggregates) that runs on another pool than the locus receiving it. A literal or store in a member runs on the member’s pool; one in a params default builds for the field it fills, so srv: std::http::Server = std::http::Server { .., handler: Routes { w: self.a } }, with srv placed on io and a on main, is refused at self.a — and so are Routes { w: { let x = self.a; x } }, mk(self.a) with fn mk(w: W) -> Routes { return Routes { w: w }; }, and the same with a local in mk:

   cross-pool alias: `W` (`self.a`) runs on `cooperative(pool = main)`; `mk(…)` hands it to `Routes`, which runs on `cooperative(pool = io)`, shares one instance across pools — build it on that side, or reach it through a method on the bus.

   A stdlib locus literal (std::http::Server { handler: … }) receives its params the same way, and a field of self the placement table places no instance for (a tuple or an array of loci, a field of interface type) runs where its owner does: handler: self.pr.0, with pr: (Routes, W) on main and the server on io, is refused. An instance the code builds itself and hands over (Routes { w: W { } }, a helper that builds and returns one) is moved, not shared, and is accepted; so is a hand-over within one pool. A locus whose form synchronizes access from another domain, and a stdlib locus (a metrics registry, a router), may be shared: their own synchronization carries the contract, and a method call on one from the wrong pool is still refused as above.

   The rule is checked statically where the walk follows the handle, and enforced at run time at every remaining site (GH #1566, spec/runtime.md § Cross-pool backstop): every instance records the domain it was built on, and a store into a locus’s field from outside its methods (not an inline scalar slot) or a method call on a locus reached any way but down self (through an interface, on the locus behind it) compares the receiver’s domain with the running code’s. A mismatch is a violation: the program prints the site, the store (or the method call, cross-pool method call with the method) and both pools, and exits 1, before the store or the call touches the other pool’s locus:

   main.hl:8:9: violation: cross-pool store into `W.name` from pool `io`; this `W` runs on pool `main`: reach it through a method on the bus

   An instance is on the domain it was built on until a locus first holds it in a field (a literal’s param, an element of an array param, a store, a field of interface type): an instance no locus held yet — one the code built and handed over through locals and parameters, Web built in fn main and handed through helpers to an io-placed server’s handler — becomes that holder’s and moves onto the domain it runs on, with everything it is in turn the first holder of (a provider composed from locals moves with the service it holds). An instance a locus already holds is shared by a later holder, not moved: it keeps its domain, so whichever side is not its owner is caught (the hand-over the check cannot follow, a builder called through a fn value, fails at the holder’s first store into it). Down self, a receiver is checked when the path goes through a field filled with anything but a value the literal or store builds right there. Hale does not refuse a use of a local after the hand-over, so a builder that kept it and reaches the instance from its own domain afterwards is caught at run time too. A receiver whose form synchronizes access from another domain, and a local bound to a locus literal the running code built (never rebound, never handed over), are not checked; a locus’s drain() and dissolve() run as its own domain wherever the runtime runs them, and an on_failure handler reaches its failed child, and the subtree the child owns, on the child’s domain — not any other instance there. A violation found inside the stdlib, which has no location of its own, is reported at the program’s last call into a stdlib locus on that thread.

   Two exemptions are by design. What a bindings { } entry builds (an adapter, a transport, a codec) belongs to no one domain: the runtime calls an adapter’s send from every publishing thread through a function pointer, and the adapter’s own synchronization carries that contract. And a stdlib locus handed a value of self at its literal (an exposure its transport, a server its handler) is driven from the pool its machinery runs on: the stdlib’s own synchronization covers it, so such a field is not checked down self.

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:

Annotation	Discipline	Trade-off
@form(hashmap)	single-pool only	densest layout, no sync overhead, cross-pool calls rejected
@form(hashmap, sync = serialized)	per-map mutex (F.32-1α)	correct cross-pool; throughput bounded by lock contention
@form(hashmap, sync = striped)	cell-level CAS + per-map rwlock for grow + cache-padded cells (F.32-1β2-v2)	parallel writers; grow path serializes; rwlock overhead can outweigh parallelism on cheap-payload workloads
@form(hashmap, sync = lockfree) (optional cap = N hint)	cell-level CAS, no rwlock or mutex on the steady-state path; remove via tombstones + lazy grow with a brief migration stall (F.32-1γ-v2)	highest measured throughput on the false-sharing bench

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.

Closure-test typing

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.

Fallible typing (v1.x-FORM-1)

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

Ty::Fallible { success, payload }

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

Source	Inferred type
fn f() -> T fallible(E)	f() has type Ty::Fallible { success: T, payload: E }
or on fallible	unwraps to T

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.

Disposition operators (or)

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

A statement or on a value-bearing fallible runs its substitute the same way, for its effect: parse(s) or { log(err); };, parse(s) or note(err); with a handler of any type, or parse(s) or 0;. (Until 2026-10-13 the build refused a block with no tail and a handler of another type there, which the check admitted.)

The value of an or whose call succeeds with () is no value: let full = push(self.marks, t) or { }; is refused at the expression, as every ()-typed expression in a value position is (spec/semantics.md § “Expressions with no value”). Write the call as a statement.

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.

ClosureViolation, the error of a violating fn (F.42)

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 statement

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

Custom payload types

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.

Synthesized stdlib payload types

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.

Winning means standing in for the builtin wherever lowering builds one under that name, and the stdlib’s own code is merged into every program: its parsers reach ParseError, std::crypto reaches CryptoError, its bounded pushes CapacityError, its closures ClosureViolation, its @form loci IndexError and KeyError, in every program whether or not the program calls them. So a program’s type of one of those names that lacks a field of the builtin’s shape (by name and primitive type) is a type error at its declaration:

main.hl:1:1: type error: user-declared `type ParseError` shadows the
stdlib's `ParseError` but is missing the expected `kind: String`
field (the stdlib's own code, merged into every program, and lowering
build `ParseError` under that name on failure). Either match the
stdlib shape, rename your type (e.g. `MyParseError`), or use
`std::str::ParseError` qualified where you need the stdlib's shape.

EmptyError and the other builtins the stdlib does not reach are refused only in a program that reaches them itself (a @form(heap), a std:: call failing with one).

Trigger	Type	Fields
@form(vec)	IndexError	kind: String, index: Int, len: Int
@form(hashmap)	KeyError	kind: String (also surfaces IndexError on key_at / entry_at — those are index-based, added 2026-05-16)
@form(ring_buffer), @form(heap)	EmptyError	kind: String
std::io::fs::* / std::io::tcp::*	IoError	kind: String, errno: Int, path: String, detail: String

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

Roles (GH #1109, #1417)

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 another seed declares may be named through the import alias, lib::reader, wherever a role is named: a requires: [...] list (a surface row’s, an @rpc attribute’s, a hub binding’s) and an includes. The path collapses to the role’s own name when the seed the alias imports declares that role, so lib::reader and the bare reader are one role and a description, a refusal and the environment’s role table all say reader. Roles are their own namespace: a library that declares role reader; and fn reader() keeps both, lib::reader in a role position is the role and lib::reader() the fn. A path whose alias the seed does not import, or whose seed declares no such role, is left as written and refused as an undeclared role in the author’s spelling.

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-primitive typing

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.

Working-set estimator (F.32-2)

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

Flag	Effect
--locality-report	Emit a per-locus stderr report listing each locus’s estimated bytes, smallest-fitting tier, and a struct / capacity / children byte decomposition. Build proceeds.
--target-cache l1|l2|l3	Evaluate each locus against the named tier’s budget. Over-budget loci surface as a stderr warning by default.
--strict	Convert the warning into a build error (exit 1 before codegen). Only meaningful in combination with --target-cache or a program that carries @locality(...) annotations.

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.

Verification responsibilities

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.