spec: intrinsic-bodies — revise AST repr to Term::Intrinsic leaf (refs #9)

Forward-fix on c42034b. plan-recon for intrinsic-bodies.1 surfaced
that the original AST representation — FnDef.body / Term::Lam.body
made Option<Term> plus an `intrinsic: bool` flag — has a ~150-site
blast radius across six crates: every body read/construct site breaks
when a mandatory public field goes optional. That blast radius is the
signal (CLAUDE.md design-rationale rule) that the representation was
wrong, not merely expensive.

The Form-A surface (user's chosen Approach 1) and the Local-Reasoning
semantics (Design X marker placement) are UNCHANGED. Only the internal
AST representation changes, which is orchestrator authority over AST
design.

New representation: a single new leaf Term variant, Term::Intrinsic
({ "t": "intrinsic" }), is the body of a compiler-supplied definition.
FnDef.body (Term) and Term::Lam.body (Box<Term>) keep their existing
types. A def is intrinsic iff matches!(body, Term::Intrinsic).

Three structural reasons (not effort):

1. Established pattern. The project adds new constructs as additive
   Term variants — Term::New, Term::Loop, Term::Recur, Term::Clone,
   Term::ReuseAs all landed this way, documented "strictly additive,
   pre-existing fixtures hash bit-identically" in
   design/contracts/0002-data-model.md. Term::Intrinsic follows it.
   Option A introduced a brand-new pattern (mandatory field → optional)
   absent from the schema.

2. Meaning at the right locus. "This body is compiler-supplied" is a
   property of the body, not the container. Term::Intrinsic sits at the
   body position — fn body, or instance-method lambda body (Design X
   local-signature placement preserved exactly).

3. Illegal state unrepresentable. Option A admitted intrinsic:true with
   body:Some(...), forcing an intrinsic-with-body reject. Under the
   variant a body is either Term::Intrinsic or a real term, never both
   — the reject is deleted, the state cannot occur. This is the same
   make-illegal-states-unrepresentable discipline as the honesty theme
   the milestone exists to serve.

Blast radius collapses from ~150 body-read/construct sites to the
exhaustive match-on-Term arms (canonical/hash/visit + schema_coverage),
which the no-wildcard Term match turns into compile errors until each
gains a Term::Intrinsic case — the project's normal new-variant
discipline.

Sections revised: § Architecture points 1/3/4, § Concrete code shapes
(Implementation shape now shows the leaf variant, not the
Option+flag), § Components, § Data flow, § Error handling (the
intrinsic-with-body row removed), § Testing strategy (the
both-body-and-intrinsic reject test removed; schema_coverage Term::Intrinsic
observation added). The scheme/ail surface examples are byte-unchanged.

Re-ran the brainstorm gates on the revision: Step-7 parse gate green
(both ail blocks exit 0, unchanged); Step-7.5 grounding-check PASS on
the four new load-bearing claims (additive-variant precedent +
contract wording, exhaustive-Term-match mechanism, mono.rs
synthesise_mono_fn destructure unchanged under preserved body type,
Term::Recur as non-reducing-leaf precedent).

docs/specs/0055-intrinsic-bodies.md

@@ -54,25 +54,50 @@ Three landing points, two iterations.
 
 **Iteration `intrinsic-bodies.1` — the mechanism.**
 
-1. **AST.** `FnDef.body` and `Term::Lam.body` become *optional*; a
+1. **AST.** A new leaf term variant `Term::Intrinsic` is the body of
-   new `intrinsic: bool` flag rides each. `intrinsic: true` ⟺
+   a compiler-supplied definition. `FnDef.body` and `Term::Lam.body`
-   `body` absent. The flag is additive and `skip_serializing_if`-gated,
+   keep their existing types (`Term` / `Box<Term>`) — they are not made
-   so every existing fixture's canonical-JSON hash stays bit-identical
+   optional. A definition is intrinsic iff its body *is*
-   (the standard additive-schema pattern, `design/contracts/0002-data-model.md`).
+   `Term::Intrinsic`. The variant is strictly additive: a fixture that
-2. **Form-A surface.** Parser accepts `(intrinsic)` as a sibling
+   does not use it serialises bit-identically (the established
-   attribute to `(body ...)` inside both `fn-def` and `lam`; the
+   additive-term-variant pattern — `Term::New`, `Term::Loop`,
-   printer emits it. Round-trip (`parse ∘ print = id`) holds by the
+   `Term::Recur`, `Term::Clone`, `Term::ReuseAs` all landed this way,
-   standard fixture gate.
+   `design/contracts/0002-data-model.md`). This is the load-bearing
-3. **Checker.** An `(intrinsic)` definition type-checks against its
+   representation choice: it puts "this body is compiler-supplied" at
-   *signature only* — there is no body to check. Two new rejects:
+   the body position where it semantically belongs, keeps the
-   (a) a definition carrying **both** a body and `intrinsic` is
+   ~150-site `body`-read/construct surface across six crates untouched
-   malformed; (b) an `(intrinsic)` definition outside a `(kernel)`-tier
+   (only exhaustive `match`-on-`Term` arms gain a case), and makes the
-   module or the prelude is rejected with `intrinsic-outside-kernel-tier`.
+   illegal "body AND intrinsic" state *unrepresentable* rather than
-4. **Codegen.** An `(intrinsic)` definition routes through
+   rejected — a body is either `Term::Intrinsic` or a real term, never
-   `intercepts::lookup`; if no intercept is registered for its
+   both. (The rejected alternative, `body: Option<Term>` + an
-   mangled name, codegen emits the existing deferral diagnostic.
+   `intrinsic: bool` flag, splits one fact across two fields, admits
-   The current "lower the body" path is simply not taken for these
+   that illegal state, and breaks every `body` consumer in the
-   definitions.
+   workspace.)
+2. **Form-A surface.** For a top-level fn, the parser accepts
+   `(intrinsic)` as a sibling clause where `(body ...)` would go and
+   maps it to `body = Term::Intrinsic`; the printer emits `(intrinsic)`
+   in that slot when the body is `Term::Intrinsic`. For a lambda,
+   `(intrinsic)` sits at the positional body slot (where the body term
+   goes today) and parses to `Term::Intrinsic`; the printer emits it
+   there. Round-trip (`parse ∘ print = id`) holds by the standard
+   fixture gate. The fn-vs-lam surface asymmetry mirrors the existing
+   one (a fn carries a named `(body X)` clause; a lambda carries its
+   body positionally) — `(intrinsic)` follows each form's existing body
+   placement.
+3. **Checker.** A definition whose body is `Term::Intrinsic`
+   type-checks against its *signature only* — there is no body term to
+   infer. One new reject: an intrinsic definition outside a
+   `(kernel)`-tier module or the prelude is rejected with
+   `intrinsic-outside-kernel-tier`. (There is no `intrinsic-with-body`
+   reject — the representation makes that state impossible, see point 1.)
+4. **Codegen.** A definition whose body is `Term::Intrinsic` routes
+   through `intercepts::lookup`; if no intercept is registered for its
+   mangled name, codegen emits the existing deferral diagnostic. The
+   current "lower the body" path is not taken for these definitions —
+   `lower_term` is never called on a `Term::Intrinsic` body (and a
+   `Term::Intrinsic` reaching `lower_term` through any other path is a
+   codegen-internal error, since an intrinsic body must be consumed by
+   the intercept route).
 5. **Ratifier.** One throwaway intrinsic in the `kernel_stub`
    fixture — a nullary `answer : () -> Int` whose intercept emits
    `ret i64 42` — drives the mechanism end-to-end (parse → check →
@@ -178,30 +203,32 @@ error: [surface-parse-error] parse error in fn-def: unknown fn attribute
 
 ### Implementation shape (secondary — the AST delta)
 
-Before → after on the two load-bearing structs. Exact bytes are the
+The change is one new leaf `Term` variant. Exact bytes are the
 planner's job; this fixes the shape only.
 
-`FnDef` (`crates/ailang-core/src/ast.rs`):
+`Term::Intrinsic` (`crates/ailang-core/src/ast.rs`):
 
 ```jsonc
-// before
+// new leaf term — the body of a compiler-supplied definition.
-{ "kind": "fn", "name": "...", "type": Type, "params": [...], "body": Term, ... }
+// Strictly additive (no skip_serializing_if needed; a fixture that
-
+// does not carry it hashes bit-identically — the same additive-variant
-// after — body optional, intrinsic flag additive
+// pattern as Term::New / Term::Loop / Term::Recur / Term::Clone).
-{ "kind": "fn", "name": "...", "type": Type, "params": [...],
+// Never reduces to a value: codegen consumes it via intercepts::lookup,
-  "body": Term,            // present ⟺ intrinsic absent/false
+// the typechecker treats a def with this body as signature-only.
-  "intrinsic": true,       // optional; omitted when false (hash-stable when omitted).
+{ "t": "intrinsic" }
-                           // When true: body MUST be absent; the def is legal only in a
-                           // (kernel)-tier module or the prelude; codegen routes through
-                           // intercepts::lookup on the mangled name.
-  ... }
 ```
 
-`Term::Lam` (same crate) takes the symmetric pair: `body` becomes
+`FnDef.body` (currently `Term`) and `Term::Lam.body` (currently
-optional, `intrinsic: bool` is added. An instance method whose body
+`Box<Term>`) are **unchanged in type** — they simply may now hold
-is a lambda (every `eq`/`compare` instance) carries the marker on the
+`Term::Intrinsic`. A top-level intrinsic fn is
-*lambda body*, **not** on the method as a whole — and this placement
+`FnDef { body: Term::Intrinsic, .. }`; an intrinsic instance-method
-is load-bearing, not incidental.
+lambda is `Term::Lam { body: Box::new(Term::Intrinsic), .. }`. "Is
+this definition intrinsic?" is `matches!(body, Term::Intrinsic)`.
+
+The marker sits at the body position — for a top-level fn that is the
+fn body; for an instance method that is the *lambda body*, **not** the
+method as a whole — and this placement is load-bearing, not
+incidental.
 
 The reason is local reasoning (`design/INDEX.md` § Goal: "every
 definition carries its full type and effect set, so a signature can
@@ -217,64 +244,71 @@ are the parameter types and return type, readable at the definition
 site. Hoisting the marker to the method (`(method eq (intrinsic))`)
 would erase that local signature — a reader would have to climb to
 the `Eq` class declaration and substitute `a := Int` mentally to
-recover it. So the marker replaces the lambda's *body*, leaving the
+recover it. So the marker is the lambda's *body* (`Term::Intrinsic`),
-lambda's typed shell — the local signature — in place. The mono pass
+leaving the lambda's typed shell — the local signature — in place. The
-(`crates/ailang-check/src/mono.rs::synthesise_mono_fn`) already reads
+mono pass (`crates/ailang-check/src/mono.rs::synthesise_mono_fn`)
-the method's parameter names and inner body out of this lambda; the
+already reads the method's parameter names and inner body out of this
-intrinsic marker rides where the dummy body sits today, so that path
+lambda (`Term::Lam { params, body, .. } => (params, *body)`); with the
-is unchanged.
+inner body being `Term::Intrinsic`, the synthesised `FnDef` carries
+`body: Term::Intrinsic` and is itself intrinsic. The destructure
+itself is unchanged — only what the inner body *is* differs.
 
-Serde note: `Option<Term>` serialises `Some(t)` as `t` (not as a
+Hash-stability note: `Term::Intrinsic` is a new enum variant, not a
-tagged wrapper), so a non-intrinsic def's `"body": {...}` is
+new field, so a fixture that does not use it serialises exactly as
-byte-identical before and after. `None` is `skip_serializing_if`-omitted.
+before — the same mechanism that kept hashes stable when `Term::New`,
-This is what keeps every existing fixture's hash stable; the
+`Term::Loop`, and `Term::Recur` were added. The `design_schema_drift.rs`
-`design_schema_drift.rs` schema mirror and the `0002-data-model.md`
+schema mirror, the `schema_coverage.rs` variant corpus (a fixture must
-contract move in the same iteration as the struct change.
+now exercise `Term::Intrinsic`), and the `0002-data-model.md` contract
+all move in the same iteration as the variant.
 
 ## Components
 
 | Component | Iteration | Change |
 |---|---|---|
-| `crates/ailang-core/src/ast.rs` | .1 | `FnDef.body` / `Lam.body` → optional; `intrinsic: bool` added to both. |
+| `crates/ailang-core/src/ast.rs` | .1 | New leaf variant `Term::Intrinsic`. `FnDef.body` / `Lam.body` types unchanged. |
-| `crates/ailang-core` canonical/hash/visit | .1 | Visitors gain an explicit intrinsic arm (no body to walk). Schema-coverage corpus extended. |
+| `crates/ailang-core` canonical/hash/visit | .1 | Exhaustive `match`-on-`Term` arms gain a `Term::Intrinsic` case (leaf, no sub-terms to walk). Schema-coverage corpus extended to exercise it. |
-| `crates/ailang-surface` (lex/parse/print) | .1 | `(intrinsic)` attribute parsed + printed in `fn-def` and `lam`; round-trip gated. |
+| `crates/ailang-surface` (lex/parse/print) | .1 | `(intrinsic)` parsed + printed: as a body-slot clause in `fn-def`, at the positional body slot in `lam`; maps to/from `Term::Intrinsic`; round-trip gated. |
-| `crates/ailang-check/src/lib.rs` | .1 | Intrinsic def checks signature-only; rejects body+intrinsic; rejects intrinsic outside kernel-tier/prelude (`intrinsic-outside-kernel-tier`). |
+| `crates/ailang-check/src/lib.rs` | .1 | A def whose body is `Term::Intrinsic` checks signature-only; rejects intrinsic outside kernel-tier/prelude (`intrinsic-outside-kernel-tier`). No `intrinsic-with-body` reject — the representation forbids that state. |
-| `crates/ailang-codegen/src/lib.rs` | .1 | Intrinsic def routes through `intercepts::lookup`; body-lowering path not taken for it. |
+| `crates/ailang-check/src/mono.rs` | .1 | `synthesise_mono_fn` lambda-destructure unchanged; an inner `Term::Intrinsic` body flows through to an intrinsic synthesised `FnDef`. |
+| `crates/ailang-codegen/src/lib.rs` | .1 | A def whose body is `Term::Intrinsic` routes through `intercepts::lookup`; `lower_term` is never called on it. |
 | `crates/ailang-kernel-stub` + `ailang-surface` parse hop | .1 | `answer` smoke intrinsic added to the stub fixture; its intercept registered. |
 | `examples/prelude.ail` | .2 | 18 dummy bodies → `(intrinsic)`. |
 | `crates/ailang-codegen/src/intercepts.rs` (pin) | .2 | `registry_contains_all_legacy_arms` upgraded to a source↔registry bijection pin. |
 | codegen dummy-body path | .2 | Removed. |
-| `design/contracts/0002-data-model.md` | .1 | `fn` + `lam` schema gain `intrinsic`; `body` documented optional. |
+| `design/contracts/0002-data-model.md` | .1 | New `{ "t": "intrinsic" }` Term entry; note in `fn`/`lam` that the body may be `Term::Intrinsic`. |
 | `design/contracts/0007-honesty-rule.md` | .2 | The prelude-dummy infraction is closed; note its resolution if the contract references it. |
 
 ## Data flow
 
 Authoring → parse → AST → check → codegen, unchanged in topology;
-the intrinsic flag is read at three of those stations:
+`Term::Intrinsic` is recognised at three of those stations:
 
-1. **Parse.** `(intrinsic)` sets `intrinsic = true`, leaves `body = None`.
+1. **Parse.** `(intrinsic)` in a fn body slot or a lambda body slot
-   A `fn-def`/`lam` carrying both `(body ...)` and `(intrinsic)` is a
+   produces a `Term::Intrinsic` body. There is no "both body and
-   parse-level malformation (or a check-level one — planner picks the
+   intrinsic" surface form to reject — the grammar offers one body
-   station; the reject must exist).
+   slot, and `(intrinsic)` either fills it or it does not.
-2. **Check.** Intrinsic def: validate the signature, skip body
+2. **Check.** A def whose body is `Term::Intrinsic`: validate the
-   inference. Enforce the kernel-tier/prelude scope. The module's
+   signature, skip body inference. Enforce the kernel-tier/prelude
-   `kernel: true` flag (or prelude identity) is already available to
+   scope. The module's `kernel: true` flag (or prelude identity) is
-   the checker via the loaded workspace.
+   already available to the checker via the loaded workspace.
-3. **Codegen.** Intrinsic def: `intercepts::lookup(mangled_name)`.
+3. **Codegen.** A def whose body is `Term::Intrinsic`:
-   Hit → emit the intercept. Miss → the existing deferral diagnostic
+   `intercepts::lookup(mangled_name)`. Hit → emit the intercept.
-   (same one raw-buf.2 reuses for unregistered `RawBuf` ops).
+   Miss → the existing deferral diagnostic (same one raw-buf.2 reuses
+   for unregistered `RawBuf` ops).
 
 ## Error handling
 
 | Condition | Diagnostic | Station |
 |---|---|---|
-| `(intrinsic)` and `(body ...)` on the same def | `intrinsic-with-body` (malformed) | parse or check |
 | `(intrinsic)` in a non-kernel, non-prelude module | `intrinsic-outside-kernel-tier` | check |
 | Intrinsic def with no registered intercept | existing codegen deferral | codegen |
 
-The middle row is the honesty-rule guard at the workspace boundary:
+The first row is the honesty-rule guard at the workspace boundary:
 user code cannot mark a body as compiler-supplied, so the lie cannot
-re-enter through user modules.
+re-enter through user modules. (There is deliberately no
+"body-and-intrinsic" row — `Term::Intrinsic` is a body, so a def
+either has it or has a real body, never both. The illegal state is
+unrepresentable, not diagnosed.)
 
 ## Testing strategy
 
@@ -286,11 +320,11 @@ re-enter through user modules.
 - Check accept: the `kernel_stub` `answer` intrinsic checks clean.
 - Check reject (scope): a user module with an `(intrinsic)` fn is
   rejected with `intrinsic-outside-kernel-tier`.
-- Check reject (malformed): a def with both body and intrinsic is rejected.
 - E2E: `answer` builds and runs, exit/print observing `42` — the
   mechanism works from source to native.
 - Schema drift: `design_schema_drift.rs` green against the new
-  `0002-data-model.md`.
+  `0002-data-model.md`; `schema_coverage.rs` observes `Term::Intrinsic`
+  in the fixture corpus.
 
 **intrinsic-bodies.2:**