# AILang — design decisions

This document records the core decisions for AILang. It is my contract with
myself across future iterations. Prefer cuts over growth.

## Goal

AILang is a programming language for LLM authors. It compiles to LLVM IR.
Performance: native, no GC for the MVP.

Optimised for:

- **Machine readability** over human ergonomics. The source is structured.
- **Local reasoning.** Every definition carries its full type and effects.
- **Provability.** Pure core language, explicit effects, optional refinements.
- **Robustness against hallucinations.** Symbols are hashable; tools can verify
  existence without spending context window.

## Project ecosystem

AILang is not just a language but an ecosystem. The language on its own is
only valuable when its surroundings make it usable, checkable, and
extensible for its target user (LLM authors). The repo therefore contains
several equally important components — none of them optional, all of them
evolving in lockstep with the language:

- **Language core** (`crates/ailang-core`, `crates/ailang-check`,
  `crates/ailang-codegen`): AST, type system, codegen.
- **Surface forms** (`crates/ailang-surface`, `crates/ailang-prose`):
  the LLM-facing renderings of a module. `ailang-surface`
  is the lossless Form-A printer/parser — the canonical authoring
  surface fixed by Decision 6, with a round-trip property
  `parse ∘ print = id` gating every release. `ailang-prose`
  is the lossy Form-B projection — human-readable prose for review and
  edit, with no parser; re-integration goes through the
  LLM-mediator round-trip documented in `docs/PROSE_ROUNDTRIP.md`.
- **CLI** (`crates/ail`): toolchain for tooling consumers — `manifest`,
  `describe`, `deps`, `check`, `build`, `parse`, `render`, `prose`,
  `merge-prose`, etc., preferably with `--json` for machine consumption.
- **Examples** (`examples/`): canonical `.ail.json` programs. They are
  specification anchors, not demos — the E2E suite hangs off them.
- **Skills** (`skills/`): specialised disciplines
  (`brainstorm`, `planner`, `implement`, `audit`, `debug`,
  `fieldtest`) plus the agent rosters they dispatch
  (`skills/<name>/agents/`). They form the project's own
  development methodology and are versioned with the codebase.
  See `skills/README.md`.
- **Docs** (`docs/`): `DESIGN.md` (canonical state),
  `docs/journals/` (per-iter decisions log; see `INDEX.md`),
  `docs/journal-archive.md` (archived monolith for pre-2026-05-11 history),
  `roadmap.md` (forward queue), `specs/` (per-milestone design
  specs), `plans/` (per-iteration implementation plans).
- **Tests**: unit tests per crate plus E2E in `crates/ail/tests/e2e.rs`. Every
  new compiler path needs a test, otherwise the feature does not count as done.

### What this document is — and the honesty rule it holds itself to

DESIGN.md describes what AILang **is now**: schema, semantics,
invariants, runtime contracts, and the rationale for each. It is
present-tense by construction. Two things never belong here:

- **Forward intent** ("planned / will back / on the path to /
  if-when X arrives") — that lives in `docs/roadmap.md`.
- **History** ("an earlier draft said / previously / what changed
  in <date> / retired in iter Y") — that lives in `docs/journals/`.

The single legitimate exception is a present-tense reserved or
deliberately-excluded claim that is explicitly and correctly
labelled (e.g. "`Diverge` is a reserved effect name with no op and
no codegen"; "No `deriving` — instances are written by hand";
"Regions were considered and rejected; see X"). The discriminator
is not whether a sentence mentions past or future, but whether the
document asserts something exists, works, or changed that does
not. Design rationale — *why* the language excludes a thing — is
in scope and present-tense; the *narrative of how the document
reached that wording* is not.

When the language grows, these components grow with it. New tools that
strengthen the LLM tooling (e.g. `ail diff`, IR snapshot diffs, new agents)
explicitly belong in the ecosystem inventory of this section and are added
here as soon as they are established.

## Project language: English

All in-tree content is written in English: source code (identifiers,
comments, string literals, CLI help), design documents, the journal, agent
prompts, READMEs, commit messages, examples, and `CLAUDE.md`. The live
conversation between user and me stays German for ergonomic reasons;
everything that lands in git is English. This keeps diffs and tooling output
uniform and matches the audience for AILang (LLM authors), for whom English
is the default.

## Feature-acceptance criterion

A proposed feature ships only if all three hold:

1. **An LLM author naturally produces code that uses it.** Without
   prompting toward the feature, the LLM reaches for it as the clean
   way to express the situation. If the feature is only used when
   explicitly mentioned, it isn't earning its keep — the LLM is the
   only author, and what the LLM doesn't reach for naturally is dead
   surface area.

2. **The feature measurably improves correctness or removes
   redundancy.** Either it eliminates a class of bugs structurally
   (the schema forbids the wrong code), or it lets the LLM express the
   same logic in fewer sites that have to stay consistent across
   edits. Aesthetic appeal — "feels elegant", "is idiomatic" — does
   not count.

3. **The feature reintroduces no bug class the core constraint exists
   to eliminate.** Criterion 1 is necessary but does *not*
   discriminate: an LLM reaches for *every* construct native to its
   imperative training distribution, so "the LLM reaches for it" is
   satisfied by exactly the constructs AILang most deliberately
   refuses. A feature can pass 1 and 2 — LLMs reach for it unprompted,
   and it removes redundancy — and still be a regression, because it
   reinstates the error surface the pure core, local-reasoning, and
   RC-acyclicity guarantees were built to remove. The decisive
   question is whether the construct re-opens a class of mistakes
   (iterated-mutable-state reasoning, silently-unbounded recursion,
   reference cycles) that a foundational invariant closes. If it does,
   it is cut even when 1 and 2 hold — *or* it must be reshaped until
   the bug class is structurally impossible rather than merely
   discouraged. A documentation note is not a reshape; the
   discriminator is whether the wrong code fails to typecheck, not
   whether a guideline advises against it. Worked example: a bare
   `while` over mutable state would pass clauses 1 and 2 yet fail
   clause 3 (it reinstates iterated-mutable-state reasoning the pure
   core exists to remove); a hypothetical "all repetition is either
   structurally-decreasing recursion over an acyclic ADT or an
   explicit named loop" iteration story would, *if it could be built
   without a documented-unenforced precondition*, pass all three —
   and the fact that the 2026-05 attempt could not (it forced a
   silent-divergence precondition; see
   `docs/specs/2026-05-16-iteration-discipline-revert.md`) is itself
   the clause-3 mechanism working as intended.

This is the positive complement to the CLAUDE.md rule that
implementation effort is not a rationale: cost is not a reason *for* a
feature, and neither is human aesthetic preference. LLM-author utility
(1, 2) is necessary; criterion 3 is the discriminator that keeps
utility from laundering the imperative paradigm back in one construct
at a time.

Two corollaries:

- **Human-attractive but LLM-neutral features are cut.** Point-free
  style, operator overloading, implicit conversions, syntactic
  shortcuts that hide structure. They reward human authors who enjoy
  compression; they cost the LLM the explicit form it relies on to
  keep RC, uniqueness, and effects locally legible.

- **Human-hostile but LLM-friendly features are kept.** JSON as
  canonical authoring surface; mandatory mode annotations on every
  fn parameter; mandatory top-level type signatures; explicit `clone`
  for shared values. These cost a human author keystrokes; they let
  the LLM reason locally without spending context window on
  cross-references.

Empirically: if a feature is proposed and the LLM does not produce it
in unprompted code samples, the feature is proposed for the wrong
reason. The orchestrator's job is to notice that and cut.

## Decision 1: source = data, not text

A module is a JSON object with a fixed schema. There is no parser for
free-form text. Typos in identifiers turn into hash-lookup errors that the
compiler proposes a fix for directly.

A textual form exists (`.ail`, S-expression-like), but only as a
bidirectional projection of the JSON form. It is intended for human reviews
and diffs.

**Canonical format:** `.ail.json` with deterministic key order.

## Decision 2: content-addressed definitions

Every top-level definition has a `hash` value (BLAKE3 over canonical JSON
without the `hash` field itself). References between definitions go primarily
by name — names are for readability. The hash is the canonical identity.

Advantages:

- Refactoring by adding new defs, not by in-place change. Old versions stay
  callable until manually removed.
- Caching of typecheck results and codegen per hash.
- Diffs show exactly which def has changed.

## Decision 3: pure core language + algebraic effects

The default is total, pure functions. Effects are declared as a set in the
function type: `(Int) -> Int ![IO]`. The effect set is a
flat, unordered, closed set of effect names, unified by set-equality —
there is no effect row variable; a signature lists exactly the effects
its body may perform.
In the MVP only the effect `IO` is wired up (its sole op is `io/print_str`).
`Diverge` (for non-termination) is reserved as an effect name but is
unimplemented — no op, no codegen, no checker injection — in the same
sense Decision 4 reserves refinements.

This is the most important LLM property: when I read a function, I can trust
its signature without reading the body.

## Decision 4: Hindley-Milner + optional refinements

MVP: HM with let-polymorphism. All types are inferable, but at the top level
they must always be explicitly annotated (for local reasoning).

Later: refinement annotations that escalate to SMT. `(i: Int | i >= 0)`. They
are reserved in the AST from the start, but in the MVP they are simply passed
through as opaque strings.

## Decision 5: emit LLVM IR as text

Instead of `inkwell` or `llvm-sys`: AILang produces `.ll` files as strings
and hands them to `clang` for linking.

Rationale:

- The LLVM IR text syntax is largely stable across versions.
- No build dependency on a specific libllvm version.
- Generated code is trivially inspectable, which makes debugging much easier.
- An LLM can read the generated IR directly, which is harder with opaque
  library calls.

Trade-off: no inline optimisations through the LLVM API. We rely on
`clang -O2` as the standard pipeline.

## Decision 6: authoring surface

Form (A) is implemented as
the `ailang-surface` crate (parser + printer). Form-A is
gated against drift by `ailang-surface/tests/round_trip.rs`, which
parses every `.ail` fixture, prints it back, re-parses, and demands
canonical-byte equality. `ail render` and both branches
of `ail describe` were rewired to use `ailang_surface::print`, making
form (A) the **sole** text projection of a module — the legacy
non-round-tripping pretty-printer code in `pretty.rs` was deleted at
the same time, leaving only diagnostic helpers (`type_to_string`,
`pattern_to_string`, `manifest`) public. The rest of this section
records the *why* of Decision 6 for the audit trail; the constraints
listed below describe the surface as shipped.

### Why this is opening up

Early development authored everything as raw `*.ail.json`. That worked
for 17 fixture files (each ≤ 60 LOC of JSON) but does not scale. Two
breaking signals:

1. The token-economy cost of the JSON-AST is massive: a single integer
   literal `1` is encoded as `{"t":"lit","lit":{"kind":"int","value":1}}`
   — ~38 tokens of structural overhead per bit of semantics. For a stdlib
   in the 200–500 def range this displaces real attention budget.
2. JSON-AST authoring exposes a class of errors (wrong field names,
   silently-accepted extra fields under `#[serde(default)]`,
   inconsistent ctor casing) that surface only at load time. The
   schema is correct-by-construction in storage but **error-prone in
   authoring**.

Decision 1 anticipated this: it says a textual form exists "as a
bidirectional projection of the JSON form." The pretty-printer already
emits S-expression-style text (see `crates/ailang-core/src/pretty.rs`).
What is missing is the inverse direction — text → AST. Decision 6
adds that inverse as **one** authoring projection alongside the
existing pretty-printer; the JSON-AST remains the source of truth.

### Architectural pin: data structure is the source of truth

The textual surface is **not** a replacement for the JSON-AST. It is
one projection among potentially many. Concretely:

- The JSON-AST keeps its role as the canonical, hashable, content-
  addressed representation of a module. All hashing, content-
  addressing, cross-module references, and typecheck/codegen input
  flow through the JSON-AST. **No new hashable form is introduced.**
- The textual surface (form A, this Decision) is the **AI authoring
  projection**: optimised for me producing programs token-efficiently
  and for foreign LLMs producing programs from a spec. It is not
  optimised for human authors and does not need to be human-pleasant.
- Future projections are explicitly anticipated: a visual / graphical
  front-end is a plausible second projection for human review and
  inspection (display being the one case where non-AI eyes matter).
  The architecture leaves room: any producer of well-formed
  `ailang-core::ast::Module` values is a valid front-end.
- **No human is expected to author AILang seriously.** Authoring is
  AI work. Display and verification, by contrast, are concerns where
  human-facing alternatives may be useful — and which can therefore
  layer their own projections on top of the same AST without
  touching the surface or the core.

In code terms: `ailang-core` owns the AST. `ailang-surface` is one
producer/consumer pair: text-form-A → AST → text-form-A. A hypothetical
`ailang-visual` would be a different producer
of the same AST. `ailang-check` and `ailang-codegen` consume only
the AST and remain projection-agnostic.

### Constraints (hard, in priority order)

1. **Formalizable for a foreign LLM.** The grammar must fit in an
   EBNF/PEG spec of ≤ 30 productions. A model that has never seen
   AILang must be able to read the spec and produce conforming source
   zero-shot. Rules out: precedence between binary operators,
   semantic indentation, maximal-munch lexing, context-sensitive
   reductions.
2. **AST-isomorphic.** Every surface form maps to exactly one AST
   shape. The full bijection between `.ail.json` and `.ail` (both
   directions, BLAKE3-stable hashing, Float-bits-hex encoding,
   workspace-CI enforcement points) is anchored as the top-level
   §"Roundtrip Invariant" — this constraint records that Decision
   6's surface-design choice must satisfy that invariant; the
   invariant itself lives at top level because the property is
   load-bearing on the language identity, not on this Decision's
   surface-design rationale.
3. **No external symbols.** ASCII only. No Greek (`∀`), no arrows
   (`→`), no subscripts. Reasoning: I substitute mojibake for
   non-ASCII characters under context pressure; foreign LLMs vary
   in how they tokenize Unicode.
4. **No precedence.** Either everything is parenthesized, or there
   are no infix operators. Prefer the latter — `add(x, 1)` over
   `x + 1`. Removes a fail mode for both me and foreign LLMs.
5. **No semantic indentation.** Block structure expressed by paired
   delimiters or terminator tokens. Indentation is informational
   only; the parser ignores it.
6. **One construct per token-list.** Every AST node corresponds to
   exactly one parenthesized form (or atom). No "sometimes you can
   omit the parens" rules.
7. **AST surface stays frozen.** The surface adapts to the AST, not
   the other way around. We do not change the JSON schema or
   invalidate hashes to make the surface prettier.

### Candidate notations (same `map` encoded in each)

The reference target — the polymorphic `map` from `examples/list_map_poly.ail.json`:

```
data List a where Nil | Cons a (List a)
fn map : forall a b. ((a) -> b, List a) -> List b
       = \f xs. match xs of Nil -> Nil
                          | Cons h t -> Cons(f(h), map(f, t))
```

#### (A) S-expression with fully-tagged AST nodes

```
(module list_map_poly

  (data List (vars a)
    (ctor Nil)
    (ctor Cons a (con List a)))

  (fn inc
    (type (fn-type (params (con Int)) (ret (con Int))))
    (params x)
    (body (app + x 1)))

  (fn map
    (type
      (forall (vars a b)
        (fn-type
          (params (fn-type (params a) (ret b)) (con List a))
          (ret (con List b)))))
    (params f xs)
    (body
      (match xs
        (case (pat-ctor Nil) (term-ctor List Nil))
        (case (pat-ctor Cons h t)
          (term-ctor List Cons
            (app f h)
            (app map f t)))))))
```

Grammar core (3-rule lexical layer + ~25 named-form productions):
```
sexpr  ::= atom | "(" sexpr* ")"
atom   ::= integer | string | ident
ident  ::= any maximal non-whitespace, non-paren run that is not
           a recognised integer or string literal.
```

The lexer recognises one delimiter (`(` / `)`) and whitespace.
Every other maximal token is classified post-hoc:
- All-digit run with optional leading `-` → integer atom.
- `"`-delimited run → string atom.
- Otherwise → ident.

Consequence: operators like `+`, `==`, `<=`, `**`, qualified
names like `io/print_str`, and cross-module references like
`std_list.map` are all single ident tokens with no special lex
rule. The only reserved tokens are `(`, `)`, and whitespace.
Bool literals (`true`, `false`) and unit (`(lit-unit)`) are
disambiguated by parser context, not by lex.

Every AST node form has a unique head keyword (`module`, `data`,
`fn`, `forall`, `fn-type`, `con`, `var`, `app`, `lam`, `match`,
`case`, `pat-ctor`, `term-ctor`, `do`, `seq`, ...). A bare atom in
a positional slot (e.g. inside `(con List a)` second position) is
a name reference whose **sort** is determined by the parent slot:

- inside `(con NAME args...)` second-and-later positions → type
  expression. Bare atom there ⇒ `Type::Var { name }`.
- inside `(app HEAD args...)` first position ⇒ `Term::Var`.
- inside `(pat-ctor CTOR fields...)` field positions ⇒
  `Pattern::Var`.
- inside `(case PAT BODY)` second position ⇒ term.

There is **no lexical case rule**. To construct a value with a
ctor, write `(term-ctor TypeName CtorName args...)`. To match
against one, write `(pat-ctor CtorName fields...)`. Capitalised
identifiers carry no special meaning to the parser. This rules
out a class of silent errors ("I forgot to capitalise `Cons` and
it parsed as a function call").

**Pros:** smallest formal grammar of any candidate (the lexical
core is 3 rules; the named-form productions are uniform — every
node a tagged list). Foreign-LLM bar lowest. Round-trip with the
existing pretty-printer is a refactor of `pretty.rs` to emit this
tagged form, plus a new parser.

**Cons:** paren density is high. `(forall (vars a b) (fn-type
...))` has more visual nesting than the current pretty-printer's
`forall a. (...) -> ...`. Verbosity is ~2× JSON for the same node
when measured in characters, but ~8× shorter in lines (the
existing JSON `box.ail.json` of 160 lines becomes ~20 lines in
this form).

#### (B) Indented record-style with explicit terminators

```
module std_list

data List(a):
  Nil
  Cons(a, List(a))
end

fn map:
  type: forall a b. fn(fn(a) -> b, List(a)) -> List(b)
  params: f, xs
  body:
    match xs:
      Nil          => Nil
      Cons(h, t)   => Cons(f(h), map(f, t))
    end
end
```

Grammar core (~20–30 productions): module-level (def/data/end), type
sub-grammar (forall, fn, con, var), term sub-grammar (lam, match,
ctor, app, lit, var, seq), pattern sub-grammar.

**Pros:** higher information density per line, closer to mainstream
ML/Haskell shape. **Cons:** four sub-grammars instead of one.
`forall a b. fn(...)` keeps a pseudo-precedence (`->` binds tighter
than the outer `fn(...)` wrapper). Foreign-LLM bar higher.

#### (C) Pretty-printer-as-source

Use exactly the format `pretty::module` already emits, plus a parser
that accepts it. The existing pretty-printer's quirks (`::` for
type-of, `[params]` for fn-params, `<a>` for type-args, `forall a. ...`,
`!IO`, `()` ambiguous between unit-arg-list and empty-form) become
the spec.

**Pros:** zero churn — the existing pretty-printer is already the
spec; only the inverse is missing. Round-trip is the identity by
construction. **Cons:** the existing format mixes four mini-dialects
(s-expr at term level, ML-shape at type level, square brackets for
params, `<>` for type args). Formalising it crisply is harder than
designing a uniform form from scratch.

### First choice and rollback plan

**Try (A) first.** Reasoning: constraint 1 (formalizable) outweighs
constraint readability. (A) has a 3-rule core grammar with one
lexical disambiguation rule. (B) doubles the rule count and
re-introduces a soft form of precedence (`->` inside `forall`).
(C) is tempting because it is zero-design but the resulting spec is
visibly heterogeneous, which is exactly what constraint 1 was meant
to rule out.

If implementing (A) reveals that paren density actively hurts my
authoring (measurable: I make more wrong-paren errors than the
JSON-AST shape produced before), roll back and try (C). (B) stays
on the shelf for a future iter only if both fail.

### Implementation outline

- `crates/ailang-surface` — new crate. **Strictly additive.** PEG
  parser produces existing `ailang-core::ast` types. No new AST
  nodes, no schema changes, no new hashable form. Pretty-printer
  for form (A) lives here too (the round-trip is the contract).
- `ailang-check`, `ailang-codegen` are **not modified**. They
  continue to consume `ailang-core::ast::Module` values regardless
  of which projection produced them.
- Round-trip test: for every `examples/*.ail.json`, parse the
  corresponding hand-written `*.ail`, canonicalise, and assert
  hash-equivalence to the original. Hash equivalence is the truth
  check; the surface ships only if every fixture round-trips
  identically.
- CLI: `ail parse <file.ail> -o <file.ail.json>`. Symmetric to
  existing `ail render`. **`.ail.json` remains a first-class input**
  to every existing subcommand; the parser is a producer, not a
  gatekeeper.

  **Both extensions accepted.** Every path-taking CLI subcommand
  accepts either `.ail` (Form A)
  or `.ail.json` (Form B) as input. For `.ail` paths the subcommand
  parses through `ailang_surface::parse` in-line and then proceeds
  with the same loaded `Module` value that `.ail.json` would have
  produced. `ail parse` remains the explicit converter — it does
  nothing the implicit dispatch in the other subcommands does not,
  but it is the supported way to materialise a stable `.ail.json`
  snapshot from a `.ail` source for diff / hash / cache purposes.
- Stdlib (`std_list`, `std_maybe`, ...) authored in
  form (A) from day one **because that is the AI authoring
  projection**, not because JSON authoring is forbidden. The
  resulting `.ail.json` is what tests and downstream tools see.

### What this Decision deliberately does not do

- It does not change which form is canonical: the JSON-AST remains
  the hashable, content-addressed representation, and all hashing,
  content-addressing, and cross-module references flow through it
  unchanged. The authored form is Form A; the JSON-AST is
  materialised in-process by callers that need it. The two
  forms are byte-isomorphic by the round-trip invariant. Form (A)
  is one projection; the JSON-AST stays canonical.
- It does not foreclose visual or graphical front-ends. The crate
  layout (`core` owns AST; `surface`/`visual`/... are siblings)
  reserves that lane.
- It does not remove `.ail.json` as input. Every existing
  CLI subcommand (`check`, `render`, `describe`, `emit-ir`,
  `build`, `run`, `manifest`, `deps`, `diff`, `workspace`,
  `builtins`) keeps its current `.ail.json` interface.

### Form refinements during implementation

Two productions in the original sketch had to be widened
during implementation to round-trip the existing AST faithfully.
Captured here for the spec record:

1. **`lam-term` carries types and effects.** The AST's `Term::Lam`
   stores parallel `params`, `param_tys`, `ret_ty`, and `effects`
   fields. The original sketch had only names. The implemented form is

   ```
   lam-term ::= "(" "lam" "(" "params" typed-param* ")"
                          "(" "ret" type ")"
                          effects-clause? body-attr ")"
   typed-param ::= "(" "typed" ident type ")"
   ```

   This keeps the no-precedence / one-construct-per-token-list
   invariants and adds no new lexical rules.

2. **`import-clause` admits an optional alias.** The AST's
   `Import.alias` is `Option<String>`; the original sketch only
   supported the `None` case. The implemented form is

   ```
   import-clause ::= "(" "import" ident ("as" ident)? ")"
   ```

   `as` is a bare ident token in this position; no special lexical
   rule is needed.

Neither change extends the grammar's rule budget meaningfully:
the 30-production ceiling of constraint 1 is intact (the parser
implements ~28 named productions). All 17 `examples/*.ail.json`
fixtures round-trip identically through `print → parse → canonical
JSON`; the three hand-written `.ail` exhibits parse to canonical
JSON identical to their corresponding `.ail.json` files.

3. **Tail-call surface.** Decision 8 ships two new
   productions, both positional analogues of their non-tail
   counterparts. Their result terms set `Term::App.tail = true` /
   `Term::Do.tail = true`; the typechecker's `verify_tail_positions`
   pass enforces that the marker is only used in tail position.

   ```
   tail-app-term ::= "(" "tail-app" term term+ ")"
   tail-do-term  ::= "(" "tail-do" ident term* ")"
   ```

   Production count: ~30, still inside the 30-rule
   constraint-1 budget. No new lexical rule (`tail-app` / `tail-do`
   are bare ident tokens; no special casing).

### Form (B) — human prose projection

AILang ships a
second textual projection of the AST: `ailang-prose`, a one-way
projection from `Module → human-readable text`. It is **not** an
authoring surface; it is the "display" projection that Decision 6's
architectural pin (line 167–176) explicitly anticipated:

> *"Future projections are explicitly anticipated: a visual /
> graphical front-end is a plausible second projection for human
> review and inspection (display being the one case where non-AI
> eyes matter). The architecture leaves room: any producer of
> well-formed `ailang-core::ast::Module` values is a valid
> front-end."*

Form (B) targets the specific failure mode where a human reviewer
needs to read an AILang module quickly. Form (A) was designed to
fit a 30-production EBNF spec and to be parsed zero-shot by foreign
LLMs; that prioritisation makes it dense and visually noisy for
human readers. Form (B) inverts the trade-offs:

- **Rust-flavoured surface.** Braces and `=>` for match arms,
  Rust-aligned 4-level operator precedence, infix arithmetic
  (`a + b`, not `+(a, b)`), unary `!` for `not`.
- **Lossy by design.** Projection elides machinery the LLM can
  re-derive: `(con T)` wrappers (`(con Int)` → `Int`), the
  `(fn-type (params ...) (ret ...))` wrap, `(term-ctor T C ...)`
  collapses to `C(...)`, redundant parens. Only the AST machinery
  whose information is recoverable from typecheck context.
- **Lossless on load-bearing detail.** Mode annotations
  (`own T`, `borrow T`), effects (`with IO`), explicit `clone`,
  `reuse-as`, doc strings, type annotations on signatures and
  lambdas, the `tail` flag — all preserved verbatim.

Critically, **form (B) has no parser**. Form (A) is round-trippable
by construction (Decision 6 constraint 2); form (B) deliberately is
not. Re-integrating prose edits requires an external LLM mediator,
not a compiler pass — see `docs/PROSE_ROUNDTRIP.md` for the
six-step cycle and the prompt template `ail merge-prose` composes.

Form (B) does not weaken any Decision 6 invariant:

- The JSON-AST remains the only hashable artefact. Prose is not
  hashed, not content-addressed, not load-bearing for any
  cross-module reference.
- Form (A) remains the canonical authoring surface. Foreign LLMs
  still author against form (A); humans review and edit through
  form (B).
- The 30-production grammar of form (A) is unchanged.
- `ailang-check` and `ailang-codegen` remain projection-agnostic;
  `ailang-prose` is a downstream consumer of `ailang-core::ast`,
  parallel to `ailang-surface` but in the rendering direction only.

The CLI gains `ail prose <m.ail.json>` (the deterministic
projection) and `ail merge-prose <m.ail.json> <edited.prose.txt>`
(the mediator-prompt composer); both are listed in the CLI section
below.

**Form-A spec embedding.** An earlier `merge-prose`
prompt instructed the LLM to emit JSON-AST and offered a 12-line
schema-essentials reminder; that combination did not give a
foreign LLM enough to produce valid output. The current prompt revises this:

- The LLM emits **Form-A** (the canonical authoring surface), not
  JSON. JSON-AST stays the only hashable artefact, but it is not
  a writing surface. The user runs `ail parse foo.new.ail`
  before `ail check` to produce the canonical JSON.
- `crates/ailang-core/specs/form_a.md` is the complete LLM-targeted
  Form-A specification — grammar, every term / pattern / type /
  def keyword, schema invariants, pitfall catalogue, four
  few-shot modules drawn from `examples/*.ail`. It is exported
  as `ailang_core::FORM_A_SPEC` and embedded verbatim in every
  `merge-prose` prompt.
- `crates/ailang-core/tests/spec_drift.rs` walks every variant of
  `Term`, `Pattern`, `Type`, `Def`, `Literal` via exhaustive
  `match` and asserts an anchor for each appears in the spec.
  The exhaustive match is the load-bearing piece: adding a new
  variant without updating the match fails compilation in this
  test, before its assertions even run. Hand-written content,
  mechanical drift detection.

The cycle's lowest-common-denominator path is the static prompt
(`ail merge-prose | client | ail parse | ail check`), which works
with any client.

### Empirical addendum — cross-model authoring measurement

Cross-model measurement against two foreign LLMs via IONOS,
temperature=0, top_p=1, max-turns=5. Two blind cohorts on the same
four MVP tasks (`t1_add_three`, `t2_length`, `t3_main_prints`,
`t4_count_zeros`); each cohort sees only its own form's mini-spec.
Subjects (both runs use the pipeline-error-formatting fix from ms.1
so JSON-cohort feedback carries the full anyhow cause chain):

- `Qwen/Qwen3-Coder-Next` —
  `experiments/2026-05-12-cross-model-authoring/runs/2026-05-12-080864/`
- `meta-llama/CodeLlama-13b-Instruct-hf` —
  `experiments/2026-05-12-cross-model-authoring/runs/2026-05-12-9197fd/`

| metric | Qwen / JSON | Qwen / AIL | CodeLlama / JSON | CodeLlama / AIL |
|---|---|---|---|---|
| reached green | 1/4 | 1/4 | 0/4 | 2/4 |
| first-attempt green | 1/4 | 1/4 | 0/4 | 2/4 |
| mean turns-to-green (green only) | 1.0 | 1.0 | — | 1.0 |
| total prompt tokens | 182,378 | 110,575 | 116,015 | 93,017 |
| total completion tokens | 14,972 | 3,474 | 2,711 | 2,234 |
| top error class | check (×3) | parse (×3) | check (×2) | parse (×2) |

Both subjects show the same direction on every metric the table
tracks. AIL is cheaper than JSON on prompt tokens (Qwen 61%,
CodeLlama 80% of the JSON cohort's spend) and cheaper on completion
tokens (Qwen 23%, CodeLlama 82%). AIL reached-green is greater than
or equal to JSON reached-green for each subject (Qwen ties at 1/4;
CodeLlama strictly dominates, 2/4 vs 0/4). The failure-class
symmetry observed on the original Qwen baseline holds for both
subjects: JSON cohorts fail at the typecheck stage, AIL cohorts at
the parse stage — each form's front-of-pipeline check. Three of the
four first-attempt-green cells observed across the two subjects are
AIL (Qwen-AIL t3, CodeLlama-AIL t1, CodeLlama-AIL t3); the
fourth is Qwen-JSON t3, the same task the original baseline already
flagged as the JSON-form's only first-attempt success. Two CodeLlama
JSON-cohort cells (`t2_length`, `t4_count_zeros`) terminated as
`api_failure` on turn 1 with zero tokens consumed — a transient
IONOS-side terminal error, not a model-output failure; CodeLlama
JSON-cohort numbers therefore average over 2 informative cells, not
4. The Qwen re-run also shifted by one cell against the cma.3
baseline (AIL 2/4 → 1/4, JSON 1/4 → 1/4) despite identical
temperature=0 inputs; this is IONOS-side state-of-day noise on a
single deterministic re-run, not an effect of the ms.1
feedback-formatting fix (which only changes JSON-cohort prompt
content).

**Scope of this addendum:** two subjects, n=1 each, deterministic.
This is a second data point pointing in the same direction as the
first, not a verdict. The universal claim of this Decision (".ail
is the AI authoring projection") would need ≥3 subjects with
statistical robustness to ratify; both current points point the
same way (AIL cohort cheaper and at-least-as-green) but neither
the sample size nor the cross-call noise observed in the Qwen
re-run is enough to close out the Decision.

## Decision 8: explicit, verified tail calls

For an LLM author, recursion is the natural iteration form
(`\n. if n == 0 then () else loop(n-1)` is what I reach for, not
a `for`-loop). Without a tail-call guarantee, every recursive
program has a silent stack-depth ceiling that no compile-time
diagnostic warns about. That is exactly the class of correctness
hazard the language exists to eliminate.

Solution: explicit, verified tail calls.

- **AST.** `Term::App { fn, args, tail: bool }` and
  `Term::Do { op, args, tail: bool }` gain a `tail` flag,
  serde-defaulting to `false` so existing fixtures load with
  `tail: false` and their hashes stay bit-identical.
- **Typecheck.** A new pass `verify_tail_positions(fn_body)`
  runs after the main type-check. It walks the body with an
  `is_tail_context: bool` threaded down. The flag is `true` at
  the start, `true` for the body of every `Term::Match` arm,
  `true` for the right operand of `Term::Seq`, `true` for the
  body of `Term::Let`, `true` for the body of `Term::Lam` (each
  Lam opens its own tail scope). The flag is `false` for: args
  of any `App`/`Do`/`Ctor`, scrutinee of `Match`, left of
  `Seq`, condition of `Let`-bound expression. When the walker
  visits an `App { tail: true }` or `Do { tail: true }`, the
  flag must be `true` at that visit; otherwise emit diagnostic
  `tail-call-not-in-tail-position`.
- **Codegen.** Emit `musttail call` (LLVM IR) for marked calls
  instead of plain `call`. LLVM rejects at IR-verification
  time if the call cannot physically be a tail call (calling
  convention mismatch, signature divergence, etc.). The reject
  surfaces as a hard build error, not a silent runtime
  surprise.
- **Form (A).** Two new keywords: `tail-app`, `tail-do`.
  Productions are positional analogues of `app`/`do` with
  `tail: true` set on the resulting term. EBNF gains 2 lines;
  total production count goes from ~28 to ~30, still inside
  the constraint-1 budget.

**What this does NOT promise.** Per the tail-call survey of existing fixtures,
many existing recursive calls are *not* in tail position
because they are arguments to constructor calls (e.g.
`Cons (f h) (map f t)`). The current pipeline adds annotation + verification;
it does **not** add a CPS transform or accumulator-form
rewrite. Programs whose recursion is constructor-blocked
will continue to be stack-bounded by recursion depth. The
canonical authoring pattern in such cases is to write the
accumulator-form variant (`map_acc`, `fold_left`, etc.)
explicitly. The stdlib ships both forms where
relevant.

Migration of existing fixtures is partial: only
`print_list`-style terminal recursions get marked. The
constructor-blocked recursions in `map`, `sort`, `insert`
remain unmarked — they cannot benefit from `musttail`
without a source-level rewrite.

## Decision 9: dual allocator — RC canonical, Boehm parity oracle

AILang ships two allocator backends with an asymmetric role:

- **RC is canonical.** `--alloc=rc` is the CLI default for
  `ail build` and `ail run`. The runtime AILang's memory model
  (RC + uniqueness inference) is designed for. New examples,
  benches, and corpus tests run under RC unless they explicitly
  pin GC.
- **Boehm stays as a parity oracle.** `--alloc=gc` remains
  reachable. Its load-bearing job is differential diagnosis: when
  RC produces a segfault, refcount underflow, or wrong stdout, the
  GC build of the same module is the cheap "memory bug or logic
  bug?" probe. The end-to-end suite includes per-example
  parity tests that run both backends and assert byte-identical
  stdout — those tests are what make the oracle real.
- **`--alloc=bump`** is unchanged: a leak-only bench instrument,
  not a production target.

Full Boehm retirement (drop libgc, remove the gc backend) reopens
when the parity oracle stops paying its keep — concretely, when a
few iter families ship without the gc arm catching anything that
the rc arm did not already catch. Until then, the cost of
keeping libgc as a build dependency is accepted in exchange for
diagnostic leverage. Decision 10 (RC + uniqueness) holds as the
specification of the canonical runtime; the rest of this section
documents the Boehm half, retained as the oracle.

**Choice: Boehm-Demers-Weiser conservative GC.** The simplest
working option:

- Replace `malloc(...)` with `GC_malloc(...)` in every IR site
  (currently `lower_ctor`'s ADT box, `lower_lambda`'s env block
  and closure pair).
- Replace the IR-level `declare ptr @malloc(i64)` with
  `declare ptr @GC_malloc(i64)`.
- Add `-lgc` to the `clang` link command (in
  `crates/ail/src/main.rs`'s `Build` / `Run` paths).
- No language-level change. No AST change. No schema change.

Rationale:

- **Mature.** Boehm has been the default conservative GC for
  decades. Linux distros ship it as `libgc` / `libgc-dev` /
  `gc` (Arch).
- **No language work.** Conservative scan of the C stack handles
  AILang's stack frames without LLVM stack-map infrastructure
  (which is its own multi-iter design).
- **Single-iter integration.** Lift-and-shift of the four
  allocation sites; all existing tests must still pass with
  identical output.

Trade-offs accepted:

- **Conservative over-retention.** A user-supplied `Int` field
  whose value happens to coincide with a heap address will pin
  that allocation. In practice, vanishingly rare for typical
  values; survivable.
- **Pause time non-deterministic.** Boehm uses stop-the-world
  mark-sweep. For LLM-author-written stdlib code at MVP scale,
  pause times are not the bottleneck.
- **Build-time dependency.** `libgc` must be installed on the
  build host. Users without it get a link-time error from
  clang, not a silent failure.

### Per-fn arena via stack `alloca`

This optimisation is layered on top of Boehm in its simplest form.
`ailang-codegen` runs an escape-analysis pre-pass over every fn
body (and every lifted lambda thunk body); allocations the pass
proves do not outlive the fn frame are lowered to LLVM `alloca`
instead of `@GC_malloc`. Allocations that may escape continue to
use `@GC_malloc`. The Boehm collector is still linked and
unchanged; this is purely an optimisation above the floor.

**Allocation mechanism: LLVM `alloca`** (not a heap arena). Stack
allocation matches the "freed at fn return" lifetime exactly,
needs no malloc/free pair, and integrates with LLVM's existing
optimiser (mem2reg / SROA may further promote the alloca'd box
to registers if the box is small and its uses are simple). No
new runtime is introduced; no language-level change; no AST or
schema change.

**Escape rule (conservative).** A `Term::Ctor` or `Term::Lam`
allocation is non-escaping iff (1) it is the value of a
`Term::Let { name = X, value = ALLOC, body = B }`, and (2) the
body `B` does not let any value derived from `X` flow past the
fn frame. "Derived from" follows two propagation rules:
- A `Term::Match` whose scrutinee is a `Var` referring to a
  tainted name propagates taint to every pattern-bound name in
  every arm. (Pattern bindings hold field projections of the
  scrutinee, which live inside the same allocation.)
- A `Term::Let { name = Y, value = Var(t), ... }` where `t` is
  tainted makes `Y` tainted in the let's body.

A tainted name "escapes" if it appears in any of: the tail
position of `B`, the arg list of any `Term::App` / `Term::Do`,
the field list of a `Term::Ctor`, or the free-var capture set of
a `Term::Lam`. The closure-pair-callee position of `Term::App`
where the callee is a bare `Var` to the tainted name is NOT an
escape (calling locally is fine).

**What this is not.** Not a region-inference system. Not
flow-sensitive within an arm. Not field-sensitive (pattern
bindings are tainted wholesale). Precision can be improved later;
correctness is the priority for this iter. A pessimistic answer
(claiming an allocation escapes when it does not) only loses
optimisation, never correctness.

**Codegen integration.** Three sites in
`ailang-codegen/src/lib.rs`:
- `lower_ctor` — ADT box.
- `lower_lambda` env block (when there are captures).
- `lower_lambda` closure pair (always 16 bytes).

Each site queries the per-fn `non_escape: BTreeSet<usize>` (raw
pointer addresses of `Term::Ctor` / `Term::Lam` AST nodes flagged
as non-escaping). On a hit the emitter writes
`alloca i8, i64 <size>, align 8`; on a miss it writes
`call ptr @GC_malloc(i64 <size>)`. The rest of the lowering (tag
store, field stores, closure-pair packing) is identical.

The closure-pair and its env share an escape verdict — they have
parallel lifetimes. If the closure pair is non-escaping, the env
is too.

## Decision 10: memory model — RC + Uniqueness with LLM-author annotations

**The GC bench (`bench/run.sh`) showed
Boehm contributing a substantial fraction of runtime on allocation-heavy workloads
that hold the heap fully live (bench notes in JOURNAL). The
mainstream "RC + inference" position is extended with mandatory
LLM-author mode annotations (`borrow` / `own`), explicit `clone`,
first-class `reuse-as`, and `drop-iterative` data attrs.**

The cost of GC is structurally in the allocate path — Boehm's
`GC_malloc` is structurally slower than a bump pointer, and the bench
workloads exercised allocate cost without collection cost.
Tracing GC's irreducible variability cannot be tuned away; RC's
costs are bounded and analysable per program point. A corpus
committed to one memory model is expensive to switch — pre-
stdlib is the cheapest moment to commit.

**Choice.** AILang's canonical memory model is reference counting
with static uniqueness inference **and explicit LLM-author
annotations on fn signatures**, in the lineage of Lean 4 / Roc /
Koka. Boehm becomes a transitional allocator (Decision 9) and is
retired when the RC pipeline matches the bump-allocator floor
within an acceptable margin (target 1.3× on `bench/run.sh`).

**Workload scope of the 1.3× target.** The 1.3× target was
calibrated on the original `bench/run.sh` corpus: linear list
sum (`bench_list_sum`) and tree walk (`bench_tree_walk`) — uniform
single-allocation-per-step workloads where one inc/dec pair
amortises against one allocation. The corpus was later extended
with `bench_closure_chain` (closure-pair allocation: each step
allocates *two* heap objects, the closure cell and its captured
env struct) and `bench_hof_pipeline` (poly-ADT + indirect
dispatch). The closure-chain fixture measures wider than the 1.3×
linear/tree target: each step pays two allocs and two decs against
one bump-pointer bump, doubling the allocation tax on closure
construction (current ratio recorded in JOURNAL bench entries).
This is a representational cost of the closure-pair layout,
not a defect in the RC implementation; a future slab/pool
allocator for fixed-shape pair cells (Decision 9 retirement
follow-up) would compress this ratio without changing semantics.

The 1.3× retirement target therefore applies to the linear /
tree / poly-ADT subset of the corpus. Closure-heavy workloads are
tracked under a wider band (the closure-chain baseline records its rc/bump ratio as the `rc_over_bump` reference value with ±15% tolerance) and
are explicitly excluded from the Boehm-retirement gate until a
slab/pool answer ships. Decision-10's RC commitment is unchanged;
what is scoped is the *quantitative* retirement criterion, not
the choice of memory model.

The architecture has two layers:

1. **Inference.** A post-typecheck pass produces a per-node
   uniqueness side table. Codegen uses it to elide inc/dec
   wherever provably redundant.
2. **LLM-author annotations.** Fn signatures carry mandatory
   `(borrow T)` / `(own T)` mode markers. Authors mark
   sharing-vs-consumption explicitly. The compiler verifies
   rather than guesses.

The combination plays to what LLMs are good at (writing slightly
more annotation per definition) and avoids what compilers are
bad at (proving sharing absent in the face of recursion +
closures + match).

### Why not other memory models

**Tracing GC.** Open-ended. Boehm's bench overhead is structurally on the allocate path (JOURNAL bench notes); tuning Boehm cannot move that
needle. A precise tracing GC would need read/write barriers,
root maps, generational machinery — months of work, with
irreducible pause-time variability at the end. The user's
framing was decisive: "Am GC kannst du ewig rumschrauben (und
bekommst trotzdem auch in 100 Jahren keine berechnbare
Performance)."

**Region inference (Tofte/Talpin / MLton-style).** Considered
seriously; rejected. Regions tie lifetimes to dynamic scope —
every value lives in some region, regions stack on entry/exit,
deallocation is bulk-by-region. The reduction: a region is an
explicit allocator with sugar plus a static check that nothing
escapes its lifetime. The deeper problem: regions assume
**stack-shaped lifetimes**. Real programs have non-stack-shaped
lifetimes — caches, memo tables, registries, lookup structures
whose lifetimes are not nested. Regions would either force these
into a `letregion` at the top of `main` (everyone's allocator
becomes the root region — useless), or require a region per
cache variant (combinatorial). RC has no lifetime-shape
assumption; it works for any DAG.

**Linear / ownership types as primary mechanism (Rust-style).**
Considered as a general-purpose alternative; rejected as primary.
Rust's borrow-checker is a great mechanism but requires the
author to thread lifetimes through every signature and accept
that some programs cannot be expressed without `unsafe`. For an
LLM-targeted language with recursion + closures everywhere, that
cost is too high — most of the source surface would be lifetime
annotations rather than logic. AILang uses a *subset* of these
ideas (mode annotations, linear consumption discipline)
selectively, layered on top of RC, where the annotations buy
concrete optimisations and never have to thread lifetimes
through callees.

### The LLM-aware sharpening

A mainstream RC implementation (think Lean 4 in default mode)
infers everything from naked AST plus a few optional hints. The
inference is conservative; whatever it can't prove unique becomes
shared and pays runtime inc/dec. AILang exploits its target
audience to push that conservative ceiling higher.

Five mechanisms.

**(1) Mandatory `(borrow T)` / `(own T)` on fn signatures.**

```
(fn list_length
  (type (fn-type (params (borrow (List Int))) (ret (con Int))))
  ...)

(fn sum_list_consume
  (type (fn-type (params (own (List Int))) (ret (con Int))))
  ...)
```

`(borrow T)` declares the parameter is read-only and lives at
most until the call returns; the caller still owns it; the
callee performs no inc/dec on it. `(own T)` declares ownership
transfer; the callee consumes the value and is responsible for
its end-of-life. The declaration is structural (visible in JSON)
and binding (the typechecker rejects bodies that contradict it).

For a Lean 4 / Roc author this is all *optional* and inferred
when omitted. AILang makes it mandatory because the LLM author
can carry the cognitive cost trivially, and the compiler gains a
precise contract at every call site instead of a probabilistic
guess.

**(2) Linear-by-default consumption with explicit `(clone X)`.**

In bodies, every binder is consumed by exactly one `own`-mode
use. If the LLM writes:

```
(let p (expensive_fn x)
  (let r1 (consume_a p)        ; consume_a takes (own); consumes p
    (let r2 (consume_b p)      ; ERROR: p already consumed
      ...)))
```

the compiler emits a structured non-linear-use diagnostic with
concrete `suggested_rewrites`:

- "make consume_a borrow": refactor consume_a's signature, no
  body change at the call site;
- "explicit clone": insert `(clone p)` at the first use;
- "fuse traversal": replace the two separate calls with a fused fn.

The LLM picks one. There is no implicit clone — sharing always
costs visible source.

**(3) Reuse hints as first-class.**

```
(fn map_inc
  (type (fn-type (params (own (List Int))) (ret (own (List Int)))))
  (params xs)
  (body
    (match xs
      (case Nil Nil)
      (case (Cons h t)
        (reuse-as xs (term-ctor List Cons (app + h 1) (app map_inc t)))))))
```

`(reuse-as SRC NEW-CTOR)` asks the codegen to allocate `NEW-CTOR`
in `SRC`'s memory slot. Compiler verifies: `SRC` is owned, this
is its last use, sizes match. On a hit: no malloc, no free — the
box is overwritten in place. On a miss: structured diagnostic
explains which precondition failed; the LLM either adjusts the
surrounding code or removes the hint.

This matches Lean 4 / Roc reuse analysis but lifts it from
"compiler-inferred when possible" to "author-asserted, compiler-
verified". The LLM applies it everywhere it expects to fire and
lets the compiler bounce the request when it can't.

**(4) `(drop-iterative)` annotation on data declarations.**

```
(data Tree (vars a)
  (ctor Leaf)
  (ctor Node a (Tree a) (Tree a))
  (drop-iterative))
```

When the refcount of a `Tree` value reaches zero, the synthesised
dec-on-zero traversal is iterative (worklist + heap-allocated
stack) instead of recursive. Avoids stack overflow on deep
structures. The LLM adds the annotation where appropriate; the
compiler refuses to emit recursive dec-cascade on annotated types.

**(5) Structured compiler diagnostics with `suggested_rewrites`.**

Every RC-mode error (use-after-consume, mode-mismatch,
reuse-as-fail, drop-cascade-too-deep) emits a JSON object
containing the failure kind, the source span, and a list of
concrete rewrite suggestions in form-A AILang. The LLM consumes
these without prose-parsing. This is the missing half of the
LLM-as-author story: the language spec defines not only what
compiles, but what the compiler tells the author when it doesn't.

### Language-design constraints (binding)

The four constraints below are necessary preconditions for RC to
be sound and complete *without* a cycle-collector backstop. They
are not new — AILang already satisfies all four — but Decision 10
makes them load-bearing rather than incidental:

1. **Strict evaluation.** Every `Term::App` argument is fully
   evaluated before the call. No laziness, no thunks. (Already
   true.)
2. **No recursive value bindings.** `(let x EXPR ...)` evaluates
   `EXPR` in a scope where `x` is *not* bound. Recursion is
   exclusively via `Term::LetRec` (which binds a fn, not a value)
   and module-level fn defs. (Already true.)
3. **No shared mutable refs.** Values are immutable once
   constructed. There is no `ref`, `IORef`, `Mutex`, or any
   primitive that allows a value to be mutated from a position
   outside its allocation. (Already true.)
4. **ADTs are acyclic by construction.** Strict evaluation +
   no-recursive-value-bindings + no-shared-mutable-refs together
   guarantee that any value graph reachable from a binding is a
   DAG. The reference graph has no cycles. (Follows from 1–3.)

Laziness, recursive value bindings, shared mutable state, or any
feature that creates cycles is rejected at design time unless the
proposal proves the cycle is collectible by an extension (e.g.
linear ownership).

### Schema additions

**Parameter modes on `Type::Fn`.**

The form-A surface for fn signatures gains mode wrappers:

```
(fn-type (params (borrow (List Int))) (ret (con Int)))
(fn-type (params (own (List Int))) (ret (own (List Int))))
```

Internally, this is *not* a new `Type` variant. Modes are
metadata on `Type::Fn` — `paramModes` and `retMode` fields run
parallel to `params` and `ret` (see §"Data model" for the JSON
schema). The substantive reasons for per-position metadata over a
`Type::Borrow` / `Type::Own` variant approach:

- **Semantic locality.** Modes are properties of fn-signature
  parameter positions, not of types in general. `Int` does not
  have a mode; a fn-parameter slot does. Embedding modes in
  `Type` would let the schema express forms like
  `(con List (borrow Int))` — syntactically possible, semantically
  meaningless (you cannot separately own/borrow a list element
  from the list it lives in). Decision 1 is "schema = data,
  schema permits exactly what is meaningful"; per-position
  metadata is the option that holds that line.
- **Compositional clarity.** A `Type` value's identity should
  depend only on the type. Two functions with the same param /
  ret types but different calling conventions share `Type::Fn.params`
  and differ only in `param_modes`. That is the right factoring:
  "what data does this carry" is one axis, "how is it transferred"
  is another. Mixing them under a single hierarchy conflates the
  two and makes both harder to reason about.
- **Future-proof against more position metadata.** If later iters
  add other per-position properties (streaming receiver, captured-
  by-closure, lifetime witness), they generalise as additional
  metadata fields on `Type::Fn` — one consistent hierarchy. The
  variant approach would force every new dimension into its own
  `Type::*` variant (`Type::Streamed`, `Type::Captured`, ...) and
  combinatorics blow up: `Type::Borrow(Type::Streamed(T))` versus
  `Type::Streamed(Type::Borrow(T))` raise questions of canonical
  ordering that don't exist when modes live in a flat metadata
  vector.

`Implicit` is the legacy / back-compat state — semantically
equivalent to `Own` but printed bare (`(con T)`, no wrapper).
`Own` and `Borrow` are explicitly annotated.

JSON canonical hash for every existing fixture stays bit-
identical: `param_modes` is skipped when every entry is
`Implicit`, `ret_mode` is skipped when `Implicit`. Existing
modules emit the same bytes as before.

**Type::Con name scoping (canonical form, since ct.1).** Within a
`.ail.json`, a `Type::Con.name` is interpreted relative to the
file's top-level `"name"` field (the owning module). Bare names
(no `.`) refer to a TypeDef in the owning module's own `defs`.
Cross-module references MUST be qualified `<owning_module>.<TypeName>`
where `<owning_module>` is a known module in the workspace.
Primitives (`Int`, `Bool`, `Str`, `Unit`, `Float`) are bare and
have no module qualifier. Bare cross-module references are a
schema violation (`WorkspaceLoadError::BareCrossModuleTypeRef`);
qualified references whose owner is unknown are also a violation
(`WorkspaceLoadError::BadCrossModuleTypeRef`). The same rule
applies to `Term::Ctor.type_name`.

Class names follow the canonical-form rule (mq.1): bare for
same-module references, `<module>.<Class>` for cross-module
references — symmetric to `Type::Con.name`'s rule from ct.1.
Three schema fields carry class references in this form:
`InstanceDef.class`, `Constraint.class`, and `SuperclassRef.class`.
`ClassDef.name` itself stays bare (defining-site context, like
`TypeDef.name`).

Method dispatch is type-driven post-mq.3 (see §"Method dispatch"
below): synth resolves a `Term::Var { name: "show" }` by consulting
the workspace's method-to-candidate-class index, filtering by
argument type (concrete) or by declared constraint (rigid-var), and
routing the residual through the registry at fn-body-end discharge.
Method-name collisions across classes are now structurally legal —
they resolve at the call site via type-driven dispatch with explicit
qualifier (`<module>.<Class>.<method>`) as the LLM-author's
disambiguation tool.

The legacy `(con T)` form is treated as `(own T)` semantically.

(An incidental observation, not a design reason: keeping `Type`
itself unchanged also avoids touching ~250 sites across the
typechecker / desugar / codegen that match on `Type` variants.
This is a tiebreaker, not a rationale — the substantive reasons
above are what justify the choice.)

**New `Term` variants.**

```
Term::Clone { value: Box<Term> }                     ; `(clone X)` — explicit RC inc
Term::ReuseAs { source: Box<Term>, body: Box<Term> } ; `(reuse-as SRC NEW-CTOR)`
```

`Term::ReuseAs` is structured as a *wrapper* around a `body`
term rather than as a `reuse_from: Option<String>` modifier on
`Term::Ctor`. Two substantive reasons:

1. **Compositional flexibility.** Reuse-as is conceptually a
   wrapper that says "this expression's allocation comes from
   `<source>`'s slot". The wrapper form generalises naturally
   if future iters introduce other allocating constructs
   (record literals, opaque box wrappers, capability cells) —
   they all become valid `body` positions. A modifier on
   `Term::Ctor` would have to be replicated on every
   constructible Term variant the language grows.
2. **Source-locality at the head.** `(reuse-as SRC NEW-CTOR)`
   reads as a single sentence with the source-binder named at
   the head. The modifier form would scatter the reuse intent
   across a child position of the constructor's argument
   syntax, separating the `source` from the rest of the
   reuse-as semantics.

The trade-off this accepts: the schema permits `Term::ReuseAs
{ body }` where `body` is not an allocating form (e.g. a
literal, a var). Such terms are caught at typecheck via a
`reuse-as-non-allocating-body` diagnostic — structural rejection
in the typechecker, not the schema. The principle: prefer
composability over schema-level rejection where the typecheck
rule is unambiguous.

**`TypeDef` attribute.**

```
TypeDef.drop_iterative: bool                         ; `(drop-iterative)`
```

All four are skipped during serialisation when absent / false /
None so canonical-JSON hashes of every fixture remain stable
until the fixture intentionally adopts the feature.

**`FnDef.suppress`.** The `suppress` field on `FnDef` carries a
list of advisory-diagnostic suppress entries; each entry has a
`code` (the diagnostic being suppressed) and a `because` (a
mandatory non-empty reason). See §"Data model" for the canonical
schema.

Form-A surface: `(suppress (code "...") (because "..."))` clause
between fn name and `(type ...)`. Multiple clauses allowed; one
per entry. Form-B (prose) renders one
`// @suppress <code>: <because>` line per entry above the doc
string — lossless, contract metadata.

Skipped from serialisation when empty so existing fixtures keep
bit-identical canonical-JSON hashes (regression-pinned by
`iter19b_empty_suppress_preserves_pre_19b_hashes` and
`iter19b_schema_extension_preserves_pre_19b_hashes`).
The canonical-form tightening in ct.1 shifted the hashes of two
cross-module fixtures (`ordering_match.ail.json` and
`test_22b1_dup_a.ail.json`); all intra-module fixtures, including
the regression-pinned `sum.ail.json` and `list.ail.json`, remain
bit-identical. The new pins are
`ct4_migrated_fixtures_have_canonical_form_hashes` (locks the
post-migration hashes) and
`ct4_unmigrated_fixtures_remain_bit_identical` (re-asserts the
existing 13a/19b/22b.1 hashes still hold).

### Advisory diagnostics

The advisory-diagnostics arc introduces the language's first
**advisory** typechecker diagnostic and the suppression mechanism
that goes with it. Decision 10's mandatory-annotation rule is
unchanged: `param_modes` and `ret_mode` remain author-required;
the typechecker does not infer them. What's new is feedback when
an authored annotation is *stricter than necessary*.

**The lint: `over-strict-mode`.** Fires on a
fn-param `p` annotated `(own T)` when:

  1. `p`'s `consume_count == 0` (uniqueness pass: the body
     never consumes `p` as a whole).
  2. For every match arm whose scrutinee is `p`, no
     **heap-typed** pattern-binder has `consume_count > 0`.

The heap-type filter is load-bearing for soundness:
`match xs { Cons(h, t) => h }` records `consume_count(h) == 1`,
but `h: Int` is read by-value — no RC traffic, no heap data
moved out of `xs`'s allocation. Filtering primitive-typed
binders is what lets the lint correctly identify `head_or_zero`
as over-strict (could be `borrow`) while staying silent on
`sum_list` where `t: List` *is* moved out.

Severity: `Warning`. `ail check`, `ail build`, `ail emit-ir` exit 1
only on at least one `Error`; warnings print but do not abort.

**The suppression: `mode-strict-because`.** Authors
who want to keep an over-strict annotation deliberately (e.g.
RC codegen-test fixtures, fns reserved for planned in-place
mutation) attach a `Suppress` entry naming the diagnostic code
and a non-empty reason. The typechecker drops matching
diagnostics from the output. Empty `because` is a hard error
(`empty-suppress-reason`); wrong-code suppresses are silent
no-ops (open-set diagnostic registry — a suppress for a code
that doesn't fire today may exist defensively for a code that
might fire after a future edit).

### Why advisory + suppress instead of inference

Three reasons, all anchored in Decision 10's framing:

  1. **Annotation states intent; inference picks
     weakest-supporting.** These often coincide today but are
     conceptually different. The annotation captures what the
     author committed to (e.g. `(own T)` reserved for a planned
     mutation that hasn't landed); inference would silently
     relax it.
  2. **Annotation is a drift-bremse.** Body change that flips
     the inferred mode produces caller-side breakage at remote
     sites. Annotation enforces the local-conflict-error pattern
     instead.
  3. **Forcing function for LLM authoring.** Without mandatory
     annotation, the LLM never has to commit to ownership intent
     before writing the body. The advisory lint plus suppress
     lets us flag accidental over-strictness without weakening
     the contract.

The suppress mechanism with mandatory-reason mirrors Rust's
`#[allow(...)]`-style escape hatch but sharpens it: the reason
is required (not optional), and it becomes part of the contract
the next reader sees. CLAUDE.md's "preserve correctness across
development cycles" is what this directly serves.

### Inference algorithm

Post-typecheck, post-`lift_letrecs`, pre-codegen pass over the
elaborated module. For each `Term` node that produces or binds a
boxed value, the pass computes a uniqueness flag:

- **Unique:** at this program point, the reference is the only
  outstanding reference to its referent.
- **Shared:** there may be multiple outstanding references.

A reference is *unique* if every path from its allocation to the
current program point passes through exactly one binding. The
inference is a forward dataflow over the AST. The annotations
(`borrow` / `own`) provide the inter-fn contract; the
inference fills in intra-fn detail.

### Codegen contract

Memory layout:

- Every heap allocation has an 8-byte refcount header, followed
  by the payload. `ailang_rc_alloc(size)` returns a pointer to
  the *payload*; the header is at `ptr - 8`.
- `ailang_rc_inc(ptr)`: load `ptr - 8`, +1, store. Non-atomic
  (single-threaded).
- `ailang_rc_dec(ptr)`: load, -1, store; if zero, recurse-dec
  child references and `free(ptr - 8)`. For `(drop-iterative)`
  types, the recursion is replaced by a worklist loop (via `drop-iterative`).

Codegen for `Term::Ctor` / `Term::Lam` env / closure pair under
`--alloc=rc` calls `ailang_rc_alloc(SIZE)`. The initial RC plumbing
stops there — inc/dec instrumentation is added once the
inference is wired up. Until then, `--alloc=rc` deliberately
leaks like the pre-Boehm era; this is purely about plumbing.

### Mode metadata is load-bearing for codegen

`param_modes` and `ret_mode` on `Type::Fn` are not merely
typechecker metadata — codegen consults both to decide where to
emit drop calls. They were promoted from
"annotation that the typechecker enforces" to "annotation that
codegen reads to keep RC correct". Recorded here so the schema
metadata's role is explicit:

**`param_modes` — drop-emission gates.**

- **Iter B: Own-param dec at fn return.** When a fn body
  fall-throughs to a `ret` (no tail-call), every parameter with
  `param_modes[i] == Own` is dec'd before the `ret` iff its
  uniqueness `consume_count == 0` and the ret value is not the
  param itself. `Borrow` and `Implicit` parameters are skipped:
  `Borrow` retains the caller's ownership by contract;
  `Implicit` carries no static caller-handed-off-ownership
  signal (it's the back-compat lane).

- **Iter A: arm-close pattern-binder dec.** When a match-arm's
  body terminates without a tail-call, every ptr-typed
  pattern-bound binder pushed by the arm is dec'd at arm close
  iff its `consume_count == 0` and it is not the arm's tail
  value, **gated on the scrutinee's static ownership**. If the
  scrutinee is a fn-param, only `Own`-mode scrutinees enable
  the dec — `Borrow` and `Implicit` scrutinees would let the
  arm dec memory the caller still references.

- **Pre-tail-call shallow-dec.** When a match-arm's
  body IS a tail call, both Iter A and Iter B are skipped (the
  block is terminated). A separate seam in `lower_match` emits
  a shallow `ailang_rc_dec` on the scrutinee outer cell BEFORE
  the tail call, gated identically on the scrutinee mode plus
  the requirement that every ptr-typed slot in the active
  ctor's pattern is in `moved_slots[scrutinee]`.

**`ret_mode` — let-binder trackability.**

- **`Term::App` drop at let-scope close.** A
  let-binder whose value is `Term::App { callee, .. }` is
  trackable for scope-close drop iff the callee's
  `ret_mode == Own`. The signal is the callee's static
  contract that ownership of the freshly heap-allocated cell
  flows to the caller. `Borrow`-returning calls remain
  non-trackable (the callee retains ownership; the caller
  holds a view, not an own ref). `Implicit`-returning calls
  remain non-trackable (back-compat lane).

The drop fn's symbol resolution for an Own-returning App:
synthesise the call's return type, resolve `Type::Con { name }`
to `drop_<owner>_<T>` (with cross-module qualification through
the import map). Falls back to shallow `ailang_rc_dec` for
returns that are not `Type::Con` (e.g. unresolved type vars on
a polymorphic call's pre-monomorphisation site; the
monomorphised copies resolve to concrete drop fns).

#### Arg-position policy for compound AST nodes

The uniqueness and linearity passes walk arguments of compound
nodes with a fixed `Position` policy. For ownership-bearing nodes:

| Node                 | Arg position | Reason                                                                                |
|----------------------|--------------|---------------------------------------------------------------------------------------|
| `Term::Ctor.args[*]` | Consume      | constructor packs values into the cell; the cell owns them afterwards                 |
| `Term::Do.args[*]`   | Borrow       | effect-op observes its arguments; the caller still owns whatever pointer it passed in |

The two policies are language rules, not per-op annotations. They
do not appear as fields on `EffectOpSig` or `Ctor`; the AST node
kind itself carries the default. The walkers that read this policy
live at `crates/ailang-check/src/uniqueness.rs` and
`crates/ailang-check/src/linearity.rs` (matched arms in both).

The Do = Borrow rule pairs with the `ret_mode == Own` letbinder-
trackability rule above: when a built-in such as `int_to_str` is
declared `ret_mode: Own` and its result is fed into an effect-op
(`io/print_str s`), the let-binder is RC-tracked for scope-close
drop *and* the effect-op does not consume it — the slab is freed
exactly once at scope close, never zero-times (RC leak under the
old Consume rule, which silenced the scope-close drop) and never
twice (double-free under a hypothetical Consume + scope-close).

**What this widening does NOT do.**

- Does not change the canonical hash. `param_modes` /
  `ret_mode` were already hash-load-bearing when introduced;
  subsequent work added codegen consumers, not new schema fields.
- Does not introduce a new `Type` variant. Mode metadata stays
  flat on `Type::Fn` (see "Schema additions" above on why).
- Does not cover let-aliases of borrowed values. A let-binder
  whose value is `Term::Var` referencing a `Borrow`-mode
  param is not yet propagated through; the param-mode gates
  treat such a binder as "owned" (its `current_param_modes`
  lookup misses, default = owned). This is a known carve-out
  shared by Iter A and the pre-tail-call shallow-dec arm; closing it is a propagation pass
  through let-bindings that has not shipped yet.

### Adjacent extensions for mutability (out of Decision 10's scope)

If future workloads need mutable arrays, hash tables, or other
inherently mutable primitives, the answer is **not** a tracing GC
backstop. The answer is a separate ownership/linear extension
that gates mutability behind static single-owner discipline. RC
+ uniqueness is the universal floor; ownership extends it for
specific high-performance primitives without rebreaking the
acyclicity invariant.

### What this Decision deliberately does not do

- **Does not infer everything.** AILang demands annotations
  *because* the LLM author can produce them effortlessly. The
  compiler does inference *plus* verification of contracts.
- **Does not require existing fixtures to migrate immediately.**
  `(con T)` is treated as `(own T)`. Existing JSON hashes
  stay bit-identical until the fixture is intentionally updated.
- **Does not commit to atomic refcounts.** AILang is
  single-threaded; refcounts are non-atomic. The embedding ABI's
  per-thread `ailang_ctx_t` keeps this correct under a host swarm:
  each thread's allocations are private to its ctx, no RC cell
  crosses a thread, so non-atomic refcounts stay sound.
- **Does not introduce regions.** Regions were considered and
  rejected; see "Why not other memory models" above.

## Decision 11: typeclasses — Haskell-lite, monomorphised, coherent

**The design pass for typeclasses. Codified after the Feature-acceptance
criterion (this document, above) was committed; the criterion is
the explicit basis for the choices below.**

AILang ships typeclasses to compress a real LLM-author redundancy:
without them, every comparable function must be written per-type
(`int_eq`, `string_eq`, `bool_eq`, `int_show`, `string_show`, …). With
typeclasses behind a monomorphising compiler, the LLM author writes
one signature with a class constraint and one method per concrete
type, and the compiler emits the same machine code as the per-type
version. No runtime cost, no dictionary passing, no vtables.

**Choice.** A deliberately narrow typeclass design — narrower than
Haskell, narrower than Rust traits — calibrated to what an LLM
author naturally produces. Five semantic axes are committed:

1. **Scope.** Multi-method, single-parameter, optional defaults,
   single-superclass relation. No multi-param classes, no
   functional dependencies, no associated types.
2. **Constraints in signatures.** Explicit and mandatory. A
   function that calls a class method must declare the constraint
   in its `forall` block. No constraint inference.
3. **Resolution.** Orphan-free coherence. An `instance C T` may be
   declared only in the module of `C` or in the module of `T`.
   Resolution is global type-directed against a workspace-built
   registry; coherence makes the lookup unambiguous.
4. **Defaults.** Opt-in via an explicit `default` keyword in the
   class body. Methods without `default` are abstract-required;
   methods with `default` may be overridden or inherited per
   instance.
5. **Class-parameter kind.** Concrete types only (kind `*`). No
   higher-kinded class params; `Functor`/`Monad`-style abstractions
   over type constructors are not expressible. The LLM-natural
   pattern is `List.map` / `Tree.map` as separate functions per
   type, which monomorphisation handles directly.

The five axes follow from the Feature-acceptance criterion: each
rejected mechanism (multi-param, higher-kinded, FunDeps, assoc
types) is one an LLM author does not unprompted produce.

### Form-A schema (the JSON authoring surface)

Three additive schema extensions; no existing module becomes invalid.

**`ClassDef`** — top-level definition kind, declares a class:

```
{ "kind": "class",
  "name": "Show",
  "param": "a",
  "superclass": null,
  "methods": [
    { "name": "show",
      "type": { /* full FnSig over `a`, with mode annotations */ },
      "default": null
    }
  ]
}
```

`superclass` is either `null` or `{ "class": <name>, "type": "a" }`
where `"a"` MUST be the same identifier as the class's own `param`.
`default` is either `null` (method is abstract-required at instance
sites) or an AST body (method is optional with the body as fallback).

**`InstanceDef`** — top-level definition kind, declares an instance:

```
{ "kind": "instance",
  "class": "Show",
  "type": "Int",
  "methods": [
    { "name": "show", "body": <AST> }
  ]
}
```

`type` is a concrete type expression, never the class param. `methods`
contains the bodies for every required method plus optional overrides
of default-bearing methods.

**`FnDef.type` extension** — the existing FnSig schema gains a
`constraints` sibling field next to `forall`:

```
"type": {
  "forall": ["a"],
  "constraints": [{ "class": "Show", "type": "a" }],
  "type": ["Fn", [...], "String"]
}
```

When `forall` is empty, `constraints` is also empty (and may be
omitted for hash stability of older definitions). Each constraint's
`type` field MUST reference a type variable bound by the surrounding
`forall`.

**Method invocation sites do NOT get a new node.** A call to a class
method is a normal `Call` node; resolution against a class is the
typechecker's job, not the parser's. The LLM author writes `show x`
exactly as for any free function.

### Resolution and monomorphisation

**Constraint collection (per function body).** During typechecking
of a body, each method call generates a residual constraint of shape
`<Class> <Type>` where `<Type>` may still contain type variables.
After local typechecking, residual constraints are checked against
the function's declared constraints (modulo α-conversion and modulo
auto-expansion through superclasses; see below). Any residual not
covered by declared constraints fires `MissingConstraint`.

**Instance registry (workspace-global).** At workspace load (see
`crates/ailang-core/src/workspace.rs`), all `InstanceDef` nodes
across all reachable modules are collected into a registry keyed by
`(class-name, canonical-hash-of-instance-type)`. Registry build
performs three checks:

- **Coherence.** Each instance's module must be either the class's
  defining module or the instance type's defining module. Otherwise
  → `OrphanInstance`.
- **Uniqueness.** No two entries share a key. Otherwise →
  `DuplicateInstance`.
- **Method completeness.** Each instance specifies every required
  (non-default) method of its class. Otherwise → `MissingMethod`.

Registry build is a one-time-per-build pass that fires before any
typechecking. Its errors are workspace-load errors, not per-call-site
errors.

**Resolution at call sites with concrete types.** When the typechecker
sees a method call where every type variable in the constraint is
substituted to a concrete type, it queries the registry. Hit →
resolved. Miss → `NoInstance`.

**Resolution at polymorphic call sites.** When type variables are
still free, the constraint propagates into the surrounding function's
constraint context — which the user MUST have declared explicitly
(per axis 2). No constraint is implicitly hoisted.

**Monomorphisation (post-typecheck, pre-codegen).** A pass between
typechecking and codegen replaces every call to a
`Type::Forall`-quantified `Def::Fn` with a call to a synthesised
monomorphic `FnDef`. Two source-body entry points share the same
mechanics in one fixpoint:

1. **Class-method entry.** For each unique `(method, concrete-type)`
   pair produced by a class-constraint residual, the pass looks up
   the resolved instance body via `Registry::entries[(class,
   type-hash)]`, substitutes the class parameter to the concrete
   type, and synthesises a top-level `FnDef` named
   `<method>__<type-surface-name>`.
2. **Free-fn entry.** For each call site to a polymorphic free
   `Def::Fn` with a fully-concrete substitution, the pass takes the
   source body directly from the polymorphic `Def::Fn`, applies
   rigid-var substitution on both the type AND the body (the body
   may contain inner `Term::Lam`s whose `param_tys` reference the
   outer Forall vars), and synthesises a top-level `FnDef` named
   `<name>__<type-surface-name-1>__<type-surface-name-2>__…`
   (concatenated in `Type::Forall.vars` declaration order; the
   N-ary case extends the single-type-var class-method shape
   bit-stably).

Both arms share:

- A fixpoint loop that keeps collecting targets until a round adds
  nothing new (a synthesised free-fn body may invoke class methods
  at concrete types, scheduling new class-method targets; a
  class-method body may invoke polymorphic free fns at concrete
  types, scheduling new free-fn targets).
- A dedup cache keyed by `(kind, base-name,
  type-hash-or-joined-hashes)` where the first component
  (`"class"` / `"free"`) guarantees disjoint keying across the
  two kinds.
- A call-site rewrite walker that rewrites bare polymorphic call
  sites — class-method-named OR poly-free-fn-named — to their
  mono symbols before codegen runs. The walker advances a single
  cursor over interleaved class-method and free-fn slots emitted
  in synth's traversal order.

After this pass, the IR contains no polymorphism, no class
machinery, no polymorphic call sites — only ordinary monomorphic
functions and direct calls. Codegen sees no difference between a
hand-written `show_int` and a synthesised `show__Int`.

**Why mono, not virtual dispatch.** Monomorphisation makes the call
target visible to the optimiser, unlocking inlining and downstream
loop transformations that virtual dispatch prevents in principle.
On a saturating branch predictor with a monomorphic indirect
target, the indirect call itself is comparable in cost to a
non-inlined direct call — the win is in what the optimiser can do
with the visible target, not in the call instruction. The
end-to-end gain shrinks toward zero on larger callee bodies and
cold call sites, but the architectural claim — "mono enables
optimisations vdisp forbids" — holds across the spectrum
(`bench/mono_dispatch.py` and the corresponding JOURNAL bench-notes
entry record the measured ratios).

The separator is `__` rather than `#` or `@` because `#` and `@`
are invalid in LLVM IR global identifiers (the IR verifier rejects
them inside `@ail_<module>_<def>` mangled names). `__` is legal in
both LLVM IR and the C ABI used by the runtime glue, and parses
unambiguously into `<method>__<type-surface-name>` because neither
component contains `__` by project convention.

**No runtime dispatch, no dictionary passing.** The monomorphisation
pass is the ONLY specialiser. Codegen sees only monomorphic
`Def::Fn`s and direct calls; the pre-iter-23.4 codegen-time
specialiser (`lower_polymorphic_call` + `module_polymorphic_fns` +
`mono_queue`) was removed in iter 23.4. A call that cannot be
monomorphised — for instance, because a constraint remains
unresolved at the entry point — is a static error, not a runtime
one. This is the LLVM-friendly form and is consistent with
Decision 10's performance commitment.

### Cross-module references in synthesised bodies

The unified mono pass (per Decision 11's milestone-23.4 reorganisation)
synthesises mono symbols for polymorphic free fns and class-method
instances in the symbol's owner module — e.g. `print__Int` lives in
`prelude` (because `print` is defined in the prelude), but a
user-ADT call site `print (MkIntBox 7)` causes synthesis of
`prelude.print__IntBox` whose body references
`show_user_adt.show__IntBox` (the user instance lives in the
user-defining module per Decision 11 coherence). The synthesised body
crosses a module boundary the source template did not.

Three invariants make this work, all installed in milestone 24's iter
24.3 and worth keeping load-bearing:

1. **`MonoTarget::FreeFn::type_args` carries canonical types
   post-collection.** At every site where `subst.apply(m)` produces a
   concrete substitution that enters `MonoTarget::FreeFn::type_args`
   (`crates/ailang-check/src/mono.rs::collect_mono_targets` and
   `::collect_residuals_ordered`), the resolved `Type` must be passed
   through `Registry::normalize_type_for_lookup(caller_module, &t)`
   before being pushed. The downstream synthesised body's Phase 3
   rewrite cursor (which runs in the OWNER module's context, not the
   caller's) keys lookups in `Registry::entries` by the canonical
   qualified form; a bare type-con reference at the type_args layer
   silently drops the cross-module mono-symbol synthesis and leaves a
   bare `Var "show"` post-mono that codegen later rejects with
   `unknown variable`.

2. **Post-mono synthesised body cross-module references may bypass
   the source template's `import_map`.** `prelude` does not import
   user modules (the auto-injection runs one-way: user workspaces
   import prelude, never the inverse). But a synthesised body for
   `prelude.print__<UserType>` references `<user_module>.show__<UserType>`,
   created by mono — not by the prelude source. Codegen's
   cross-module name-resolution must accept this: at
   `crates/ailang-codegen/src/lib.rs::resolve_top_level_fn` (Var-
   resolution), `::lower_app`'s cross-module call arm, and
   `::synth_with_extras`'s Var arm, the resolution first tries the
   current module's `import_map`, then falls back to a direct
   `module_user_fns` / `module_def_ail_types` lookup against the
   prefix. Both ends were independently typechecked under their own
   module contexts before mono ran; the cross-module reference is a
   post-mono construct, not a source-language one.

3. **FreeFnCall synth pushes one residual per declared forall-
   constraint.** At `crates/ailang-check/src/lib.rs`'s synth Var arm
   for the `prefix.suffix` free-fn path, when the type is a
   `Type::Forall { vars, constraints, body }`, instantiation produces
   fresh metavars for the `vars` AND pushes one `ResidualConstraint`
   per entry in `constraints` (with rigid vars substituted by the
   freshly-generated metavars). The downstream discharge loop at
   `check_fn`'s post-synth phase resolves each residual against the
   workspace registry; if no instance satisfies the residual at the
   unified concrete type, the `NoInstance` diagnostic fires at
   typecheck (correctly), not at codegen (confusingly). Without the
   residual push, milestone-23-shape negative cases (e.g. `print f`
   where `f : Int -> Int`) silently typecheck and surface as
   `unknown variable: show` from codegen instead of the right
   typecheck-phase NoInstance Show.

The three invariants are lockstep partners: invariant (1) creates the
cross-module reference, invariant (2) makes codegen able to resolve
it, invariant (3) makes the typecheck-time discharge fire correctly
when no instance exists. A future refactor that loosens any one of
the three breaks the user-ADT trajectory; the test pins at
`crates/ail/tests/codegen_import_map_fallback_pin.rs` (invariant 2),
`crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` (invariant 3
+ lockstep), and the existing `crates/ail/tests/show_user_adt`
fixture (full trajectory) collectively protect the contract.

### Defaults and superclasses

**Defaults.** A `ClassDef.methods[i].default` is either `null` (the
method is required at instance level) or an AST body. When an
`InstanceDef` does not specify a method that has a default, the
typechecker uses the default body for that instance, with the class
param substituted to the instance type. Default bodies may call
other methods of the same class (the canonical example is
`default ne x y = not (eq x y)`); the called methods resolve at
monomorphisation time against the same instance.

**Superclasses.** A `ClassDef.superclass` of `{ "class": "Eq",
"type": "a" }` declares that any `instance C T` requires a
corresponding `instance Eq T` to exist. The check fires at
workspace-load time: for each `InstanceDef` whose class declares a
superclass, the registry is queried for the matching superclass
instance. Missing → `MissingSuperclassInstance`.

**Superclass auto-expansion in constraint contexts.** When a function
declares `Ord a` as a constraint, the typechecker treats the constraint
context as `{ Ord a, Eq a }` for the purposes of `MissingConstraint`
checking. This is the one deviation from "alles sichtbar": the
extension is anchored in the class's own `superclass` field, so the
relation is schema-visible at the class declaration even when the
constraint at the function site reads `Ord a` alone.

Superclass chains are linear (single-superclass relation per class)
and auto-expansion closes transitively across the chain.

**No `deriving`.** AILang does not auto-derive instances. `instance Eq
MyType` must be written by hand.

### Diagnostic categories

The typeclass layer introduces three families of diagnostics. Exact
wording is fixed; the categories and their triggers are:

**Workspace-load (registry-build) diagnostics:**

- `OrphanInstance` — instance is not in class's or type's module.
- `DuplicateInstance` — two instances match the same key.
- `MissingSuperclassInstance` — superclass instance absent.
- `MissingMethod` — instance omits a required method.
- `OverridingNonExistentMethod` — instance specifies a method not in
  the class.

(`MethodNameCollision` was retired at iter mq.3. Cross-class method
sharing is now structurally legal; ambiguity surfaces at the call
site via `AmbiguousMethodResolution` or, for class-fn name overlap,
via the `class-method-shadowed-by-fn` warning. See §"Method
dispatch" below.)

**Class-schema diagnostics** (validation of class declarations):

- `InvalidSuperclassParam` — superclass `type` differs from the
  class's own `param`.
- `ConstraintReferencesUnboundTypeVar` — a constraint mentions a
  type variable not bound by the surrounding `forall`.

A class param appearing in applied position (e.g., `f a` where `f`
is the class param) is rejected earlier by the canonical-form
validator as `BareCrossModuleTypeRef` — `f` is a bare,
non-primitive name not declared as a `TypeDef` in the owning
module — so the dedicated `KindMismatch` diagnostic was retired
at iter ctt.3.

**Typecheck diagnostics** (per function body):

- `MissingConstraint` — body's residual constraint is not covered
  by declared (and superclass-expanded) constraints.
- `NoInstance` — fully concrete constraint has no registry entry.
  mq.2 adds an optional `candidate_classes` field surfacing the
  multi-candidate set when the bare-method dispatch path's filter
  collapses to zero registry survivors.
- `AmbiguousMethodResolution` (mq.2) — a monomorphic `Term::Var`
  call site survives both type-driven and constraint-driven filters
  with more than one candidate class. LLM-author writes the explicit
  qualifier form `<module>.<Class>.<method>` to disambiguate.
- `UnknownClass` (mq.2) — an explicit class qualifier in
  `Term::Var.name` names a qualified class that is not in the
  workspace's candidate-class index for the method.
- `class-method-shadowed-by-fn` (mq.3, warning) — a `Term::Var`
  resolved via fn lookup precedence (locals → caller-module-fn →
  imported-fn) while a class method of the same name also exists
  in the workspace. Fn resolution proceeds; the warning surfaces
  the shadow so the LLM-author can disambiguate via explicit
  class-qualified call if the shadow was unintentional.

There is no `AmbiguousInstance` diagnostic at the registry level —
coherence (`DuplicateInstance` at registry build, W2) makes
per-`(class, type)` ambiguity structurally impossible. Cross-class
method ambiguity is a separate concern resolved at the call site
via `AmbiguousMethodResolution` (see §"Method dispatch" below).

### Method dispatch

Post-mq.3, dispatch is two-mode:

**Polymorphic call sites** (inside a fn body with `forall` +
constraint set): the constraint names the class via the qualified
`Constraint.class` field (canonical-form per mq.1). Synth's
residual carries the class name directly; constraint-discharge at
fn-body-end matches against the workspace registry by
`(class, type_hash)` key.

**Monomorphic call sites**: synth consults the workspace-flat
`Env.method_to_candidate_classes: BTreeMap<MethodName,
BTreeSet<QualifiedClassName>>` index, then runs the 5-step
dispatch rule:

1. Parse the `Term::Var.name` for an optional class qualifier
   (last-dot-segment is the method name; everything before is the
   qualified class).
2. If `method_to_candidate_classes` has no entry for the method
   name, fall through to the existing Var-arm branches (free fn
   lookup, dot-qualified cross-module).
3. Qualifier present: filter candidates to the named class. Empty
   result fires `UnknownClass`. Singleton survivor proceeds.
4. Qualifier empty (bare-method form): singleton candidate proceeds
   directly; multiple candidates yield a multi-candidate residual
   for discharge-time refinement.
5. At discharge, refinement runs: concrete `type_` filters
   candidates via the workspace registry; rigid-var `type_` filters
   via the active fn's declared constraints
   (`env.active_declared_constraints`). Single survivor discharges;
   multiple survivors fire `AmbiguousMethodResolution` (concrete) or
   `MissingConstraint` (rigid-var); zero survivors fire `NoInstance`
   (concrete) or `MissingConstraint` (rigid-var).

The `method_to_candidate_classes` index is the load-bearing data
structure for this routing — its construction in `build_check_env`
inverts the per-module `class_methods` maps (themselves tuple-keyed
by `(qualified-class, method)` post-mq.3) to a workspace-flat
method-name-to-class-set map.

Class-fn collisions resolve at the call site, not at workspace load
time: the fn lookup precedence (locals → caller-module-fn →
imported-fn) runs ahead of the class-method branch. When both
sides have a match, the fn wins and a `class-method-shadowed-by-fn`
warning surfaces the shadow.

### What the typeclass design explicitly does NOT support

Each of the following is rejected by either schema (parser cannot
express the construct) or by an enumerated diagnostic. The
combination of axis-1 (single-param, no FunDeps, no assoc) and
axis-5 (kind `*` only) covers the space.

- **Multi-parameter classes** (`class Foo a b where ...`). Schema
  rejects: `ClassDef.param` is a string, not a list.
- **Higher-kinded class params** (`class Functor f`). Rejected at
  workspace-load time: `BareCrossModuleTypeRef` from canonical-form
  validation fires before class-schema validation if any method
  body uses the param as a `Type::Con` head — bare non-primitive
  names must be declared as a `TypeDef` in the owning module, and
  a class param is not.
- **Higher-rank polymorphism** (`forall a. (forall b. b -> b) -> a`).
  Already rejected at parse time per the typeclass-conversation
  rationale recorded in JOURNAL; constraint-bearing
  signatures inherit that prohibition.
- **Existential / dyn dispatch** (`exists a. Show a => a`,
  heterogeneous lists like `[Show]`). Schema does not express
  existentials. The LLM-natural alternative is sum types.
- **Associated types** (`class Container c where type Element c`).
  Schema does not express type-level methods.
- **Functional dependencies** (`class Convert a b | a -> b`). Required
  only for multi-param classes; entails by axis 1.
- **`deriving` / auto-derivation** (`data Foo = ... deriving (Eq)`).
  Future iteration, gated separately on Feature-acceptance.
- **Numeric literal defaulting.** `1` does not auto-resolve to `Int`
  under an ambiguous `Num a` constraint. Bare polymorphic literals
  with multiple satisfying instances fire `NoInstance` with a hint
  to annotate. The LLM-author writes `1 : Int` or `1 : Float`.
- **Orphan-with-warning mode.** Coherence is hard. `OrphanInstance`
  is always an error, never a warning. The corollary `--allow-orphans`
  flag is not provided.

### Prelude (built-in) classes

Milestone 22 ships **no built-in Prelude classes**.
An earlier draft committed to a fixed Prelude (Show / Eq / Ord on the
primitives), but the implementation work to wire `int_to_str` as a
heap-allocated-string runtime primitive proved substantively
separable from the typeclass machinery itself, and the LLM-utility
case for primitive `Show` is weak (LLM-natural form is `int_to_str
x`, not `show x` through a single-instance class). The user-class
end-to-end path is the milestone's typeclass acceptance gate
(the user-defined-class fixture: `class Foo a` + `data IntBox` +
`instance Foo IntBox`); see `docs/specs/2026-05-09-22-typeclasses.md`
"Amendments" for the substantive rationale.

Milestone 23 amends the above: the prelude now ships the `Ordering`
ADT, the `Eq` and `Ord` classes, primitive `Eq Int/Bool/Str` and
`Ord Int/Bool/Str` instances, and the five polymorphic free-fn helpers
`ne` / `lt` / `le` / `gt` / `ge`. Operator routing through `Eq`/`Ord`
and `print`-rewire remain out of scope per their original substantive
reasons (bench rebaseline, milestone-24 dependency on the post-mq
dispatcher); `Show` itself ships in milestone 24. Float has neither
`Eq` nor `Ord` instance per §"Float semantics"; a polymorphic helper
invoked at Float fires `NoInstance` at typecheck with a Float-aware
diagnostic cross-referencing this section.

Milestone 24 amends the above further: the prelude ships `class Show
a where show : (a borrow) -> Str` and primitive `Show Int`,
`Show Bool`, `Show Str`, `Show Float` instances (iter 24.2). Float
**is** included in Show (unlike Eq/Ord) — IEEE-754 makes structural
equality and total ordering semantically dubious, but textual
representation of a Float is well-defined modulo the NaN-spelling
caveat in §"Float semantics". Each `Show <T>` instance body is a
single-application lambda invoking the corresponding runtime primitive
(`int_to_str`, `bool_to_str`, `str_clone`, `float_to_str`); no codegen
intercept is required. The polymorphic helper `print : forall a. Show
a => a -> () !IO` shipped in iter 24.3 with body
`\x -> let s = show x in do io/print_str s` (explicit let-binder for
heap-Str RC discipline per eob.1 Str carve-out). The let-binder is
structurally pinned by `crates/ail/tests/print_mono_body_shape.rs`.
Routing through `print` is the path for non-`Str` primitives;
`io/print_str` is the only built-in direct-output effect-op.

### Heap-Str primitives

The runtime ships a small family of operations that produce or
transform heap-allocated `Str` values uniformly across static-Str
and heap-Str inputs (the consumer ABI is identical between
realisations — see §"Str ABI"). All take their input(s) by `borrow`
and return an owned `Str`. Each is registered as a builtin in
`crates/ailang-check/src/builtins.rs`, lowered inline in
`crates/ailang-codegen/src/lib.rs::lower_app` to a `call ptr @ailang_<name>`,
and backed by a `runtime/str.c` C helper.

- `int_to_str : (borrow Int) -> Str` (iter 24.1) — decimal rendering
  of an `Int`. Backs `Show Int` in the prelude.
- `bool_to_str : (borrow Bool) -> Str` (iter 24.1) — `"true"`/`"false"`.
  Backs `Show Bool` in the prelude.
- `float_to_str : (borrow Float) -> Str` (iter 24.1) —
  type-installed; codegen is reserved and not yet shipped.
- `str_clone : (borrow Str) -> Str` (iter 24.1) — allocates a fresh
  heap-Str copy of the input's bytes. Backs `Show Str` in the prelude.
- `str_concat : (borrow Str, borrow Str) -> Str` (iter str-concat,
  2026-05-13) — combines two `Str` values into a single owned `Str`.
  General-purpose; commonly used in Show bodies for labelled output
  (`(app str_concat "label=" (app int_to_str x))`).

The four Show-backers above are not directly observable to the
LLM-author writing a `Show <T>` instance — the prelude's instance
bodies dispatch into them. `str_concat` IS directly observable
because the LLM-author calls it explicitly when authoring an
instance body that wants to combine fragments.

Primitive output for `Str` values goes through `io/print_str`
directly; values of other primitive types route through the
polymorphic `print` helper (§"Polymorphic print"), which feeds
the heap-Str result of `show x` into `io/print_str`.

`==`, `<`, `<=`, `>`, `>=` REMAIN primitive operators (unchanged
from the original draft). Class methods are accessed by name (`eq x y`,
`lt x y`, …), not via these operators. Routing operators through
classes is deliberately deferred — it would require migrating every
existing fixture and would re-baseline the bench corpus, which is a
new-baseline decision rather than an iter detail.

`Num` is NOT in milestone 22. Arithmetic operators (`+`, `-`, `*`,
`/`) stay primitive and per-type. Class-based numeric overloading
would invoke literal-defaulting which axis-7 already excluded.

### What this decision does NOT commit to

- **Operator routing.** `==`, `<`, etc. stay primitive in milestone
  22. Class-routing operators is a future-iteration option, not a
  Decision-11 commitment.
- **Form-B (prose) projection of class/instance.** The prose
  renderer for the class/instance schema nodes is one-way (no
  parser by design); the render in
  `crates/ailang-prose/src/lib.rs` is a placeholder and
  informational only.
- **Specific monomorphised-symbol naming format.** Milestone 22
  uses `<method>__<type-surface-name>` for primitive type targets
  (e.g. `show__Int`) and `<method>__<8-hex-prefix>` for compound
  types (where `<8-hex-prefix>` is the BLAKE3 hash of the canonical
  type bytes). The `__` separator was chosen over `#` and `@` for
  LLVM IR identifier legality.
- **Mode annotations on class methods.** Class method signatures
  ARE full FnSigs and DO carry mode annotations per Decision 10;
  the convention is `borrow` for read-only methods. User-defined
  classes pick modes per method.
- **Number of Prelude classes.** Milestone 22 ships zero (no
  Prelude). A future Prelude milestone gates class additions on
  the Feature-acceptance criterion at the time of proposal.

## Roundtrip Invariant

Every well-formed AILang module has a canonical `.ail.json`
representation (the hashable, content-addressed JSON-AST) and a
hand-authored `.ail` representation (Form A, the authoring
projection). The JSON-AST is derived from `.ail` in-process by
consumers that need it; the round-trip is now the *property* of
that derivation, not the byte-level agreement of two on-disk forms.

Concretely:

1. **Parse-determinism.** For every well-formed `.ail` text `t`,
   `ailang_surface::parse(t)` produces a unique AST. The parser is
   a pure function of input — no randomness, no time dependence,
   no environment leak. Hashing `canonical::to_bytes(parse(t))` is
   therefore well-defined for any `.ail` source.

2. **Idempotency under print.** For every well-formed `.ail` text
   `t`, `canonical(parse(t)) == canonical(parse(print(parse(t))))`.
   The printer is a left-inverse of the parser modulo canonical
   form: print-then-parse is a no-op on the canonical bytes.

3. **CLI-pipeline idempotency.** For every `.ail` fixture, the
   public CLI pipeline `ail parse | ail render | ail parse` is
   byte-identical to direct `ail parse` of the source `.ail`.
   Pins drift that crate-internal tests cannot see.

4. **Carve-out anchor.** Seven `.ail.json`-only fixtures
   (subject-matter rejection tests) survive in the corpus by
   structural necessity. They participate in their own dedicated
   rejection-shape tests, not in the round-trip gate. (The prelude is
   embedded as `examples/prelude.ail` in `ailang-surface` and parsed
   at compile time via `ailang_surface::parse_prelude`.)

Hashing is the consequence the language depends on: BLAKE3 of the
canonical bytes is well-defined for any `.ail` source via parse-
determinism. An LLM author writes `.ail`; the build derives the
canonical hash without ambiguity.

### Float literals are inside the invariant

Float literals carry an IEEE-754 bit pattern, not a decimal
approximation. The canonical encoding is
`{"kind":"float","bits":"<16-lowercase-hex>"}` and the surface
emits the same bits-hex string. NaN, ±Inf, signed zero, and subnormals all
round-trip exactly because the JSON-number path is bypassed (see
§"Float semantics", "Form-A serialisation"). Floats are not an
exception to the invariant — the bits-hex encoding is the
mechanism that keeps them *inside* it.

### Enforcement

The invariant is workspace-CI-enforced by five tests, each
operating on the `examples/` corpus via dynamic `read_dir`
collection (no hardcoded fixture list, so newly added fixtures
inherit the gate automatically):

- `crates/ailang-surface/tests/round_trip.rs::parse_is_deterministic_over_every_ail_fixture`
  — for every `.ail`, parse twice and assert canonical-byte
  equality between the two ASTs. Direction 1 above.
- `crates/ailang-surface/tests/round_trip.rs::parse_then_print_then_parse_is_idempotent_on_every_ail_fixture`
  — for every `.ail` text `t`, `parse(t)` and `parse(print(parse(t)))`
  produce canonical-byte-equal AST. Direction 2 above.
- `crates/ail/tests/roundtrip_cli.rs::cli_parse_then_render_then_parse_is_idempotent`
  — for every `.ail`, the public CLI pipeline `ail parse | ail render | ail parse`
  reproduces canonical bytes byte-identical to direct `ail parse`.
  Pins drift internal tests cannot see.
- `crates/ailang-core/tests/schema_coverage.rs::every_ast_variant_is_observed_in_the_fixture_corpus`
  — every variant of `Def`, `Term`, `Pattern`, `Literal`, `Type`,
  and `ParamMode` appears in at least one `.ail` fixture (corpus
  flipped from `.ail.json` to `.ail` at iter form-a.1). New AST
  variants fail compile until the visitor and corpus are extended
  in lockstep.
- `crates/ailang-core/tests/carve_out_inventory.rs::examples_ail_json_inventory_matches_carve_outs`
  — exactly the seven named carve-out files exist under
  `examples/*.ail.json` at any commit. A new `.ail.json` or a
  missing carve-out fails the test.

A new fixture or a new AST variant that violates the invariant
fails one of these tests; the fix is in render or parse code,
never by relaxing the test.

### Why this is anchored at top level

The invariant is a property of the language identity, not of any
one surface-design Decision. Decision 6 introduces the `.ail`
surface and lists round-trip-as-property as one of its
constraints, but the property is load-bearing for every
downstream concern that treats the two forms as exchangeable:
content-addressed hashing, the LLM-author's choice of authoring
form, the integrity of fixture cross-references, and the
prerequisite for empirical cross-model authoring-form studies.
Lifting it out of Decision 6 makes the property quotable on its
own and reviewable by the architect agent at every milestone
close.

## Mangling scheme

All AILang functions are mangled to `@ail_<module>_<def>` — even in the
single-module case. Constants likewise (`@ail_<module>_<const>`). Global
string literals carry a short hint for readability:
`@.str_<module>_<hint>_<idx>` (e.g. `@.str_sum_fmt_int_0`). The entry point
is a `define i32 @main()` trampoline (C / LLVM ABI) that calls
`@ail_<entry-module>_main()`. `source_filename` exists exactly once per
workspace and carries the entry-module name (`<entry-module>.ail`).

## Convention: qualified cross-module references

Cross-module calls use **no** new AST node. Instead, a `Term::Var { name }`
with exactly one dot in the name is a qualified reference: `<prefix>.<def>`.

- `<prefix>` is an import alias (`import { module: "X", as: "<prefix>" }`)
  or, when imported without an alias, the module name itself.
- `<def>` is the name of a top-level definition in the target module.
- Def names MUST NOT contain a dot — the typechecker reports
  `invalid-def-name` with `ctx: { "reason": "contains-dot" }`.
- The workspace loader finds all reachable modules; the
  typechecker (`check_workspace`) resolves dotted names through the
  import map. Diagnostic codes: `unknown-module` (prefix not imported),
  `unknown-import` (module found, def not).

Hash stability: no new AST node, no renamed fields — all previous module
hashes stay bit-identical.

## Env construction

The check environment carries two parallel per-module overlays for
ADT definitions: `env.types: IndexMap<String, TypeDef>` is the
**owning index** — it stores the full definition keyed by bare type
name. `env.ctor_index: IndexMap<String, CtorRef>` is the **reverse
index** — it maps each constructor name back to its owning type, so
ctor-by-name lookups run in O(1) rather than searching every type's
ctor list.

The split is not a refactor wart. The two maps have distinct
semantic roles: an owning data index, and a derived lookup
accelerator over the same data. Collapsing them into one
variant-keyed map (`Map<Name, EntryKind>`) would force every
type-iterator and every ctor-lookup site to discriminate the variant
tag, reversing the optimisation the reverse index exists to
provide.

The check-side per-module rebuild of both overlays at
`crates/ailang-check/src/lib.rs:1342-1384` is intentionally
retained: the in-band `DuplicateCtor` diagnostic at the same site
consumes the rebuilt per-module `env.ctor_index`. The mono-side
overlay was narrowed to types-only at iter ct.3.2 because its
consumer is the runtime ctor lookup, which became type-driven
post-ct.2.2 — a different consumer story, hence a different
overlay shape. The asymmetry between the check side and the mono
side is by design and is pinned by
`crates/ailang-check/tests/duplicate_ctor_pin.rs`.

## Embedding ABI

`ail build --emit=staticlib` compiles a module to a relocatable
`lib<entry>.a` (program objects only) plus a separate
`libailang_rt.a` (the RC runtime: `rc.c` + `str.c`), with **no**
`@main` trampoline and **no** `MissingEntryMain` requirement — a
kernel module is a library.

Each `fn` carrying `(export "<sym>")` (schema: `FnDef.export`) is
emitted as an externally-visible C entrypoint `@<sym>` forwarding to
the internal `@ail_<module>_<fn>`. The symbol is author-chosen and
decoupled from the `ail_<module>_<def>` mangling so a module/fn
rename does not move the C symbol.

The embedding ABI accepts `Int` (lowered `i64`), `Float` (lowered
`double`), or a single-constructor record of those (crossing as a
bare `ptr` to the frozen box layout below); the fn's effect set must
be empty. **Frozen as of M3**: a future compiler change MUST NOT
move the box offsets below or invert the host-free rule.
These are enforced at `ail check` (`export-non-scalar-signature`,
`export-has-effects`) — an effectful or non-scalar export *fails to
typecheck*. Every exported entrypoint takes a mandatory leading `ailang_ctx_t*`
(M2): a per-thread embedding context created by `ailang_ctx_new()`
and released by `ailang_ctx_free()`, owned by the calling thread for
its lifetime. The host links one `ailang_ctx_t` per OS worker thread
and the runtime accounts RC alloc/free into it (no shared mutable
runtime state — the swarm artefact is data-race-free, sanitiser-
verified). The staticlib swarm artefact is **RC-only**:
`ail build --emit=staticlib` rejects `--alloc=gc`/`--alloc=bump`
(the shared Boehm collector is not swarm-safe). The value/record
layout is **frozen as of M3** (see "Frozen value layout" below); the
ctx-threaded C signature is the M2 shape.

Export parameters are written **bare**: a scalar type carries no
`own`/`borrow` mode (a single-constructor record export parameter,
by contrast, carries `own`/`borrow` — the ownership contract the
frozen value layout below specifies). The
canonical M1 export shape:

```
(fn step
  (export "backtest_step")
  (type
    (fn-type
      (params (con Int) (con Int))
      (ret (con Int))))
  (params state sample)
  (body
    (app + state (app * sample sample))))
```

`ail emit-ir <module> --emit=staticlib` prints this kernel's LLVM
IR (the external `@<sym>` forwarders, no `@main`) instead of the
executable-path `main`-required rejection — the Decision-5
IR-readability affordance for a `main`-free kernel.

### Frozen value layout (M3 — one-way commitment)

For a single-constructor `data T` whose `n` fields are each `Int`
or `Float`, a value of `T` crossing the embedding C boundary is a
bare payload pointer `p`:

| bytes | content |
|---|---|
| `p - 8 .. p` | `uint64_t` refcount header (`HEADER_SIZE = 8`) |
| `p + 0 .. p + 8` | `int64_t` constructor tag (written; `0` for the single ctor — no elision) |
| `p + 8 + i*8` | field `i`, declaration order: `int64_t` for `Int`, IEEE-754 `double` bit-pattern for `Float` |

Total box payload size = `8 + n*8`. This is the layout codegen
emits today (`match_lower.rs` `lower_ctor`); it is **frozen** — a
future compiler change MUST NOT move these offsets.

**Construction (host → kernel input).** The host MUST obtain an
input record's storage from `ailang_rc_alloc(8 + n*8)` (returns the
payload pointer with the refcount header pre-set to `1`, payload
zeroed), then write the tag (`0`) and the scalar fields at the
offsets above. A raw `malloc` is a contract violation:
`own`-consume and `ailang_rc_dec` both require the runtime's 8-byte
header at `p - 8` initialised to `1`.

**Ownership follows the declared mode** (the §"Mode metadata is
load-bearing for codegen" contract, as the C ABI): a `(own (con
T))` parameter transfers ownership in — the kernel consumes it
(Iter-B drop-at-return); the host MUST NOT touch or `dec` it after
the call. A `(borrow (con T))` parameter is retained by the host —
the kernel does not consume it; the host frees it. The return value
is always owned by the host.

**Free (host side).** `ailang_rc_dec(payload)`. Leak-free for an M3
record because every field is a scalar — `ailang_rc_dec` is
header-only and an M3 record has no boxed children. A record with
boxed fields (`Str`/`List`/nested record) is **not** an M3 type
(rejected by the export gate); a recursive typed-free for that
shape is an additive M4 concern, not a contradiction of this
freeze.

## Data model

The on-disk JSON-AST is what the toolchain hashes, typechecks, and
lowers. **This section is the canonical schema.** The Rust types in
`crates/ailang-core/src/ast.rs` are the in-memory projection of it;
when the two disagree, this section wins, and the drift test
`crates/ailang-core/tests/design_schema_drift.rs` fires. Every
additive field is declared with `skip_serializing_if` so pre-existing
fixtures keep bit-identical canonical-JSON hashes — that gating
contract is what makes growing the schema cheap.

### Module

```jsonc
{
  "schema": "ailang/v0",
  "name": "<id>",
  "imports": [{ "module": "<id>", "as": "<id>" }],
  "defs": [Def...]
}
```

### Def

`kind ∈ { "fn", "const", "type", "class", "instance" }`. All five
are real surface forms.

```jsonc
// fn (the unit that gets a content hash)
{ "kind": "fn",
  "name": "<id>",
  "type": Type,            // typically Type::Fn, optionally wrapped in Forall
  "params": ["<id>"...],   // names bound in body, in type.params order
  "body": Term,
  "doc": "<optional string>",
  "export": "<optional C symbol>", // omitted when absent (hash-stable when omitted); see §"Embedding ABI"
  "suppress": [Suppress...] // omitted when empty
}

// const (top-level value; codegen emits as a global; body must be pure)
{ "kind": "const",
  "name": "<id>",
  "type": Type,
  "value": Term,
  "doc": "<optional string>"
}

// type (algebraic data type; parameterised)
{ "kind": "type",
  "name": "<id>",
  "vars": ["<id>"...],     // type parameters; omitted when empty (hash-stable when omitted)
  "ctors": [
    { "name": "<id>", "fields": [Type...] }  // nullary ctor: fields = []
    ...
  ],
  "doc": "<optional string>",
  "drop-iterative": true   // opt-in; omitted when false (hash-stable when omitted)
}

// class (typeclass declaration; see Decision 11)
{ "kind": "class",
  "name": "<id>",          // class name (e.g. "Show")
  "param": "<id>",          // single class parameter, kind *
  "superclass": null,       // or { "class": "<id>", "type": "<param>" } — "class": canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names" / mq.1)
  "methods": [
    { "name": "<id>",
      "type": Type,         // FnSig over the class param
      "default": Term       // optional fallback body; null = abstract-required
    }
    ...
  ],
  "doc": "<optional string>"
}

// instance (typeclass instance; see Decision 11)
{ "kind": "instance",
  "class": "<id>",          // class being instantiated; canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names" / mq.1)
  "type": Type,             // concrete type expression (never the class param)
  "methods": [
    { "name": "<id>", "body": Term }
    ...
  ],
  "doc": "<optional string>"
}
```

**`Suppress`** (entry in `FnDef.suppress`):

```jsonc
{ "code": "<diagnostic-code>",   // e.g. "over-strict-mode"
  "because": "<author reason>"   // must be non-empty;
                                 // empty/whitespace fires `empty-suppress-reason` (Error)
}
```

### Term (expression)

```jsonc
{ "t": "lit", "lit": Literal }
{ "t": "var", "name": "<id>" }

// fn application; tail flag triggers musttail under codegen.
// `tail` is omitted when false (hash-stable when omitted).
{ "t": "app",  "fn": Term, "args": [Term...], "tail": false }

{ "t": "let",  "name": "<id>", "value": Term, "body": Term }

// Local recursive let. Always fn-shaped. The desugar pass
// lifts most `letrec` to a synthetic top-level fn; `lift_letrecs`
// finishes the job after typecheck for the residue that captures
// let-bound names. Post-codegen, no `letrec` survives.
{ "t": "letrec",
  "name": "<id>", "type": Type, "params": ["<id>"...],
  "body": Term, "in": Term }

{ "t": "if",   "cond": Term, "then": Term, "else": Term }

// Effect-op invocation. `op` is "<eff>/<op>" (e.g. "io/print_str").
// `tail` triggers musttail (omitted when false).
{ "t": "do",   "op": "<eff>/<op>", "args": [Term...], "tail": false }

// Ctor application; `args` omitted when empty.
{ "t": "ctor", "type": "<id>", "ctor": "<id>", "args": [Term...] }

{ "t": "match", "scrutinee": Term, "arms": [Arm...] }

// Anonymous fn value; free vars captured from enclosing scope.
{ "t": "lam",
  "params": ["<id>"...],
  "paramTypes": [Type...],
  "retType": Type,
  "effects": ["<id>"...],
  "body": Term }

// Sequencing. Semantically `let _ = lhs in rhs`; lhs must be Unit.
{ "t": "seq",   "lhs": Term, "rhs": Term }

// Explicit RC clone. Codegen lowers as
// `call void @ailang_rc_inc(ptr %v)` before returning %v under `--alloc=rc`.
{ "t": "clone", "value": Term }

// Explicit reuse-as hint. `body` must be allocating
// (typically `ctor` or `lam`); `source` must be a bare `var`. Codegen
// lowers as in-place rewrite under `--alloc=rc`.
{ "t": "reuse-as", "source": Term, "body": Term }

// loop-recur iter 1: strict iteration block. `binders` declares
// one or more loop parameters (name, type, init), evaluated in
// order on loop entry; `body` is in scope of all binders. The
// loop's value is `body`'s value on the iteration that exits via a
// non-`recur` branch. Strictly additive (no `skip_serializing_if`;
// pre-existing fixtures hash bit-identically — none carry the tag).
// No totality claim — an infinite loop is legal. See
// `docs/specs/2026-05-17-loop-recur.md`.
{ "t": "loop",
  "binders": [ { "name": "<id>", "type": Type, "init": Term }, ... ],
  "body": Term }

// loop-recur iter 1: re-enter the lexically innermost enclosing
// `loop`, rebinding its binders positionally to `args`. Transfers
// control (no fall-through); valid only in tail position of its
// enclosing loop (enforced at typecheck, `recur-not-in-tail-position`).
{ "t": "recur",
  "args": [ Term, ... ] }
```

In the MVP, `do` is only a direct call to a built-in effect op (no
handler). A `lam` term constructs an anonymous function value; free
variables of its body are captured from the enclosing scope.

Loop binders are alloca-resident: typecheck binds them in the
ordinary local scope plus a positional `loop_stack`, and codegen
lowers them as entry-block allocas. Capturing a `loop` binder into a
lambda body is rejected at typecheck via
`CheckError::LoopBinderCapturedByLambda`. See
`docs/specs/2026-05-17-loop-recur.md`.

**`Literal`**:

```jsonc
{ "kind": "int",  "value": <i64> }
{ "kind": "bool", "value": <bool> }
{ "kind": "str",  "value": "<utf-8>" }
{ "kind": "unit" }
{ "kind": "float", "bits": "<16-lowercase-hex>" }
```

**`Pattern`** (the `pat` field of an `Arm`; discriminator `p`):

```jsonc
{ "p": "wild" }                                   // _
{ "p": "var",  "name": "<id>" }                   // x — binds the value
{ "p": "lit",  "lit": Literal }
{ "p": "ctor", "ctor": "<id>", "fields": [Pattern...] } // fields omitted when empty
```

Patterns are linear: each pattern variable may appear at most once.

### Type

```jsonc
// Type-constructor application. `args` omitted when empty
// (hash-stable when omitted, for non-parameterised cases like Int, Bool, ...).
{ "k": "con", "name": "<id>", "args": [Type...] }   // "name": canonical form (bare for same-module / primitives, "<module>.<TypeName>" for cross-module; see §"Type::Con name scoping" / ct.1)

// Function type. Decision 10 added paramModes/retMode as
// metadata on Type::Fn — they are NOT separate Type variants, so every
// existing match-arm in the typechecker (unify, occurs, apply) keeps
// working. `paramModes` omitted when every entry is "implicit";
// `retMode` omitted when "implicit" (hash-stable when omitted).
{ "k": "fn",
  "params":     [Type...],
  "paramModes": [ParamMode...],
  "ret":        Type,
  "retMode":    ParamMode,
  "effects":    ["<id>"...] }

{ "k": "var", "name": "<id>" }

// Top-level polymorphism only. `constraints` carries class
// constraints (Decision 11); omitted when empty (hash-stable when omitted).
{ "k": "forall",
  "vars": ["<id>"...],
  "constraints": [{ "class": "<id>", "type": "<id>" }, ...],   // "class": canonical form (bare for same-module, "<module>.<Class>" for cross-module; see §"Class names" / mq.1)
  "body": Type }
```

**`ParamMode`** (Decision 10):

```
"implicit"   — unannotated / back-compat. Treated as `own` by the typechecker.
"own"        — (own T) — caller transfers ownership; callee consumes.
"borrow"     — (borrow T) — caller retains ownership; callee may not consume.
```

`implicit ≡ own` semantically; the distinction exists so existing
unannotated fixtures continue to serialize without the mode wrapper and keep their
canonical-JSON hash.

## Pipeline

```
.ail.json  ─┐
            ├─ load + validate schema
            ├─ resolve names + assign hashes
            ├─ desugar (AST → AST)
            ├─ typecheck (HM, effect rows; mode-strict per Decision 10)
            ├─ lift_letrecs (post-typecheck AST → AST)
            ├─ lower to MIR (SSA-like, named SSA values)
            ├─ emit LLVM IR (.ll)
            └─ clang -O2 *.ll -o binary
                  --alloc=rc → emits inc/dec     (@ailang_rc_inc / _dec; canonical, default)
                  --alloc=gc → links libgc       (@GC_malloc; parity oracle)
```

Two allocator backends share the same MIR. `--alloc=rc` is the
canonical backend committed to in Decision 10 and the CLI default.
The typechecker enforces
`(own)` / `(borrow)` modes, codegen emits `ailang_rc_inc` / `_dec`
calls at the points dictated by linearity, and `Term::Clone` /
`Term::ReuseAs` materialise into actual rc-bumps and in-place
rewrites respectively. `--alloc=gc` selects the transitional Boehm
backend; `--alloc=rc` is the canonical backend (Decision 10) and the
CLI default.

The **desugar** pass (`ailang-core::desugar::desugar_module`) runs
before typecheck and codegen in every entry point of `ailang-check`
and `ailang-codegen`. It is a pure AST → AST rewriter — currently
only flattens nested constructor patterns, but is the chosen
home for any future surface-smoothing rewrites that should not bloat
the core AST or the backends. **Critical invariant:** `CheckedModule.symbols`
in the `check` entry point continues to hash from the *original*
on-disk module, not the desugared one, so `ail diff` and `ail manifest`
report identities that match the canonical JSON the user is editing.

The **lift_letrecs** pass (`ailang-check::lift_letrecs`)
runs **after** typecheck and **before** codegen, but only on the
`build` / `run` paths — the `check` subcommand stops at typecheck
and never sees a lifted module. It eliminates every `Term::LetRec`
that the desugar pass left in place (the case where at least one
capture is `Term::Let`-bound, so its type is only knowable after
inference). The output is a module with synthetic `<hint>$lr_N`
top-level fns appended, ready for codegen. Synthetic FnDefs added
by this pass do **not** appear in `CheckedModule.symbols` — same
invariant as the desugar-pass lifts.

## CLI

```
ail check     <module.ail.json>          — loads, validates, typechecks
ail manifest  <module.ail.json>          — table: name :: type !effects [hash]
ail describe  <module> <name>            — detail of a definition (form-A body)
ail render    <module.ail.json>          — JSON-AST  → form-A text  (exact inverse of `parse`)
ail parse     <module.ail>              — form-A text → canonical JSON-AST
ail prose     <module.ail.json>          — JSON-AST  → form-B (lossy human prose, no parser)
ail merge-prose <m.ail.json> <m.prose.txt>
                                         — compose the LLM-mediator prompt for the prose round-trip
                                           (see docs/PROSE_ROUNDTRIP.md)
ail deps      <module.ail.json>          — list cross-module references
ail diff      <a.ail.json> <b.ail.json>  — content-addressed def-level diff
ail workspace <entry.ail.json>           — list all modules transitively reachable from entry
                                           (`--json` for machine output;
                                           `manifest --workspace` and `diff --workspace`
                                           extend single-module subcommands to workspaces)
ail builtins                             — list built-in fns and effect ops
ail emit-ir   <module> [--emit=staticlib]  — writes .ll (staticlib: a main-free kernel's IR, no @main)
ail build     <module> [--emit=staticlib]  — full pipeline → binary (staticlib: lib<entry>.a + libailang_rt.a)
ail run       <module>                   — build + execute (tempdir), passthrough exit code
```

## Verification and correctness (across cycles)

1. **Snapshot tests** for the pretty-printer and IR emit. The diff makes
   regressions visible immediately.
2. **Property tests** for the JSON ↔ pretty-print roundtrip.
3. **End-to-end tests** for `examples/` with expected program output.
4. **Hash stability**: a test ensures the same def always produces the same
   hash.
5. **CI pin** of the outputs in `tests/expected/`.
6. **Rustdoc cleanliness**: `cargo doc --no-deps` runs warning-free.
   Fixing a rustdoc warning is part of the iteration that
   introduced it, not a follow-up.

## Float semantics

`Float` is IEEE-754 binary64 (LLVM `double`). One float type ships;
no `f32` variant. The runtime / codegen contract:

**Guaranteed:**

- Every individual builtin (`+`/`-`/`*`/`/`/`neg`/`<`/`==`/...) lowers
  to a single LLVM IR instruction on the Float arm:
  `fadd/fsub/fmul/fdiv double`, `fneg double`, `fcmp olt/ole/ogt/oge
  double`, `fcmp oeq double`, `fcmp une double` (for `!=`). On a
  fixed `(target triple, LLVM version)` pair, the bit pattern of
  the result of any single op is reproducible.
- NaN and ±Inf propagate per IEEE 754 — no silent collapse to zero,
  no trap. Arithmetic on a NaN operand produces NaN; division by
  zero produces ±Inf; `0.0 / 0.0` produces NaN.
- `-0.0` and `+0.0` are distinct bit patterns at the canonical-JSON
  hash level (`{"bits":"0000000000000000",...}` vs
  `{"bits":"8000000000000000",...}` — distinct `def_hash`s) but
  compare equal via `==` per IEEE (`fcmp oeq double` returns true
  for `+0 == -0`). This asymmetry is the correct IEEE behaviour;
  it does mean `def_hash`-equality is finer than `==`-equality on
  Float.
- `==` returns `false` whenever either operand is NaN
  (`fcmp oeq` is the ordered-equal predicate; ordered = both
  operands non-NaN).
- `!=` returns `true` whenever either operand is NaN (`fcmp une`
  is the unordered-or-not-equal predicate). This matches Rust
  `f64::ne` and IEEE-`!=` exactly.
- `is_nan` (`fcmp uno double %x, %x`) returns `true` iff `x` is
  NaN. Bit-pattern-based NaN detection without dependence on the
  payload bits.
- `int_to_float` (`sitofp`) is exact for `|n| < 2^53`,
  round-to-nearest-even otherwise.
- `float_to_int_truncate` (`@llvm.fptosi.sat.i64.f64`) is total:
  NaN → 0, +Inf → i64::MAX, -Inf → i64::MIN, finite-out-of-range
  saturates, finite-in-range truncates toward zero. Matches Rust
  `as i64` semantics (since 1.45).

**Unspecified:**

- FMA contraction. LLVM may fold `fadd (fmul a b) c` into
  `fma a b c`. Bit results may differ between an op-emitted-in-
  isolation pattern and an op-folded-into-FMA pattern.
- Reassociation. The compiler may reorder a chain like
  `(a + b) + c` into `a + (b + c)`, producing a bit-different
  result on numerically sensitive inputs.
- Subnormal flushing modes. If the target enables FTZ (flush-to-
  zero) or DAZ (denormals-are-zero), subnormal results round to
  zero; AILang does not enable these flags but does not forbid the
  target from doing so.
- The exact NaN bit pattern produced by an op. Any quiet NaN bit
  pattern is conformant; `0.0 / 0.0` may produce
  `0x7ff8000000000000` on one target and a different qNaN on
  another.
- The textual rendering of NaN through `float_to_str` (the runtime
  C helper that backs `instance Show Float` and, post-iter-rpe.1,
  every Float-typed `print` call). The libc `printf("%g", nan)`
  glue used by `float_to_str` is permitted to emit `nan` / `-nan`
  / `NaN` etc. depending on libc version and the NaN's sign bit;
  AILang does not normalise this, since the prose / surface-print
  paths render NaN as the explicit `"NaN"` spelling and Float
  rendering is for human-readable output, not round-trip.

The same libc-`%g` rendering applies to `show 1.5` / `show nan` /
`show inf` via `instance Show Float` (which calls `float_to_str`
internally — see §"Prelude (built-in) classes" for the Show ship).
The NaN-spelling caveat above is observable via `do print x` for
Float-typed `x`; the rendering is libc-version-dependent and
target-libc-specific. AILang does NOT canonicalise Float textual
representation; the LLM-author who needs deterministic Float
rendering for cross-platform test fixtures should bypass `show` /
`print` and emit a custom formatter.

These are the Rust / Swift / standard-LLVM defaults — not
research-grade reproducibility guarantees. The stronger guarantee
(e.g. Pythonic `float.fromhex`-level bit reproducibility across
ops) would require `-ffp-contract=off` plus per-op intrinsic
selection — out of scope for the milestone; revisit only if a real
use case appears.

**Form-A serialisation:** Float literals carry the IEEE-754
bit pattern as a 16-character lowercase hex string in the canonical
JSON: `{"kind":"float","bits":"<16-hex>"}`. Routing through the
JSON *string* path (not `serde_json::Number`) preserves bit
stability across `serde_json` versions and lets NaN / ±Inf
round-trip through Form-A — JSON numbers cannot represent them.

**Pattern matching:** `Pattern::Lit` on `Literal::Float` is hard-
rejected at typecheck (`CheckError::FloatPatternNotAllowed`). IEEE
semantics make Float patterns semantically dubious — NaN never
matches via IEEE-`==`, and bit-exact equality is rarely what an
LLM-author wants. Use ordering operators (`<`, `>`, ...) and
`is_nan` to discriminate Floats.

`float_to_str` (Float → Str) and `int_to_str` (Int → Str) are
fully wired through checker, codegen, and runtime. Both allocate
a fresh heap-Str slab at the call site (see "Str ABI" below for
the dual realisation) and carry `ret_mode: Own` so the let-binder
for the call result is RC-tracked and the slab is freed at scope
close.

**Str ABI.** A `Str` is a pointer to a structure with `i64 len` at
offset 0 followed by `len` bytes plus a trailing `NUL` at offset 8.
Two realisations share this consumer ABI:

| Realisation | Origin                                          | rc_header | Memory                                  |
|-------------|-------------------------------------------------|-----------|-----------------------------------------|
| static-Str  | string literals (`@.str_*` LLVM globals)        | none      | `.rodata`, packed-struct `<{ i64, [N+1 x i8] }>` |
| heap-Str    | runtime allocations (`int_to_str`, `float_to_str`, ...) | yes, at `payload - 8` | `malloc`'d via `ailang_rc_alloc(8 + len + 1)` |

Every consumer (`@puts`, `@strcmp`, `@ail_str_eq`,
`@ail_str_compare`) GEPs `+8` from the Str pointer to reach the
bytes, regardless of realisation. The byte-comparison semantics
are inherited from libc `strcmp` — locale-independent, NUL-
terminated.

The heap-Str realisation participates in standard RC: the
`rc_header` slot eight bytes before the `len` field is managed
by `ailang_rc_alloc` / `ailang_rc_inc` / `ailang_rc_dec` exactly
like any other RC-allocated cell. The static-Str realisation has
no `rc_header` slot at all; the bytes at `payload - 8` belong to
the previous global in `.rodata` and reading them is undefined.

**The static-Str non-RC invariant is enforced at codegen.** Two
mechanisms keep static-Str pointers out of `ailang_rc_dec` along
every shipping execution path: (1) the non-escape lowering pass
(iter 18b) and the move-tracking partial-drop logic (iter 18d.3)
prevent let-binders or pattern-binders for static-Str literals
from reaching scope-close drop emission; (2) the `Type::Con { name: "Str" }`
carve-outs in `field_drop_call` and in the `Term::App` arm of
`drop_symbol_for_binder` (both in `crates/ailang-codegen/src/drop.rs`)
route the rare case that *does* reach drop emission through
`ailang_rc_dec`, which itself only fires for heap-Str at runtime
(static-Str pointers never carry a live rc_header; if codegen ever
let one through, the runtime would corrupt `.rodata`-adjacent
memory). No runtime guard backs the invariant up; the codegen
proof is the protection.

## What is not (yet) supported

Snapshot of the current boundary. Items move out of this list
as iterations land; the JOURNAL records when.

- No effect handlers — only the built-in `IO` op (`io/print_str`).
  `Diverge` is a reserved effect name with no op and no codegen.
- No refinements / SMT escalation.
- No HM inference inside bodies. Top-level def types are explicit;
  polymorphism is opt-in via `Type::Forall { vars, body }`. Inside
  a body, lambdas check monomorphically against their declared type.
- Polymorphic fns must be **directly called** at the use site.
  Passing a polymorphic fn as a value (`let f = id in f(42)`) is
  not yet supported — it would need one closure-pair global per
  instantiation, deferred.
- No higher-rank polymorphism. Passing a polymorphic fn to another
  polymorphic fn (`apply(id, 42)`) is not supported.
- No recursive `let` for non-fn values. Plain `let x = … in …` only
  sees `x` inside the body, not inside its own RHS — recursive value
  bindings would break Decision 10's acyclicity invariant. Recursive
  *fn* bindings are supported via `Term::LetRec` (`{ "t": "letrec",
  ... }`); the desugar pass lifts most occurrences to a synthetic
  top-level fn, with `lift_letrecs` finishing the residue after
  typecheck.
- No visibility rules in imports. Every top-level def of an imported module
  is reachable; there is no `pub` / `priv`.

What **is** supported (and used as the smoke test for the pipeline):

- Int, Bool, Unit, **Str**, **Float** as primitive types.
- `if`, `let`, function calls, recursion.
- Effects on function signatures, with `do op(args)` for direct effect
  ops (`io/print_str`). The per-type print ops
  `io/print_int`, `io/print_bool`, `io/print_float` were retired in
  iter rpe.1; the polymorphic `print` (§"Polymorphic print") is the
  canonical output path for non-Str values.
- **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`) of type
  `forall a. (a, a) -> a` (codegen-restricted to `{Int, Float}`);
  `%` of type `(Int, Int) -> Int` (Int-only — `fmod` semantics for
  Float deferred); ordering operators and `!=` (`!=`, `<`, `<=`,
  `>`, `>=`) of type `forall a. (a, a) -> Bool` (codegen-restricted
  to `{Int, Float}`); polymorphic `neg : forall a. (a) -> a`
  (codegen-restricted to `{Int, Float}`; Float arm uses LLVM
  `fneg double` for correct `-0.0` handling); logical
  `not : (Bool) -> Bool`; conversions
  `int_to_float : (Int) -> Float`,
  `float_to_int_truncate : (Float) -> Int` (saturating, NaN → 0),
  `float_to_str : (Float) -> Str`,
  `int_to_str : (Int) -> Str` (both allocate a heap-Str slab at
  call time and return it with `ret_mode: Own`; see "Str ABI" for
  the dual heap-/static-Str realisation); inspection
  `is_nan : (Float) -> Bool` (LLVM
  `fcmp uno`); Float bit-pattern constants `nan : Float`,
  `inf : Float`, `neg_inf : Float` (resolved as bare values, lower
  to direct hex-float `double` SSA constants at use site); the IO
  effect op `io/print_str`; **`==` : forall a.
  (a, a) -> Bool**; and **`__unreachable__ : forall a. a`**.
  - **`==` is polymorphic.** The typechecker accepts
    `==` at any type whose two sides agree (the rigid `a` of the
    `Forall` is unified by HM at the use site). Codegen
    monomorphises and dispatches on the resolved AIL arg type:
    `Int` → `icmp eq i64`; `Bool` → `icmp eq i1`;
    `Str` → `call @strcmp(ptr, ptr)` then `icmp eq i32 0`
    (`@strcmp` is declared in the LLVM IR header alongside
    `@printf` / `@GC_malloc`); `Unit` → constant `i1 true`
    (Unit has a single inhabitant; both sides are still
    evaluated for any side effects); `Float` → `fcmp oeq double`.
    ADT and `Fn` arg types are rejected at codegen with a
    `CodegenError::Internal` mentioning `==` and the offending
    type — neither has a canonical structural-equality scheme
    yet, and the language deliberately does not silently elide
    the check. **`!=` for Float uses `fcmp UNE double` (NOT
    `one`)** — `one` is "ordered and not equal" and would return
    false for `nan != nan`, violating IEEE-`!=`.
  - **`__unreachable__`** is a polymorphic bottom value: a use of
    `__unreachable__` typechecks against any expected type at
    the use site and codegens to the LLVM `unreachable`
    instruction (UB if ever executed). It is the chain
    machinery's deepest fall-through for matches that the
    typechecker proved exhaustive, and it is available to user
    code as an explicit panic primitive
    (`(if cond __unreachable__ ...)` for assertions or
    impossible branches). Reference site is
    `Term::Var { name = "__unreachable__" }` / form-A bare
    `__unreachable__`.
- **ADTs + pattern matching.** Sub-patterns of a Ctor pattern may be `Var`, `Wild`,
  another `Ctor`, or a literal. The desugar pass flattens
  nested Ctor patterns into a chain of let + match and rewrites every
  `Pattern::Lit` (top-level or sub-) to a `Term::If` on `==` before
  typecheck/codegen — see `ailang-core::desugar` and Pipeline above.
- Literal patterns at top level and inside Ctor sub-patterns (via desugar).
  `(pat-lit 0)` and `(pat-ctor Cons (pat-lit 0) _)` both
  parse and lower; the rewrite is to `Term::If { cond = (== sv lit) }`,
  so any literal kind whose `==` is supported is authorable. With `==`
  polymorphic over `Int`/`Bool`/`Str`/`Unit`, that
  covers every lit kind the AST ships — including `(pat-lit "hi")`
  over a `Str` scrutinee, exercised by `examples/eq_demo.ail.json`.
- **Imports + qualified cross-module references** via dotted names.
  Extends to **types and constructors**: a foreign
  module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as
  `(term-ctor std_pair.Pair MkPair x y)` and `(pat-ctor MkPair x y)`
  inside that scrutinee. Std-library demos (`examples/std_*_demo.ail.json`)
  exercise this end-to-end.
- **AI-authoring text surface, form (A)** (Decision 6). The `ailang-surface` crate parses `.ail` form-A
  text into a canonical `ailang-core::ast::Module` and prints any module
  back as form-A text. `ail render` and `ail describe` use it as the
  sole text projection; `ail parse` is the inverse direction. Round-trip
  identity (text → AST → JSON → AST → text) is gated by
  `ailang-surface/tests/round_trip.rs` over every shipped fixture.
- **Memory management via Boehm conservative GC** (Decision 9),
  with **per-fn arena via stack `alloca` for non-escaping allocations**
  layered on top. Every ADT box, lambda env, and closure
  pair allocates either via `@GC_malloc` (escaping; Boehm-managed) or
  via LLVM `alloca` (non-escaping; freed at fn return). The decision
  is made by an escape-analysis pre-pass over the fn body — see
  Decision 9's "Per-fn arena via stack `alloca`" subsection.
  Boehm-only soak tests are unchanged: `examples/gc_stress.ail.json`
  and `examples/std_list_stress.ail.json` still allocate via
  `@GC_malloc` because their boxes flow into other fns and escape.
  The per-fn-arena path is exercised end-to-end by
  `examples/escape_local_demo.ail.json`.
- **First-class function references.** A top-level fn name (or
  qualified `prefix.def`) used as a `Term::Var` is a fn-value.
- **Anonymous lambdas with capture.** `Term::Lam` constructs a
  closure that captures any free variables of its body from the
  enclosing scope. All fn-values share a single ABI: a `ptr` to a
  closure pair `{ thunk_ptr, env_ptr }`. Top-level fns get an auto-
  generated adapter and a static closure pair (env = null) so they
  remain passable as values without heap overhead.
- **Polymorphism via `Type::Forall`** at top-level def types.
  Use sites instantiate fresh metavars; unification pins them against
  the concrete types of the call args. Codegen monomorphises on
  demand: each unique instantiation emits a specialised LLVM fn
  mangled `@ail_<m>_<def>__<descriptor>` (e.g. `id__I` for `id` at
  `Int`, `apply__I_I` for `apply` at `(Int, Int)`).
- **Parameterised ADTs.** `TypeDef.vars: Vec<String>`
  declares type parameters; `Type::Con.args: Vec<Type>` carries the
  type arguments at use sites. Both fields default to empty and are
  skipped during serialization, so canonical-JSON hashes of every
  existing definition stay bit-identical (regression test in
  `crates/ailang-core/src/hash.rs`). Ctor and match codegen stay
  inline at every use site — there is no specialised ADT symbol —
  but LLVM field types are derived per use site by substituting
  through `cdef.ail_fields`. The substitution is read off the call's
  arg types (ctor) or the scrutinee's `Type::Con.args` (match). An
  unresolved `Type::Var` reaching `llvm_type` is a hard error
  rather than a silent fallback to `ptr`.
Pipeline regression smoke tests:

- `examples/sum.ail.json` → prints 55 (recursion, arithmetic).
- `examples/list.ail.json` → prints 42 (ADTs + match).
- `examples/hof.ail.json` → prints 42 (first-class fn-refs, indirect call).
- `examples/closure.ail.json` → prints 42 (lambda capturing a let-bound var).
- `examples/list_map.ail.json` → prints 2/4/6 (ADTs + closure + recursive
  HOF + IO; the dogfood smoke test).
- `examples/sort.ail.json` → prints sorted [3,1,4,1,5,9,2,6,5,3,5]
  one-per-line (insertion sort over an 11-element list).
- `examples/poly_id.ail.json` → prints 42 then "true" (polymorphic
  identity at `Int` and `Bool`; two specialised fns emitted).
- `examples/poly_apply.ail.json` → prints 42 (polymorphic `apply`
  with a fn-typed parameter; `apply(succ, 41)`).
- `examples/box.ail.json` → prints 42 (parameterised ADT round-
  trip: `MkBox(42)` constructed, then projected by a polymorphic
  `unbox : forall a. (Box<a>) -> a` and printed).
- `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match
  over `Maybe<Int>`: `or_else(Some(7), 99)` then
  `or_else(None, 99)`).
- `examples/std_list_demo.ail.json` → exercises
  `std_list`'s combinators (length, sum, reverse, take/drop-style
  uses) end-to-end against `std_list`'s `List<a>`.
- `examples/std_maybe_demo.ail.json` → exercises `std_maybe`
  combinators over `Maybe<Int>`, including `from_maybe` and `map`.
- `examples/std_either_demo.ail.json` → first program with
  three distinct type variables in a single fn (the `either`
  eliminator), monomorphised six different ways in the IR.
- `examples/std_pair_demo.ail.json` → drives every
  `std_pair` combinator (fst, snd, swap, map_first, map_second);
  expected output 7, 9, 9, 7, 8, 18.
- `examples/nested_pat.ail.json` → first program to use a
  nested `(pat-ctor Cons a (pat-ctor Cons b _))`; the desugar pass
  flattens it into a chain that the existing flat-match codegen
  consumes. Prints 30 for a 3-element input list.
