# Wolf Language Specification — 10: Types

Status: normative, v1 (campaign c27, sprint s113). Anchors `[type.*]`.
The numeric-literal typing rules this chapter writes down were, before
D54, scattered across s13 (the unification-with-levels engine), D49 (the
operator bridge), and s17 (the closed coercion set); D54 unified them
and this chapter is their single home. Implemented by `wolf_sema`
(literal kinds are variable constraints in `unify`, the cast lowers in
`wolf_wir`). Evidence: `.docs/planning/02-decisions.md` D54, D49; the
`corpus/typecheck/numlit_*` and `corpus/faults/cast_*` litmus files are
the checkable consequences.

The claim this chapter buys: an integer literal reads as the number it
denotes in the float context it is written into — `0` is `0.0` when
`0.0` is expected — while a concrete *value* never silently changes its
type. The `.0`-on-everything tax and the `let a: int = 3` workaround
both retire; the C usual-arithmetic-conversions footgun does not follow.

---

## §1 Numeric literals `[type.numlit]`

A numeric literal is untyped at birth: it carries a **kind**, not a
type, and acquires its type from the context it is written into or, if
no context decides, from a defaulting rule. The four rules below are one
system.

- `[type.numlit.kind]` Every numeric literal has one of two kinds:
  `{integer}` (a digit sequence, `0x…` hex, `_` separators — no dot, no
  exponent) or `{float}` (a literal with a fraction dot or an exponent).
  The kinds are **distinct** and neither is a type: `{integer}` and
  `{float}` name constraints a real type must satisfy. A literal's kind
  is fixed by its spelling and never changes; what a literal *adopts* is
  a type (§`[type.numlit.adopt]`), never a kind.

- `[type.numlit.adopt]` **An integer literal satisfies a float
  expectation.** In a position whose expected type is a float
  (`f32`/`f64`), an `{integer}`-kind literal resolves as that float:
  `let x: f64 = 0`, `c <= 200` with `c: f64`, and a bare `0` argument to
  an `f64` parameter are all legal, and mean `0.0`, `200.0`, `0.0`. This
  is **sound and lossless** because a literal carries no computation
  history — `0` denotes the exact value `0`, representable in the float
  with no rounding — and it is **one-directional**: a `{float}`-kind
  literal never satisfies an integer expectation (`let n: int = 0.0` is
  refused, E0401), because `0.0` is not an integer denotation. Adoption
  is a property of **literals only**; a concrete value never adopts
  (§`[type.numlit.value]`).

- `[type.numlit.propagate]` **Adoption propagates through an arithmetic
  or comparison term.** The operators `+ - * / %` and `< <= > >= == !=`
  bridge to their arithmetic/ordering meaning over the numeric
  primitives (the D49 lineage extended from comparison to arithmetic by
  D54; same static-dispatch-over-visible-primitive-impls temperament, no
  erasure, no implicit value coercion). Because the operands of a term
  share one type through the checker's unification, a float expectation
  reaching **any** point of the term pins the **whole** term: in
  `c * 1.8 + 32` with `c: f64`, the `32` (and, absent an `f64` `c`, the
  `1.8` and every other literal in the term) resolves as `f64`, and the
  arithmetic is float arithmetic. The **reach** is exactly the term
  connected by these operators and the expectation flowing into its
  root: adoption does not cross a binding (`let n = 0; …` fixes `n`'s
  type at the binding, §`[type.numlit.value]`), and into a call it
  reaches only the declared parameter type. The soundness consequence,
  pinned: `let x: f64 = 1 / 2` is `0.5` — both literals adopt `f64`
  *before* `/` runs, so it is float division — whereas `let n: int =
  1 / 2` is `0`, integer division, the two literals having adopted
  `int`. The operator chooses int-vs-float by its operands' resolved
  type, never by the literals' spelling.

- `[type.numlit.default]` **A literal with no reachable numeric context
  defaults by kind.** When no expectation decides a literal's type, an
  `{integer}` literal resolves as `i32` and a `{float}` literal as
  `f64` (the s13 rule), applied once at the end of the enclosing body,
  not as a solver step. Defaulting is a *rule*, never a guess: a literal
  whose kind itself cannot be determined is an inference error (E0405),
  and a literal reached by two **incompatible** concrete expectations
  (an `f64` from one side and an `i32` from another) is the ordinary
  type mismatch (E0401, `[type.numlit.ambig]`) — the checker names the
  conflict and the spelled `as` fix, it never picks one side.
  **A bound is context** (wolf-lang#347, 2026-09-15). An `{integer}`
  literal whose only context is a type parameter under a trait bound —
  `refund(340)` under `fn refund[T: Neg](charged: T) -> T` — is not a
  literal with no context: the bound constrains it. It still takes
  `i32` when `i32` satisfies every bound recorded against it; when
  `i32` does not, it takes `int` if `int` does (the language's integer
  type, the one every `impl … for int` names), else the one other
  integer type that does. With none, or with two or more other
  candidates, the rule's `i32` stands and the unmet bound is E0502,
  whose note says the literal defaulted and names the candidates. No
  runtime cost; a static rule, and a `{float}` literal is unchanged.
  Witness `corpus/traits/bound_literal_default.lu`.

- `[type.numlit.ambig]` Ambiguity is a **named error, never a guess.**
  If a single literal is required to be two incompatible concrete types
  at once, the checker reports E0401 at the literal, naming both
  requirements and their origins, with the `as`-conversion fix — the
  same diagnostic that reports any type mismatch. No literal is ever
  resolved by choosing arbitrarily between live expectations.

## §2 Values are spelled `[type.numlit.value]`

A concrete numeric **value** never implicitly changes its type. `let n =
0` fixes `n`'s type **at the binding**, and which type that is belongs
to §`[type.numlit.default]`: `i32` when nothing in the body decides it,
`int` (or any other type) where a later use in the same body does —
`take_int(n)` pins it, because defaulting is applied once at the end of
the enclosing body and a reachable expectation gets there first. Either
way the VALUE is then fixed: `let x: f64 = n` is **refused** (E0401) —
the `.0` of adoption is a literal's privilege, not a value's. **The
literal written at the binding is not that later type.** It has no
context of its own (`[type.numlit.propagate]`: adoption does not cross
a binding), so it takes `i32` and must fit it: `let big = 5000000000`
followed by `take_int(big)` is **E0415** at the literal, because the
call decides `big`'s type but never the literal's. The same holds when
the initializer is a term made only of literals (`3000000000 + 1`,
`-3000000000 * 2`, `0 - 9223372036854775807 - 1`). A term with any other
operand has that operand's type as its own context, so `packed /
10000000000` with `packed: int` is an `int` division; and a literal in
a call argument, a comparison operand or a block inside the
initializer has that position's context instead.
The spelling that means a wider literal is the annotation, `let big:
int = 5000000000`. This is the X3 safety posture and the closed-coercion-set
discipline of the memory model (`[mem.dyn.unsize]`'s "the coercion table
grows by addition, never by a new implicit mechanism"): C's
usual-arithmetic-conversions and Swift's exponential-search overloading
are both declined. A value's conversion is the spelled `as` cast.
**The cost, stated:** zero — binding and defaulting are static, and a
refusal adds no instruction to any accepted program. (Corrected
2026-09-15 by s163 for wolf-lang#403, filed by s165: this section said
`let n = 0` fixes `n` as `int` "by `[type.numlit.default]`", and that
rule says `i32`; the two could not both be right, and the
implementation follows `i32`. Measured at trunk `4b56441`: an unused
`let big = 5000000000` is E0415 on both wolf tiers, "the literal does
not fit `i32`", and `trap(overflow)` on lupin 0.1.36; add
`take_int(big)` and wolf runs it, the later use having pinned `int`
before the rule fires. The section's own point — a value never
implicitly changes its type — was never at issue. Witnesses:
`typecheck/numlit_fit.lu`, `typecheck/numlit_value_refused.lu`.
Corrected 2026-10-02 by s202 for wolf-lang#458: that last measurement
was the defect, not the rule. A later `int` use typed the literal as
well as the binding, so `let c = 922337203685477580` compared with an
`int` ran as 64-bit on every wolfgang lane while lupin 0.1.43 trapped
it as outside `i32`. The literal now takes `i32` at the binding on
checked, native and release (E0415), which is lupin's answer; a later
use still types the binding, so `let n = 0; take_int(n)` and `var i =
0` compared with `xs.len` are unchanged. No corpus row and no
boreutils or lobo build moved. Witnesses:
`typecheck/numlit_binding_literal.lu`, `numlit_binding_literal_call.lu`,
`numlit_binding_literal_term.lu`, and the control
`numlit_binding_value_later_use.lu`.)

## §3 The numeric cast `[type.numlit.cast]`

`as` between numeric types is the **only** spelling of a value
conversion, and its numeric arms are closed and total:

- `[type.numlit.cast.widen]` **`int as float` is free.** An integer
  value widens to a float (`n as f64`, `n as f32`) with the platform
  round-to-nearest for the rare wide-integer case; there is no semantic
  question and no trap. `int as int` widening is the sign/zero-extend of
  the memory model (source signedness decides), unchanged.

- `[type.numlit.cast.trunc]` **`float as int` truncates toward zero and
  traps if the result does not fit.** `3.7 as int` is `3`, `-3.7 as int`
  is `-3` (the `fptosi`/`fptoui` default, C-familiar truncation). If the
  truncated value does not fit the target integer — overflow, or a NaN
  input, which fits no integer — the cast **traps** (`trap(overflow)`,
  `[conf.trap.set]`), joining the checked-arithmetic trap family: it is
  the `255 + 1`-on-a-`u8` event, not C's undefined behavior and not a
  silent saturating clamp. Rounding other than truncation is a spelled
  `std.math` call (`x.round() as int`); saturation, if ever wanted, is a
  named `std` function — the cast itself never guesses. Target
  signedness (`fptosi` vs `fptoui`) follows the target type.

- `[type.numlit.cast.wrap]` **`wrapping[T] as int` is value-preserving
  and traps out of range** (D56). Leaving the wrapping domain is a
  conversion of the held VALUE, not a reinterpretation of its bits: a
  `wrapping[u64]` holding `2^63` or more does not fit `i64`, so the cast
  **traps** (`trap(overflow)`, `[conf.trap.set]`), joining the same
  checked-arithmetic trap family as the float row — never the silent
  bit-cast to a negative number that the earlier lowering emitted (the
  "cast that lies" D54 forbids). An in-range value converts unchanged;
  the widening unsigned direction (`wrapping[u32] as int`) zero-extends
  and never traps. A bit-reinterpretation, if ever wanted, is a distinct
  explicit unsafe-tier operation, never this `as` cast's silent default —
  the same posture as saturation on the float row.

- `[type.numlit.cast.narrow]` **An integer cast keeps the value, and
  traps if the target cannot hold it.** `as` between two integer types
  (`int`, `uint`, `i8`–`i64`, `u8`–`u64`, and a `wrapping[T]` source)
  converts the VALUE. Where the target holds every value of the source
  (a wider type of the same signedness, or an unsigned source into a
  wider signed type) the cast is total: it extends by the source's
  signedness and never traps. Every other pair is a **narrowing cast**:
  a narrower width, or a change of sign at any width (`int as uint`,
  `u32 as i32`, `i8 as u64`). A narrowing cast checks the value against
  the target's range and keeps it unchanged when it fits (`200 as u8` is
  `200`, `-1 as i16` is `-1`); when it does not fit (`256 as u8`, `-1 as
  u64`, `128 as u8 as i8`), the cast **traps** (`trap(overflow)`,
  `[conf.trap.set]`), the same family as `[type.numlit.cast.trunc]` and
  `[type.numlit.cast.wrap]` (which is this rule's unsigned-to-signed
  case). Truncation to the low bits is spelled through the wrapping
  family, whose cast target masks to its width and never traps
  (wolf-lang#131): `x as wrapping[u8] as u8` is `x`'s low eight
  bits, `300 as wrapping[u8] as u8` is `44`, `-1 as wrapping[u32] as
  u32` is `4294967295`, `200 as wrapping[i8] as i8` is `-56`. A
  bit-reinterpretation between signednesses is that spelling too
  (`x as wrapping[u64] as …`), never the plain cast. `byte` is not an
  integer type and keeps its own truncating bridge
  (`[type.byte.cast]`). **The cost, stated:** one compare and a branch
  to the trap per narrowing cast whose value is not known at compile
  time; a total cast and a wrapping target cost nothing. Ruled K12
  (STATUS #31, wolf-lang#533) as the checked machine and lupin already
  answered; until then native and release refused the narrower widths
  and reinterpreted the bits on a change of sign. Witnesses:
  `corpus/faults/cast_narrow_*.lu`, `corpus/typecheck/cast_narrow_*.lu`,
  and `crates/wolf_driver/tests/narrow_cast_lanes.rs` (every ordered
  pair of the ten integer types at the target's boundary values, on
  four machines).

## §3b The float remainder `[type.float.rem]`

- `[type.float.rem]` **`%` on a float is C's `fmod`** — the remainder
  of the truncated division: `7.5 % 3.0` is `1.5`, `-7.5 % 3.0` is
  `-1.5` (the sign is the **dividend's**, not the divisor's), `x % 0.0`
  and `inf % y` are NaN, and nothing traps — floats are IEEE and X3's
  trap law is integer law (`[type.numlit.cast.trunc]`'s trap is a
  cast's, not an operator's). Not the IEEE `remainder` function, which
  rounds the quotient to nearest-even and would make `7.5 % 3.0` be
  `-1.5`; `fmod` is what every neighbour language's `%` means at a
  float, what LLVM's `frem` is defined as, and what this compiler's own
  comptime folder has answered since it could fold a float at all.
  Ruled at s156 (wolf-lang#327), where `%` was the one arithmetic
  operator the checker admitted, the constant folder folded and the
  checked machine evaluated while the native rung refused the program —
  so `[type.trait.op]`'s `impl Rem for f64 { fn rem(self, other: Self)
  -> Self { self % other } }` could not be written, and `Num` at `f64`
  had a hole in it. Witness: `corpus/typecheck/float_rem.lu`, both
  tiers.

## §3c Wrapping division and negation `[type.wrap.div]`

`/` and `%` on a `wrapping[T]` divide the **values** the operands hold,
truncating toward zero as the checked division does: `wrapping[u64]`'s
`(2^64 - 1) / 10` is `1844674407370955161` and its `% 10` is `5`;
`wrapping[i8]`'s `-7 / 2` is `-3` and `-7 % 2` is `-1`. An unsigned
quotient or remainder never leaves its width; a signed one leaves it at
one point only, `MIN / -1`, which **wraps to `MIN`** (and `MIN % -1` is
`0`), the family's two's-complement meaning. A zero divisor is still the
`div-zero` trap (`[mem.ub]`'s table): wrapping names what happens past
the width, and a zero divisor has no quotient at any width. Negation
wraps the same way: `-x` on a `wrapping[T]` is `0 - x` at the width, so
`-MIN` is `MIN` and `-(5 as wrapping[u8])` is `251`. On a plain unsigned
type `-x` is `0 - x` in that type, X3's checked subtraction: `0` for
`x == 0` and the `overflow` trap for every other `x`. **The cost,
stated:** an unsigned wrapping `/` or `%` is the unsigned divide; a
signed one adds a compare and a branch around the divide when the
divisor is not a constant (a constant divisor other than `-1` is the
plain divide, and `-1` is the negation). (Written 2026-10-09 by s220
for wolf-lang#538, where native and release refused every wrapping
`/` and `%` ("no idiv.wrap op"), the checked machine divided a
`wrapping[u64]` as signed (`u64::MAX / 10` was `0`) and a negative
`wrapping[i8]` as its mask, and lupin computed the answers above. The
clause writes down lupin's answer; it is not a new meaning. Negation
was found by the same lane: `-MIN` trapped at a wrapping type on
native and release, and `-x` on a `u8` printed `251` there and `-5` on
the checked machine where lupin trapped.) Witnesses:
`typecheck/int_truth_wrap_div_unsigned.lu`,
`typecheck/int_truth_wrap_div_signed.lu`,
`typecheck/int_truth_wrap_neg.lu`, `faults/int_truth_wrap_div_zero.lu`,
`faults/int_truth_neg_u8_trap.lu`, `faults/int_truth_neg_u64_trap.lu`.

## §4 The `char` type `[type.char]`

- `[type.char]` **`char` is a Unicode scalar value** (D58, s121): its
  domain is `0..=0x10FFFF` **excluding** the surrogate gap
  `0xD800..=0xDFFF` — exactly the set of values UTF-8 can encode. Not a
  byte (`'é'` is one `char`, two bytes — the byte tier stays
  `bytes()`), not a grapheme (an accented letter typed as base +
  combining accent is two `char`s even when it renders as one glyph),
  not a UTF-16 code unit (no wolf value holds a surrogate, ever — the
  same D24 invariant that makes every `str` valid UTF-8). **Layout: 4
  bytes, alignment 4** — an `i32`-shaped scalar at every tier
  (`List[char]` strides by 4; the value crosses the runtime's C seam
  widened to `i64` like every sub-word scalar). The representation
  invariant — every `char` value IS a scalar — means the i32's sign
  bit is never set, so signed machine compares are scalar-value order.
  `char` is **not** an integer type: no arithmetic, no numeric-literal
  adoption (`let c: char = 65` is a type error; write `65 as char`),
  no indexing with one. The only numeric bridges are the two casts of
  `[type.char.cast]`.

- `[type.char.lit]` A `char` literal is one scalar between single
  quotes — `'a'`, `'é'`, `'🐺'` — with the string escape set plus
  `\'`: `\n \t \r \\ \' \" \0 \xNN \u{1–6 hex}` (grammar:
  `[gram.lex.char]`). A `\x`/`\u` escape naming a non-scalar (the
  surrogate gap, or above `0x10FFFF`) is refused at the literal
  (E0110): the value a `char` cannot hold is the value its literal
  cannot spell — the same domain the trapping cast enforces at run
  time. Distinct spellings of one scalar are one value: `'\n'` equals
  `'\u{A}'`.

- `[type.char.order]` **`char` orders by scalar value.** Equality and
  the comparisons (`== != < <= > >=`) are total and locale-free —
  scalar order, not collation and not glyph order (`'z' < 'é'` because
  `0x7A < 0xE9`). The same temperament as `[mem.str.order]`'s byte
  order: cheap, deterministic, honest about not being a collator.

- `[type.char.cast]` **`char as int` is total; `int as char` traps on
  a non-scalar.** Every scalar fits an `int`, so the outbound cast has
  no failure case (`'a' as int` is `97`). The inbound cast is D56's
  trapping family (`trap(overflow)`, `[conf.trap.set]`): a value that
  is **negative**, **above `0x10FFFF`**, or **inside the surrogate gap
  `0xD800..=0xDFFF`** names no character, and admitting it would mint
  a `char` that cannot be UTF-8-encoded — un-writable into any `str`
  without breaking D24. The gap edges are legal: `0xD7FF as char` and
  `0xE000 as char` both convert. Other widths cast through `int`; a
  checkable conversion (a `from_int -> char ! {domain}` shape) is
  std's to name over this primitive, never a second cast semantics.

- `[type.char.interp]` **`{c}` prints the character**, never the
  code-point number: the hole renders as the scalar's UTF-8 encoding,
  and a format spec on a char hole takes the `str` spec surface
  (fill/align/width — width in bytes, D25); numeric specs (`{c:x}`)
  are the E0413 mismatch they look like. The number is spelled, not
  ambient: `{c as int}`.

## §4b The `byte` type `[type.byte]`

- `[type.byte]` **`byte` is an 8-bit unsigned scalar** (D72, s135): its
  domain is `0..=255`, exactly the values one octet holds — what comes
  off a socket, a file, or a `str`'s UTF-8 encoding, one value per
  byte. **Layout: 1 byte, alignment 1** — an `i8`-shaped storage cell
  at every tier (`List[byte]` **strides by 1**, so a byte buffer
  charges one ledger byte per payload byte under
  `[mem.region.account.1]` — the property wolf-lang#203 measured the
  absence of; a `byte` struct field is one byte at its layout offset;
  the value crosses the runtime's C seam zero-extended to `i64` like
  every sub-word scalar). Every `byte` value IS an octet, so loads
  zero-extend and machine compares are unsigned compares. `byte` is
  **not an integer type** — the posture is `char`'s (`[type.char]`),
  so there is one rule for width-bearing scalars rather than two: no
  numeric-literal adoption (`let b: byte = 65` is the type mismatch
  E0401, whose note names the fix; write `65 as byte` — in every
  position, a `match` arm included: a `byte` scrutinee binds or
  wildcards, and a literal arm is spelled over `b as int`), no closed
  arithmetic (a `byte` never holds the result of `+`,
  `[type.byte.op]`), no indexing with one, and no literal suffix
  (there is no suffix inventory; `65 as byte` is the spelling, and
  the name is `byte`, not `u8` — an alias arrives only if an inventory
  ever does). `byte` is a builtin type NAME resolved in type position
  like `int` and `char`, not a keyword: `[gram.inv.kw]`'s closed set
  stays at 50.

- `[type.byte.cast]` **`byte as int` widens; `int as byte` truncates.**
  The outbound cast is total — every octet fits an `int`
  (`200 as byte as int` is `200`) — and is a zero-extension, never a
  sign-extension, because the domain has no negatives. The inbound
  cast is the **only** narrowing `as` in the language that never
  traps: it keeps the value's low eight bits and discards the rest, so
  `255 as byte` is `255`, `256 as byte` is `0`, `300 as byte` is `44`,
  and `-1 as byte` is `255` — the low-bits meaning `wrapping[u8]`'s
  narrowing already has, ruled for `byte` because a byte type exists
  to hold the low octet of whatever arithmetic produced it (a mask, a
  shift, a checksum step), and a trap there would make every such site
  an `as wrapping[u8] as …` dance. The boundary values `0`, `255`,
  `256`, `-1` are the witness. This is a ruled answer for ONE target,
  not the general narrowing cast's range-check question (s27's, still
  open for `i32`/`u16`/…). Other widths cast through `int`
  (`x as int as byte`); `byte` and `char` bridge through `int` too
  (`b as int as char`); there is no `byte as f64`. W0401 (a literal
  outside the target's range) does not fire on `as byte`: truncation
  is the clause, not an accident.

- `[type.byte.op]` **Every arithmetic and bitwise operator widens a
  `byte` operand to `int` first, and the result is `int`.** `b + 1`,
  `b * 2`, `b & 0x0F`, `b >> 4`, `b1 + b2` and `-b` are `int`-typed:
  the operands are read through `[type.byte.cast]`'s widening and the
  operation is `int`'s — X3 checked arithmetic, so `b1 + b2` cannot
  overflow and `b - 1` on a zero byte is `-1`, an `int`, neither a
  trap nor a wrap. Narrowing the result back is spelled:
  `(b + 1) as byte`. A `{integer}` literal beside a byte operand
  adopts `int`; a mixed term `b + n` with `n: int` is legal and `int`.
  The consequence is that `byte` has no compound assignment — `b += 1`
  is the E0401 an `int` assigned to a `byte` is, because `b + 1` is an
  `int`. **Comparisons are total and closed**: `== != < <= > >=`
  between two `byte`s compare octet values (unsigned order — `200 as
  byte > 100 as byte`); `<=>` yields `int`; `byte` against `int` is
  the ordinary type mismatch — widen the byte.

- `[type.int.not]` **`!` on an integer is its bitwise complement.**
  *(s213 for wolf-lang#575; ruled A by the maintainer 2026-10-07,
  ruling #51: `!` on integers, over B a `~` operator and C a named
  function.)* `!x` on every integer type (`int`, `uint`,
  `i8`…`i64`, `u8`…`u64`, `wrapping[T]`) flips every bit of `x` at its
  own width and has `x`'s type: `-x - 1` for a signed width, `max - x`
  for an unsigned one (`!(0 as u32)` is `4294967295`). It is total —
  never a trap, never a wrap to observe — and a literal operand adopts
  the type its context expects first, as with `-`: `x & !0xfff` with
  `x: u64` masks with `0xffff_ffff_ffff_f000`, and `const MASK: u32 =
  !0xfff` folds at comptime. A `byte` operand widens to `int` first, as
  every bitwise operator's does (`[type.byte.op]`): `!b` is `int`, and
  `(!b) as byte` is the octet's complement. `!` on `bool` is logical
  not, unchanged; on a float, a `char` or any other type it is E0409.
  Every machine answers it at every width; the checked machine refused
  a `u64`/`uint` complement by name until s220 (wolf-lang#551), when it
  learned to hold the type's upper half. Witnesses: `typecheck/int_not_mask.lu`,
  `typecheck/int_not_signed.lu`, `typecheck/int_not_byte.lu`,
  `typecheck/int_not_float.lu` (`fail(E0409)`).

- `[type.byte.interp]` **`{b}` prints the number** — the decimal octet
  value, `0` through `255`, never a character: a byte is a quantity,
  and the character it might encode is `str`'s business
  (`[mem.str.chars]`). A format spec on a byte hole takes the integer
  spec surface (`{b:x}` is `ff` at most), the same surface `int` has,
  because the hole widens the byte to `int` before formatting.

## §4c Interpolation of every value `[type.interp]`

(Appended 2026-09-09, s143 — wolf-lang#268. `{x}` was ruled per
primitive — `[type.char.interp]`, `[type.byte.interp]`, the s38 float
rendering — and for nothing else: the reference interpreter rendered
every value it holds, the compiler refused every hole that was not a
primitive, and the book's largest one-machine family (10 samples at
wolf 0.2.8) was exactly that gap. These clauses adopt the
interpreter's rendering, byte for byte, as the language's — it was
the only rendering anyone had written down, in code — and name the
values that have none.)

- `[type.interp.value]` A hole renders its value by the value's type,
  recursively, and **the same bytes whether the hole is printed or
  built into a `str`** (`"{x}"` in value position materializes exactly
  what `print("{x}")` writes). A `str` inside a composite renders as
  its bytes, unquoted — `Doc { title: regions, words: 900 }`, not
  `"regions"`; interpolation is for reading, not for round-tripping.
  **An integer hole renders the value its type holds**, in decimal
  with a `-` only on a negative value: a `u64`, `uint` or
  `wrapping[u64]` at `2^64 - 1` prints `18446744073709551615` (never
  `-1`), and a signed `wrapping[i8]` holding `-56` prints `-56` (never
  its bit pattern `200`). The radix kinds of `[type.interp.spec]` render
  the same value (`{x:x}` of that `u64` is `ffffffffffffffff`). This is
  the `Display` of the value, not a new rendering: the reference
  interpreter has always printed it, and until s220 (wolf-lang#551,
  #538, #553) native and release printed a 64-bit unsigned value above
  `i64::MAX` as its signed bits in a spec-less hole, and the checked
  machine printed a negative signed narrow `wrapping` value as its
  unsigned mask. Witnesses: `typecheck/int_truth_*.lu` and
  `crates/wolf_driver/tests/int_truth_lanes.rs`, which also prints
  seeded random values of all eighteen integer types on four machines.
  A format spec (`{x:>8}`) is defined on the primitive holes
  (`[type.char.interp]`'s `str` surface, the integer surface, the
  float surface) and on nothing composite: a spec on a composite is a
  refusal, never silently ignored (wolf-lang#10's rule).
- `[type.interp.spec]` **The format spec, one clause** (wolf-lang#28's
  §7.4, which was never written under that number; the grammar's
  `FORMAT_SPEC` production cites this clause). A hole may carry a spec
  after its first top-level `:` (`[gram.amb.fmtcolon]`):
  `[[fill] align] ['+'] ['0'] [width] ['.' precision] [type]`, where
  `fill` is any single BYTE, `align` is `<` `^` `>`, `width` and
  `precision` are decimal digits capped at 65535, and `type` is one of
  `b o x X e E f`. Every spec is comptime-known — the grammar admits no
  computed spec — so a spec the grammar cannot read is **E0412** at the
  spec and a field applied to a type it cannot describe is **E0413**,
  never a silently ignored field and never a run-time failure.
  **Meaning.** `width` is a minimum in bytes (D25) and never truncates;
  `fill` defaults to a space; alignment defaults to LEFT for `str`,
  `char` and `bool` and RIGHT for numbers; `^` puts the odd fill byte on
  the right. `0` zero-pads a number AFTER its sign — `{n:08}` of 42 is
  `00000042`, `{n:06}` of -42 is `-00042`, `{n:+08}` is `+0000042` —
  and combining `0` with an explicit fill or alignment is E0412, the
  spec must pick one. `+` marks a non-negative number (zero takes it)
  and never hides a negative float's sign (`-0.0` stays `-0`); it is
  E0413 off a number. `precision` is digits after the point on an
  `f64` (fixed-point when no `type` is given) and a maximum length in
  bytes on a `str` that never splits a code point (`{"é":.1}` is
  empty); on an integer or a `bool` it is E0413. `b` `o` `x` `X` render
  an integer sign-magnitude with no prefix (`-255` in `x` is `-ff`), and
  are E0413 on a float, a `str` or a `bool`; `e` `E` render a float in
  `%e` style with a signed exponent of at least two digits, `f`
  fixed-point, each with precision 6 when none is given. With no
  `type` and no precision an `f64` renders as the shortest decimal that
  reads back as the same bits. A `char` takes the `str` surface and a
  `byte` the integer surface (`[type.char.interp]`,
  `[type.byte.interp]`). A spec on a composite hole is refused
  (`[type.interp.value]`) and on a `!T` hole is E0413
  (`[type.interp.union]`). **`Show` is superseded:** #28's proposed
  user-type trait, `fmt(self, spec: str) -> str`, is not the
  language's; a user type's bare hole renders by `[type.interp.agg]`,
  and a spec on it is the composite refusal. **The cost, stated:** zero
  parsing at run time on every tier — sema parses and validates each
  spec once, the checked machine renders from the parsed form, and the
  native tiers pass the packed spec to the runtime's formatter as an
  immediate; the rendering itself is one pass over the value's digits
  plus the padding bytes. Measured on linux at wolf 0.2.14 on
  `--checked` and `--native` and lupin 0.1.36, eighteen specs render
  byte-identically on all three and the E0412/E0413 refusals agree in
  code and span. Witnesses: `strings/format_spec_full.lu`,
  `strings/format_spec_width.lu`, `strings/float_format.lu`,
  `strings/format_spec_malformed.lu` (`fail(E0412)`),
  `strings/format_spec_mismatch.lu` (`fail(E0413)`). (Written
  2026-09-15, s163 — wolf-lang#28. The semantics are s38's, executable
  since in `wolf_sema::fmtspec` and member-by-member wolf-std sc05's
  reference functions; the clause writes down what both machines have
  converged on, and #28's item 3 — `{n:08}` absorbed into the width —
  is fixed on both.)
- `[type.interp.agg]` **`()` renders `()`**; a tuple `(a, b)` — the
  elements in order, `, `-separated, in parentheses; a struct
  `Name { f: v, g: w }` — the type's name, a space, `{`, then each
  field as ` f: v` with `,` between, then ` }` (a zero-field struct is
  `Name { }`); a `List` `[a, b]` — the elements in order,
  `, `-separated, `[]` when empty. An enum value renders its variant
  **qualified**, `Enum.Variant`, with the payload as `(p1, p2)` when
  the variant carries one — the spelling the program constructs it
  by. Weighed and rejected: the bare variant name — `Rgb(1, 2, 3)`
  reads as a row tag, and rows and variants are different things
  (D30 rows are structural; a variant belongs to its enum).
- `[type.interp.row]` A caught row value (`else |err|`, a `match`
  binding) renders as **the tag's name**, then `(p1, p2)` when the
  tag carries a payload, each payload rendered by its own rule:
  `too_short`, `BadDigit(q, 1)`, `closed`. The name is the tag as the
  program spells it, module-qualified by nothing — tags are
  structural (D30), so there is nothing to qualify by.
- `[type.interp.union]` A `!T` value renders as **its ok payload when
  it holds one, and as its row (`[type.interp.row]`) when it does
  not** — the value's two halves are two values, and the hole prints
  whichever is there. `{popped}` after `let popped = xs.pop()` reads
  `3` or `none`. This is a reading rule, not a handling rule: `?` and
  `else` still decide what the program does with the row. **A format
  spec does not apply to a `!T` hole**: `{m[k]:>5}` is **E0413** at the
  spec (s156, wolf-lang#323), because the value is two values and a
  spec describes one — fill and width would be padding a number on one
  path and a tag's name on the other, and the type-directed fields
  (`x`, `.3`, `+`) have no payload to be checked against until the row
  is handled. `[type.row.operand]`'s posture, applied to specs: handle
  the row, then format what is left (`{m[k] else 0:>5}`, `{x?:>5}`, a
  `match`). Both machines refused this shape already — the checked
  tier at its `fmt_hole`, the WIR emitter at its `emit_value` — while
  sema let it through, so what is a typing question arrived as
  `unsupported — a format spec on a non-primitive value` at run time on
  both tiers, reading as a missing feature. The bare hole is
  unaffected; it is this clause's own rule. Witness:
  `corpus/grammar/interp_fmtcolon.lu`.
- `[type.interp.reason]` An exit reason (`[conc.proc.exit]`) renders
  as its class name with its payload in parentheses: **`normal(v)`**
  with the proc's `int` result (the value the body returned — a body
  whose result is not an `int` reports `normal(0)`), **`error(Tag)`**
  with the row that crossed the boundary rendered per
  `[type.interp.row]`, **`killed`**, **`cancelled`**, and
  **`fault(kind)`** with the trap kind from `[conf.trap.set]`'s
  vocabulary (`fault(bounds)`).
- `[type.interp.none]` Some values have **no rendering the language
  promises**: a channel, a proc, a task scope, a region value, a raw
  pointer, a fn value, a `dyn` object, a shared-tier handle. An
  implementation may print its own bookkeeping for them (the
  interpreter prints `channel#3`, `region#1@2`) or refuse the hole by
  name (the compiler does); a program must not depend on either, and
  a conformance witness may not interpolate one. Weighed and
  rejected: ruling the interpreter's bookkeeping as the rendering —
  it names ids the compiled program does not have.

## §5 `str` concatenation `[type.str]`

- `[type.str.concat]` **`+` and `+=` on two `str`s are
  interpolation-append** (D62, ruled from live dogfooding — the
  interpreter's behavior is the language): `s + u` is legal exactly
  when BOTH operands are `str`, and means precisely `"{s}{u}"` — a
  new `str` whose bytes are the operands' bytes in order (UTF-8
  concatenation is closed; no boundary can be violated). `+` on a
  `str` and a `char`, either order, is the same operation: `s + c`
  is `"{s}{c}"` and `c + s` is `"{c}{s}"` — the `char` contributes
  its scalar's UTF-8 bytes (a `char` is text, D58, with exactly one
  rendering; wolf-lang#278). `+` chains left-associatively; `s += u`
  and `s += c` are `s = s + u` and `s = s + c`, in every place shape
  an assignment admits. This is a builtin operator on the builtin
  type, like `==` on `str` — NOT a trait bridge (no `Add` trait
  opens; D49's bridge shape is untouched).

- `[type.str.concat.mix]` **Mixed operands stay E0409** — `str + int`,
  `int + str`, and their `+=` forms. The `int` rows stay because `+`
  is not a formatter: an integer has more than one rendering (sign,
  radix, width — `{n}`, `{n:x}`, `{n:>4}`) and a bare `+` would pick
  one silently. A `char` is not a mix (`[type.str.concat]`): it is
  text with one rendering. The `int` conversion is spelled where it
  always was: inside an interpolation hole (`t += "{count}"`).
  Interpolation remains the general surface and is unchanged; `+` is
  its `str`-and-text special case, not a replacement.

- `[type.str.concat.cost]` **The cost model is interpolation's**: a
  fresh `str` per application — the compiler lowers `+` onto the same
  strbuf path an interpolated string materializes through, so `+=` in
  a loop is quadratic, never an amortized push. `std.strbuf` is the
  builder. The diagnostics say so beside the refusal note. The fresh
  `str` is an allocation site in the ambient region for the escape
  rule — `[mem.region.escape]` (s153, wolf-lang#310).

## §6 Closures `[type.closure]`

(Appended 2026-09-09, s145 — wolf-lang#268's `return` inside a closure
family: seven of the book's samples, chapter 16's receivers among
them, spell `let r = ch.recv() else |_| { return }` inside a spawned
closure. Every machine that ran them agreed on what the `return`
means; only the compiler's typing withheld it.)

- `[type.closure.return]` **`return` inside a closure returns from the
  closure.** Its operand types against the closure's own result — the
  result the context fixes for a closure checked against a fn type,
  the one inferred from the body's tail otherwise (a `return` and the
  tail meet at one type), the declared return type on a nested `fn` —
  and a bare `return` is the unit result. The enclosing function is
  out of reach: no `return` in a closure body leaves the function the
  closure was written in, on any tier, and the closure's own `defer`s
  run on the way out exactly as a function's do. `?` follows the same
  frame (its row is the closure's, s73). This is the meaning every
  reader assumed and every machine already ran; it is written down so
  the typing can admit it.

## §7 The unit context `[type.unit]`

(Appended 2026-09-10, s146 — wolf-lang#275: `chan.send` was typed `()`
on the compiler while `[conc.chan.close]` says a send after close
returns an error value. Typing it `() ! {closed, cancelled}` turned
every `for i in … { ch.send(i) }` and every else-less
`if ready { ch.send(1) }` into a type mismatch — s144 counted 13
corpus witnesses, 26 sites, and chapter 12 on every page — because no
clause said what a fallible unit-typed value *means* where `()` is
expected. This section is that clause; `send`'s row follows it in
`[conc.chan.close]`.)

- `[type.unit.context]` **A unit context is a position whose expected
  type is `()`.** The closed list: the body of a `for`, `while`, or
  `loop`; the then-block of an `if` with no `else`, and every block of
  an `if … else if …` chain that ends without one; the body of a
  function or method whose result is `()`, declared or omitted, and
  the operand of a `return` in one; the body of a closure checked
  against a `fn(…) -> ()` type; and any block, `match` arm, or `else`
  branch checked against one of those. The tail of a block in a unit
  context is consumed by no one: the block's value is `()` whatever the
  tail's type.

- `[type.unit.discard]` **A `!T` tail in a unit context is a discard,
  warned (W0601), never a mismatch.** The value's row is lost — and,
  when `T` is not `()`, the value with it — and the compiler says so at
  the tail with the diagnostic a non-trailing `!T` statement has drawn
  since s67. s146 admitted `!()` only, on the reading that a `!int`
  tail where `()` is expected is a mismatch on the `int` exactly as a
  plain `int` tail is; s154 retired that half (wolf-lang#326). It was
  the same rule about position the clause had just refused, one level
  in: `(mut xs).pop()` as a STATEMENT in a unit body is W0601, and the
  identical line at the body's tail was E0401 "must return `()`" —
  a return-type diagnosis of a discard, whose fix-it sent the reader
  to manufacture a value nobody uses. The plain `int` tail keeps
  E0401; what moves is the row, which is the thing being discarded.
  W0601 names `let _ = …` at a value-carrying tail — the spelling that
  makes the discard visible — beside `?` and `else`. The two readings,
  costed before choosing:

  | | (i) handled — a `!()` tail is a mismatch | (ii) discarded — W0601 |
  |---|---|---|
  | what the reader learns | a `!()` statement is warned and the same statement one line lower, at the block's tail, is refused: *position* decides | one rule — a `!T` nobody consumes is a warned discard, wherever it sits |
  | the shortest fire-and-forget send | `ch.send(v) else {}` — the same silent discard, spelled longer and warned nowhere | `ch.send(v)`, with the warning naming what it drops |
  | a `closed` send the program never looks at | refused at a tail; compiles, warned, one line earlier | compiles, warned, at every site; refused under `--deny-warnings` |
  | programs written before the clause | every statement-tail send is an error: the 13 witnesses, chapter 12 | none changes meaning (`[diag.sev.warn]`); a warning-clean corpus or book spells the handling or declares the warning |
  | `send`'s type fix (#275) | breaking | non-breaking |

  (ii) is the rule. Its cost is real — the row *can* be lost — and it
  is the cost W0601 already carries for every other fallible call in
  the language; (i)'s price is a rule about position, which the
  language has no other instance of and just retired one of (#276).
  The warning cites its hazard by name (`[diag.sev.warn]`): the send
  after close that `[conc.chan.close]` was written so a sender could
  see, unseen. The three spellings that see it are the ones the
  warning already names — propagate with `?`, handle with `else`, or
  bind it away — and the corpus witnesses spell the first.

  (Measured 2026-10-03 by s207 for wolf-lang#541. **Lost means lost on
  every machine.** W0601 fired on all three lanes, and native and
  release then discarded (lupin too, but for an else-less `if`'s
  raising value, which it binds — wolf-interp#179), while the checked
  machine handed the row on:
  a unit function's raising tail left `main` with `error: bad`, a
  raising statement in `main` stopped it, and `let v = if c {
  maybe(n) }` bound the value (`3`) or the row (`none`) where the
  block's value is `()`. The checked machine now discards at every
  tail the checker records as a unit-context discard and at every
  non-trailing `!T` statement, and a `?` inside either still
  propagates, because that row was consumed. "The operand of a
  `return`" in a unit function is on the closed list too:
  `return boom()` there stopped native and release with an internal
  error and propagated on checked; it is the same discard now.
  Witnesses `corpus/rows/unit_discard_*.lu`.)
  (Ruled 2026-10-03, ruling #34 = A, by s208 for wolf-lang#541 part 2.
  **The list has no exception.** An else-less `if` — or a chain that
  ends without an `else` — that is itself the tail of a fallible
  function (`fn g(c: bool) -> () ! {bad} { if c { boom() } }`) is the
  same unit context it is one line higher: its then-block's raise is
  discarded, warned (W0601), and the `if`'s value `()` is what `g`'s
  `!()` takes as its ok value. So is the same `if` ending a closure
  checked against `fn(…) -> () ! {…}`. Until s208 all four machines
  handed that raise to the caller with no W0601 — except an else-if
  chain, which native and release already discarded while the checked
  machine and lupin raised — and it was the one place a raise left a
  function with no `?` and no `return` to mark it. A `?`, a `return`
  or an `else` in the then-block is not a discard and is untouched:
  wolf-std's `move_file` (`std/fs/fs.lu`), the one such tail across
  1,868 fallible functions downstream and in the corpus, ends in a `?`
  and answers as before. A value-carrying row there (`if c { maybe(9)
  }` ending a `-> () ! {none}` function) is the discard with its value,
  where the compiler had refused the `int` (E0401). A bare tag as that
  then-block's tail (`if c { bad }`) is the construct it is in the
  statement form — declined by name on the compiler (`unsupported`, "an
  error-row tag outside `!T` context") and discarded by lupin; `return
  bad` is the spelling that raises. Witnesses `corpus/rows/unit_discard_tail_if*.lu`; lupin's
  half is wolf-interp#179.)

- `[type.unit.consume]` **A closure body with no fixed result is not a
  unit context.** `s.spawn(fn() { ch.send(v) })` infers `fn() -> !()`
  from its tail as `[type.closure.return]` says, and the scope consumes
  the value: a task completing with an error value re-raises at the
  scope exit (`[conc.task.fail]`). That is the row reaching the one
  reader who can act on it, not a discard, and it draws no warning.
  Inside such a closure a loop body is a unit context as everywhere
  else: `s.spawn(fn() { for i in 1..=n { ch.send(i) } })` warns at the
  send, and `ch.send(i)?` is the spelling that hands the loop's
  failure to the scope.

## §8 Functions `[type.fn]`

(Appended 2026-09-10, s148 — wolf-lang#284. Both machines check a
body's tail against the declared return type and refuse a `()` tail
under `-> str` or `-> !int`, and no clause said so directly: the rule
was read out of `[gram.expr.block]` — a block's value is its trailing
expression — together with `[gram.expr.tagident]`, a clause about tag
resolution that names "a fallible function's tail" only inside its
list of checked positions. wolf-interp#73 found the interpreter
reading neither: it ran the body and exited with a status the program
never wrote, and wollf wl10 measured the gap at 56 of 2,153 generated
programs. The rule is written here so a witness can cite a clause that
is about it.)

- `[type.fn.ret]` **A body is checked against its declared result.**
  The body block's value (`[gram.expr.block]`: its trailing expression,
  `()` when the block ends in a statement) is checked against the
  function's declared return type, and so is the operand of every
  `return`. For a fallible function — `-> T ! row` or `-> !T` — the
  tail is checked against the ok half `T`: a bare tag resolves to the
  declared row first (`[gram.expr.tagident]`), a nested row flattens
  into it (`[gram.type.row.flatten]`), and a plain `T` coerces to the
  union. `()` is not `T`: a body under `-> str` or `-> !int` that ends
  in a `while`, a `print`, or any other statement is **E0401 at the
  tail**, naming the declaration as the origin — never a `()` printed
  and never an exit status a runtime invents (wolf-interp#69's shape
  one level up). The omitted return type is `()`, and the one place a
  fallible tail is not a mismatch is the unit context: a `!T` tail
  where `()` is expected is a warned discard, `[type.unit.discard]`.
  Witnesses: `typecheck/tail_declared_str.lu`,
  `typecheck/tail_declared_union.lu`.
- `[type.fn.value]` **A closure is a `fn` value whatever it captures,
  and a capturing closure's value copies its captures when it is
  created.** A named function, a capture-free closure and a capturing
  closure are all values of their fn type — passed as an argument,
  returned, bound and called through the binding — the same
  `fn(int) -> int` to every callee, and nothing marks which stood
  behind it. What a capturing closure holds is a COPY of each captured
  binding's value, taken once, where the closure is written: the value
  never sees a later write to a captured place (W1102 says so at the
  write), and while the value is still needed a write to a captured
  `var` is E1002 — the shared loan of `[mem.tier0.borrow.2]`, which is
  what makes copy and reference indistinguishable to a conforming
  program. A `var` is therefore captured by its value at creation,
  never by its place; a captured region value is refused by name (open
  it in the enclosing frame); a captured value must outlive every
  frame the closure value leaves — returning a closure that captured a
  frame-local list is the list's escape, E1010, as if the list itself
  were returned. Positions: a capturing closure may be bound, passed,
  returned, or be a closure body's tail; inside a container or a
  struct literal it is refused by name until that borrow story is
  written. Cost: one record allocation per capturing closure value, in
  the ambient region (`[abi.native.closure]`), its captures copied in.
  Witnesses: `typecheck/fn_value_capturing.lu` (chapter 4's program,
  verbatim), `typecheck/fn_value_captured_int.lu`,
  `typecheck/fn_value_captured_var_write.lu` (`fail(E1002)`). (Ruled
  2026-09-10, s150 — wolf-lang#300: c25 had ruled the pair stays in
  its frame and c05/#117 deferred closures as values; the chapter that
  teaches functions as values was the one the maintainer met it in.)

- `[type.fn.never]` **A function declared `-> never` never returns.**
  *(s213 for wolf-lang#572; ruled A by the maintainer 2026-10-07,
  ruling #50: `-> never`, over B `-> !` and C `#[noreturn]`.)*
  `never` is a built-in type name (`[type.byte]`'s kind of name, not a
  keyword: `[gram.inv.kw]`'s closed set is unchanged), written only as
  a function's return type — a body, a bodyless `extern "c" fn`
  (`[abi.link.extern]`), a fn type. It is the bottom type the literal
  `assert(false)`, `return`, `break`, `continue` and a `loop` with no
  `break` already have: a **call** to such a function has type `never`
  and therefore fits wherever a value is wanted — an `else` handler's
  arm, a `match` arm, a `let` initializer — without a dead value after
  it. The body of a `-> never` function must itself be bottom: its
  value (`[type.fn.ret]`) is a call to another `never` function,
  `assert(false)`, or a `loop` with no `break`, and it holds no
  `return`; a body that can reach its end, or a `return`, is **E0401**
  at the tail or at the `return`, naming the declaration. A bodyless
  `extern "c" fn f() -> never` is the programmer's claim about the
  foreign function (a `_Noreturn void` in C, `[abi.c.types]`: it
  crosses as `void`); the compiled tiers emit the call and then the
  unreachable trap, so a foreign function that does return stops the
  program there (`trap(assert)`), never runs on with no value. A
  binding named `never` shadows nothing a program can spell, so W0304
  exempts it, as it exempts `range`. Witnesses:
  `typecheck/fn_never_handler_arm.lu`, `typecheck/fn_never_extern.lu`,
  `typecheck/fn_never_reaches_end.lu` (`fail(E0401)`),
  `typecheck/fn_never_return.lu` (`fail(E0401)`).

## §8b Generic parameters `[type.generic]`

(Appended 2026-09-15, s163 — wolf-lang#319, wolf-interp#84, wollf's
sealed heldout wh-001. `[gram.item.fn]` gives `generic_param` its
production and stops there: nothing said how many types one `T` may
stand for in one call, and both machines answered E0401 for a `Rect`
and a `Square` passed as two `T`s on a rule written nowhere.)

- `[type.generic.bind]` **A type parameter binds once per call.** At a
  call of a generic function, each type parameter stands for exactly
  ONE type for the whole call, found by unification across every
  position of the signature that names it — a parameter typed `T`,
  and `T` nested inside a parameter's type (`xs: List[T]`). Argument
  positions are unified left to right: the first argument whose type
  fixes `T` binds it, and a later argument whose type disagrees with
  that binding is **E0401 at that argument** — the primary span is the
  disagreeing argument, never the call and never the argument that
  bound. There is no widening to a common type, no implicit `dyn`, and
  no second instantiation inside one call: `sum_areas[T: Area](a: T,
  b: T)` called with a `Rect` and a `Square` is refused at the
  `Square`, and a program that wants both declares two parameters
  (`[T: Area, U: Area](a: T, b: U)`). The bound is checked against the
  one bound type (E0502). What the diagnostic's secondary label names
  as the origin — the parameter's declaration, or the argument that
  bound — is diagnostic quality and not comparison surface
  (`[proto.cmp.phase]` compares the code and the primary span).
  **The cost, stated:** zero at run time. Binding is a static fact; a
  call compiles to a direct call of the one monomorphic instance its
  binding names, so a second agreeing call reuses that instance and a
  disagreeing call is not a program. Witnesses:
  `typecheck/generic_bind_once.lu` (wh-001, verbatim),
  `typecheck/generic_bind_scalar.lu`.

## §9 The error row as a value `[type.row]`

(Appended 2026-09-10, s148 — wolf-lang#284, wolf-interp#81. A bare
`!T` in operator position was refused by both machines, and the rule
was stated nowhere: it was inferred by inverting `[type.interp.union]`'s
carve-out — an interpolation hole may *read* a `!T` without handling
it, so a hole is the one place that happens, so an operator has no
reading at all. That works, and it is a clause about string holes
carrying a rule about operators. The rule is written here, beside
`[type.str.concat.mix]`, which fixes its code.)

- `[type.row.operand]` **A `!T` is two values, never one, and no
  operator reads it.** `?`, `else` and a `match` are the whole of how
  a row is handled; `[type.interp.union]`'s rendering is a reading,
  not a handling; no cast and no coercion narrows a `!T` to its `T`.
  An operator — arithmetic, comparison, logic, bitwise, shift — applied
  to a `!T` operand is **E0409**, the code `[type.str.concat.mix]`
  spends on "this operator is not defined on these operands", and it
  is E0409 **on either side of the operator**: `n + 1` and `1 + n`,
  `n <= 5` and `5 <= n` are one refusal, because the fact refused is
  the same one — no operator has a `!T` in its family. The fix is to
  handle the row first (`n? + 1`, `(n else 0) + 1`). Weighed and
  rejected: reporting the row as a mismatch (E0401) against the
  operand that fixed the operator's type. That sentence says the row
  *could* have been in the family had it been the other type, which it
  could not; and a code that depends on which side the row sits on is
  a rule about position, of which the language has no other instance
  (`[type.unit.discard]` retired one at #276). **The cost, stated:**
  zero — a static refusal, with no instruction added to any accepted
  program. Status at 0.2.14 (re-measured by s163): both machines
  answer E0409 on either side and for both operator families, at the
  same span on all three witnesses (wolf `--checked` and lupin 0.1.36);
  the s148 split — the compiler's E0401 with the row on the right,
  lupin 0.1.31's E0401 for a comparison — is closed on both sides.
  Witnesses: `rows/negative/row_operand_add.lu`,
  `rows/negative/row_operand_compare.lu`,
  `rows/negative/row_operand_rhs.lu`.
- `[type.row.else]` **An `else` handles its scrutinee's own row, and
  nothing else.** In `e else f` and `e else |p| f`, the handler runs
  when `e` itself yields an error of `e`'s row — a fallible call's
  own failure, an absent `Map` key, a block whose value is a row — and
  only then. A `?` that fires *inside* `e` (in a call argument, an
  index, a nested `else`'s scrutinee, a block within `e`) propagates
  out of the enclosing function, past every `else` it sits under, as
  a `?` does anywhere; so does a `return` of a row from inside `e`.
  `look(m, key()?) else 0` answers 0 when `look` misses and leaves the
  function with `key`'s row when `key` fails. This is the reading the
  types already give: the scrutinee's type is `T ! R` with `R` the
  scrutinee's own row, the `?` strips its operand's row from that type
  and checks it against the function's, and the handler pattern types
  over `R` alone — so a handler that caught an inner `?` would bind a
  tag its own pattern was never typed against. E0809's note ("an
  `else` handler runs for every error its operand can carry") says
  the same thing from the coverage side. (Ruled 2026-09-30, the
  maintainer's #18 = A, s191 — wolf-lang#492. The checked machine's
  `else` caught a propagating `?` from inside its scrutinee and bound
  the fallback; native, release and lupin 0.1.42 propagated. **The
  cost, stated:** zero on native and release, which already lower it
  this way; one flag test on the checked machine. The rest of the
  error vocabulary — `?`'s target in general, `errdefer` — stays in
  the reserved `err` namespace's unwritten document.) Witnesses:
  `rows/else_try_call_arg.lu`, `rows/else_try_index.lu`,
  `rows/else_try_nested_else.lu`, `rows/else_try_handler.lu`,
  `rows/else_try_block.lu`, `rows/else_return_tag.lu`, and the
  control `rows/else_own_failure.lu`.
- `[type.row.defer]` **A `?` inside a `defer` or `errdefer` expression
  is refused.** A deferred expression runs while its function is
  already leaving — the function's result is formed and the
  `defer`/`errdefer` chain of `[mem.model.order]` is running on the
  way out — so an error a `?` would propagate from inside it has
  nowhere honest to go: replacing the result already on its way out
  would lose that result, and dropping the `?`'s error would hide it.
  The shape is **E0611** at compile time on every machine, and the
  refusal reads the whole deferred expression: a `?` in a call
  argument, an interpolation hole, a binding or a block under the
  `defer` is the same refusal. The fix is to handle the row inside the
  deferred expression (`defer close(f) else |e| note(e)`) or to move
  the fallible call out of the `defer` into the body, where its `?` has
  a function to leave. A `?` inside a closure defined under the
  `defer` is that closure's own propagation (`[type.row.else]`'s
  reading of frames) and is not refused by this clause. (Ruled
  2026-10-02, the maintainer's #19 = refused, s196 — wolf-lang#498.
  Before the ruling the machines parted three ways: native and release
  overflowed the compiler's stack lowering the shape, the checked
  machine ran the deferred `?` and dropped its error, lupin 0.1.42 made
  it the function's result. **The cost, stated:** zero — a static
  refusal, with no instruction added to any accepted program; lupin
  0.1.43 ran the shape and was pinned by version as pre-mirror in the
  gate; lupin 0.1.44 refuses it, E0611 at the `?`.) Witnesses:
  `rows/negative/try_in_defer.lu`, `rows/negative/try_in_errdefer.lu`,
  `rows/negative/try_in_defer_block.lu`, and the control
  `rows/defer_else_handles.lu`.
- `[type.row.match]` **A `match` over a fallible value has two
  halves, sorted by name.** The scrutinee has type `T ! {row}`. An arm
  is a **row arm** — a tag of the row by name, binding its payload
  when it has one: `none => …`, `Io(e) => …` — or a **value arm** —
  any pattern over `T`, exactly as a `match` over `T` today: `0 => …`,
  `v => …`, `Line(k) => …`. An identifier (or a path head) that names
  a tag of the scrutinee's row is a row arm; anything else is a value
  pattern; `_` covers whatever is left on both halves. The arms are
  tried in source order, and neither half sees the other: a row value
  can match only a row arm or `_`, a value only a value arm or `_`,
  so a binding `v` after the tags takes the whole of `T` and leaves
  the row to a later `_`, which is then reachable, not dead. The
  match must cover every tag of the row and the whole of `T`;
  **E0801** names the missing tag (`` `eof` ``) or the uncovered
  value half (`` `_` (the value half, `int`) ``), with the engine's
  usual witness for a partly covered `T` (`` `1` ``). The expression's
  type is the arms' type, and the row is consumed as an `else`
  consumes it (`[type.row.operand]`): it handles the scrutinee's own
  row only, so a `?` that fires *inside* the scrutinee leaves the
  function past the arms (`[type.row.else]`). A tag of the row that
  is also a variant of `T` (`Shape ! {Line(int)}` beside `Shape.Line`)
  is **E0816**, refused by name whether or not an arm spells it —
  never guessed; `else |e| match e { … }` keeps the halves apart and
  keeps working beside this form. Shapes the rule does not name — an
  or-pattern mixing a row arm with a value pattern, an `@`-binding at
  the top of an arm — are refused by name. The grammar is unchanged:
  `[gram.pat]` already spells a bare tag as `IDENT` and a tag with a
  payload as `path '(' pattern… ')'`. (Ruled 2026-10-02, the
  maintainer's #21 "yes, as proposed", s197 — wolf-lang#497. Before
  it, every wolfgang lane refused the form as unsupported and lupin
  0.1.42 ran it with no clause to say which was right. **The cost,
  stated:** zero on an accepted program beyond what `else |e| match
  e` already costs — one `is_err` test and one arm chain per half on
  native and release; the checked machine dispatches by the flow it
  already carries.) Witnesses: `rows/match_row_bare_tag.lu`,
  `rows/match_row_payload_tag.lu`, `rows/match_row_wild_each_half.lu`,
  `rows/match_row_nested.lu`, `rows/match_row_try_scrutinee.lu`, the
  control `rows/match_row_else_control.lu`, and the refusals
  `rows/negative/match_row_missing_tag.lu`,
  `rows/negative/match_row_missing_value.lu`,
  `rows/negative/match_row_tag_variant_collision.lu`.

This chapter deliberately does **not** write the full numeric tower
(mixed integer-width arithmetic, a complete `Add`/`Mul` trait hierarchy
beyond what literal adoption needs) nor the general narrowing integer
cast's range-check question (s27's, still open — the wrapping row above
is the value-preservation answer only for leaving the wrapping domain,
and `[type.byte.cast]`'s truncation is the answer for ONE target, the
octet) —
D54 is the literal story, D56 the wrapping escape, and the cast's numeric
directions, no more. `char`'s method surface (classification,
case-mapping, the checkable conversion) is std's tier over the
primitive (D58), not this chapter's; so is `byte`'s (the `bytes`
library over `List[byte]` — D72, wolf-std sc35; the language's own
byte producers and consumers — `str.bytes()`, `str_from_utf8`, the
`fs_*`/`net_*` byte calls — speak `List[byte]` since s136, #231).

## §10 The `Map` `[type.map]`

(Appended 2026-09-11, s152 — wolf-lang#11, #154, ruled by the
maintainer. The count exercise in the book's chapter 5 carried a
parallel `List` for one reason: no program could ask a `Map` whether
a key was bound. std's `has`/`get`/`get_or`/`remove`/`tally` existed
and executed on neither machine — their `[K: Eq]` bound dispatched
nowhere — and an absent-key read answered `()`, the one unchecked,
untyped read in the language. The maintainer's question, verbatim:
"is the sole purpose of the list to check and see if we've seen it
already, because we have no apparent way of checking the existence of
a key since `map[key] = blah` will create it? My gut instinct is I
can pull the count exercise off with a map alone." They were right;
this section and `[mem.map.absent]` are the answer. `Map` stays
prelude-ambient and builtin-typed like `List` (D50: std-DEFINED once
generic data can carry it; this clause rules the KEY PROTOCOL that
filing left open, not the home).)

- `[type.map.key]` **`Map[K, V]` admits `str`, `int`, `char` and
  `bool` keys this edition.** These are the four whose equality the
  language itself defines, so `m[k]` can ask "is this key bound?"
  without any user code deciding what "the same key" means: two `str`
  keys are one key when their bytes are (`[mem.str.order]`'s `==`),
  two `int`/`char`/`bool` keys when their values are. Every other
  type is **E0418 where the key is spelled** — in `Map[K, V]()` and
  in a signature position (`fn f(m: Map[Point, int])`) alike, with
  the same words. A **struct key waits on derived equality**, by
  name: `[K: Eq]` on a user type is the ruling this clause does not
  make, and until it is made a struct is keyed by one of the four
  (an `id: int`, a `name: str`, a `str` built from its fields). A
  float has no key equality at all (`nan != nan` would make a key
  that can never be found again); a container has none the language
  will spell. Inside a generic body `Map[K, V]` with a rigid `K`
  elaborates unchecked — the golden rule — and each instantiation is
  checked where it spells its key. **`[K: Eq]` is satisfied by the
  four**: std.cmp's `impl Eq for int`, `bool` and `str` are ordinary
  impls of an ordinary trait (`char`'s is wolf-std sc44's, filed with
  this clause), the bound dispatches through them, and so std.map's
  five key functions — `has`, `get`, `get_or`, `remove`, `tally` —
  execute on a `Map` keyed by any of the four, on both tiers
  (`corpus/memory/map_std_keys.lu` is their bodies word for word over
  a local `Eq`). **The surface** the language types, beside the index
  of `[mem.map.absent]`: `Map[K, V]()` constructs; `m.len` counts
  entries (`count()` is the same number); `m.is_empty()` probes;
  `m.clear()` drains (a `mut` receiver); `m.remove(k)` erases a key
  through a `mut` receiver and answers `V ! {none}` — the erased value,
  or the `none` row with the map unchanged, the read's shape
  (`[mem.map.absent]`) — and the remaining entries keep their order
  (ruled by D50 on #11, landed 2026-09-15 as wolf-lang#344; **cost**:
  one scan to the key and a shift of the entries after it, nothing
  freed, on both tiers — `corpus/memory/map_remove.lu`); `m.pairs()` answers a fresh
  `List[(K, V)]` of every entry, which `for (k, v) in m.pairs()`
  destructures. **Iteration order is unspecified and consistent**:
  `pairs()` reports one order for an unmodified map and promises
  nothing else — both machines answer insertion order at this pin,
  and a program that depends on it depends on an implementation.
  Iterating the map value itself (`for x in m`) is not ruled and
  refuses by name. Witnesses: `corpus/memory/map_count.lu` (the count
  exercise on a map alone), `map_std_keys.lu`, `map_int_keys.lu`,
  `map_char_bool_keys.lu` (both tiers); `corpus/typecheck/map_struct_key.lu`
  (E0418). Cost stated: the interpreter's key set and its `Map` read
  (wolf-interp, filed with the clause); std.map's header and F-0011's
  filed question (wolf-std sc44); the book's §5.2 and its tally
  samples (wolf-book bs40).

## §11 Operators through traits `[type.trait.op]`

(Appended 2026-09-11, s155 — wolf-lang#5, the bridge, ruled by the
maintainer on reading chapter 5's `total[T]`. The compiler answered
`xs[0] + 1` under a bare `T` with "no trait covers this operator yet
(operator traits are a later sprint)", and the maintainer, hitting it
as a learner, asked whether the sprint should be bumped up "now that
we've encountered it in the wild — we want to attract people to the
language with friendliness". This section is that sprint. Positions
surveyed: Rust (operator traits with an output type — the checking,
minus the wordiness), Go (type sets — the ergonomics, without a second
kind of bound), Java (no path at all — the cautionary case). D49's
riders stand: nothing is synthesized, and the primitive impls are the
substrate.)

- `[type.trait.op]` **An operator dispatches through a trait when its
  left operand is a type parameter or a user type.** The table:

  | operator | trait member | shape |
  |---|---|---|
  | `a + b` `a - b` `a * b` `a / b` `a % b` | `Add.add` `Sub.sub` `Mul.mul` `Div.div` `Rem.rem` | `fn add(self, other: Self) -> Self` |
  | `-a` | `Neg.neg` | `fn neg(self) -> Self` |
  | `a == b`, `a != b` | `Eq.eq` (`!=` is its negation) | `fn eq(self, other: Self) -> bool` |
  | `a < b` `a <= b` `a > b` `a >= b` | `Ord.cmp` read against `Less`/`Greater` | `fn cmp(self, other: Self) -> Ordering` |
  | `a <=> b` | `Ord.cmp` — the `Ordering` itself | |

  `a + b` IS `Add.add(a, b)`: the same checking, the same dispatch
  record, the same lowering as the qualified call, with the operands
  as `read` arguments (a place is lent for the call, never moved, so
  `a` serves two operators without a `copy`). **When it applies**: the
  left operand's type is a type parameter (`T`) or a user nominal
  type (a struct, an enum, a `distinct`); **never two primitives** —
  `int + int`, `str == str`, `f64 < f64`, `str + char` stay the
  builtin operations they were (`[type.numlit]`, `[mem.str.order]`,
  `[type.str.concat]`), whatever impls are in scope. **Which trait**:
  on a type parameter, the bound must name a trait called `Add` (etc.)
  — a bare `T` is **E0501** at the definition with the note "add `T:
  Add` to the bound" and a machine edit that inserts it; on a user
  type, the trait called `Add` **reachable** at the operator — the name
  in scope if one is bound, else the `Add` declared by the operand
  type's own module (coherence already implies it: `Ordering`'s
  operators are `std.cmp`'s), else the `Add` declared by a module this
  file imports, which is what "bring `Add` into scope" means to a
  reader who wrote `use std.ops` (s156, wolf-lang#336 — the lookup was
  bare-name only, and since `use std.cmp` binds `cmp` and nothing else,
  importing a library's type was the very thing that made its operators
  undispatchable: every user type any library publishes had operators
  that worked inside its own module and nowhere else). Two imported
  modules declaring one operator trait is no answer and keeps the
  E0301. An import binding an operator trait by name (`use cmp.Eq`) is
  **used**, for the unused-import rule (E0305), by any operator of that
  trait the file spells: unused imports are reported before the checker
  chooses any operator's trait, so the spelling is what counts (`-`
  counts for both `Sub` and `Neg`), and a file that spells none still
  hears E0305 (wolf-lang#352, `traits/op_eq_item_import/`). Nothing by that name reachable is **E0301** naming the trait
  and the three places looked in, and a type without an impl is
  **E0502** naming the trait and the operator, discharged with the
  body's other obligations. `!`, `&&`, `||` and the bitwise
  family have no trait this edition: on a type parameter they stay
  E0501 saying so. **Homogeneous this edition**: the method's
  receiver and other operand are `Self` and the result is `Self`
  (`bool` for `eq`, a nominal `Ordering` for `cmp`) — no output type
  parameter; a trait of the table's name whose method has another
  shape is **E0514** at the operator ("`Add.add` is not `fn add(self,
  other: Self) -> Self`"), and heterogeneous operands (`Money * int`)
  wait on a stated need. The right operand is checked against the
  left's type; a literal adopts it (`m + 1` on a `Money` is the
  ordinary mismatch, since `1` is not a `Money`). **Nothing is
  synthesized** (D49): a struct or enum without `impl Eq` does not
  compare, structurally or otherwise. Compound assignment (`a += b`)
  on a user type is not ruled here and refuses as it did (E0409).
  **On primitives the traits' impls are the same operations**: std's
  `impl Add for int { fn add(self, other: Self) -> Self { self + other
  } }` and its siblings for `f64`, `char`, `bool`, `str` (where the
  builtin operator exists) are what `[T: Add]` instantiated at `int`
  runs, so the machine add is what the generic body does — the
  instance calls the impl, and the impl is the builtin. Witnesses:
  `corpus/traits/op_total_num.lu` (the chapter's `total` at `int` and
  `f64`), `op_money.lu` (`Add`, `Sub`, `Neg` on a struct),
  `op_eq_inverting.lu` (an inverting `impl Eq` IS consulted —
  wolf-lang#176's row), `op_ord_struct.lu` (the ordering family and
  `<=>`), all four on both tiers; `golden_arith.lu` and
  `golden_eq.lu` (the bare `T`), `op_missing_impl.lu` (E0502),
  `op_hetero_add.lu` (E0514), `op_eq_no_trait.lu` (E0301),
  `op_eq_imported.lu`'s pair (the reachable trait, s156). Cost
  stated: the interpreter's operator dispatch on a struct and its
  alias-form parse (wolf-interp, filed with the clause); std.ops's
  five traits, `Neg`, and the primitive impls (wolf-std sc44); the
  book's §5.3 transcript and §5.5 boundary sentence (wolf-book bs41).

- `[type.trait.op.alias]` **`trait Num = Add + Sub + Mul + Div + Rem +
  Eq + Ord` is an alias bound.** The `=` form of `trait_item`
  (`[gram.item.trait]`) declares no members: a bound naming it means
  every trait in its list, in every position a bound is read — the
  body's capabilities (`[T: Num]` grants `+` through `Add`), the
  instantiation's obligations (each trait is checked, and an unmet
  one is E0502 naming that trait, never `Num`), and the impl search
  (`satisfies` never asks about the alias). An alias may name an
  alias; a cycle is E0503 at the alias, once. An alias is not
  implemented (`impl Num for T` is E0507 — implement its traits) and
  is not a `dyn` object. std's `Num` is the one the chapter's `fn
  total[T: Num](xs: List[T], zero: T) -> T` reads; a program that
  spells its own `Num` gets the same reading. The witness is
  `op_total_num.lu`'s `Num`, word for word std's.

---

## §12 The list literal `[type.list.lit]`

(s158, wolf-lang#154 / BACKLOG B23. The grammar half is
`[gram.expr.list]`; this is the typing half.)

- `[type.list.lit.elem]` **The element type unifies across the
  elements, left to right.** `[1, 2, 3]` is `List[i32]` — its
  elements are bare `{integer}` literals and default exactly as
  `[type.numlit.default]` says, `i32` when nothing in the body decides
  otherwise (corrected 2026-09-21 by s175 for wolf-lang#347's third
  clause: this sentence said `List[int]` while the defaulting rule
  and both compiler tiers say `i32`; measured at trunk `2f8deb7f` and
  at 0.2.15, `let xs = [1, 2, 3]` then `let n: i32 = xs[0]` runs on
  both tiers and `let ys = [5000000000]` is E0415, "does not fit
  `i32`", on both — witnesses `typecheck/list_lit_elem_i32.lu`,
  `typecheck/list_lit_elem_unfit.lu`); `["a", "b"]`
  is `List[str]`; `[[1], [2, 3]]` is `List[List[i32]]`. The first
  element fixes the type the rest are checked against, so the **first
  element that does not fit is the error site** — E0401 at that
  element, with the first element's span as the "because", never at
  the whole literal and never at the last element. A literal of one
  element is that element's type; nesting is ordinary recursion, the
  inner literals typing before the outer one unifies them. Numeric
  literals default exactly as they do anywhere else
  (`[type.numlit]`): `[1, 2]` in a `List[i32]` context is `List[i32]`,
  and the literals adopt, they do not force.
- `[type.list.lit.expect]` **An expected type flows in.** In an
  annotated `let`/`var`, a call argument, a field initializer, a
  declared return and a declared element position, the expected
  `List[T]` is pushed into the literal and every element is checked
  against `T` directly — so `let xs: List[i64] = [1, 2]` needs no
  widening step and `f([])` against `fn f(xs: List[str])` is
  `List[str]`. An expected type that is not a `List` is E0401 at the
  literal, not at an element: the shape is wrong before the contents
  are.
- `[type.list.lit.empty]` **`[]` takes its element type from the
  context, or it is E0419.** There is nothing in an empty literal to
  infer from, and wolf does not leave a type open to be decided by a
  later use (`[type.numlit]`'s posture: inference reads down, never
  back up). `let xs: List[int] = []`, `f([])` against a declared
  parameter and `-> List[str] { [] }` all type; bare `let xs = []` is
  **E0419**, and the message names the annotation that would fix it,
  with the spelling for this binding written out. This is the one
  place a list literal needs help, and the diagnostic says which help.
- `[type.list.lit.value]` **The value is a fresh `List[T]`**, an
  allocation into the ambient region, with the elements evaluated
  left to right exactly once each before the list exists
  (`[mem.model.order]`) — the same value `List[T]()` followed by
  `push` per element produces, and the same value a slice produces
  (`[mem.list.slice]`). The literal is sugar with no new lifetime, no
  new ownership rule and no static storage: `[1, 2, 3]` written twice
  is two lists. **Not at comptime this edition**: a list literal inside
  a `comptime fn` is refused by name on both tiers, because CTFE stays
  scalar until the mutable-container model lands (BACKLOG B26, ruled
  2026-09-11, wolf-lang#101) — the literal is sugar for a container,
  and the container is the thing the evaluator does not have.

## §13 The range type `[type.range]`

(s158, wolf-lang#24 / BACKLOG B19 — ruled 2026-09-11. `range` was the
one type the compiler could build a value of and not name.)

- `[type.range.name]` **`range[int]` and `range[char]` are types**,
  spelled like any other type application (`[gram.type]`), legal in
  every type position — parameter, `let`/`var` annotation, field,
  return, element. `range` is an ordinary identifier the prelude binds
  **in type position only** — there is no `range(…)` constructor, a
  range value being spelled `a..b` — so a declaration named `range`
  shadows nothing a program can spell and is NOT the W0304 hazard
  `List` is (`List[int]()` IS an expression, so a module declaring its
  own `List` really is severed from the container; `var range = true`
  severs nothing, and two of the corpus's own `os_random` witnesses
  spell it — the word is too ordinary to tax). `range` with no
  argument is E0405 (the element type is not inferable from the name
  alone) and a `range[T]` for any other `T` is E0401 — the family is closed at the two types
  `..` iterates, exactly `[mem.iter.range]`'s closed builtin family.
  The type was already the one diagnostics printed (`range[int]` is
  how a mismatched `2..7` has always been rendered); this clause makes
  what they print spellable.
- `[type.range.endpoints]` **A range VALUE has two present, plain
  endpoints.** `a..b` and `a..=b` are `range[T]`; the end-relative
  and open-sided spellings — `^n`, `a..`, `..b`, `..=b` — are
  **subscript-position only** and are not values of this type, because
  each of them is a shorthand that a collection's length resolves at
  the subscript and nothing resolves anywhere else. That surface is
  stated once here and cited, not restated, by `[mem.list.slice]` and
  the `str` slice clauses. Outside a subscript, `let r = 1..` is
  refused by name at the site rather than typed — a conservatism
  refusal, not a diagnostic, so it is pinned in the checker's own
  tests and not in the corpus (which records verdicts, and there is no
  verdict for "the language does not spell this"). (The refusal is not
  new: the reference implementation has refused range values outside
  `for` headers since D25; the clause writes the boundary down and
  moves the supported side of it into the language.)
- `[type.range.accessor]` **`start` and `end` read the endpoints**,
  as properties, spelled without parentheses the way `xs.len` is —
  `r.start` and `r.end` are `T`. **`end` is exclusive, always**:
  `(2..7).start` is 2 and `(2..7).end` is 7, and `a..=b` **normalizes
  at construction** to `end = b + 1` under the checked arithmetic
  `[mem.iter.range]` already rules, so `(2..=7).end` is 8 and
  `0..=T.MAX` traps `overflow` where it is built, not where it is
  read. One exclusive `end` is what makes `len` and `contains`
  writable at all (`end - start`, `start <= x && x < end`), which is
  the gap wolf-std F-0030 filed; two accessors whose meaning depended
  on a spelling the type does not carry would not close it. **The
  cost, stated:** one checked add where an inclusive range VALUE is
  built, and nothing anywhere else — `start`, `end` and every loop
  over a value read two words, and a `for` over a range header never
  builds a value at all (`[type.range.value]`), so its bound is the
  loop's own arithmetic, unchanged. (Corrected 2026-09-15 by s163,
  wolf-lang#383: this clause said the reference interpreter had
  normalized at construction since its first range arm. It had not —
  measured at lupin 0.1.36 (`6e94436`) by wolf-interp is49, `..=` was
  carried as a flag to the `for` loop and the bound computed there on
  unchecked `i128`, so `0..=int.MAX` as a value neither trapped nor
  normalized. The machines agree because is49 mirrored this clause,
  not by construction.)
- `[type.range.value]` A range passes as a parameter, returns, binds,
  and iterates; `for` is **unchanged** in every way
  (`[mem.iter.for]`/`[mem.iter.range]` still describe the loop, and a
  `for` over a range header still lowers without ever materializing
  one). A range is not ordered, not a collection, and has no `len` property
  of its own — `r.end - r.start` is the count, spelled in the program
  that wants it, and std.range is where the named functions live
  (wolf-std F-0030's `contains`, `len`, `clamp_to`, unwritable until
  this clause). The witnesses are
  `grammar/range_type_param.lu`, `grammar/range_type_return.lu`,
  `grammar/range_type_inclusive.lu`, `grammar/range_type_char.lu`,
  `grammar/range_type_overflow.lu` (the normalization's price, trapped
  where the range is built).

## §14 Error-set aliases `[type.err.alias]`

(s158, wolf-lang#36 / BACKLOG B20 — ruled 2026-09-11 on s155's alias
precedent, `[type.trait.op.alias]`. The item grammar is
`[gram.item.error]`.)

- `[type.err.alias.transparent]` **An alias is a spelling, never a
  type.** `error IoErrors = {none, parse, io}` makes `T ! IoErrors`
  and `T ! {none, parse, io}` **the same type**, interchangeable in
  both directions, with no conversion between them and no coarsening
  function anywhere. This is argued from D30 and not a preference:
  rows are structural and `?` propagates by width subtyping, so a
  nominal error set would create a second way for two rows to be the
  same and a cast between them. The alias has no identity a program
  can observe — it cannot be compared, matched on, or made a `dyn`
  object, and `impl` over it is E0507 the way it is over a trait
  alias.
- `[type.err.alias.union]` **Aliases compose by naming.** An alias's
  name in a row entry expands to its tags: `error ConfigErrors =
  {IoErrors, parse}` is `{none, parse, io}` ∪ `{parse}` =
  `{none, parse, io}`. **Resolution decides**, in one step: a row
  entry whose path names an error-set alias in scope is that alias's
  tags; every other path is a tag. Tags are structural, so the union
  merges a repeated tag into one, and a tag whose two sources disagree
  on payload types is E0609 — exactly `[gram.type.row.flatten]`'s
  rule, which this clause reuses rather than restates: an alias is one
  more layer, and layers flatten. An alias entry carries no payload
  (`{IoErrors(int)}` is E0601): the alias already names what its tags
  carry.
- `[type.err.alias.qualified]` **The qualified spelling of an alias is
  the alias.** A row entry's path resolves exactly as a type path
  does: a bare name is this module's alias or one this file bound with
  `use m.Alias`; `m.Alias` reaches it through the module binding.
  Whichever spelling names it, the entry expands to the alias's tags —
  `-> int ! fs.IoErrors` is `-> int ! {not_found, denied, io}` — so
  `[type.err.alias.transparent]`'s "the same type, interchangeable in
  both directions" holds across a module boundary exactly as it holds
  inside one. A private alias named from another module is E0304, the
  resolver's own refusal for a private member, never a silent row.
  Ruled 2026-09-21 (s175, wolf-lang#434, wolf-std F-0138): at 0.2.15
  the qualified spelling was accepted and contributed no tags, so `?`
  under it was E0602 listing exactly the alias's three tags — the
  worst of the three readings the filing named, and the reason
  wolf-std's `tests/fs/alias_row.lu` kept a local copy of std's alias.
  **Cost:** none — resolution is static and the expansion is the same
  syntax read from the alias's own declaration. Witnesses
  `rows/error_alias_qualified/` (qualified and `use`-bound, both
  propagating back into a spelled-out row); refused
  `rows/negative/error_alias_private/` (E0304).
- `[type.err.alias.cycle]` **A cycle is E0610**, reported once, at the
  alias — the sibling of E0503 for trait aliases and of E0513 for
  associated-type bindings. `error A = {B}` with `error B = {A}` is
  one diagnostic naming the loop, not a hang and not a report per
  member. An alias may name an alias to any depth that terminates.
- `[type.err.alias.diag]` **Diagnostics expand the alias and keep
  naming tags.** The missing-tag report that names exactly which tags
  a handler does not cover is the best thing rows have, and an alias
  does not take it away: the report lists TAGS, and mentions the alias
  as the source of the ones it contributed ("`parse` and `io` come
  from `IoErrors`"), never "expected `IoErrors`". A rendered type
  prints the tags, for the same reason — a reader who has to go and
  read an alias declaration to know what a signature raises has lost
  what the row was for. The witnesses are `rows/error_alias_row.lu`,
  `rows/error_alias_union.lu`, `rows/error_alias_transparent.lu`,
  `rows/error_alias_ident.lu`; refused:
  `rows/negative/error_alias_cycle.lu`,
  `rows/negative/error_alias_open.lu`.

## §15 Methods on std data `[type.method]`

(s166, wolf-lang#390 — ruled by the maintainer 2026-09-15, option 1:
`par` stays, and the combinators come first because `par` is one.
Until this section both machines refused every method on `List`,
`Map` or `str` that was not a builtin: the compiler with "cannot
compile this yet — methods on generic std data (the std surface)" at
two sites in the checker, lupin with "`List` has no method … in this
machine's std subset". std had the operations the whole time, as free
functions over the container — `list.any(xs, p)` executed on every
lane at wolf-std `073aa19` — and no rule said how the method spelling
reaches them. wolf-lang#154 is the book's filing of the same gap.)

- `[type.method.home]` **Each std data type has one home module.**

  | receiver type | home module |
  |---|---|
  | `List[T]` | `std.list` |
  | `Map[K, V]` | `std.map` |
  | `str` | `std.str` |
  | `range[int]`, `range[char]` | `std.range` |

  The table is closed: `Pool`, the conc handles, `Shared`/`Weak`, the
  raw pointer, the other primitives and every user type have no home
  module, and a method on them is exactly what it was — builtin,
  inherent (`impl`) or trait. A home module's **method candidates** are
  its `pub fn` items whose first parameter's type, with the function's
  own generics as unknowns, is spelled with the receiver's type
  constructor — `fn any[T](xs: List[T], …)` and `fn sum(xs: List[int])`
  are `List` candidates; the private `at` and a `pub fn` whose first
  parameter is an `int` are not. The home module is part of the type's
  surface, not an import: a method call reaches it **with no `use`**,
  and binds no name — `xs.any(p)` in a file that never wrote `use
  std.list` compiles, and `list` is still not in scope there.

- `[type.method.resolve]` **`recv.name(args)` IS `home.name(recv,
  args)`.** Resolution of a method call on a receiver with a home
  module, in order, stopping at the first step that finds `name`:
  (1) the language's builtin methods on the type (`push`, `pop`,
  `get`, `first`, `last`, `is_empty`, `count`, `clear` on `List`;
  `pairs`, `is_empty`, `clear` on `Map`; the `[mem.str]` family on
  `str`; `par`, `[conc.task.par]`); (2) the home module's method
  candidates named `name`; (3) trait methods from traits in scope,
  D27's second step, unchanged. At step (2) the call is **the free
  call**: the receiver is the first argument, checked against the first
  parameter with the candidate's generics fresh, then `args` against the
  rest — the same instantiation, the same dispatch record, the same
  instance and the same code as `list.any(xs, p)` written out, so the
  two spellings are one call and no program can tell them apart. The
  receiver's mode is spelled, as on every method (X1): a candidate whose
  first parameter is `mut` is called `(mut xs).sort_by(less)`, and a
  receiver whose written mode disagrees with the first parameter's is
  E0804. A candidate whose first parameter does not unify with the
  receiver — `std.list`'s `sum(xs: List[int])` on a `List[str]` — is
  not a match: the call is **E0403**, the "no method" refusal every
  receiver already gets, and its note names the candidate it found and
  the first parameter that did not fit. A name found at step (1) never reaches
  step (2): std's container rule forbids a home-module function that
  shadows a working builtin (wolf-std API-CONVENTIONS §8), and where one
  exists anyway (`std.list`'s `push` and `get`, written before the
  builtins had methods) the builtin answers the method spelling and
  the std function answers the qualified one, and the two agree —
  std's obligation, not the resolver's. Wrong arity at step (2) is
  E0402 counted against the written arguments, the receiver excluded.
  A method on a receiver with no home module that no step finds is the
  refusal it was.

  Why receiver-typed resolution and not an inherent-method table. (a)
  **One body.** A table in the compiler and another in the interpreter
  would be the third and fourth copies of an operation std already
  ships and tests on every lane; `[mem.str.empty]` is the record of
  what two agreeing copies of an unwritten rule do on the next input.
  Resolution to the function makes `xs.any(p)` and `list.any(xs, p)`
  the same call by construction, not by review. (b) **It is where the
  types are going.** D50 makes `List` and `Map` std-DEFINED once
  generic data can carry them, and a std-defined type's methods live in
  its own module — so the home module is already the place the method
  set will be, and this clause moves no function when D50 lands. (c)
  **Coherence.** Only the home module is searched. Weighed and
  rejected: uniform call syntax over every module in scope (D-style
  UFCS), under which `xs.frob()` would mean different functions in two
  files that import differently — the method set of `List[int]` would
  be a property of the importer, which is what D27's fixed order and
  its "no fallback chains" exist to prevent. Here the set is a function
  of the std revision alone, which is also what lets lupin mirror it
  and the book print it. A program that wants its own method on a
  `List` writes a trait and `impl`s it, and step (3) finds it.

- `[type.method.root]` **The home module comes from the std root.** It
  is loaded from the std root, the same tree `use std.list` reads: the
  configured std (`--std-root`, then `WOLF_STD`, then a `std` path
  dependency in `wolf.pkg`), or, with none configured, the default — a
  `std` directory beside the `wolf` binary, where the release archive
  ships wolf-std at a pinned commit (ruling #29) — for a hosted target
  only: a freestanding build (`[abi.target.none]`) reads no default,
  since the shipped std is the hosted library. With no std root at
  all (a build from source with nothing configured), a call that
  reaches step (2) is **E0301** naming the home module and the ways to
  configure a root — never a silent fall-through, and never a builtin
  stand-in.
  Step (1) needs no std, so every builtin method, `par` included, runs
  on a bare `wolf run`. **The cost, stated.** At run time, nothing: a
  method call through a home module is the free call, one instance per
  distinct instantiation exactly as the written-out call would make.
  At compile time, the home module is loaded, parsed and checked once
  per build when some call in the program names one of its candidates,
  and not at all otherwise; its own imports come with it
  (`std.map`'s `std.cmp`), as they would for `use std.map`.

- `[type.method.take]` **`take` is the ownership verb, and is never a
  method name** (wolf-lang#154's naming window, closed here). `take` is
  a reserved word (E0008 at every name position: no std function can
  be called `take`, which wolf-std measured on both machines at sc44),
  and the combinator it would have named is already the language's:
  the first `n` elements are the slice `xs[..n]` (`[mem.list.slice]`),
  which faults `bounds` when `n > xs.len`, and the clamped prefix is
  `xs[..min(n, xs.len)]`. The same holds for the suffix a `skip` or
  `drop` would name: `xs[n..]`. So no prefix or suffix combinator is
  added under any name — a second spelling of a working builtin is the
  one thing std's §8 forbids. `xs.take(n)` parses (member position is
  keyword-transparent) and is refused as a method no step finds, with a
  note naming both slices. Weighed and rejected: renaming the verb
  (`take` is spelled at every consuming call site in the corpus and the
  book, and it reads as what it does) and a contextual keyword (a word
  that is a verb in one position and a method in another is the
  ambiguity the reserved-word rule exists to prevent). Cost: none — it
  is a naming rule, and the slice's cost is `[mem.list.slice]`'s.

## §16 The combinators `[type.comb]`

(s166, wolf-lang#390 and #154's combinator row. The book's chapter 5
has promised `totals.pairs().sorted_by(…)` since bs00, and
`corpus/wordcount.lu` — the canonical program — has spelled
`sorted_by`, `take`, `merge` and `par` since reports/05, refused at
`resolve` for as long as it has existed.)

- `[type.comb.eager]` **The combinators are eager.** Each takes a
  `List` (a `range` for `collect`) and answers a finished value — a
  fresh `List`, a scalar, or a row — never a lazy adapter. A chain
  `xs.filter(p).map(f)` builds one intermediate `List` per stage.
  Weighed and rejected this edition: lazy adapters in the Rust shape.
  Each adapter is a generic struct holding a closure, and a capturing
  closure inside a struct is refused by name (`[type.fn.value]`)
  until its borrow story is written; the chain needs `Iter[T]` dispatch
  on every adapter; and the ambient-region cost of an eager stage is
  stated and bounded where the adapter's is neither. Fusing a chain's
  stages into one loop is a permitted optimization — it changes an
  allocation count and no printed byte — and is not promised.

- `[type.comb.set]` **The set.** Every row is a `std.list` function
  (a `std.range` one for `collect`) called by `[type.method.resolve]`
  step (2) — sc50 (wolf-std) writes them — except `par`, which is the
  language's. `f`, `keep`, `step`, `less` are fn values
  (`[type.fn.value]`): a named function, or a closure, capturing or not.

  | method | signature (first parameter is the receiver) | row | cost |
  |---|---|---|---|
  | `map` | `map[T, U](xs: List[T], f: fn(T) -> U) -> List[U]` | none | one fresh `List[U]` of `xs.len` in the ambient region; `xs.len` calls of `f` |
  | `filter` | `filter[T](xs: List[T], keep: fn(T) -> bool) -> List[T]` | none | one fresh `List[T]`, at most `xs.len`; `xs.len` calls |
  | `fold` | `fold[T, A](xs: List[T], init: A, step: fn(A, T) -> A) -> A` | none | no allocation of its own; `xs.len` calls, left to right |
  | `sum` | `sum(xs: List[int]) -> int` | none; traps `overflow` | none; checked addition left to right (X3) |
  | `sort_by` | `sort_by[T](mut xs: List[T], less: fn(T, T) -> bool)` | none | stable; O(n log n) calls of `less`, O(n) scratch in the ambient region |
  | `sorted_by` | `sorted_by[T](xs: List[T], less: fn(T, T) -> bool) -> List[T]` | none | `sort_by` over a fresh copy; `xs` untouched |
  | `sorted` | `sorted[T: cmp.Ord](xs: List[T]) -> List[T]` | none | `sorted_by` with `<` (`[type.trait.op]`; the builtin `<` on the primitives) |
  | `enumerate` | `enumerate[T](xs: List[T]) -> List[(int, T)]` | none | one fresh `List` of pairs; indices from 0 |
  | `zip` | `zip[T, U](xs: List[T], ys: List[U]) -> List[(T, U)]` | none | one fresh `List` of `min(xs.len, ys.len)` pairs |
  | `collect` | `collect[T](r: range[T]) -> List[T]` (`T` is `int` or `char`, `[type.range.name]`) | none; traps as the range's `for` does | one fresh `List` of the range's length |
  | `par` | `xs.par(f)`, `f: fn(T) -> U` or `fn(T) -> U ! E` | `E`, when `f` has one | `[conc.task.par]` |

  **What a combinator copies** (stated 2026-09-15 with s165's
  `[mem.tier0.move.3]` and `[mem.tier0.mode.read]`, and wolf-lang#384,
  #366 and #385's ruling). The receiver is `read`, so a combinator never
  hands the caller's own value on: `fold`'s accumulator starts as the
  lent seed and outlives the activation, so the seed **copies** (`copy
  init`). The elements `filter`, `sorted_by`, `sorted`, `enumerate` and
  `zip` keep are `push`ed into a fresh `List`, and **`push` copies a
  non-`Copy` element** (wolf-lang#385, ruled 2026-09-15; `push(take x)`
  is the move, and s167 implements both) — so each of those combinators
  pays one copy per element it keeps, and `map`, whose pushed value is
  `f`'s own temporary, spells `take` and pays nothing, as does
  `enumerate` for the pair it builds. **Every such copy is deep**: one
  allocation and a buffer copy for every `List` or `Map` reached, so a
  combinator over a `List[List[int]]` pays per container and not per
  element, while a `str` element shares its bytes. A caller who wants
  the elements moved rather than copied has `take` at its own call.

  The functions `std.list` already ships over fn values — `any`, `all`,
  `count_where`, `index_where`, `find_where`, `min_by`, `max_by` — are
  method candidates by the same rule and need no row here.
  **The relation is `bool`-shaped.** `sort_by` takes `less(a, b)`, read
  "`a` goes before `b`", and a stable sort keeps equal elements in
  input order: `std.list`'s callable tier has been bool-shaped since
  sc13, `[type.trait.op]` reads `<` as exactly that question, and
  measured at this revision on both native tiers neither `a <=> b` on
  `int` ("this operator in WIR lowering") nor a merge that tests an
  `Ordering` (`std.sort.sorted_by`: "an enum or row test inside a
  product pattern") lowers — so an `Ordering` comparator would be a
  signature no compiled program could call. `std.sort`'s
  `Ordering`-taking pair keeps its qualified spelling; the method is
  `std.list`'s. **`zip` stops at the shorter list** rather than
  trapping: a length mismatch is not an access out of range, and every
  pair it yields is one both lists hold. **`sum` is `List[int]`'s this
  edition**: a generic `sum[T: Add]` needs a zero, and no `Zero` trait
  is ruled; `xs.fold(0.0, fn(a, x) a + x)` is the `f64` spelling.
  **A fallible `f`** — a closure whose body uses `?` — is `par`'s
  alone: `map`'s `U` is a value type, and the serial spelling of a
  fallible map is the `for` loop with `?`, or `par`, whose failure rule
  is `[conc.task.fail]`'s.

- `[type.comb.builtin]` **`par` is the only builtin, and why.** Every
  other row is writable in wolf over `for`, `push` and a fn value, and
  so it is std's (sc50), with lupin free to run std's body or its own
  equivalent. `par` is not writable in wolf, for three reasons that are
  each sufficient: its chunk count is the runtime's scheduling decision,
  which `[conc.det.flow]` forbids std to make; its tasks read one
  `List` from several tasks at once and write disjoint slots of one
  result, which safe wolf can spell only through a `sync` wrapper or a
  channel, each costing a lock or a box per element that the desugar
  does not pay; and its capture check is spawn's applied to a closure
  that runs in several tasks. So `par` is a builtin method on `List[T]`,
  found at `[type.method.resolve]` step (1), and needs no std root.