# 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//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 / 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, `` 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 -o `. 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`; 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 ` (the deterministic projection) and `ail merge-prose ` (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` (raw pointer addresses of `Term::Ctor` / `Term::Lam` AST nodes flagged as non-escaping). On a hit the emitter writes `alloca i8, i64 , align 8`; on a miss it writes `call ptr @GC_malloc(i64 )`. 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 `.` where `` 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, `.` 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 (`..`) 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 } ; `(clone X)` — explicit RC inc Term::ReuseAs { source: Box, body: Box } ; `(reuse-as SRC NEW-CTOR)` ``` `Term::ReuseAs` is structured as a *wrapper* around a `body` term rather than as a `reuse_from: Option` modifier on `Term::Ctor`. Two substantive reasons: 1. **Compositional flexibility.** Reuse-as is conceptually a wrapper that says "this expression's allocation comes from ``'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 : ` 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__` (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": , "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": } ] } ``` `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 ` ` where `` 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 `__`. 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 `______…` (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__` mangled names). `__` is legal in both LLVM IR and the C ABI used by the runtime glue, and parses unambiguously into `__` 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__` references `.show__`, 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 `..` 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>` 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 ` 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_`, 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 ` 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 `__` for primitive type targets (e.g. `show__Int`) and `__<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__` — even in the single-module case. Constants likewise (`@ail__`). Global string literals carry a short hint for readability: `@.str___` (e.g. `@.str_sum_fmt_int_0`). The entry point is a `define i32 @main()` trampoline (C / LLVM ABI) that calls `@ail__main()`. `source_filename` exists exactly once per workspace and carries the entry-module name (`.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: `.`. - `` is an import alias (`import { module: "X", as: "" }`) or, when imported without an alias, the module name itself. - `` 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` is the **owning index** — it stores the full definition keyed by bare type name. `env.ctor_index: IndexMap` 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`) 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.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 "")` (schema: `FnDef.export`) is emitted as an externally-visible C entrypoint `@` forwarding to the internal `@ail__`. The symbol is author-chosen and decoupled from the `ail__` 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 (modes apply only to heap-shaped types, which the scalar-only rule above forbids at an export boundary anyway). 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 --emit=staticlib` prints this kernel's LLVM IR (the external `@` 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": "", "imports": [{ "module": "", "as": "" }], "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": "", "type": Type, // typically Type::Fn, optionally wrapped in Forall "params": [""...], // names bound in body, in type.params order "body": Term, "doc": "", "export": "", // 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": "", "type": Type, "value": Term, "doc": "" } // type (algebraic data type; parameterised) { "kind": "type", "name": "", "vars": [""...], // type parameters; omitted when empty (hash-stable when omitted) "ctors": [ { "name": "", "fields": [Type...] } // nullary ctor: fields = [] ... ], "doc": "", "drop-iterative": true // opt-in; omitted when false (hash-stable when omitted) } // class (typeclass declaration; see Decision 11) { "kind": "class", "name": "", // class name (e.g. "Show") "param": "", // single class parameter, kind * "superclass": null, // or { "class": "", "type": "" } — "class": canonical form (bare for same-module, "." for cross-module; see §"Class names" / mq.1) "methods": [ { "name": "", "type": Type, // FnSig over the class param "default": Term // optional fallback body; null = abstract-required } ... ], "doc": "" } // instance (typeclass instance; see Decision 11) { "kind": "instance", "class": "", // class being instantiated; canonical form (bare for same-module, "." for cross-module; see §"Class names" / mq.1) "type": Type, // concrete type expression (never the class param) "methods": [ { "name": "", "body": Term } ... ], "doc": "" } ``` **`Suppress`** (entry in `FnDef.suppress`): ```jsonc { "code": "", // e.g. "over-strict-mode" "because": "" // must be non-empty; // empty/whitespace fires `empty-suppress-reason` (Error) } ``` ### Term (expression) ```jsonc { "t": "lit", "lit": Literal } { "t": "var", "name": "" } // 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": "", "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": "", "type": Type, "params": [""...], "body": Term, "in": Term } { "t": "if", "cond": Term, "then": Term, "else": Term } // Effect-op invocation. `op` is "/" (e.g. "io/print_str"). // `tail` triggers musttail (omitted when false). { "t": "do", "op": "/", "args": [Term...], "tail": false } // Ctor application; `args` omitted when empty. { "t": "ctor", "type": "", "ctor": "", "args": [Term...] } { "t": "match", "scrutinee": Term, "arms": [Arm...] } // Anonymous fn value; free vars captured from enclosing scope. { "t": "lam", "params": [""...], "paramTypes": [Type...], "retType": Type, "effects": [""...], "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": "", "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": } { "kind": "bool", "value": } { "kind": "str", "value": "" } { "kind": "unit" } { "kind": "float", "bits": "<16-lowercase-hex>" } ``` **`Pattern`** (the `pat` field of an `Arm`; discriminator `p`): ```jsonc { "p": "wild" } // _ { "p": "var", "name": "" } // x — binds the value { "p": "lit", "lit": Literal } { "p": "ctor", "ctor": "", "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": "", "args": [Type...] } // "name": canonical form (bare for same-module / primitives, "." 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": [""...] } { "k": "var", "name": "" } // Top-level polymorphism only. `constraints` carries class // constraints (Decision 11); omitted when empty (hash-stable when omitted). { "k": "forall", "vars": [""...], "constraints": [{ "class": "", "type": "" }, ...], // "class": canonical form (bare for same-module, "." 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 `$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 — loads, validates, typechecks ail manifest — table: name :: type !effects [hash] ail describe — detail of a definition (form-A body) ail render — JSON-AST → form-A text (exact inverse of `parse`) ail parse — form-A text → canonical JSON-AST ail prose — JSON-AST → form-B (lossy human prose, no parser) ail merge-prose — compose the LLM-mediator prompt for the prose round-trip (see docs/PROSE_ROUNDTRIP.md) ail deps — list cross-module references ail diff — content-addressed def-level diff ail workspace — 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 [--emit=staticlib] — writes .ll (staticlib: a main-free kernel's IR, no @main) ail build [--emit=staticlib] — full pipeline → binary (staticlib: lib.a + libailang_rt.a) ail run — 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____` (e.g. `id__I` for `id` at `Int`, `apply__I_I` for `apply` at `(Int, Int)`). - **Parameterised ADTs.** `TypeDef.vars: Vec` declares type parameters; `Type::Con.args: Vec` 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` and printed). - `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match over `Maybe`: `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`. - `examples/std_maybe_demo.ail.json` → exercises `std_maybe` combinators over `Maybe`, 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.