AILang/docs/plans/0103-prep.3-kernel-tier-modules.md

# prep.3 — Kernel-tier modules + `param-in` — Implementation Plan

> **Parent spec:** `docs/specs/0052-kernel-extension-mechanics.md`
>
> **For agentic workers:** REQUIRED SUB-SKILL: use the `implement`
> skill to run this plan. Steps use `- [ ]` checkboxes for tracking.

**Goal:** Ship the third and terminal iteration of the kernel-extension-mechanics milestone: two coupled schema additions (`Module.kernel`, `TypeDef.param-in`), their Form-A surface, the generalisation of the hardcoded `prelude` auto-injection into a flag-driven multi-module mechanism, generic `param-in` checker enforcement with a new diagnostic, and a stub kernel crate as the end-to-end ratifying fixture.

**Architecture:** Both schema fields are strictly additive — `Module.kernel` uses `skip_serializing_if = "is_false"`, `TypeDef.param_in` uses `skip_serializing_if = "BTreeMap::is_empty"` — so every pre-existing fixture's canonical-JSON hash is bit-stable except `prelude.ail`, which intentionally gains `(kernel)`. The workspace-load migration replaces the hardcoded `&["prelude"]` literal at `crates/ailang-surface/src/loader.rs:108` with a `modules.values().filter(|m| m.kernel)` derivation; the same `parse_prelude()` injection at line 103 remains because the prelude has no on-disk manifest in user workspaces. The `param-in` enforcement adds one diagnostic (`ParamNotInRestrictedSet`) and one pass in `check_type_well_formed`'s `Type::Con` arm; restriction data lives on the TypeDef and is consulted generically — no special-cased extension type in the checker.

**Tech Stack:** `ailang-core` (schema + workspace-load), `ailang-surface` (Form-A parse/print + loader), `ailang-check` (diagnostic + enforcement), new `ailang-kernel-stub` crate (ratifying fixture), `serde` for the additive serialisation, `BTreeMap`/`BTreeSet` for deterministic `param-in` iteration order.

---

## Open-question decisions (committed before plan-write)

The plan-recon report flagged four open questions. Each is resolved here so no task carries a TBD:

- **OQ1 — Form-A grammar for `(param-in ...)`.** **Decision:** one outer clause carrying one or more inner var-lists: `(param-in (a Int Float) (b Str))`. Mirrors `(ctors (A …) (B …))`; one parser arm, one printer arm; JSON BTreeMap shape is unambiguous. Rejected alternative: repeated `(param-in ...)` clauses (would force list-of-clauses gathering and break the "one attribute, one arm" parser pattern used elsewhere).
- **OQ2 — Stub form: programmatic vs `module.ail.json` embed.** **Decision:** programmatic. The stub crate's `src/lib.rs` exports `pub fn parse_kernel_stub() -> Module { parse(STUB_AIL).expect(...) }`, mirror of `parse_prelude` at `crates/ailang-surface/src/loader.rs:41-43`. `STUB_AIL` is a `const &str` carrying the Form-A source of the stub module. One source of truth, no embedded canonical-JSON duplication.
- **OQ3 — `WorkspaceLoadError::ReservedModuleName` shape.** **Decision:** keep `{ name: String }`. Only the doc comment and diagnostic message text change. No second consumer for a `reserved_set: Vec<String>` field today; adding it now is premature mechanism.
- **OQ4 — `crates/ailang-core/src/workspace.rs:2655`.** **Decision:** the line lives in test code (`mq1_qualified_instancedef_class_accepted` body) and is one of ~20 test sites that pass `&["prelude"]` to `validate_canonical_type_names`. The validator helpers' signatures do not change in prep.3 — only the loader's *value* threaded into `build_workspace` changes. Test sites remain `&["prelude"]` literals; no migration.

---

## Files this plan creates or modifies

**Create:**

- `crates/ailang-kernel-stub/Cargo.toml` — new internal crate, mirror of `crates/ailang-prose/Cargo.toml` shape (package metadata + `ailang-surface.workspace = true`, `ailang-core.workspace = true`).
- `crates/ailang-kernel-stub/src/lib.rs` — exposes `parse_kernel_stub() -> Module`; `STUB_AIL` is a `const &str` carrying the Form-A source.
- `crates/ailang-core/tests/workspace_kernel.rs` — integration tests for auto-import semantics (kernel-tier visibility without explicit `(import ...)`, two kernel-tier modules co-load, explicit-import-overrides-auto-import precedence).

**Modify (source code):**

- `crates/ailang-core/src/ast.rs:29-42` — `Module` gains `pub kernel: bool` with `#[serde(default, skip_serializing_if = "is_false")]`.
- `crates/ailang-core/src/ast.rs:135-170` — `TypeDef` gains `pub param_in: BTreeMap<String, BTreeSet<String>>` with `#[serde(default, skip_serializing_if = "BTreeMap::is_empty", rename = "param-in")]`; new `use std::collections::{BTreeMap, BTreeSet}` import at the top of the file.
- ~130 `Module { ... }` struct-literal sites across `crates/{ailang-prose, ailang-codegen, ailang-surface, ailang-check, ailang-core}/src/` and `crates/{ailang-check, ailang-surface}/tests/` — add `kernel: false,` to each (mechanical sweep; the additive `#[serde(default)]` covers deserialise paths, only Rust struct literals break).
- ~30 `TypeDef { ... }` struct-literal sites across `crates/{ailang-prose, ailang-codegen, ailang-check, ailang-core}/src/` and `crates/{ailang-check, ailang-core}/tests/` — add `param_in: BTreeMap::new(),` to each.
- `crates/ailang-surface/src/parse.rs:283-335` — `parse_module` gains a `(kernel)` attribute case before the defs/imports loop.
- `crates/ailang-surface/src/parse.rs:354-436` — `parse_data` (TypeDef parser) gains a `(param-in (var t1 t2 ...) ...)` case in its inner attribute loop.
- `crates/ailang-surface/src/print.rs:17-33` — `Module` printer emits `(kernel)` when `module.kernel == true`.
- `crates/ailang-surface/src/print.rs:103-135` — `write_type_def` emits `(param-in (<var> <T1> ...) ...)` blocks when `!td.param_in.is_empty()`.
- `crates/ailang-surface/src/loader.rs:88-110` — `load_workspace`: hardcoded `&["prelude"]` literal and the `"prelude"` reservation literal replaced by derivation from `modules.values().filter(|m| m.kernel)`. The `parse_prelude()` injection at line 103 stays.
- `crates/ailang-core/src/workspace.rs:307-312` — `ReservedModuleName` doc comment + diagnostic prose update; variant shape `{ name: String }` unchanged.
- `crates/ailang-core/src/workspace.rs:465-493` — `build_workspace` doc-comment update (signature unchanged; doc clarifies the implicit-imports list is caller-derived from the kernel-flag filter).
- `crates/ail/src/main.rs:1234-1244` — CLI mapping for `ReservedModuleName` diagnostic — human message text update.
- `crates/ailang-check/src/lib.rs:721-742` — new `CheckError::ParamNotInRestrictedSet` variant adjacent to existing `NewArgKindMismatch`.
- `crates/ailang-check/src/lib.rs:797-798` — `CheckError::code()` arm for the new variant.
- `crates/ailang-check/src/lib.rs:876-879` — `CheckError::ctx()` arm for the new variant.
- `crates/ailang-check/src/lib.rs:1920-1998` — `check_type_well_formed`'s `Type::Con` arm walks the resolved TypeDef's `param_in` and emits `ParamNotInRestrictedSet` on violation. New in-source tests in the same file's `#[cfg(test)] mod tests` block: `param_in_accepts_allowed_type`, `param_in_rejects_disallowed_type`.
- `examples/prelude.ail:1` — module header gains `(kernel)`.

**Modify (tests):**

- `crates/ailang-core/tests/design_schema_drift.rs` — append three new round-trip tests (`module_kernel_flag_round_trips`, `typedef_param_in_round_trips`, `kernel_stub_module_round_trips`) modelled on the existing `term_new_round_trips`/`term_new_type_arg_round_trips` (lines 559-629). Also `param_in` field added to the `TypeDef` literal at line 323-329 (compile gate).
- `crates/ailang-surface/tests/prelude_module_hash_pin.rs:27` — refresh the pinned hex hash because the prelude's canonical-JSON now contains `"kernel": true`; Honesty-Rule provenance comment block above the literal quoting prep.3 (mirrors lines 15-25 prior re-pin reasons).
- `crates/ailang-surface/tests/round_trip.rs` (or analogous existing surface round-trip file) — fixtures for `(kernel)` in module header and `(param-in ...)` in TypeDef body.

**Modify (design ledger):**

- `design/contracts/0002-data-model.md:14-23` — Module schema block gains `"kernel": true   // optional; omitted when false (hash-stable when omitted)` line and a "see prep.3 of the kernel-extension-mechanics milestone" footnote in the prose section.
- `design/contracts/0002-data-model.md:55-66` — TypeDef schema block gains `"param-in": { "<var>": ["<TypeName>", ...] }   // optional; omitted when empty (hash-stable when omitted)` line.
- `design/INDEX.md:111` — annotation update for the `kernel-extensions` row (the `(design accepted 2026-05-28; impl in progress)` annotation transitions to reflect milestone-close state once prep.3 lands).
- `design/models/0007-kernel-extensions.md:1-12 + 215-276` — STATUS header transitions prep.3 from "in progress" to "shipped"; sections describing the kernel-tier mechanism and `param-in` transition from forward-looking ("will resolve…") to present-state ("resolves…").

---

### Task 1: `Module.kernel` schema field + struct-literal sweep + drift round-trip + data-model anchor

**Files:**
- Modify: `crates/ailang-core/src/ast.rs:29-42`
- Modify: ~130 `Module { ... }` struct-literal sites enumerated by `rg -n '\bModule \{' --type rust crates/` — top concentrations: `crates/ailang-codegen/src/lib.rs` (~22 sites), `crates/ailang-check/src/lib.rs` (~25 sites), `crates/ailang-check/src/linearity.rs` (~14 sites), `crates/ailang-check/src/uniqueness.rs` (~5 sites), `crates/ailang-check/src/reuse_shape.rs` (~3 sites), `crates/ailang-core/src/desugar.rs` (~16 sites), `crates/ailang-core/src/pretty.rs` (~1 site), `crates/ailang-prose/src/lib.rs` (~2 sites), `crates/ailang-surface/src/parse.rs` (1 site at line 329), `crates/ailang-surface/src/print.rs` (~5 sites), `crates/ailang-check/tests/workspace.rs` (~6 sites), `crates/ailang-check/tests/duplicate_ctor_pin.rs` (1 site), `crates/ailang-core/src/workspace.rs` (~4 test-helper sites in `mod tests`).
- Test: `crates/ailang-core/tests/design_schema_drift.rs` — append `module_kernel_flag_round_trips`.
- Modify: `design/contracts/0002-data-model.md:14-23` — anchor block.

- [ ] **Step 1: Add `Module.kernel` field**

In `crates/ailang-core/src/ast.rs`, replace the existing Module struct definition at lines 29-42 with:

```rust
pub struct Module {
    /// Schema identifier; must equal [`crate::SCHEMA`] at load time.
    pub schema: String,
    /// Module name. By convention matches the file stem
    /// (`<name>.ail.json`); the [`crate::workspace`] loader enforces
    /// this on import.
    pub name: String,
    /// Kernel-tier flag. When `true`, the module's top-level type
    /// names and free defs are visible to every consumer without an
    /// explicit `(import …)` declaration. Strictly additive: omitted
    /// from canonical JSON when `false`, so every pre-existing
    /// fixture's hash is bit-stable. See prep.3 of the
    /// kernel-extension-mechanics milestone.
    #[serde(default, skip_serializing_if = "is_false")]
    pub kernel: bool,
    /// Imports of other modules. Resolved by the workspace loader as
    /// `<root_dir>/<module>.ail.json`.
    #[serde(default)]
    pub imports: Vec<Import>,
    /// Top-level definitions in declaration order.
    pub defs: Vec<Def>,
}
```

(`is_false` already exists at `crates/ailang-core/src/ast.rs:931`; no new helper.)

- [ ] **Step 2: Surface compile errors across the workspace**

Run: `cargo build --workspace 2>&1 | rg 'missing field .kernel.' | wc -l`
Expected: a positive integer ~130 (each `Module { ... }` literal site missing the new field; the exact count is informational — the next step uses the build's own error list as the work queue).

- [ ] **Step 3: Mechanical sweep — add `kernel: false,` to every Module struct-literal site**

For each compile error of shape `error[E0063]: missing field \`kernel\` in initializer of \`ailang_core::ast::Module\``, open the file/line, insert `kernel: false,` into the struct literal. Insertion order convention: between `name: ...,` and `imports: ...,` (mirrors the field declaration order in `ast.rs`). For one-line literals, the field becomes a comma-separated element; for multi-line literals, it gets its own line at the same indentation as the surrounding fields.

Example (`crates/ailang-surface/src/parse.rs:329` — the parser's only construction):

Before:
```rust
Ok(Module {
    schema: SCHEMA.to_string(),
    name,
    imports,
    defs,
})
```

After:
```rust
Ok(Module {
    schema: SCHEMA.to_string(),
    name,
    kernel: false,
    imports,
    defs,
})
```

(`parse_module` will set `kernel` from the parsed `(kernel)` attribute in Task 3; for now the parser still emits `kernel: false` by default, matching modules that have no attribute. Task 3 replaces this literal with the parsed value.)

- [ ] **Step 4: Compile-gate**

Run: `cargo build --workspace 2>&1 | tail -5`
Expected: no `error[E0063]` lines; build succeeds (warnings are acceptable but the build must terminate with exit code 0).

- [ ] **Step 5: Update Module schema anchor in data-model contract**

In `design/contracts/0002-data-model.md`, replace lines 14-23 with:

```markdown
### Module

```jsonc
{
  "schema": "ailang/v0",
  "name": "<id>",
  "kernel": true,                                  // optional; omitted when false (hash-stable when omitted). Kernel-tier modules are auto-imported by every consumer. See prep.3 of the kernel-extension-mechanics milestone.
  "imports": [{ "module": "<id>", "as": "<id>" }],
  "defs": [Def...]
}
```
```

(The kebab/case naming check in `design_schema_drift.rs`'s anchor scan will accept the bare `kernel` key because it is camelCase-already; the lowercase Rust field name serialises unchanged.)

- [ ] **Step 6: Add `module_kernel_flag_round_trips` drift test**

Append to `crates/ailang-core/tests/design_schema_drift.rs` (after the existing `term_new_type_arg_round_trips` at line 629):

```rust
/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of
/// `Module.kernel`. Property protected: when `true`, the key
/// serialises as the bare `"kernel": true` flag adjacent to
/// `"name"`; when `false`, it is omitted entirely from canonical
/// JSON (preserving the bit-identical hash of every pre-existing
/// fixture). A future edit that renames the field, drops the
/// `skip_serializing_if`, or changes its boolean shape breaks the
/// pin in lockstep with the data-model document.
#[test]
fn module_kernel_flag_round_trips() {
    let m_on = Module {
        schema: ailang_core::SCHEMA.to_string(),
        name: "k".into(),
        kernel: true,
        imports: vec![],
        defs: vec![],
    };
    let json_on = serde_json::to_value(&m_on).expect("serialise kernel: true");
    assert_eq!(
        json_on["kernel"], true,
        "kernel: true must appear as a bare boolean key"
    );

    let m_off = Module {
        schema: ailang_core::SCHEMA.to_string(),
        name: "k".into(),
        kernel: false,
        imports: vec![],
        defs: vec![],
    };
    let json_off = serde_json::to_value(&m_off).expect("serialise kernel: false");
    assert!(
        json_off.get("kernel").is_none(),
        "kernel: false must be omitted from canonical JSON (hash-stability)"
    );

    let recovered: Module =
        serde_json::from_value(json_on).expect("Module with kernel: true round-trips");
    assert!(recovered.kernel);
}
```

- [ ] **Step 7: Run drift tests**

Run: `cargo test --workspace --test design_schema_drift module_kernel_flag_round_trips`
Expected: 1 passed.

Run: `cargo test --workspace --test design_schema_drift`
Expected: all prior drift tests pass; the new one passes. Result line: `N passed; 0 failed`.

---

### Task 2: `TypeDef.param_in` schema field + struct-literal sweep + drift round-trip + data-model anchor

**Files:**
- Modify: `crates/ailang-core/src/ast.rs:20` (imports) + `crates/ailang-core/src/ast.rs:135-170` (struct).
- Modify: ~30 `TypeDef { ... }` struct-literal sites enumerated by `rg -n '\bTypeDef \{' --type rust crates/` — top concentrations: `crates/ailang-check/src/lib.rs` (~12 sites), `crates/ailang-prose/src/lib.rs` (~6 sites), `crates/ailang-codegen/src/lib.rs` (~2 sites), `crates/ailang-check/tests/workspace.rs` (~4 sites), `crates/ailang-check/tests/duplicate_ctor_pin.rs` (2 sites), `crates/ailang-surface/src/parse.rs` (1 site at line 429), `crates/ailang-core/tests/spec_drift.rs` (1 site at line 281), `crates/ailang-core/tests/design_schema_drift.rs` (1 site at line 323), `crates/ailang-check/src/reuse_shape.rs` (1 site), `crates/ailang-check/src/linearity.rs` (~2 sites), `crates/ailang-core/src/desugar.rs` (1 site at line 2175).
- Test: `crates/ailang-core/tests/design_schema_drift.rs` — append `typedef_param_in_round_trips`.
- Modify: `design/contracts/0002-data-model.md:55-66` — anchor block.

- [ ] **Step 1: Add `use std::collections::{BTreeMap, BTreeSet}` import**

In `crates/ailang-core/src/ast.rs`, locate the existing `use` block at the top of the file (currently absent for `BTreeMap`/`BTreeSet` per `head -25` inspection during recon). Add:

```rust
use std::collections::{BTreeMap, BTreeSet};
```

(Insert above the existing `use serde::{Deserialize, Serialize};` line.)

- [ ] **Step 2: Add `TypeDef.param_in` field**

In `crates/ailang-core/src/ast.rs`, after the `drop_iterative` field at lines 164-169 and before the closing brace at line 170, insert:

```rust
    /// Closed-set restriction on type-parameter instantiation. Maps
    /// each var name (drawn from [`Self::vars`]) to a set of allowed
    /// concrete type names. When non-empty, the checker enforces
    /// that every `Type::Con { name: <self.name>, args }` carries an
    /// `args[i]` whose outermost type-name lies in the restricted
    /// set for that variable.
    ///
    /// Serialised as `"param-in": { "<var>": ["<T>", ...] }`
    /// (kebab-case); the field is **omitted when empty**, preserving
    /// the canonical-JSON hash of every fixture that does not
    /// restrict.
    ///
    /// See prep.3 of the kernel-extension-mechanics milestone and
    /// the new diagnostic
    /// [`crate::check::CheckError::ParamNotInRestrictedSet`].
    #[serde(
        default,
        rename = "param-in",
        skip_serializing_if = "BTreeMap::is_empty"
    )]
    pub param_in: BTreeMap<String, BTreeSet<String>>,
```

- [ ] **Step 3: Surface compile errors**

Run: `cargo build --workspace 2>&1 | rg 'missing field .param_in.' | wc -l`
Expected: a positive integer ~30.

- [ ] **Step 4: Mechanical sweep — add `param_in: BTreeMap::new(),` to every TypeDef struct-literal site**

For each `error[E0063]: missing field \`param_in\` in initializer of \`ailang_core::ast::TypeDef\``, open the file/line, insert `param_in: BTreeMap::new(),` into the struct literal. Insertion order: after `drop_iterative: ...,` and before the closing `}`.

The `BTreeMap` import is already present in `crates/ailang-core/src/ast.rs`; for other crates that construct `TypeDef`, the use statement at the top of each file must mention `BTreeMap` via either `use std::collections::BTreeMap;` (if absent) or import along with existing collection imports.

Example (`crates/ailang-surface/src/parse.rs:429`):

Before:
```rust
Ok(TypeDef {
    name,
    vars,
    ctors,
    doc,
    drop_iterative,
})
```

After:
```rust
Ok(TypeDef {
    name,
    vars,
    ctors,
    doc,
    drop_iterative,
    param_in: BTreeMap::new(),
})
```

(Add `use std::collections::BTreeMap;` near the top of `parse.rs` if absent. Verify by running `rg 'use std::collections::BTreeMap' crates/ailang-surface/src/parse.rs` — empty result means add it.)

- [ ] **Step 5: Compile-gate**

Run: `cargo build --workspace 2>&1 | tail -5`
Expected: no `error[E0063]` lines; build succeeds.

- [ ] **Step 6: Update TypeDef schema anchor in data-model contract**

In `design/contracts/0002-data-model.md`, replace lines 56-66 with:

```markdown
// type (algebraic data type; parameterised)
{ "kind": "type",
  "name": "<id>",
  "vars": ["<id>"...],     // type parameters; omitted when empty (hash-stable when omitted)
  "ctors": [
    { "name": "<id>", "fields": [Type...] }  // nullary ctor: fields = []
    ...
  ],
  "doc": "<optional string>",
  "drop-iterative": true,  // opt-in; omitted when false (hash-stable when omitted)
  "param-in": { "<var>": ["<TypeName>", ...] }   // closed-set restriction per type variable; omitted when empty (hash-stable when omitted). See prep.3 of the kernel-extension-mechanics milestone.
}
```

- [ ] **Step 7: Add `typedef_param_in_round_trips` drift test**

Append to `crates/ailang-core/tests/design_schema_drift.rs`:

```rust
/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of
/// `TypeDef.param_in`. Property protected: when non-empty, the map
/// serialises under the kebab-case key `"param-in"`; when empty,
/// it is omitted entirely (preserving the bit-identical hash of
/// every fixture that does not restrict). The BTreeMap/BTreeSet
/// choice gives deterministic iteration order (alphabetical) so
/// the canonical-JSON bytes are reproducible. A future edit that
/// renames the field, drops the `skip_serializing_if`, or changes
/// the inner collection type breaks the pin in lockstep with the
/// data-model document.
#[test]
fn typedef_param_in_round_trips() {
    use std::collections::{BTreeMap, BTreeSet};

    let mut restrict: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
    restrict.insert(
        "a".into(),
        ["Int".to_string(), "Float".to_string()].into_iter().collect(),
    );

    let td_on = TypeDef {
        name: "T".into(),
        vars: vec!["a".into()],
        ctors: vec![],
        doc: None,
        drop_iterative: false,
        param_in: restrict.clone(),
    };
    let json_on = serde_json::to_value(&td_on).expect("serialise param_in non-empty");
    let pi = json_on.get("param-in").expect(
        "non-empty param_in serialises under kebab key `param-in`",
    );
    let allowed = pi["a"].as_array().expect("inner value is a Type-name array");
    assert_eq!(allowed.len(), 2);
    // BTreeSet iteration order is alphabetical:
    assert_eq!(allowed[0], "Float");
    assert_eq!(allowed[1], "Int");

    let td_off = TypeDef {
        name: "T".into(),
        vars: vec![],
        ctors: vec![],
        doc: None,
        drop_iterative: false,
        param_in: BTreeMap::new(),
    };
    let json_off = serde_json::to_value(&td_off).expect("serialise param_in empty");
    assert!(
        json_off.get("param-in").is_none(),
        "empty param_in must be omitted from canonical JSON (hash-stability)"
    );

    let recovered: TypeDef =
        serde_json::from_value(json_on).expect("TypeDef with param_in round-trips");
    assert_eq!(recovered.param_in, restrict);
}
```

- [ ] **Step 8: Run drift tests**

Run: `cargo test --workspace --test design_schema_drift typedef_param_in_round_trips`
Expected: 1 passed.

Run: `cargo test --workspace --test design_schema_drift`
Expected: all drift tests pass.

---

### Task 3: Form-A surface — `(kernel)` module-header attribute

**Files:**
- Modify: `crates/ailang-surface/src/parse.rs:283-335` — `parse_module` gains a `(kernel)` attribute case.
- Modify: `crates/ailang-surface/src/print.rs:17-33` — Module printer emits `(kernel)` when set.
- Test: `crates/ailang-surface/tests/round_trip.rs` (or the file that holds surface round-trip fixtures; verify with `rg -l 'round_trip' crates/ailang-surface/tests/`).

- [ ] **Step 1: Locate the existing module-header attribute precedent**

Run: `rg -n '"drop-iterative"|drop_iterative' crates/ailang-surface/src/parse.rs | head -6`
Expected: hits in `parse_data` (~lines 385-413 per recon). The `(drop-iterative)` attribute parsing in `parse_data` is the structural mirror for `(kernel)` in `parse_module` — both are bare flag attributes (no inner data).

- [ ] **Step 2: Add `(kernel)` parsing to `parse_module`**

Open `crates/ailang-surface/src/parse.rs`. Inside `parse_module` (starts at line 283), after the line that calls `expect_ident("module name")?` (around line 286) and before the main `(import|data|fn|...)` dispatch loop, parse zero or more bare attribute clauses.

Insert a local `let mut kernel = false;` before the dispatch loop. Then, at the top of the loop body, before the existing `(import|...)` cases, add:

```rust
            Some("kernel") => {
                // (kernel) — bare flag, no inner content.
                self.expect_close_paren_after_keyword("kernel")?;
                kernel = true;
            }
```

(The exact helper-method names follow the surrounding parser style. If `expect_close_paren_after_keyword` doesn't exist, mirror the close-paren consumption pattern used immediately after `(drop-iterative)` in `parse_data`'s arm — typically `self.expect(Token::CloseParen)` or `self.consume_close_paren("kernel")`. Implementer reads the local idiom and applies it.)

At the bottom of `parse_module`, where the existing `Ok(Module { ... })` literal is constructed (line 329 per Task 1), thread `kernel` into the struct literal in place of the `false` placeholder Task 1 inserted:

Before (after Task 1):
```rust
Ok(Module {
    schema: SCHEMA.to_string(),
    name,
    kernel: false,
    imports,
    defs,
})
```

After:
```rust
Ok(Module {
    schema: SCHEMA.to_string(),
    name,
    kernel,
    imports,
    defs,
})
```

- [ ] **Step 3: Add `(kernel)` printing to `Module` print**

Open `crates/ailang-surface/src/print.rs`. Locate the `Module` print function (around lines 17-33; recon reports the function emits `(module <name>` then iterates imports/defs).

After the `(module <name>` head is emitted and before the imports block, insert (matching the surrounding line-write idiom):

```rust
    if m.kernel {
        // (kernel) attribute marks this as a kernel-tier module —
        // every consumer auto-imports its types and free defs.
        writeln!(w, "  (kernel)")?;
    }
```

(Exact indent and writer macro follow the local style in `print.rs`. If the printer's existing convention is `write!(w, ...)` instead of `writeln!`, mirror it.)

- [ ] **Step 4: Write a round-trip test for `(kernel)`**

Locate the existing surface round-trip test file with: `rg -l '#\[test\]' crates/ailang-surface/tests/`. The canonical file is `crates/ailang-surface/tests/round_trip.rs` (or equivalent). Append:

```rust
/// prep.3 (kernel-extension-mechanics): the `(kernel)` module-header
/// attribute round-trips Form-A → JSON → Form-A bit-identical and
/// preserves the parsed bool through both halves.
#[test]
fn kernel_module_header_round_trips() {
    let src = "(module k (kernel))\n";
    let m = ailang_surface::parse(src).expect("Form-A parse of (kernel) module");
    assert!(m.kernel, "parsed kernel: true");

    let printed = ailang_surface::print(&m).expect("print the kernel module");
    // Round-trip: print, re-parse, kernel still true.
    let m2 = ailang_surface::parse(&printed).expect("re-parse printed form");
    assert!(m2.kernel, "kernel: true survives round-trip");

    // Default form (no (kernel)) stays kernel: false.
    let plain = ailang_surface::parse("(module p)\n").expect("Form-A parse plain module");
    assert!(!plain.kernel);
}
```

- [ ] **Step 5: Compile-gate + run new test**

Run: `cargo build --workspace 2>&1 | tail -3`
Expected: build succeeds.

Run: `cargo test --workspace -p ailang-surface kernel_module_header_round_trips`
Expected: 1 passed.

- [ ] **Step 6: Regression-protect existing surface tests**

Run: `cargo test --workspace -p ailang-surface 2>&1 | tail -5`
Expected: all surface tests pass (Form-A surface change is additive).

---

### Task 4: Form-A surface — `(param-in (var t1 t2 ...))` TypeDef attribute

**Files:**
- Modify: `crates/ailang-surface/src/parse.rs:354-436` — `parse_data` gains a `(param-in ...)` case.
- Modify: `crates/ailang-surface/src/print.rs:103-135` — `write_type_def` emits `(param-in ...)` blocks when set.
- Test: `crates/ailang-surface/tests/round_trip.rs` — fixture for `(param-in ...)`.

- [ ] **Step 1: Add `(param-in ...)` parsing to `parse_data`**

Open `crates/ailang-surface/src/parse.rs`. Inside `parse_data` (starts at line 354), the inner attribute-loop dispatches on `doc / ctor / drop-iterative` (per recon, lines 374-427). Add a `param-in` arm.

Before the loop, insert: `let mut param_in: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();` (matching the local-var convention used for `vars`, `ctors`, etc.).

Inside the loop, add an arm for `Some("param-in")`:

```rust
            Some("param-in") => {
                // (param-in (a Int Float) (b Str) ...) — one outer
                // clause carrying one or more inner var-lists.
                while !self.peek_close_paren() {
                    self.expect_open_paren("inner var-list of (param-in ...)")?;
                    let var = self.expect_ident("type-variable name")?;
                    let mut allowed = BTreeSet::new();
                    while !self.peek_close_paren() {
                        let tname = self.expect_ident("allowed type-name")?;
                        allowed.insert(tname);
                    }
                    self.expect_close_paren()?;
                    if param_in.insert(var.clone(), allowed).is_some() {
                        return Err(self.err_at(format!(
                            "param-in: duplicate var binding `{}`",
                            var
                        )));
                    }
                }
                self.expect_close_paren()?;
            }
```

(The helper names `peek_close_paren`, `expect_open_paren`, `expect_close_paren`, `expect_ident`, `err_at` follow the local parser style. If exact spellings differ, the implementer reads the surrounding arms — particularly the `ctor` arm, which has a similar nested-list shape — and adopts the local idiom verbatim.)

In the unknown-attribute error path at line 420, extend the error message to mention `param-in` alongside the existing attribute names.

At the bottom of `parse_data`, where `Ok(TypeDef { ... })` is constructed (line 429 per Task 2), thread `param_in` into the struct literal in place of the `BTreeMap::new()` placeholder Task 2 inserted:

Before (after Task 2):
```rust
Ok(TypeDef {
    name,
    vars,
    ctors,
    doc,
    drop_iterative,
    param_in: BTreeMap::new(),
})
```

After:
```rust
Ok(TypeDef {
    name,
    vars,
    ctors,
    doc,
    drop_iterative,
    param_in,
})
```

Ensure `use std::collections::{BTreeMap, BTreeSet};` is at the top of `parse.rs` (Task 2 may already have added `BTreeMap`; extend to `{BTreeMap, BTreeSet}` if needed).

- [ ] **Step 2: Add `(param-in ...)` printing to `write_type_def`**

Open `crates/ailang-surface/src/print.rs`. Locate `write_type_def` (around lines 103-135; recon reports a `drop_iterative` emit at lines 126-133 — the structural mirror).

After the `drop_iterative` block and before the closing of the `(type ...)` form, insert:

```rust
    if !td.param_in.is_empty() {
        // (param-in (a Int Float) (b Str) ...) — BTreeMap/BTreeSet
        // give deterministic alphabetical iteration order.
        write!(w, "  (param-in")?;
        for (var, allowed) in &td.param_in {
            write!(w, " ({}", var)?;
            for tname in allowed {
                write!(w, " {}", tname)?;
            }
            write!(w, ")")?;
        }
        writeln!(w, ")")?;
    }
```

(Adapt indent/writer macro to the local style. The convention is single-space separation between inner items.)

- [ ] **Step 3: Write a round-trip test for `(param-in ...)`**

Append to `crates/ailang-surface/tests/round_trip.rs`:

```rust
/// prep.3 (kernel-extension-mechanics): the `(param-in (var t1 t2 ...))`
/// TypeDef attribute round-trips Form-A → JSON → Form-A bit-
/// identical and preserves the parsed BTreeMap through both halves,
/// including the BTreeSet's deterministic alphabetical iteration
/// order.
#[test]
fn typedef_param_in_round_trips_surface() {
    let src = concat!(
        "(module m\n",
        "  (data T (vars a)\n",
        "    (param-in (a Int Float))\n",
        "    (ctors (MkT a))))\n"
    );
    let m = ailang_surface::parse(src).expect("Form-A parse of (param-in ...)");
    let td = match &m.defs[0] {
        ailang_core::ast::Def::Type(t) => t,
        _ => panic!("expected Type def"),
    };
    let allowed = td.param_in.get("a").expect("var `a` bound in param_in");
    assert!(allowed.contains("Int"));
    assert!(allowed.contains("Float"));
    assert_eq!(allowed.len(), 2);

    let printed = ailang_surface::print(&m).expect("print the module");
    let m2 = ailang_surface::parse(&printed).expect("re-parse printed form");
    let td2 = match &m2.defs[0] {
        ailang_core::ast::Def::Type(t) => t,
        _ => panic!("expected Type def after round-trip"),
    };
    assert_eq!(td2.param_in, td.param_in, "param_in survives round-trip");
}
```

- [ ] **Step 4: Compile-gate + run new test**

Run: `cargo build --workspace 2>&1 | tail -3`
Expected: build succeeds.

Run: `cargo test --workspace -p ailang-surface typedef_param_in_round_trips_surface`
Expected: 1 passed.

Run: `cargo test --workspace -p ailang-surface 2>&1 | tail -5`
Expected: all surface tests pass.

---

### Task 5: Prelude becomes kernel-tier + loader generalisation

**Files:**
- Modify: `examples/prelude.ail:1` — gains `(kernel)` attribute.
- Modify: `crates/ailang-surface/src/loader.rs:88-110` — `load_workspace` migrates from hardcoded `&["prelude"]` to flag-driven derivation.
- Modify: `crates/ailang-core/src/workspace.rs:307-312` — `ReservedModuleName` doc + diagnostic prose.
- Modify: `crates/ailang-core/src/workspace.rs:465-493` — `build_workspace` doc comment update.
- Modify: `crates/ail/src/main.rs:1234-1244` — CLI mapping for `ReservedModuleName` diagnostic.
- Modify: `crates/ailang-surface/tests/prelude_module_hash_pin.rs:27` — refresh hex hash + Honesty-Rule comment.

- [ ] **Step 1: Add `(kernel)` to the prelude**

Open `examples/prelude.ail`. The first line is currently `(module prelude` (verified by recon). Edit to:

```
(module prelude (kernel)
```

(Bare `(kernel)` immediately after the module name on the same line. Whitespace/format follows the existing module's style.)

- [ ] **Step 2: Migrate the loader's hardcoded prelude paths**

Open `crates/ailang-surface/src/loader.rs`. Replace lines 95-110 (the body of `load_workspace`) with:

```rust
pub fn load_workspace(entry: &Path) -> Result<Workspace, WorkspaceLoadError> {
    let (entry_name, root_dir, mut modules) =
        ailang_core::workspace::load_modules_with(entry, load_module)?;

    // parse_prelude() injects the built-in prelude into the
    // workspace. The prelude module's source carries `(kernel)`, so
    // it surfaces in the kernel-tier auto-import set below.
    if modules.contains_key("prelude") {
        return Err(WorkspaceLoadError::ReservedModuleName {
            name: "prelude".to_string(),
        });
    }
    modules.insert("prelude".to_string(), parse_prelude());

    // Derive the implicit-imports list from `kernel: true` modules.
    // Replaces the previous hardcoded `&["prelude"]` literal: any
    // workspace-loaded module that carries the kernel flag is now
    // auto-imported. See prep.3 of the kernel-extension-mechanics
    // milestone.
    let kernel_names: Vec<String> = modules
        .values()
        .filter(|m| m.kernel)
        .map(|m| m.name.clone())
        .collect();
    let implicit_imports: Vec<&str> =
        kernel_names.iter().map(String::as_str).collect();

    ailang_core::workspace::build_workspace(
        entry_name,
        root_dir,
        modules,
        &implicit_imports,
    )
}
```

(`build_workspace`'s signature does not change; only the value of its fourth argument is now caller-derived. The `kernel_names: Vec<String>` lives across the borrow scope so the `&[&str]` slice is valid.)

- [ ] **Step 3: Update `ReservedModuleName` doc + diagnostic prose**

Open `crates/ailang-core/src/workspace.rs`. At lines 307-312, replace the variant's doc comment and (if the variant carries a literal message) any embedded prose with:

```rust
    /// A user workspace contains a module whose name collides with
    /// a built-in kernel-tier module that the loader auto-injects.
    /// The current built-in set is `prelude` (and, in test/dev
    /// builds, `kernel_stub`); future base extensions may add more.
    /// Previously this variant fired specifically for `prelude`;
    /// since prep.3 of the kernel-extension-mechanics milestone, it
    /// fires for any built-in kernel module name.
    ReservedModuleName { name: String },
```

(The struct shape `{ name: String }` is unchanged per OQ3. Only the doc comment changes. If the variant has a `#[error(...)]` attribute carrying a literal message, update it to:

```rust
    #[error("workspace module `{name}` collides with a built-in kernel-tier module name (reserved)")]
```

Verify by searching `rg -nE '#\[error\(' crates/ailang-core/src/workspace.rs | rg ReservedModuleName -B0 -A0` — the literal lives near the variant declaration.)

- [ ] **Step 4: Update `build_workspace` doc comment**

In `crates/ailang-core/src/workspace.rs:465-476`, update the function-level doc comment for `build_workspace` to clarify the new caller-derived semantics. Replace any wording of the form "implicit_imports = typically just prelude" with:

```rust
/// `implicit_imports` is the list of module names every consumer
/// should auto-import without an explicit `(import …)` declaration.
/// The caller (typically `ailang_surface::loader::load_workspace`)
/// derives this list from the kernel-tier filter: every loaded
/// module with `kernel: true` enters the list. Since prep.3 of the
/// kernel-extension-mechanics milestone, this is the flag-driven
/// generalisation of the prior hardcoded `&["prelude"]` literal.
```

(Exact placement: above the `pub fn build_workspace(...)` signature, replacing or extending the existing doc block.)

- [ ] **Step 5: Update CLI mapping for `ReservedModuleName`**

Open `crates/ail/src/main.rs`. At lines 1234-1244, the `ReservedModuleName` arm of the diagnostic translator currently emits prose referencing `prelude` specifically. Update the user-facing message to:

```rust
        WorkspaceLoadError::ReservedModuleName { name } => Diagnostic {
            code: "WORKSPACE_RESERVED_MODULE_NAME".into(),
            message: format!(
                "Module `{}` collides with a built-in kernel-tier module name. The built-in set is reserved; pick a different module name.",
                name
            ),
            // …other fields unchanged…
        },
```

(Exact field set and surrounding match shape follow the existing arm. The `ctx` field, if present, keeps the `name` entry.)

- [ ] **Step 6: Refresh the prelude hash pin**

Open `crates/ailang-surface/tests/prelude_module_hash_pin.rs`. Above the literal hex hash at line 27, add a new comment block in the established style (mirror lines 15-25 — two prior re-pin reasons are logged there):

```rust
// prep.3 (kernel-extension-mechanics) — prelude becomes kernel-tier:
// `examples/prelude.ail` gains the `(kernel)` module-header attribute,
// which serialises as `"kernel": true` in the canonical JSON. This
// changes the prelude's content hash deterministically; the new hex
// pin replaces the prior `562a03fc57e7e017`. The behaviour
// `prelude_free_fns.rs` protects (12 free fns callable bare in every
// consumer) is unchanged — only the code path migrates from the
// hardcoded `&["prelude"]` literal to the kernel-flag filter.
```

Then determine the new hash. Run: `cargo test --workspace -p ailang-surface --test prelude_module_hash_pin -- --nocapture 2>&1 | rg -A2 'assertion .*failed' | head -10`. The failure message reports the *actual* hash. Copy that hex value into the test file's pin literal in place of the old one. Re-run to confirm green:

Run: `cargo test --workspace -p ailang-surface --test prelude_module_hash_pin`
Expected: PASS.

- [ ] **Step 7: Regression-protect `prelude_free_fns.rs`**

Run: `cargo test --workspace -p ail --test prelude_free_fns 2>&1 | tail -5`
Expected: all tests pass. (This is the explicit regression for the prelude code-path migration — observable behaviour must be identical.)

- [ ] **Step 8: Regression-protect CLI assertion test**

Run: `cargo test --workspace -p ail --test ct1_check_cli 2>&1 | tail -5`
Expected: all tests pass. (The CLI mapping update at Step 5 changed user-facing prose; ct1 may assert on it. If a test asserts the old prelude-specific prose, update the assertion to the new wording. The diagnostic *code* is unchanged.)

- [ ] **Step 9: Workspace-wide test sweep**

Run: `cargo test --workspace 2>&1 | tail -5`
Expected: all tests pass.

---

### Task 6: New crate `crates/ailang-kernel-stub/` + kernel-stub drift round-trip

**Files:**
- Create: `crates/ailang-kernel-stub/Cargo.toml`
- Create: `crates/ailang-kernel-stub/src/lib.rs`
- Modify: workspace-root `Cargo.toml:3-9` (members list).
- Modify: `crates/ailang-surface/src/loader.rs:load_workspace` — inject `parse_kernel_stub()` alongside `parse_prelude()`.
- Test: `crates/ailang-core/tests/design_schema_drift.rs` — append `kernel_stub_module_round_trips`.

- [ ] **Step 1: Create the crate's `Cargo.toml`**

Verify the precedent layout: `cat crates/ailang-prose/Cargo.toml`. Mirror its top-level shape. Write `crates/ailang-kernel-stub/Cargo.toml`:

```toml
[package]
name = "ailang-kernel-stub"
version.workspace = true
edition.workspace = true

[lib]
path = "src/lib.rs"

[dependencies]
ailang-core.workspace = true
ailang-surface.workspace = true
```

(If `ailang-prose`'s `Cargo.toml` has additional shared fields like `license`, `repository`, or `[package]`-level inherits — mirror them.)

- [ ] **Step 2: Create `src/lib.rs` with the stub module's Form-A source**

Write `crates/ailang-kernel-stub/src/lib.rs`:

```rust
//! Kernel-tier stub module — minimal ratifying fixture for the
//! kernel-extension-mechanics milestone (prep.3).
//!
//! The stub exists solely to exercise the four shipped mechanisms
//! end-to-end: `Module.kernel`, `TypeDef.param-in`, `Term::New` (via
//! the stub's own `new` def), and type-scoped resolution (the stub's
//! type and `new` are visible to every consumer without an
//! `(import …)` declaration).
//!
//! No domain content. The stub may be retired or repositioned when
//! a real second kernel-tier consumer (the `raw-buf` milestone) lands.

use ailang_core::ast::Module;

/// Source-of-truth Form-A text for the stub kernel module. Parsing
/// this string is byte-equivalent to the canonical JSON produced
/// from the resulting `Module` value (round-trip-pinned by
/// `kernel_stub_module_round_trips` in `design_schema_drift.rs`).
const STUB_AIL: &str = r#"(module kernel_stub (kernel)

  (type StubT (vars a)
    (param-in (a Int Float))
    (ctors (Stub a)))

  (fn new
    (doc "Construct StubT<Int> from an Int. Exercises Term::New end-to-end.")
    (type (fn-type (params (con Int)) (ret (con StubT (con Int)))))
    (params x)
    (body (term-ctor StubT Stub x))))
"#;

/// Parse the embedded stub kernel module. Mirror of
/// [`ailang_surface::loader::parse_prelude`] (both return their
/// home crate's built-in kernel-tier module).
///
/// Panics on parse failure — the stub is build-time-validated by
/// every drift test run, so a parse failure here is a build-
/// correctness bug, not a runtime concern.
pub fn parse_kernel_stub() -> Module {
    ailang_surface::parse(STUB_AIL).expect("kernel_stub source must parse as a Module")
}
```

- [ ] **Step 3: Register the crate in the workspace**

Open the workspace-root `Cargo.toml`. Locate the `[workspace] members = [...]` array (lines 3-9 per recon). Add `"crates/ailang-kernel-stub"` to the list (alphabetical position by convention, between `ailang-core` and `ailang-prose` if the list is sorted).

- [ ] **Step 4: Inject the stub via the loader**

Open `crates/ailang-surface/src/loader.rs`. In `load_workspace` (rewritten in Task 5), add stub injection alongside `parse_prelude()`:

```rust
    if modules.contains_key("prelude") {
        return Err(WorkspaceLoadError::ReservedModuleName {
            name: "prelude".to_string(),
        });
    }
    modules.insert("prelude".to_string(), parse_prelude());

    if modules.contains_key("kernel_stub") {
        return Err(WorkspaceLoadError::ReservedModuleName {
            name: "kernel_stub".to_string(),
        });
    }
    modules.insert(
        "kernel_stub".to_string(),
        ailang_kernel_stub::parse_kernel_stub(),
    );
```

(The kernel-flag filter built later in `load_workspace` automatically picks up `kernel_stub` because its source carries `(kernel)`.)

Add the corresponding dependency in `crates/ailang-surface/Cargo.toml`:

```toml
ailang-kernel-stub.workspace = true
```

(Or, if workspace dependency inheritance is not yet used for this crate edge, the explicit `ailang-kernel-stub = { path = "../ailang-kernel-stub" }`. Mirror the local convention.)

- [ ] **Step 5: Add `kernel_stub_module_round_trips` drift test**

Append to `crates/ailang-core/tests/design_schema_drift.rs`:

```rust
/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of
/// the kernel-stub module — exercises all three new schema items
/// in a single fixture (`Module.kernel = true`, one TypeDef with
/// `param-in`, one Term::New-targetable `new` def). A future edit
/// that breaks any of the three additive schema fields will trip
/// this pin in lockstep with the per-field round-trip tests
/// (`module_kernel_flag_round_trips`, `typedef_param_in_round_trips`,
/// `term_new_round_trips`).
#[test]
fn kernel_stub_module_round_trips() {
    let m = ailang_kernel_stub::parse_kernel_stub();
    assert!(m.kernel, "stub module is kernel-tier");
    assert_eq!(m.name, "kernel_stub");

    let json = serde_json::to_value(&m).expect("serialise stub module");
    assert_eq!(json["kernel"], true);
    assert_eq!(json["name"], "kernel_stub");

    let recovered: Module =
        serde_json::from_value(json).expect("stub module round-trips through serde");
    assert!(recovered.kernel);
    assert_eq!(recovered.name, "kernel_stub");

    // Locate the StubT TypeDef and confirm param_in is intact.
    let td = recovered.defs.iter().find_map(|d| match d {
        ailang_core::ast::Def::Type(t) if t.name == "StubT" => Some(t),
        _ => None,
    }).expect("StubT TypeDef present in stub module");
    let allowed = td.param_in.get("a").expect("StubT.a restricted");
    assert!(allowed.contains("Int"));
    assert!(allowed.contains("Float"));
}
```

Add the test crate's dev-dependency on `ailang-kernel-stub` in `crates/ailang-core/Cargo.toml`'s `[dev-dependencies]` block:

```toml
ailang-kernel-stub.workspace = true
```

- [ ] **Step 6: Compile-gate + run new tests**

Run: `cargo build --workspace 2>&1 | tail -3`
Expected: build succeeds (the new stub crate compiles; loader changes compile; drift test compiles).

Run: `cargo test --workspace --test design_schema_drift kernel_stub_module_round_trips`
Expected: 1 passed.

Run: `cargo test --workspace --test design_schema_drift`
Expected: every drift test passes.

---

### Task 7: `CheckError::ParamNotInRestrictedSet` variant + enforcement in `check_type_well_formed` + in-source tests

**Files:**
- Modify: `crates/ailang-check/src/lib.rs:721-742` — new `CheckError` variant.
- Modify: `crates/ailang-check/src/lib.rs:797-798` — `code()` arm.
- Modify: `crates/ailang-check/src/lib.rs:876-879` — `ctx()` arm.
- Modify: `crates/ailang-check/src/lib.rs:1920-1998` — `check_type_well_formed`'s `Type::Con` arm.
- Test: `crates/ailang-check/src/lib.rs` in-source `#[cfg(test)] mod tests` block — `param_in_accepts_allowed_type`, `param_in_rejects_disallowed_type`.

- [ ] **Step 1: Add the new `CheckError` variant**

Open `crates/ailang-check/src/lib.rs`. Locate the existing `CheckError::NewArgKindMismatch` variant at lines 733-742 (recon found it). After the `NewArgKindMismatch` variant and before whatever variant follows (or before the enum's closing `}`), insert:

```rust
    /// `param-in` violation: a `Type::Con` for a TypeDef that
    /// restricts a type variable was instantiated with a type-arg
    /// outside the allowed set. The diagnostic carries the type
    /// name (which TypeDef restricts), the variable name (which
    /// var was violated), the rejected concrete type name
    /// (`found`), and the allowed set (`allowed`). See prep.3 of
    /// the kernel-extension-mechanics milestone.
    #[error(
        "type-arg `{found}` is not in the restricted set for type-variable `{var}` of `{type_name}`"
    )]
    ParamNotInRestrictedSet {
        type_name: String,
        var: String,
        found: String,
        allowed: Vec<String>,
    },
```

(Vec<String> rather than BTreeSet<String> in the diagnostic payload because diagnostics' ctx field is JSON-ish; the order of `allowed` for the user message is deterministic via the source BTreeSet's natural order.)

- [ ] **Step 2: Add the `code()` arm**

At lines 797-798 (the arm for `NewArgKindMismatch`), after that arm and inside the same `match` block, add:

```rust
            CheckError::ParamNotInRestrictedSet { .. } => "param-not-in-restricted-set",
```

- [ ] **Step 3: Add the `ctx()` arm**

At lines 876-879 (the arm for `NewArgKindMismatch`), after that arm and inside the same `match` block, add:

```rust
            CheckError::ParamNotInRestrictedSet { type_name, var, found, allowed } => {
                vec![
                    ("type_name".into(), serde_json::json!(type_name)),
                    ("var".into(), serde_json::json!(var)),
                    ("found".into(), serde_json::json!(found)),
                    ("allowed".into(), serde_json::json!(allowed)),
                ]
            }
```

(Mirror the surrounding arms' return type and helper-macro conventions; the implementer reads the `NewArgKindMismatch` arm and adopts the local idiom.)

- [ ] **Step 4: Add enforcement in `check_type_well_formed`**

Open `check_type_well_formed` (lines 1920-1998). Locate the `Type::Con { name, args }` arm — after the TypeDef lookup at line 1961 (`td_opt`) and before recursing into `args` at line 1969, insert the param-in walk:

```rust
        if let Some(td) = td_opt {
            // param-in enforcement: every restricted var must have
            // its corresponding positional arg's outermost type-name
            // in the allowed set.
            for (var, allowed) in &td.param_in {
                let var_position = td.vars.iter().position(|v| v == var);
                let Some(pos) = var_position else {
                    // Defensive: param_in keys should always match
                    // TypeDef.vars (enforced at workspace-load).
                    continue;
                };
                let Some(arg_ty) = args.get(pos) else {
                    // Arity mismatch is a separate diagnostic; skip
                    // param-in check when the arg slot does not exist.
                    continue;
                };
                // Peel the outermost type-name out of the arg.
                if let ailang_core::ast::Type::Con { name: arg_name, .. } = arg_ty {
                    if !allowed.contains(arg_name) {
                        return Err(CheckError::ParamNotInRestrictedSet {
                            type_name: name.clone(),
                            var: var.clone(),
                            found: arg_name.clone(),
                            allowed: allowed.iter().cloned().collect(),
                        });
                    }
                }
                // Non-Con arg-types (Forall vars, fn types, etc.) are
                // not currently restrictable by param-in — the spec
                // names the mechanism as a "closed-set type-parameter
                // restriction" over named concrete types. Future
                // axes (structural-predicate-based restriction) are
                // out of scope per the spec's § Out of scope.
            }
        }
```

(Exact placement: the implementer reads the surrounding context — particularly the existing arity-check arm — and inserts the param-in pass immediately after TypeDef resolution and before the recursive args walk.)

- [ ] **Step 5: Add RED test `param_in_rejects_disallowed_type`**

Locate the in-source `#[cfg(test)] mod tests { ... }` block at the end of `crates/ailang-check/src/lib.rs` (line ~6900+; existing test fns like `new_type_not_constructible` live here). Append:

```rust
    /// prep.3 (kernel-extension-mechanics): param-in enforcement.
    /// A `Type::Con { name: "StubT", args: [Type::Con { name: "Str" }] }`
    /// against a TypeDef whose `param_in["a"] = {"Int","Float"}` fires
    /// `ParamNotInRestrictedSet` with the right type-name, var, found,
    /// and allowed-set payload.
    #[test]
    fn param_in_rejects_disallowed_type() {
        use std::collections::{BTreeMap, BTreeSet};

        let mut restrict: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
        restrict.insert(
            "a".into(),
            ["Int".to_string(), "Float".to_string()].into_iter().collect(),
        );
        let stub_td = ailang_core::ast::TypeDef {
            name: "StubT".into(),
            vars: vec!["a".into()],
            ctors: vec![],
            doc: None,
            drop_iterative: false,
            param_in: restrict,
        };
        let m = ailang_core::ast::Module {
            schema: ailang_core::SCHEMA.to_string(),
            name: "k".into(),
            kernel: false,
            imports: vec![],
            defs: vec![ailang_core::ast::Def::Type(stub_td)],
        };

        // Build a workspace with this single module and call
        // check_type_well_formed on (con StubT (con Str)).
        let ty = ailang_core::ast::Type::Con {
            name: "StubT".into(),
            args: vec![ailang_core::ast::Type::Con {
                name: "Str".into(),
                args: vec![],
            }],
        };

        // Use whichever helper the existing in-source tests use to
        // run check_type_well_formed on a synthetic Type+Module pair;
        // mirror the call shape of `new_type_not_constructible` two
        // arms above.
        let err = check_type_in_module(&m, &ty)
            .expect_err("(con StubT (con Str)) violates param_in");
        match err {
            CheckError::ParamNotInRestrictedSet { type_name, var, found, allowed } => {
                assert_eq!(type_name, "StubT");
                assert_eq!(var, "a");
                assert_eq!(found, "Str");
                assert!(allowed.contains(&"Int".to_string()));
                assert!(allowed.contains(&"Float".to_string()));
            }
            other => panic!("expected ParamNotInRestrictedSet, got {other:?}"),
        }
    }
```

(`check_type_in_module` is the placeholder for whichever helper the existing in-source tests use to drive `check_type_well_formed`. The implementer reads `new_type_not_constructible` and the surrounding helpers, and adopts the local convention. If the existing tests inline a checker context creation rather than calling a helper, mirror that.)

- [ ] **Step 6: Add GREEN test `param_in_accepts_allowed_type`**

Append the GREEN counterpart in the same module:

```rust
    /// prep.3 (kernel-extension-mechanics): param-in enforcement
    /// accepts a type-arg inside the allowed set. Same TypeDef as
    /// the RED test, but `(con StubT (con Int))` — Int is in
    /// {Int, Float}, so the check passes.
    #[test]
    fn param_in_accepts_allowed_type() {
        use std::collections::{BTreeMap, BTreeSet};

        let mut restrict: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
        restrict.insert(
            "a".into(),
            ["Int".to_string(), "Float".to_string()].into_iter().collect(),
        );
        let stub_td = ailang_core::ast::TypeDef {
            name: "StubT".into(),
            vars: vec!["a".into()],
            ctors: vec![],
            doc: None,
            drop_iterative: false,
            param_in: restrict,
        };
        let m = ailang_core::ast::Module {
            schema: ailang_core::SCHEMA.to_string(),
            name: "k".into(),
            kernel: false,
            imports: vec![],
            defs: vec![ailang_core::ast::Def::Type(stub_td)],
        };

        let ty = ailang_core::ast::Type::Con {
            name: "StubT".into(),
            args: vec![ailang_core::ast::Type::Con {
                name: "Int".into(),
                args: vec![],
            }],
        };

        check_type_in_module(&m, &ty).expect("(con StubT (con Int)) passes param_in");
    }
```

- [ ] **Step 7: Run new tests + ensure exhaustiveness compile-gate clean**

Run: `cargo test --workspace -p ailang-check param_in_rejects_disallowed_type`
Expected: 1 passed.

Run: `cargo test --workspace -p ailang-check param_in_accepts_allowed_type`
Expected: 1 passed.

Run: `cargo build --workspace 2>&1 | rg 'non-exhaustive\|missing.*ParamNotInRestrictedSet' | wc -l`
Expected: 0. (The variant addition forces exhaustive `match CheckError { ... }` sites to be updated; the three explicit arms inserted in Steps 1-3 cover the only exhaustive-match sites per `crates/ailang-check/src/lib.rs:754, 805, 917` enumerated by recon. If any other site flares, fix in-place with a trailing arm if the surrounding context allows non-exhaustive matching, or with a fully-specified arm otherwise.)

Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5`
Expected: all checker tests pass.

---

### Task 8: Workspace-load integration tests — `crates/ailang-core/tests/workspace_kernel.rs`

**Files:**
- Create: `crates/ailang-core/tests/workspace_kernel.rs`

- [ ] **Step 1: Locate the integration-test pattern**

Read `crates/ailang-core/tests/workspace_pin.rs:1-22` for the dev-dep posture (the integration-test crate is the home for tests that call `ailang_surface::load_workspace`, per the documented dev-dep cycle constraint). The pattern: create a temp directory, write `.ail` source files, call `ailang_surface::load_workspace(entry)`, assert on the resulting `Workspace`.

- [ ] **Step 2: Write three integration tests**

Create `crates/ailang-core/tests/workspace_kernel.rs`:

```rust
//! prep.3 (kernel-extension-mechanics): workspace-load tests for
//! kernel-tier auto-import. These tests exercise the flag-driven
//! generalisation of the prior hardcoded `&["prelude"]` literal —
//! every loaded module with `kernel: true` joins the implicit-
//! imports list.

use std::collections::BTreeMap;
use tempfile::TempDir;

/// Write a Form-A source file into the temp dir and return its path.
fn write_module(dir: &TempDir, name: &str, src: &str) -> std::path::PathBuf {
    let path = dir.path().join(format!("{}.ail", name));
    std::fs::write(&path, src).expect("write fixture");
    path
}

#[test]
fn kernel_tier_module_auto_imports_without_explicit_import() {
    // Consumer has no `(import …)` declaration; the kernel-tier
    // module's types should still resolve.
    let dir = TempDir::new().expect("tempdir");
    write_module(
        &dir,
        "k_mod",
        r#"(module k_mod (kernel)
  (type KT (vars a) (ctors (KCtor a))))
"#,
    );
    let entry = write_module(
        &dir,
        "consumer",
        r#"(module consumer
  (fn use_kt
    (type (fn-type (params (con KT (con Int))) (ret (con Unit))))
    (params k) (body unit)))
"#,
    );

    let ws = ailang_surface::load_workspace(&entry).expect("workspace loads");
    assert!(
        ws.modules.contains_key("k_mod"),
        "k_mod was loaded into the workspace"
    );
    // The consumer's reference to bare `KT` resolves through the
    // kernel-flag-driven implicit-imports list. The workspace must
    // validate without producing a `BareCrossModuleTypeRef` error.
    // (Exact API for "did validation pass" follows whichever
    // accessor `Workspace` exposes; the implementer mirrors the
    // pattern used in `workspace_pin.rs`.)
}

#[test]
fn two_kernel_tier_modules_coload() {
    let dir = TempDir::new().expect("tempdir");
    write_module(&dir, "k_a", "(module k_a (kernel) (type A (ctors (AC))))\n");
    write_module(&dir, "k_b", "(module k_b (kernel) (type B (ctors (BC))))\n");
    let entry = write_module(
        &dir,
        "consumer",
        r#"(module consumer
  (fn use_ab
    (type (fn-type (params (con A) (con B)) (ret (con Unit))))
    (params a b) (body unit)))
"#,
    );

    let ws = ailang_surface::load_workspace(&entry).expect("workspace with two kernel modules");
    assert!(ws.modules.contains_key("k_a"));
    assert!(ws.modules.contains_key("k_b"));
}

#[test]
fn explicit_import_takes_precedence_over_auto_import() {
    // When a consumer has an explicit `(import k_mod)` declaration,
    // the existing precedence rule keeps the explicit form; the
    // auto-import does not double-resolve or change behaviour.
    // This test pins the precedence rule's continuity through the
    // loader migration.
    let dir = TempDir::new().expect("tempdir");
    write_module(
        &dir,
        "k_mod",
        "(module k_mod (kernel) (type KT (ctors (KC))))\n",
    );
    let entry = write_module(
        &dir,
        "consumer",
        r#"(module consumer
  (import k_mod)
  (fn use_kt
    (type (fn-type (params (con KT)) (ret (con Unit))))
    (params k) (body unit)))
"#,
    );

    let ws = ailang_surface::load_workspace(&entry).expect("explicit + auto coexist");
    assert!(ws.modules.contains_key("k_mod"));
    // No error from double-resolution. Workspace validation passes.
}
```

(If `Workspace.modules` is not the actual field name on the `Workspace` type, the implementer adapts to whatever accessor exists — `workspace_pin.rs` shows the canonical access pattern. If `tempfile` is not yet a dev-dependency of `ailang-core`, add it to `[dev-dependencies]` in `crates/ailang-core/Cargo.toml`.)

- [ ] **Step 3: Verify `tempfile` is available as a dev-dependency**

Run: `rg -n 'tempfile' crates/ailang-core/Cargo.toml`
Expected: at least one hit under `[dev-dependencies]`. If absent, add `tempfile = "3"` to `[dev-dependencies]`.

- [ ] **Step 4: Compile-gate + run new tests**

Run: `cargo build --workspace 2>&1 | tail -3`
Expected: build succeeds.

Run: `cargo test --workspace --test workspace_kernel`
Expected: 3 passed.

- [ ] **Step 5: Workspace-wide regression sweep**

Run: `cargo test --workspace 2>&1 | tail -5`
Expected: all tests pass.

---

### Task 9: Doc-state updates — INDEX.md + whitepaper STATUS + forward→present transitions

**Files:**
- Modify: `design/INDEX.md:111`
- Modify: `design/models/0007-kernel-extensions.md:1-12, 215-276`

- [ ] **Step 1: Update INDEX.md milestone annotation**

Open `design/INDEX.md`. Locate the `kernel-extensions` row (line 111 per recon). The current annotation likely reads `(design accepted 2026-05-28; impl in progress)`. Replace with text reflecting the milestone-close state:

```markdown
| kernel-extensions | design/models/0007-kernel-extensions.md | Whitepaper for the kernel-extensions design; mechanisms milestone closed YYYY-MM-DD (prep.1, prep.2, prep.3 landed); raw-buf and series milestones pending. |
```

(`YYYY-MM-DD` is the close date — typically today's date when prep.3 lands.)

- [ ] **Step 2: Update whitepaper STATUS header**

Open `design/models/0007-kernel-extensions.md`. The STATUS section at lines 1-12 currently describes the design as forward-looking. Replace the relevant lines with the present-state framing:

```markdown
# Kernel extensions — design whitepaper

**Status:** Mechanisms milestone closed YYYY-MM-DD (kernel-extension-mechanics; iterations prep.1, prep.2, prep.3). The base-extension and library-extension milestones (`raw-buf`, `series`) are pending. The four language-level mechanisms — type-scoped namespacing, `Term::New`, kernel-tier modules + auto-import, and `param-in` — are shipped and ratified by the stub kernel crate (`crates/ailang-kernel-stub/`).
```

(Mirror the existing whitepaper STATUS-header convention; if the file uses a different fenced-block or front-matter style, preserve it.)

- [ ] **Step 3: Transition mechanism sections from forward→present**

In `design/models/0007-kernel-extensions.md`, sections at lines 215-237 (kernel-tier auto-import) and 239-276 (param-in) currently use forward-looking language ("after the kernel-extensions design lands, …", "we will …", "future …"). For each such forward-looking sentence about a *now-shipped* mechanism, rewrite to present-state:

- "We will introduce kernel-tier modules …" → "Kernel-tier modules are modules with `kernel: true` set in their schema header. Every loaded kernel-tier module's top-level types and free defs auto-import into every consumer."
- "The `param-in` restriction will allow …" → "The `param-in` restriction is a closed-set type-parameter restriction declared on TypeDefs: `pub param_in: BTreeMap<String, BTreeSet<String>>`, serialised as the kebab-cased `param-in` key. The checker enforces it during `Type::Con` well-formedness."
- "We will need a stub module to …" → "The stub module `crates/ailang-kernel-stub/` ratifies the mechanism end-to-end. It exercises `kernel: true`, `param-in`, and `Term::New` in one fixture; no domain content."

(The implementer reads each forward-looking sentence and rewrites in present-state. Forward-looking framing remains for the *still-pending* base-extension and library-extension milestones — those are explicitly out of scope per § Out of scope of the parent spec.)

- [ ] **Step 4: Confirm no remaining forward-tense in shipped sections**

Run: `rg -n 'will (introduce|allow|need|ship|implement|add) ' design/models/0007-kernel-extensions.md`
Expected: matches occur only in sections that describe the **still-pending** `raw-buf` and `series` milestones. Matches inside sections describing prep.1/prep.2/prep.3 mechanisms are bugs from this step — re-edit.

- [ ] **Step 5: cargo doc clean**

Run: `cargo doc --no-deps --workspace 2>&1 | tail -10`
Expected: no new warnings (doc-comments added in Tasks 1, 2, 6, 7 carry no inline LaTeX or broken intra-doc links).

- [ ] **Step 6: Final workspace test sweep**

Run: `cargo test --workspace 2>&1 | tail -5`
Expected: all tests pass.

Run: `bench/check.py 2>&1 | tail -10`
Expected: no performance regression beyond noise — this milestone touches resolver/parser/schema, not codegen/runtime; regression is unexpected but the regression script is part of the close-out per audit discipline.

---

## Self-review notes

1. **Spec coverage.** Every numbered item in the spec's § Iteration prep.3 maps to a task:
   - Schema additions (`Module.kernel`, `TypeDef.param_in`) → Tasks 1, 2.
   - Form-A surface (`(kernel)`, `(param-in …)`) → Tasks 3, 4.
   - Workspace-load generalisation → Task 5 (prelude migration + loader rewrite).
   - Generic checker enforcement of param-in → Task 7.
   - `ParamNotInRestrictedSet` diagnostic → Task 7.
   - `ReservedModuleName` repurposed → Task 5 Step 3 + Step 5.
   - New `crates/ailang-kernel-stub/` crate → Task 6.
   - Drift pins (`module_kernel_flag_round_trips`, `typedef_param_in_round_trips`, basic stub-module round-trip) → Tasks 1 Step 6, 2 Step 7, 6 Step 5.
   - Workspace-load tests → Task 8.
   - Hash-pin refresh for prelude → Task 5 Step 6.
   - § Acceptance criteria item 8 (whitepaper STATUS + forward→present) → Task 9 Steps 2-4.
   - § Acceptance criteria item 9 (INDEX.md annotation) → Task 9 Step 1.

2. **Placeholder scan.** Grepped this document for "TBD", "TODO", "fill in later", "similar to Task", "add appropriate error handling": no hits.

3. **Type consistency.** `Module.kernel` (bool), `TypeDef.param_in` (BTreeMap<String, BTreeSet<String>>), `ParamNotInRestrictedSet { type_name, var, found, allowed }`, `parse_kernel_stub()`, `kernel_stub` module name — all used consistently across tasks.

4. **Step granularity.** Each step is one mechanical action: write a struct edit, run a command, write a single test function. The 130-site `Module { ... }` sweep in Task 1 Step 3 is the largest single step — handled as a mechanical replace-all driven by the compiler's error list (the implementer's "iterate over `cargo build` errors and fix each" pattern, not a 130-step plan).

5. **No commit steps.** Confirmed: no `git commit` instructions anywhere.

6. **Pin/replacement substring contiguity.** The only verbatim-text edits are in `design/contracts/0002-data-model.md` (Task 1 Step 5, Task 2 Step 6) and the prelude hash refresh (Task 5 Step 6). None pair a presence-pin with a soft-wrappable replacement — the data-model edits are full block replacements, and the hash pin's new hex literal is whatever the failing test reports.

7. **Compile-gate vs. deferred-caller ordering.** The two struct-addition tasks (1 and 2) each include the full sweep of their respective struct-literal sites inside the same task as the field declaration. The compile gate at the end of each task validates that no caller is deferred. The `CheckError` variant addition (Task 7) includes the three accessor-arm updates (code/ctx/match exhaustiveness) inside the same task as the variant declaration, plus the workspace-wide build check (Step 7).

8. **Verification-command filter strings resolve.** Each `cargo test --test` invocation targets either a known existing test file (`design_schema_drift`, `prelude_module_hash_pin`, `prelude_free_fns`, `ct1_check_cli`) or a new file created in the same task (`workspace_kernel`). Each `--test`-with-filter form names a test function created earlier in the same task (`module_kernel_flag_round_trips`, `typedef_param_in_round_trips`, `kernel_module_header_round_trips`, `typedef_param_in_round_trips_surface`, `kernel_stub_module_round_trips`, `param_in_rejects_disallowed_type`, `param_in_accepts_allowed_type`). No silently-skipped filter strings.

---

## Handoff

This plan is ready for the `implement` skill. Standard mode dispatch:

```
ailang-implement-orchestrator
  mode: standard
  iter_id: prep.3-kernel-tier-modules
  plan_path: docs/plans/0103-prep.3-kernel-tier-modules.md
```

The whole plan runs in one orchestrator dispatch (no task-range split anticipated — tasks are sequenced by their dependency chain: 1→2 are schema, 3→4 are surface, 5 migrates prelude+loader, 6 lands the stub crate, 7 ships the diagnostic+enforcement, 8 validates workspace-load behaviour, 9 closes the documentation state).

On `DONE`, the orchestrator (Boss) commits as one cohesive iter-level commit with subject `iter prep.3-kernel-tier-modules (DONE 9/9): kernel-tier modules + param-in + stub crate — closes #33`. The commit body covers: the four shipped mechanisms, the prelude code-path migration with prelude_free_fns regression-protection, the stub crate's role as ratifying fixture, and the milestone-close transition in INDEX.md + the whitepaper.