# Typed MIR — the check→codegen elaboration boundary — Design Spec

**Date:** 2026-05-31
**Status:** Approved
**Authors:** orchestrator + Claude

## Goal

Introduce a typed mid-level IR (`MIR`) as the single artefact that
crosses the `check` → `codegen` boundary, carrying every fact `check`
proves — node types, statically-resolved callees, parameter modes /
consume counts, and value representation (heap vs. static `Str`) — so
that **codegen re-derives nothing**.

Today there is no such artefact. `crates/ail/src/main.rs:2293` calls
`ailang_check::check_workspace(&ws)`, discards its result, and at
`:2348` hands `ailang_codegen::lower_workspace(&ws)` the *raw*
`Workspace`. `CheckedModule`
(`crates/ailang-check/src/lib.rs:1283`) carries only top-level
`(Type, hash)` — zero interior annotation. Codegen therefore runs four
independent re-derivations of information `check` already computed:

1. **Type synthesis** at every node — `synth_with_extras`
   (`crates/ailang-codegen/src/lib.rs:3242`, ~270 lines) + `synth_arg_type`
   (`:3238`), a second inference engine mirroring the checker's
   lookup ladder.
2. **Callee resolution** — `type_home_module` (`:2809`), "mirrors the
   checker's TypeDef-first ladder", replicated at three sites, plus
   `is_static_callee` (`:2830`).
3. **Uniqueness / mode** — `infer_module_with_cross` (`:1002`), the
   *identical* pass `ailang-check::linearity` already ran; codegen
   re-runs it to recover `consume_count` for drop placement
   (`:2326` comment: "the typechecker has already pinned uniqueness").
4. **Str representation** — the `!is_str` gate on the `Term::Recur`
   superseded-value dec (`~:2131`), a conservatism codegen cannot
   resolve because it lacks the heap/static distinction.

Every member of the raw-buf bug family (#43 / #46 / #47 / #49 / #51 /
#53 — all "check-clean, build-divergent") is a point where codegen's
re-derivation disagreed with what `check` knew, patched one leg at a
time. This milestone removes the re-derivation architecture itself.

### Framing — these are regression guards, not RED→GREEN bugs

As of 2026-05-31 (HEAD) the acute crashes are **already patched** leg
by leg:

| Program | Status at HEAD | Held green by |
|---|---|---|
| #51 `(new RawBuf (con Int) 3)` used via `size` only | **builds** | `ee4107c` (check-side — honours the written type-arg) |
| #53 `(new Counter 42)` over a user ADT | **builds** | `420703d` (codegen-side mirror — "symmetric to check") |
| #49 heap-`Str` loop binder across `recur` | **builds, leaks `live=3`** | unfixed — the one open leg, `#[ignore]`'d (`02775b5`) |

So the milestone is **not** "make three crashing programs compile."
It is "**remove the codegen re-derivation whose leg-by-leg patches
keep these programs green today — without breaking their correctness —
and close the one genuinely-open leg (#49) structurally instead of
with a fourth patch.**" The check-side corrections (`ee4107c`,
`#46`/`744ad41`) are *healthy* — they correctly populate what MIR will
carry, and they stay. The codegen-side mirrors (`420703d`, the
`synth_with_extras` loop-binder replay in `db710b1`, the `recur` dec
legs) are the disease, and they are deleted as their information
moves into MIR.

The empirical acceptance evidence is therefore: **#51 and #53 keep
building while `synth_with_extras` / the `type_home` mirrors that hold
them green are deleted** (correctness survives removal of the
re-derivation), plus **#49 goes `live=3` → `live=0`** (the one
RED→GREEN).

## Architecture

A new leaf crate `ailang-mir` defines the IR types. It is a neutral
bridge: `ailang-check` depends on it to *produce* MIR, `ailang-codegen`
depends on it to *consume* MIR. The edge `codegen → check` already
exists (`crates/ailang-codegen/Cargo.toml`), so no cycle is created;
`ailang-mir` itself has no AILang-crate dependencies except
`ailang-core` (for `Type`).

```
.ail.json ─ parse ─ resolve ─ desugar ─ typecheck ─ lift ─ monomorphise ─┐
                                                                          │  lower_to_mir  (NEW, in ailang-check)
                          monomorphised AST ───────────────────────────  ┴──▶  MirModule  ──▶  emit LLVM IR
                                                  (typed, mode/callee/rep-annotated)   (codegen: reads, derives nothing)
```

- The **authoring AST** (Form A, content-addressed, hashable) is
  **unchanged**. MIR is a compiler-internal *derived* form — never
  authored, never hashed, never round-tripped. This preserves the
  authoring contract: an author writes no type the checker already
  infers (the feature-acceptance redundancy bar).
- `lower_to_mir` runs **after monomorphisation**, on the post-mono
  workspace — the same artefact codegen lowers today. It is *not* a
  phase of `check_workspace` (which stops at typecheck, pre-mono): if
  MIR were built pre-mono it would not carry the monomorphic
  specialisations `monomorphise_workspace` appends and codegen emits,
  reintroducing the very check↔codegen gap this milestone closes. The
  build path is wrapped by one front-end entry point,
  `elaborate_workspace`, that runs check → lift → mono → lower_to_mir
  and yields a `MirWorkspace` on success or the existing
  `Vec<Diagnostic>` on a type error.
- **One type engine, not two.** `lower_to_mir` walks the post-mono AST
  with check's own canonical `synth` to fill `ty` on every node. This
  is still a type walk — `synth` is a pure `&Term → Type` function and
  the AST carries no node-ids, so MIR cannot be a side-table read; it
  is built inline by walking. What the milestone removes is not the
  walk but the *second engine*: codegen's `synth_with_extras` is a
  hand-copied mirror of `synth` that drifts from it (every raw-buf bug
  is a drift point). Replacing the mirror with a single post-mono call
  to the canonical `synth`, materialised as MIR, deletes the drift
  class structurally — there is no longer a second implementation to
  disagree.
- `lower_workspace*` in codegen take `&MirWorkspace` instead of
  `&Workspace`. The `Emitter` fields and methods that re-derive
  (`locals`' carried `Type`, `synth_with_extras`, `type_home_module`,
  the second `infer_module_with_cross` run) are deleted; their
  consumers read the MIR annotation directly.

This also resolves a standing **model drift**:
`design/models/0003-pipeline.md` already advertises "lower to MIR
(SSA-like, named SSA values)" — an artefact that never existed. This
milestone makes the model true.

## Concrete code shapes

### User-facing programs (the boundary's witnesses — parse-gated)

These three `.ail` programs are the milestone's empirical anchor. All
three are `ail check`-clean today (the disagreement is downstream of
check), so they exercise exactly the boundary this milestone owns.

**#51 — element type carried only by the author's annotation** (a
`RawBuf` read only for its `size`; nothing else observes the element
type). Regression guard: must keep building as the codegen element-type
re-derivation is removed.

```ail
(module new_rawbuf_size_only
  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (let b (new RawBuf (con Int) 3)
        (app print (app RawBuf.size b))))))
```

**#53 — monomorphic `(new T …)` over a user ADT**, the dotted callee
`Counter.new` that codegen resolves today only via a hand-copied
mirror of the checker's ladder. Regression guard: must keep building
once the mirror is deleted and the callee arrives pre-resolved in MIR.

```ail
(module new_counter_user_adt
  (data Counter (ctor MkCounter (con Int)))
  (fn new (type (fn-type (params (con Int)) (ret (con Counter)))) (params n)
    (body (term-ctor Counter MkCounter n)))
  (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params)
    (body (let c (new Counter 42) (do io/print_str "ok\n")))))
```

**#49 — heap-`Str` loop binder replaced across `recur`** (the seed is
a static literal, each `recur` rebinds to a fresh `str_concat` heap
slab). The one RED→GREEN: leaks `live=3` today (one slab per `recur`
iteration superseded without a drop); must reach `live=0`.

```ail
(module loop_recur_str_binder
  (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params)
    (body
      (let s
        (loop (acc (con Str) "x") (i (con Int) 0)
          (if (app ge i 3)
              acc
              (recur (app str_concat acc "y") (app + i 1))))
        (app print s)))))
```

### Implementation shape (secondary — before → after)

**MIR node — the bridge type** (new, `ailang-mir`). Each node carries
the facts codegen used to re-derive:

```rust
// ailang-mir/src/lib.rs  (NEW)
pub struct MirModule { pub name: String, pub defs: Vec<MirDef> }
pub struct MirDef { pub name: String, pub sig: Type, pub body: MTerm }

pub enum MTerm {
    Lit  { lit: Literal, ty: Type },
    Var  { name: String, ty: Type },
    Call { callee: Callee, args: Vec<MArg>, ty: Type, tail: bool },  // (2) callee pre-resolved
    Let  { name: String, mode: Mode, init: Box<MTerm>, body: Box<MTerm>, ty: Type },  // (3) mode
    New  { type_name: String, elem: Option<Type>, args: Vec<MTerm>, ty: Type },        // (1) elem carried
    Recur{ args: Vec<MArg>, ty: Type },
    Str  { lit: String, rep: StrRep },   // (4) Heap | Static — set by lower_to_mir
    // … one variant per Term node, each with `ty`
}
pub struct MArg  { pub term: MTerm, pub mode: Mode, pub consume_count: u32 }  // (3)
pub enum Callee  { Static { module: String, fn_name: String, sig: Type }, Builtin { name: String, sig: Type }, Indirect(Box<MTerm>) }  // (2) — sig carries the callee fn-type for drop ret_mode; Builtin for inline-lowered operators/intrinsics
pub enum StrRep  { Heap, Static }  // (4)
pub enum Mode    { Owned, Borrow }
```

**check boundary** (`ailang-check`):

```rust
// before — crates/ailang-check/src/lib.rs:1283
pub struct CheckedModule { pub symbols: IndexMap<String, (Type, String)> }   // signatures only

// after — one front-end entry wraps check → lift → mono → lower_to_mir
pub fn elaborate_workspace(ws: &Workspace) -> Result<MirWorkspace, Vec<Diagnostic>>;
// runs the full front end and lowers the POST-mono workspace to MIR.
// (check_workspace stays for the diagnostics-only callers — `ail check`,
//  which stops at typecheck; elaborate_workspace is the build path.)
```

**codegen boundary** (`ailang-codegen`):

```rust
// before — crates/ailang-codegen/src/lib.rs:278 + the Emitter re-derivers
pub fn lower_workspace(ws: &Workspace) -> Result<String>;
fn synth_with_extras(&self, t: &Term, …) -> Result<Type>;   // ~270 lines — DELETED
fn type_home_module(&self, …) -> Option<String>;            // ×3 mirrors — DELETED
let uniqueness = infer_module_with_cross(module, …);        // 2nd pass — DELETED

// after — codegen consumes MIR, reads annotations
pub fn lower_workspace(mir: &MirWorkspace) -> Result<String>;
// e.g. a Call's target is `callee` (no is_static_callee lookup);
//      a node's type is `mterm.ty()` (no synth);
//      drop placement reads `MArg.consume_count` (no re-inference).
```

## Components

- **`ailang-mir` (new crate):** `MirModule` / `MirDef` / `MTerm` /
  `Callee` / `Mode` / `StrRep` / `MirWorkspace`. Leaf; depends only on
  `ailang-core`.
- **`ailang-check::lower_to_mir` (new module):** walks the
  **monomorphised** AST with check's canonical `synth` and emits
  `MTerm`, filling `ty` on every node. Later iterations fill `callee`
  (mir.2), `mode` / `consume_count` (mir.3), `rep` (mir.4).
- **`ailang-check::elaborate_workspace` (new entry):** the single
  front-end function — runs `check_workspace` (diagnostics gate),
  `lift_letrecs`, `monomorphise_workspace`, then `lower_to_mir` on the
  post-mono workspace. Returns `MirWorkspace` or the diagnostics. This
  moves the mono orchestration out of the CLI and behind one boundary.
- **`ailang-codegen` (rewired):** entry points take `&MirWorkspace`;
  the four re-derivers are removed iteration by iteration as their
  annotation lands in MIR.
- **CLI (`crates/ail/src/main.rs`):** the build path calls
  `elaborate_workspace` (which now subsumes the explicit `lift` + `mono`
  steps the CLI orchestrated) and threads `MirWorkspace` into
  `lower_workspace*`. `check` / diagnostics paths stay on
  `check_workspace`; the `emit-ir` path builds MIR via the same
  front-end entry.

## Data flow

`Workspace (AST)` → `typecheck` (unchanged) → `lift` (unchanged) →
`monomorphise` (unchanged) → `lower_to_mir` (post-mono AST + canonical
`synth` → `MirWorkspace`) → `lower_workspace` (`MirWorkspace` → LLVM IR
text) → `clang`. The single type-inference engine is check's `synth`:
`lower_to_mir` calls it once over the post-mono bodies to materialise
MIR, and codegen reads the result rather than running its own
`synth_with_extras` mirror. The remaining `synth` walk inside
`typecheck` (pre-mono, for diagnostics) and the `lower_to_mir` walk
(post-mono, for MIR) are not redundant — they run on different
workspaces for different purposes, and both are the *same* canonical
engine, never a divergent copy.

## Error handling

`lower_to_mir` runs only on a typechecked module, so it encounters no
*type* errors. A failure to lower (e.g. an unresolved callee that the
checker accepted — exactly today's check↔codegen disagreement) is an
**internal compiler error**, surfaced as a distinct
`MirLoweringError`, not a user diagnostic: by construction, if check
passed, lowering must succeed. This is the structural property the
milestone buys — the class "check-clean but codegen-divergent" becomes
a single guarded invariant (`elaborate_workspace` returns `Ok` ⇒ MIR
is complete ⇒ codegen cannot fall through to an `UnknownVar`).

## Testing strategy

- **Regression guards (green → must stay green):** the #51 and #53
  programs above, plus the full existing workspace suite, run after
  *each* re-deriver removal. The property: deleting the codegen
  re-derivation does not change observable output.
- **#49 RED→GREEN:** `crates/ail/tests/loop_recur_str_binder_no_leak_pin.rs`
  — the `#[ignore]` is lifted in mir.4; `live=0` under `AILANG_RC_STATS`.
- **Re-derivation-is-gone pins:** each iteration adds a guard that the
  removed function is absent (e.g. a codegen unit test that the
  resolved callee comes from MIR, not a ladder walk) so the
  re-derivation cannot silently return.
- **`elaborate ⇒ codegen-total` invariant:** a test that a curated set
  of check-clean programs all lower to MIR and emit IR — the
  structural replacement for the bug family.

## Iteration decomposition

Strategy: MIR is structurally complete over all 17 `Term` variants
(`crates/ailang-core/src/ast.rs:436`) from mir.1 (codegen consumes it
fully — no AST/MIR dual path). Each iteration adds **one** annotation
class and deletes the matching codegen re-derivation.

| Iter | Adds to MIR | Deletes from codegen | Acceptance |
|---|---|---|---|
| **mir.1** | structural MIR + `ty` on every node | `synth_with_extras` + `synth_arg_type` | whole suite green (regression); `synth_with_extras` gone |
| **mir.2** | `Callee::Static` pre-resolved | `type_home_module` ×3 + `is_static_callee`; **lockstep pair `lower_app ↔ is_static_callee` struck from CLAUDE.md** | #53 guard green via MIR |
| **mir.3** | `Mode` + `consume_count` | second `infer_module_with_cross` run (`:1002`) | #43/#47 guards green; drop placement reads MIR |
| **mir.4** | `StrRep` (loop-carried `Str` ⇒ `Heap` via `str_clone` at loop entry) | the `!is_str` `recur` dec gate | #49 `live=0`; `#[ignore]` lifted |
| **mir.5** | element-type / `Term::New` fully on MIR + **ledger** | last re-derivation residue | #51 guard green via MIR; ledger consistent |

> mir.2 refinement (discovered in planning, `docs/plans/0116-mir.2-callee-static.md`):
> `Callee` gains a `Builtin { name, sig }` variant (operators / str-num
> intrinsics have no `module`/`fn_name`) and a `sig: Type` on each
> resolved variant (codegen's drop path reads the callee `ret_mode` off
> it — the lossless replacement for the pre-mir.2 `Indirect(inner).ty()`
> read; this is NOT a mir.3 pull-forward, the `MArg` param-modes stay at
> mir.1 defaults). `type_home_module` is fully deletable: its
> value-position consumer (`resolve_top_level_fn`) is unreachable for
> type-scoped names in the current corpus, so the acceptance
> "type_home_module grep-clean" holds.

mir.5 carries the ledger work as part of the milestone (per CLAUDE.md:
contract changes ship with the iteration that needs them):

- **New contract** `design/contracts/NNNN-check-codegen-boundary.md`:
  the invariant "codegen re-derives nothing; MIR is total over what
  check proved; `elaborate_workspace` ⇒ codegen cannot fall through."
- **Revise** `design/contracts/0013-typeclasses.md:106-120`: the
  passage that *blesses* codegen-side cross-module re-resolution as
  correct-by-design is retracted — resolution now lives in MIR.
- **Correct** `design/models/0003-pipeline.md`: the "lower to MIR"
  line becomes true (point at the real stage).
- **INDEX** `design/INDEX.md`: add the boundary contract row; the
  `qualified-xref` / codegen rows re-point at MIR consumption.
- **Issue hygiene:** close #51 / #53 (now structurally held, not
  patch-held); milestone #7 (raw-buf) is reset to **not met** and
  subsumed — #49/#51/#53 become MIR-iteration acceptance, not a
  separate patch track.

## Acceptance criteria

1. `ailang-codegen` contains **no** type synthesis, no callee-ladder
   walk, and no uniqueness inference: `synth_with_extras`,
   `synth_arg_type`, `type_home_module`, and the
   `infer_module_with_cross` call are removed; grep-clean.
2. The build path is `Workspace → elaborate_workspace → MirWorkspace →
   lower_workspace`; codegen's public entry points take
   `&MirWorkspace`.
3. The #51 and #53 programs build and run unchanged across every
   iteration (correctness survives re-deriver removal).
4. The #49 program reaches `live=0`; its test's `#[ignore]` is lifted.
5. The `lower_app ↔ is_static_callee` lockstep pair is gone from
   CLAUDE.md (structurally unnecessary), and 0013's blessed
   re-resolution passage is retracted.
6. `design/models/0003-pipeline.md`'s MIR line names the real stage;
   the new boundary contract is in INDEX.
7. The full workspace test suite is green at each iteration close.