AILang/docs/DESIGN.md

# 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` (Iter 14c)
  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` (Family 20)
  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.
- **Agents** (`agents/`): specialised sub-prompts (implementer,
  architect, tester, debugger) that form the project's own LLM tooling.
  They are a versioned part of the repo. See `agents/README.md`.
- **Docs** (`docs/`): DESIGN.md (what and why), JOURNAL.md (history).
- **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.

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.

## 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 row-polymorphic
(`![IO | r]`). In the MVP only the effects `IO` and `Diverge` (for infinite
loops) are wired up.

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 (Iter 14b)

**Status: shipped.** Form (A) was chosen in Iter 14b and implemented as
the `ailang-surface` crate (parser + printer) in Iter 14c. Form-A is
gated against drift by `ailang-surface/tests/round_trip.rs`, which
parses every `.ailx` fixture, prints it back, re-parses, and demands
canonical-byte equality. In Iter 15e, `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 in
the same iter, 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

Iters 1 through 14a 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` (new in
Iter 14c) 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. Round-trip surface → AST → canonical JSON → AST → surface
   is the identity (modulo formatting). Hashes computed via the
   round-tripped JSON must equal hashes of the same module written
   directly in JSON.
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_int`, 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 (Iter 14c onwards, not done in 14b)

- `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 `*.ailx`, 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.ailx> -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.
- Iter 14d: 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 promote form (A) to the source of truth. 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 Iter 14c implementation

Two productions in the original 14b 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 14b 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 `.ailx` exhibits parse to canonical
JSON identical to their corresponding `.ail.json` files.

3. **Tail-call surface (Iter 14e).** 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 after Iter 14e: ~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 (Family 20)

**Status: shipped.** Family 20 (Iter 20a–20d, 2026-05-08) 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.

**Iter 20f update — Form-A spec embedding.** The 20d `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. 20f 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.ailx`
  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/*.ailx`. 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 discussion of richer integration paths (LLM tool-use, MCP
server, LSP) was deferred — all three layer additively on the
static-prompt path 20f ships, which remains the
lowest-common-denominator fallback that always works.

## Decision 7: redundancy removal — `Term::If` is not a primitive

**Status: REVERTED in Iter 14g.** This decision was made on shaky grounds —
applying CLAUDE.md's "no redundancies" rule to a case that turned out to
be primitive control flow, not redundancy. The post-removal match-on-Bool
form (3× the tokens, asymmetric `pat-wild` for the false case) was
worse for token economy and worse for the natural shape of the language.
`Term::If` is restored. The text below is preserved for the audit trail.

`Term::If { cond, then, else_ }` is semantically a subset of
`Term::Match` on `Bool`. Per CLAUDE.md the language must contain no
redundancies; two AST nodes for the same operation produces an
authoring decision with no semantic content and an extra codegen
path. Iter 14d removes `Term::If`. Migration shape on the JSON side:

  {"t":"if","cond":C,"then":A,"else":B}
    →
  {"t":"match","scrutinee":C,
    "arms":[
      {"pat":{"p":"lit","lit":{"kind":"bool","value":true}},"body":A},
      {"pat":{"p":"wild"},"body":B}]}

The wildcard arm satisfies the typechecker's
`primitive-needs-wildcard` rule. A future iter may upgrade the
exhaustiveness check to recognise the `true`+`false` arm pair as
covering Bool without a wildcard; until then, wildcard is the
canonical migration target.

No schema version bump (no third-party consumes `ailang/v0`).
Hash invalidation for the three migrated fixtures (`sum`, `sort`,
`max3`) is intentional; the new hashes become the new identity.

## 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 14d tail-call survey,
many existing recursive calls are *not* in tail position
because they are arguments to constructor calls (e.g.
`Cons (f h) (map f t)`). 14e 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 (15a onward) ships both forms where
relevant.

The 14d migration of existing fixtures will be 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

**Status: half-retirement as of 2026-05-09.** Originally framed
(2026-05-07) as "transitional Boehm until the RC pipeline
(Iters 18a–18g) lands and the default flips"; then re-framed
(2026-05-08) as a symmetric dual-allocator policy with Boehm as
the CLI default. The 2026-05-09 revision flips the asymmetry to
match Decision 10:

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

The `--alloc=bump` mode introduced for the bench is a
measurement tool, not a production target.

Through Iter 14e, every ADT box, lambda env, and closure pair was
allocated with bare `malloc` and never freed. That worked for the
17 test fixtures (all small, all short-lived) but is incompatible
with any real workload — a stdlib `fold` over a million-element
list would leak a million boxes. The "Goal" section's "no GC for
the MVP" framing predates the parameterised-ADT pipeline (Iter 13)
and the explicit-recursion expectation (Iter 14e); both make a
collector necessary.

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

A future iter may layer a per-fn-arena optimisation on top: when
a fn's return type contains no boxed ADT, ADT boxes allocated
inside that fn cannot escape, so an arena freed at fn return is
sound by construction (per the 14e GC notes). That requires
escape analysis, the corresponding AST/IR plumbing, and is its
own design pass. Boehm-everything is the floor; arena is an
optimisation above it.

### Per-fn arena via stack `alloca` (Iter 17a)

Iter 17a layers exactly that optimisation, 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

**Committed 2026-05-08, after the GC bench (`bench/run.sh`) showed
Boehm contributing ~60% of runtime on allocation-heavy workloads
that hold the heap fully live. Sharpened later the same day: the
mainstream "RC + inference" position was 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 ~2.8× 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. Iter 21'b extended the corpus
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's measured `rc/bump = 4.14×`
reflects the doubled allocation tax on closure construction —
each step pays two allocs and two decs against one bump-pointer
bump. 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 21'g baseline records `4.14×`
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 number (~60% allocate-
path overhead) is structural; 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.)

A future iter that proposes any of laziness, recursive value
bindings, shared mutable state, or any feature that creates
cycles must either prove the cycle is collectible by an
extension (e.g. linear ownership) or be rejected at design time.

### Schema additions

**Iter 18a — 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`:

```rust
Type::Fn {
    params: Vec<Type>,
    param_modes: Vec<ParamMode>,   // same length as params
    ret: Box<Type>,
    ret_mode: ParamMode,
    effects: Vec<String>,
}

enum ParamMode { Implicit, Own, Borrow }   // default: Implicit
```

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 (pre-18a) state — semantically
equivalent to `Own` but printed bare (`(con T)`, no wrapper).
`Own` and `Borrow` are explicitly annotated.

JSON canonical hash for every pre-18a 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.

The legacy `(con T)` form is treated as `(own T)` semantically
throughout the 18-series; a later iter (deferred) makes the
explicit annotation mandatory and rejects `Implicit` for boxed
parameter types.

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

**Iter 18c/18d — 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. This is the same trade-off
Decision 7 made for `Term::If`'s relationship to nested
`Term::Match`: prefer composability over schema-level
rejection where the typecheck rule is unambiguous.

**Iter 18e — `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.

**Iter 19b — `FnDef.suppress`.**

```rust
FnDef.suppress: Vec<Suppress>                        ; advisory diagnostic suppress list

struct Suppress {
    code: String,        // diagnostic code being suppressed
    because: String,     // mandatory non-empty reason
}
```

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 pre-19b 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`).

### Advisory diagnostics — Iter 19a-arc

The 19a-arc (19a / 19a.1 / 19b) 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` (Iter 19a + 19a.1).** 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`. The first ever Warning-level diagnostic;
prior to 19a all diagnostics were `Error`. CLI exit semantics
adjusted: `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` (Iter 19b).** 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 (Iter 18c)

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
from 18a (`borrow` / `own`) provide the inter-fn contract; the
inference fills in intra-fn detail. (Implementer-level detail in
the Iter 18c brief.)

### Codegen contract (Iter 18b, 18c)

Memory layout (Iter 18b):

- 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 (Iter 18e).

Codegen for `Term::Ctor` / `Term::Lam` env / closure pair under
`--alloc=rc` calls `ailang_rc_alloc(SIZE)`. Iter 18b stops there
— inc/dec instrumentation is added in Iter 18c, 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 (Iter 18d–18g)

`param_modes` and `ret_mode` on `Type::Fn` are not merely
typechecker metadata — codegen consults both to decide where to
emit drop calls. The 18d.4 / 18g shipping work moved them 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.

- **Iter 18g.1: 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.**

- **Iter 18g.2: `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).

**What this widening does NOT do.**

- Does not change the canonical hash. `param_modes` /
  `ret_mode` were already hash-load-bearing as of Iter 18a; the
  18d–18g iters add 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 18g.1; closing it is a propagation pass
  through let-bindings that has not shipped yet.

### Migration plan

1. **Iter 18a:** `(borrow T)` / `(own T)` annotations as a
   language feature. Schema, parser, JSON, typechecker. No
   codegen change. `(con T)` ≡ `(own T)`. Existing fixtures
   unchanged.
2. **Iter 18b:** RC runtime. `runtime/rc.c` with header layout +
   alloc/inc/dec. Codegen `--alloc=rc` routes allocation through
   `rc_alloc`; **no inc/dec yet**. `--alloc=gc` remains default.
3. **Iter 18c:** uniqueness inference + codegen inc/dec
   instrumentation. Combines 18a's annotations with intra-fn
   dataflow. Linear-by-default enforcement turns on. `(clone X)`
   in the `Term` schema.
4. **Iter 18d:** reuse hints + reuse analysis. `(reuse-as ...)`
   form. Codegen rewrites dec+malloc into in-place overwrite when
   the precondition holds.
5. **Iter 18e:** `(drop-iterative)` data attr. Worklist-based
   free for annotated types.
6. **Iter 18f:** RC validation bench. RC validated within target
   on `bench/run.sh` (live=0; tail latency 23× better than Boehm;
   RSS lower). Retirement of Boehm executes in two steps: first a
   default-flip (2026-05-09 — `--alloc=rc` becomes the CLI default,
   GC retained as parity oracle; see Decision 9 above); second a
   full removal once the oracle stops paying its keep (gating
   condition: a few iter families with no GC-only diagnostic
   wins).
7. **Iter 19a / 19a.1 / 19b:** advisory `over-strict-mode` lint
   + precise sub-binder analysis with heap-type filter +
   `FnDef.suppress` suppression mechanism with mandatory-reason.
   First `Severity::Warning` diagnostic; CLI exit gated on Error
   only. Decision 10's mandatory-annotation rule is unchanged.

### 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. Concrete design deferred until the need
materialises with a real workload.

### What this Decision deliberately does not do

- **Does not infer everything.** An earlier draft of this
  Decision said "uniqueness is fully inferred" — that was the
  mainstream RC position. The 2026-05-08 follow-up discussion
  replaced it: 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.**
  Iter 18a treats `(con T)` as `(own T)`. Existing JSON hashes
  stay bit-identical until the fixture is intentionally updated.
- **Does not commit to atomic refcounts.** AILang is currently
  single-threaded. If/when concurrency arrives, atomic-vs-non-
  atomic will be a separate decision per allocation kind.
- **Does not introduce regions.** Regions were considered and
  rejected; see "Why not other memory models" above.

## Mangling scheme (Iter 5c)

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 (Iter 5b)

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 (Iter 5a) finds all reachable modules; the
  typechecker (Iter 5b, `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.

## Data model

The on-disk JSON-AST is what the toolchain hashes, typechecks, and
lowers. Every node in this section is the schema mirror of an enum or
struct in `crates/ailang-core/src/ast.rs`; whenever the two disagree,
`ast.rs` is the source of truth. 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" }`. All three 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>",
  "suppress": [Suppress...] // Iter 19b, 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; Iter 5; parameterised since Iter 13a)
{ "kind": "type",
  "name": "<id>",
  "vars": ["<id>"...],     // type parameters; omitted when empty (pre-13a hash-stable)
  "ctors": [
    { "name": "<id>", "fields": [Type...] }  // nullary ctor: fields = []
    ...
  ],
  "doc": "<optional string>",
  "drop-iterative": true   // Iter 18e opt-in; omitted when false (pre-18e hash-stable)
}
```

**`Suppress`** (Iter 19b — 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 is Iter 14e (musttail under codegen).
// `tail` is omitted when false (pre-14e hash-stable).
{ "t": "app",  "fn": Term, "args": [Term...], "tail": false }

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

// Local recursive let (Iter 16b.1). Always fn-shaped. The desugar pass
// lifts most `letrec` to a synthetic top-level fn; `lift_letrecs` (16b.3)
// 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_int").
// `tail` per Iter 14e (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 (Iter 8b); free vars captured from enclosing scope.
{ "t": "lam",
  "params": ["<id>"...],
  "paramTypes": [Type...],
  "retType": Type,
  "effects": ["<id>"...],
  "body": Term }

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

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

// Iter 18d.1: 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 }
```

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 (see
Iter 8 closure conversion in JOURNAL).

**`Literal`**:

```jsonc
{ "kind": "int",  "value": <i64> }
{ "kind": "bool", "value": <bool> }
{ "kind": "str",  "value": "<utf-8>" }
{ "kind": "unit" }
```

**`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
// (pre-13a hash-stable for non-parameterised cases like Int, Bool, ...).
{ "k": "con", "name": "<id>", "args": [Type...] }

// Function type. Decision 10 (Iter 18a) 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" (pre-18a hash-stable).
{ "k": "fn",
  "params":     [Type...],
  "paramModes": [ParamMode...],
  "ret":        Type,
  "retMode":    ParamMode,
  "effects":    ["<id>"...] }

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

// Top-level polymorphism only.
{ "k": "forall", "vars": ["<id>"...], "body": Type }
```

**`ParamMode`** (Iter 18a / Decision 10):

```
"implicit"   — pre-18a / unannotated. 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 pre-18a
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, Iter 16a)
            ├─ typecheck (HM, effect rows; mode-strict per Decision 10)
            ├─ lift_letrecs (post-typecheck AST → AST, Iter 16b.3)
            ├─ 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
since 2026-05-09: 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. Boehm-on-`--alloc=gc` is on the path to
retirement; see the JOURNAL queue.

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 (16a), 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`, Iter 16b.3)
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 16b.2 lifts in desugar.

## 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.ailx>              — form-A text → canonical JSON-AST
ail prose     <module.ail.json>          — JSON-AST  → form-B (lossy human prose, no parser; Family 20)
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>                   — writes .ll
ail build     <module>                   — full pipeline → binary
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.
   Maintained by the `ailang-docwriter` agent (Iter 13d onward); fixing a
   rustdoc warning is part of the iter that introduced it, not a follow-up.

## What is not (yet) supported

Snapshot of the boundary as of Iter 16a. Items move out of this list
as iterations land; the JOURNAL records the exact iteration. Recently
**lifted** gates that used to live here: cross-module ADTs (lifted in
Iter 14h via qualified `module.Type` / `module.Ctor` references in
both `(con ...)` and `(term-ctor ...)` / `(pat-ctor ...)` positions);
GC for ADT boxes, lambda envs, and closure pairs (Boehm conservative
collector wired up in Iter 14f, see Decision 9); nested constructor
sub-patterns inside `match` (lifted in Iter 16a via the desugar pass);
literal sub-patterns inside a Ctor pattern (lifted in Iter 16c — the
desugar pass rewrites every `Pattern::Lit` to a `Term::If` on `==`,
both at the top level of an arm and inside a Ctor sub-pattern);
`==` extended from Int-only to a polymorphic
`forall a. (a, a) -> Bool` over `Int`/`Bool`/`Str`/`Unit` (lifted
in Iter 16e — codegen monomorphises and dispatches on the
resolved arg type; ADT/Fn arg types are rejected at codegen).

- No effect handlers — only the built-in IO and Diverge ops.
- 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 local recursive `let`. `let f = ... in ...` only sees `f`'s
  binding inside the body, not inside its own RHS — recursion needs
  a top-level def.
- 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** as primitive types.
- `if`, `let`, function calls, recursion.
- Effects on function signatures, with `do op(args)` for direct effect
  ops (`io/print_int`, `io/print_bool`, `io/print_str`).
- **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`, `%`) of
  type `(Int, Int) -> Int`; ordering operators and `!=` (`!=`,
  `<`, `<=`, `>`, `>=`) of type `(Int, Int) -> Bool`; logical
  `not : (Bool) -> Bool`; the IO effect ops listed above;
  **`==` : forall a. (a, a) -> Bool** (Iter 16e); and
  **`__unreachable__ : forall a. a`** (Iter 16d).
  - **`==` is polymorphic** (Iter 16e). 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). 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. The other
    comparison ops stay Int-only; their codegen path emits
    `icmp s{lt,le,gt,ge,ne}` over `i64`.
  - **`__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** (Iter 3, extended in Iter 16a/16c).
  Sub-patterns of a Ctor pattern may be `Var`, `Wild`, another `Ctor`
  (Iter 16a), or a literal (Iter 16c). 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 (Iter 16c,
  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. After
  Iter 16e (`==` 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
  (Iter 5). Extends to **types and constructors** (Iter 14h): 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 / Iter 14b–14c,
  exclusive in 15e). The `ailang-surface` crate parses `.ailx` 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 / Iter 14f),
  with **per-fn arena via stack `alloca` for non-escaping allocations**
  layered on top (Iter 17a). 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` (Iter 17a fixture).
- **First-class function references** (Iter 7). A top-level fn name (or
  qualified `prefix.def`) used as a `Term::Var` is a fn-value.
- **Anonymous lambdas with capture** (Iter 8). `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 (Iter 12).
  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** (Iter 13). `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
  pre-13a 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` (Iter 15a/15b) → 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` (Iter 15c) → exercises `std_maybe`
  combinators over `Maybe<Int>`, including `from_maybe` and `map`.
- `examples/std_either_demo.ail.json` (Iter 15d) → 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` (Iter 15f) → 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` (Iter 16a) → 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.