From 7b8596cef0681ad9682caa173aa7657cdd2c16bc Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 28 May 2026 13:14:35 +0200 Subject: [PATCH] =?UTF-8?q?spec:=20kernel-extension-mechanics=20=E2=80=94?= =?UTF-8?q?=20three-iter=20prep=20milestone?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/specs/2026-05-28-kernel-extension-mechanics.md: per-milestone implementation container for the four language-level mechanisms described in design/models/kernel-extensions.md. Three iterations, each independently shippable: - prep.1 — Type-scoped namespacing. Resolver change so `.` resolves to the type's home module. Migrates ~14 std-library example fixtures from `std_X.Y`-style cross-module references to type-scoped form. Hash pins refreshed in lockstep (ailang-core + ailang-surface — full blast-radius walk, per the hash-pin-audit lesson from schema-camelcase-fix). - prep.2 — Term::New. New AST variant and Form-A keyword `(new T args...)`, calls the `new` def in T's home module. Uses prep.1's resolution. - prep.3 — Kernel-tier modules + `param-in`. Schema flag `Module.kernel` + TypeDef `param-in` field. Workspace-load generalises the existing hardcoded prelude auto-injection (loader.rs:98-108 + workspace.rs:308-311, 467, 2655) into a flag-driven mechanism; prelude itself gains `kernel: true` as a code-path migration (consumer-observable behaviour unchanged — prelude_free_fns.rs regression test stays green). A new minimal ailang-kernel-stub crate ratifies the mechanism without domain content. Five new diagnostics across the three iters: TypeScopedMemberNotFound, TypeScopedReceiverNotAType, NewTypeNotConstructible, NewArgKindMismatch, ParamNotInRestrictedSet. BareCrossModuleTypeRef and BadCrossModuleTypeRef diagnostics repositioned (still "type name not resolvable" but with revised remediation pointers). Each iter's spec section carries explicit `## Canonical form decision`, `## Blast radius`, and `## Integration with existing mechanisms` subsections — the migration-policy discipline made visible per spec section. Grounding-check (two dispatches): first BLOCK on prelude auto-injection mis-framing (claimed it was a new mechanism; in fact prelude is hardcoded-auto-injected today), corrected inline; second PASS after the revised two-tier-architecture framing also landed. All load-bearing assumptions ratified by named tests in the working tree. Out of scope, named explicitly: the raw-buf milestone (#7), the series milestone (#8), record-element SoA support, LSP/MCP integration for `ail describe`, higher-kinded `param-in`, and primitive-instance intercept migration (deferred to #7 when there is a real second consumer for the registry). Refs Gitea milestone #6. --- .../2026-05-28-kernel-extension-mechanics.md | 713 ++++++++++++++++++ 1 file changed, 713 insertions(+) create mode 100644 docs/specs/2026-05-28-kernel-extension-mechanics.md diff --git a/docs/specs/2026-05-28-kernel-extension-mechanics.md b/docs/specs/2026-05-28-kernel-extension-mechanics.md new file mode 100644 index 0000000..11c3e91 --- /dev/null +++ b/docs/specs/2026-05-28-kernel-extension-mechanics.md @@ -0,0 +1,713 @@ +# Kernel extension mechanics — Design Spec + +**Date:** 2026-05-28 +**Status:** Draft — awaiting user spec review +**Authors:** Brummel (orchestrator) + Claude +**Reference:** `design/models/kernel-extensions.md` for the +architectural whitepaper. This spec covers the *first* of three +milestones implementing the kernel-extensions design: the +language-level mechanisms (this milestone), the `raw-buf` base +extension (Rust intercepts emitting LLVM IR — the only tier that +needs implementation outside AILang itself), and the `series` +library extension (pure AILang code wrapping RawBuf). The two +follow-up milestones will be brainstormed after this one closes. + +## Goal + +Ship the four language-level mechanisms that the kernel-extensions +design requires, with zero domain-specific code (no Series, no +Matrix, nothing per-extension). After this milestone, the language +supports: + +1. Type-scoped namespacing — `.` resolves to the + member's def in the type's home module. +2. The `new` term construct — `(new T arg1 arg2 ...)` calls the + `new` def in T's home module. +3. Kernel-tier modules — `Module.kernel: bool` flag with + auto-import of all top-level defs and types. +4. `param-in` — closed-set type-parameter restriction on TypeDefs. + +The milestone closes when all four mechanisms are on main, their +diagnostics are formulated and tested, the schema-drift pin +ratifies the new tags, and a stub kernel-tier module exists +purely as a test fixture to exercise the mechanism end-to-end +(no domain operations, just a marker type with a `new`). + +## Architecture + +The four mechanisms live in different layers: + +- **Schema layer** (`ailang-core`): `Module.kernel`, `TypeDef.param-in`, + `Term::New`. Three additive fields/variants, each `skip_serializing_if` + so existing fixtures hash-stable. +- **Surface layer** (`ailang-surface`): new keyword `new`, + new module header attribute `(kernel)`. Print symmetry preserved. +- **Resolver / Checker layer** (`ailang-check`): type-scoped member + resolution, `param-in` enforcement, `Term::New` arg-kind checking. +- **Workspace-load layer** (`ailang-core::workspace`): kernel-tier + auto-import. + +Codegen layer is *not* touched in this milestone. `Term::New` with +a kernel-tier consumer would need codegen support, but we ship the +mechanisms first and exercise them with non-codegen tests +(`ail check` clean is the bar). Codegen integration for kernel +extensions happens in the Series milestone, where the first real +intercept-registry use case forces the codegen-side mechanism. + +A stub kernel module (`crates/ailang-kernel-stub/`) ships as part +of this milestone purely to ratify the mechanism. It contains: + +- One TypeDef with `param-in` set to a small allowed set. +- One `new` def with a deliberately constrained signature. +- The `kernel: true` flag. + +The stub never reaches codegen — `ail check` is the verification +endpoint. When the Series milestone follows, the stub may be +retired or repositioned as a regression fixture. + +## Concrete code shapes + +### Iteration prep.1 — Type-scoped namespacing + +**Worked author example (this is what the LLM writes after prep.1 +lands):** + +``` +(module consumer + (import std_maybe) + + (fn classify + (type (fn-type + (params (con Int)) + (ret (con Maybe (con Int))))) + (params x) + (body + (if (app eq x 0) + (term-ctor Maybe Nothing) + (term-ctor Maybe Just x)))) + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (app print (app Maybe.from_maybe 99 (app classify 7)))))) +``` + +Key shifts from today's surface: + +- `(con Maybe (con Int))` — bare type, no `std_maybe.` prefix in + the type position. (Today this is `(con std_maybe.Maybe (con Int))`.) +- `(app Maybe.from_maybe 99 ...)` — type-scoped op access. (Today: + `(app std_maybe.from_maybe 99 ...)`.) +- `(term-ctor Maybe Just x)` — bare type name in `term-ctor`. (Today: + `(term-ctor std_maybe.Maybe Just x)`.) +- The `(import std_maybe)` declaration stays — it brings the + `Maybe` type into the consumer's type namespace. (Future + alternative `(import Maybe from std_maybe)` is out of scope.) + +**Implementation shape (before → after).** + +`ailang-check`'s resolver: today, when seeing `Term::Var { name: "std_maybe.from_maybe" }`, +it splits at `.`, looks up `std_maybe` as a module, finds +`from_maybe` in that module's defs. After: the same call site +with `Term::Var { name: "Maybe.from_maybe" }` first tries to +resolve `Maybe` as a type (look up TypeDef in the workspace), +then if a TypeDef is found, locates the home module, then looks +up `from_maybe` in the home module's defs. If the receiver is +neither a module nor a type, emit `TypeScopedReceiverNotAType`. +If the receiver is a known type but the member is not in its +home module, emit `TypeScopedMemberNotFound`. + +The module-as-receiver path remains supported for free-standing +defs (not associated with a single type) but is no longer the +canonical form for type-associated operations. + +**Type-position resolution.** `Type::Con { name: "Maybe", args }` +in a signature: today the workspace-load rejects bare cross-module +type refs via `BareCrossModuleTypeRef`. After prep.1, the resolver +first checks whether `Maybe` is in scope (imported by name); if +yes, it resolves to the imported type. The `BareCrossModuleTypeRef` +diagnostic narrows to: "type name not in scope (no matching import, +no kernel-tier provider)". Kernel-tier types are in scope without +imports (prep.3). + +**Canonical form decision.** Type-scoped form is canonical for +type-associated operations. Module-scoped form is retired for +this use case; it remains valid only for module-free defs (defs +that do not take a specific type as receiver) and as a workspace +collision disambiguator (no current collisions exist). + +**Blast radius.** Per `grep -rE 'std_(maybe|pair|list|either)\.' examples/ crates/`: + +- **`.ail` example fixtures** (~14 files): `ct_2_bare_cross_module.ail`, + `ct_3b_bad_qualified_known_module.ail`, `nested_pat.ail`, + `std_either.ail`, `std_either_demo.ail`, `std_either_list.ail`, + `std_either_list_demo.ail`, `std_list.ail`, `std_list_demo.ail`, + `std_list_more_demo.ail`, `std_list_stress.ail`, `std_maybe.ail`, + `std_maybe_demo.ail`, `std_pair.ail`, `std_pair_demo.ail`. + Each rewritten from `std_X.Y` to `Y` (type-scoped) where Y is + type-associated. The defining modules (`std_maybe.ail` etc.) + may keep their internal references unchanged (intra-module refs + are bare today already). +- **Corresponding `.ail.json` fixtures** for round-trip and hash-pin tests. +- **Hash-pin files** (2): `crates/ailang-core/tests/hash_pin.rs` and + `crates/ailang-surface/tests/prelude_module_hash_pin.rs`. Both + refreshed with new hashes. Each refresh carries an Honesty-Rule + provenance comment quoting the prep.1 commit and naming the + surface change. +- **Source-side reference** in `crates/ailang-{check,codegen,surface}/src/` + and `crates/ail/tests/e2e.rs` (~7 files): inspect during recon + whether they hardcode `std_maybe`/`std_pair`-style identifiers + in diagnostic strings or test fixtures. Diagnostic strings + update to new vocabulary; test fixtures update to type-scoped. + Production type-resolution logic is the new code. +- **Drift test** `crates/ailang-core/tests/design_schema_drift.rs` + gains a new pin that exercises the type-scoped resolution end- + to-end at the schema level. + +The 14 `.ail` examples are rewritten atomically with the resolver +change in a single iteration commit. Walking *every* test crate +for hash-pin sites is mandatory (per the +`hash-pin blast-radius audit` lesson from `schema-camelcase-fix`). + +**Integration with existing mechanisms.** + +- `BareCrossModuleTypeRef` / `BadCrossModuleTypeRef` diagnostics + are repurposed: they fire when a type name is not in scope by + any path (import, kernel-tier, type-scoped). The class of + errors they detect narrows, the underlying user-facing message + becomes more helpful (it can suggest the import or the + type-scoped form). +- Module-scoped access remains the path for free-standing fns + (e.g. a hypothetical `std_math.factorial` that doesn't have a + receiver type). No retirement of the module-scope mechanism + itself. +- Class method dispatch (see [method-dispatch](../../design/contracts/method-dispatch.md)) + is orthogonal. `(app show x)` continues to type-dispatch via the + Show instance; this is not type-scoped namespacing. +- `term-ctor` and `pat-ctor` continue to use bare ctor names + inside the scrutinee — `(term-ctor Maybe Just x)` works + because `Maybe` is now in scope via type-scoped resolution. + +### Iteration prep.2 — `new` term construct + +**Worked author example (after prep.2; uses a non-kernel test +type to exercise the construct):** + +``` +(module new_demo + (data Counter + (ctor MkCounter (con Int))) + + (fn new + (doc "Build a Counter initialised to the given value.") + (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) + (match c + (case (pat-ctor MkCounter x) (app print x))))))) +``` + +The `(new Counter 42)` desugars to: look up `Counter`'s home +module (this very module), find the `new` def, call it with `42`. + +For a future kernel-tier consumer with a `new` taking a Type arg: + +``` +; (Future Series, exercised in milestone 2.) +(let s (new Series (con Float) 3) + ...) +``` + +Here the first arg `(con Float)` is parsed as a Type (per the +`NewArg::Type` discriminator), the second `3` as a Term. + +**Implementation shape.** + +New AST variant in `ailang-core/src/ast.rs`: + +```rust +pub enum Term { + // ... + New { + type_name: TypeName, + args: Vec, + }, +} + +pub enum NewArg { + Type(Type), + Value(Term), +} +``` + +Serialised JSON: + +```jsonc +{ "t": "new", + "type": "Series", + "args": [ + { "kind": "type", "value": { ... type expr ... } }, + { "kind": "value", "value": { ... term expr ... } } + ] +} +``` + +`type_name` carries no module qualifier — it is resolved via +type-scoped lookup at check time (depends on prep.1). + +**Form-A surface.** Lex/Parse adds `new` as a keyword. Production: + +``` +⟨new⟩ ::= '(' 'new' ⟨TypeName⟩ ⟨NewArg⟩+ ')' +⟨NewArg⟩ ::= ⟨Type⟩ ; matches if token sequence parses as a Type production + | ⟨Term⟩ ; otherwise +``` + +The disambiguation between Type and Term args is by syntactic +form: a Type starts with `(con …)`, `(fn-type …)`, `(borrow …)`, +`(own …)`, etc. — the existing Type-production keywords. A Term +in arg position is anything else. + +**Checker.** When elaborating `Term::New { type_name, args }`: + +1. Look up `type_name` via type-scoped resolution → home module. +2. Find `new` def in that home module. If missing, emit + `NewTypeNotConstructible`. +3. Check arg count against `new`'s signature. +4. For each arg position: the signature's param kind (Type or + Value) must match the `NewArg` kind. Mismatch emits + `NewArgKindMismatch`. +5. If `new`'s signature includes a `forall` over a type variable + instantiated by a Type-positional arg, bind that variable to + the supplied type. Apply `param-in` restriction (prep.3) if + declared. + +**Canonical form decision.** `new` is the canonical construction +form when construction is *functional* (calls a function). It +does not replace `term-ctor`, which remains canonical for +named-data-ctor construction in ADTs. + +**Blast radius.** Small. No existing fixture uses a `new` keyword +or pattern, since the keyword does not exist today. The schema +additions are new variants and new JSON tags; existing fixtures +emit unchanged bytes (no `t: "new"` appears anywhere today). +A new in-source test in `ailang-check/src/lib.rs`'s +`#[cfg(test)]` module exercises the resolution path on the +`new_demo` example fixture above. + +**Integration with existing mechanisms.** + +- `term-ctor` continues to construct ADT values via named data + ctors. The two constructs answer different design needs (see + whitepaper). +- The `new` keyword does not collide with any existing identifier + (no def named `new` exists in current workspace per `grep`). + If a user-defined module ever wanted to call something `new`, + that name is now reserved as a Form-A keyword — they have to + pick a different name. Pre-production stage, no breakage risk. +- Type-scoped resolution (prep.1) is the dependency: `Term::New` + uses it to find the home module of `type_name`. + +### Iteration prep.3 — Kernel-tier modules + `param-in` + +This iteration ships two coupled mechanisms in one atomic step, +because the `param-in` restriction is the first checker behavior +that depends on the workspace knowing about kernel-tier modules +(the stub kernel module is the test fixture for both). + +**Worked author example — kernel-tier stub module (this is the +test fixture, not user-facing code):** + +``` +; crates/ailang-kernel-stub/module.ail.json (or programmatic form) +; The stub module exists only to exercise the mechanism — both +; `kernel: true` auto-import and `param-in` enforcement. +(module kernel_stub (kernel) + + (type StubT (vars a) + (param-in (a Int Float)) + (ctors (Stub a))) + + (fn new + (doc "Construct StubT — 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)))) +``` + +**Worked consumer (no `(import kernel_stub)` needed — kernel-tier):** + +``` +(module stub_consumer + ; No import line. kernel_stub is auto-imported. + + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let s (new StubT 42) + (match s + (case (pat-ctor Stub x) (app print x))))))) +``` + +The `(new StubT 42)` form names the unapplied type constructor +`StubT`; the resolver looks up `StubT`'s home module (`kernel_stub`), +finds `new` there, types the call against `new`'s signature +`(Int) -> StubT Int`. The result type `StubT Int` triggers a +`param-in` check on the type-arg `Int` — `Int ∈ {Int, Float}` so +it passes. A pattern match on `(pat-ctor Stub x)` extracts and +prints the wrapped Int. + +**Worked rejection — `param-in` violation:** + +``` +(fn bad + (type (fn-type + (params (con StubT (con Str))) ; Str not in {Int, Float} + (ret (con Unit)))) + (params s) + (body unit)) +; expected: ParamNotInRestrictedSet on `(con StubT (con Str))` +``` + +**Implementation shape.** + +Schema additions in `ailang-core/src/ast.rs`: + +```rust +pub struct Module { + // ... + #[serde(default, skip_serializing_if = "is_false")] + pub kernel: bool, +} + +pub struct TypeDef { + // ... + #[serde(default, skip_serializing_if = "BTreeMap::is_empty", + rename = "param-in")] + pub param_in: BTreeMap>, +} +``` + +Both `skip_serializing_if` so existing TypeDefs and Modules hash- +identical. + +**Form-A surface.** Module header gains `(kernel)` attribute: + +``` +(module foo (kernel) ...) +``` + +TypeDef body gains optional `(param-in (var type1 type2 ...))` block: + +``` +(type T (vars a) + (param-in (a Int Float)) + (ctors)) +``` + +**Workspace-load.** Today, the loader hardcodes a single auto- +injected module: `crates/ailang-surface/src/loader.rs:98-108` +unconditionally calls `parse_prelude()` and threads the literal +`&["prelude"]` slice into `ailang_core::workspace::build_workspace` +as the implicit-imports list. The reservation of `prelude` as +an auto-injected name is documented at `workspace.rs:308-311`, +and the build contract at `workspace.rs:467`. This is the +mechanism that makes the prelude's 12 free fns (`ne`, `lt`, +`le`, `gt`, `ge`, `print`, `float_eq`...`float_ge`) callable bare +in every consumer module today (ratified by +`crates/ail/tests/prelude_free_fns.rs`). + +prep.3 *generalises* this single-name auto-injection into a +flag-driven multi-module mechanism. After prep.3: + +- `workspace::build_workspace`'s implicit-imports parameter is + derived from "all modules in the workspace with `kernel: true`", + not from a hardcoded literal. +- `loader.rs`'s `parse_prelude()` injection remains (prelude is a + built-in module — it has no on-disk manifest in user + workspaces and must be injected from the compiler's own + resources), but the *naming* of `prelude` as the implicit + import is no longer hardcoded; it follows from prelude's + `kernel: true` flag. +- Other kernel-tier modules (e.g. the stub crate, future Series + crate) are loaded through the normal workspace discovery and + picked up by the same `kernel: true` filter. + +The name-resolution precedence rule (explicit imports beat +auto-import) is the existing behaviour, retained. + +**Checker.** When resolving `Type::Con { name, args }`: + +1. After standard TypeDef lookup, fetch `param_in` from the + TypeDef. +2. For each entry `(var, allowed_set)`: + - Locate the positional `args[i]` corresponding to `var` (by + name lookup in TypeDef's `vars`). + - Walk `args[i]` to its outermost type-name (peel through + mode wrappers). + - If not a primitive type name in `allowed_set`, emit + `ParamNotInRestrictedSet { type_name, var, found, allowed }`. + +The check is *generic*: nothing in the checker mentions Series +or any specific extension type. The restriction is data-driven +from the TypeDef. + +**Canonical form decision.** `param-in` is the canonical form for +closed-set type-parameter restrictions. Marker classes (a class +with no methods, used solely for type-tagging) are not +introduced as a parallel mechanism. + +**Blast radius.** + +- The `prelude` module gains `kernel: true`. **This is a code- + path migration, not a behaviour change.** Prelude has 12 free + fns today (`examples/prelude.ail:85-148`: `ne`, `lt`, `le`, + `gt`, `ge`, `print`, `float_eq`, `float_ne`, `float_lt`, + `float_le`, `float_gt`, `float_ge`) plus its three classes. + All 12 free fns are already callable bare in consumer modules + via the hardcoded auto-injection at `loader.rs:98-108`. After + prep.3, the same 12 fns remain callable bare — but the + reachability path is the generic `kernel: true` filter, not + the hardcoded `&["prelude"]` literal. Consumer-observable + behaviour: identical. Code-path: rewritten. The hash-pin + refresh in `crates/ailang-surface/tests/prelude_module_hash_pin.rs` + is required because the canonical-JSON of the prelude module + now contains `"kernel": true`, which changes the module hash; + the test file gets the new hash plus an Honesty-Rule + provenance comment quoting prep.3. +- `crates/ailang-surface/src/loader.rs` and + `crates/ailang-core/src/workspace.rs` lose the hardcoded + prelude-specific paths; they gain the flag-driven equivalent. + Detailed sites: `loader.rs:98-108`, `workspace.rs:308-311, + 467, 2655`. The `WorkspaceLoadError::ReservedModuleName` + diagnostic (currently fires when a user workspace contains a + module named `prelude`) is repositioned: any module named the + same as an auto-injected built-in kernel module is reserved, + not specifically `prelude`. For this milestone the list is + still just `prelude` + the new stub. +- The new `crates/ailang-kernel-stub/` crate is created with + its `module.ail.json` and the build wiring to feed it into + the workspace load. +- The schema-drift pin in `crates/ailang-core/tests/design_schema_drift.rs` + gains entries for `kernel`, `param-in`, and a basic stub + module round-trip. +- `crates/ail/tests/prelude_free_fns.rs` continues to pass + unchanged — that is the explicit regression-protection that + the prelude code-path migration is behaviour-equivalent. +- Workspace-load tests under `crates/ailang-core/tests/` gain + a new fixture exercising auto-import of the stub kernel + module from a consumer with no `(import ...)` declaration. + +**Integration with existing mechanisms.** + +- The prelude module's role in the workspace loader is unified + with the kernel-tier mechanism. The hardcoded prelude-name + paths today exist concretely at `loader.rs:98-108` (the + `parse_prelude()` injection + `&["prelude"]` literal) and + `workspace.rs:308-311, 467, 2655` (reservation + contract + docs). They are migrated to read `module.kernel` from each + loaded module's schema and build the implicit-imports list + from the resulting set. Single named mechanism for + "module is auto-imported"; no module name is hardcoded as + special. +- Class constraints (existing) and `param-in` (new) coexist — + see the whitepaper's "marker class" discussion. +- `Term::New` (prep.2) uses `param-in` via the standard checker + path — when `new`'s return type is `T` with `a` restricted, + the type-arg supplied at the new-site is validated. +- The existing primitive-instance codegen intercept + (`try_emit_primitive_instance_body` in `ailang-codegen`) is + *not* touched in this milestone. Its migration to a plugin + registry happens in the Series milestone, where there is a + real second consumer for the registry. Single-consumer + registries are premature mechanism. + +## Components + +| Component | Crate | What changes | +|-----------|-------|-------------| +| AST schema | `ailang-core` | `Module.kernel`, `TypeDef.param-in`, `Term::New`, `NewArg` | +| Form-A surface | `ailang-surface` | `new` keyword, `(kernel)` module attr, `(param-in ...)` typedef attr | +| Workspace-load | `ailang-core::workspace` | Kernel-tier auto-import scope | +| Resolver | `ailang-check` | Type-scoped member resolution, `Term::New` arg-kind check, `param-in` enforcement | +| Drift pin | `ailang-core/tests/design_schema_drift.rs` | New schema tags ratified | +| Hash pins | `ailang-core/tests/hash_pin.rs`, `ailang-surface/tests/prelude_module_hash_pin.rs` | Refreshed for the rewrites | +| Std fixture migration | `examples/*.ail` (~14 files) | `std_X.Y` → type-scoped form | +| Stub kernel crate | `crates/ailang-kernel-stub/` | New, minimal — exercises the mechanism | + +## Data flow + +A `.ail` consumer module that uses a kernel-tier type: + +1. **Workspace load.** Each module's manifest is read. Kernel-tier + modules are collected; their type names and def names enter + the auto-import scope. +2. **Parse.** The consumer's `(con Series ...)` (or `(con StubT ...)` + in this milestone's stub) parses to `Type::Con { name: "Series" }`. + `(new Series ...)` parses to `Term::New { type_name: "Series", args: [...] }`. + `(app Series.at s i)` parses to `Term::App { callee: Term::Var { name: "Series.at" }, args }`. +3. **Resolve.** Type-scoped resolver looks up `Series` in the + workspace TypeDef registry (auto-imported via kernel-tier). + `Series.at` resolves to the `at` def in Series's home module + (the stub or, in milestone 2, the Series crate). +4. **Type-check.** `param-in` enforcement runs on `Type::Con { + name: "Series", args }` — element type must be in the allowed + set. `Term::New` arg-kind check runs on the args. Standard + type-check otherwise. +5. **Done at `ail check`.** Codegen is out of scope this milestone. + +## Error handling + +New diagnostics introduced this milestone (all in `ailang-check`): + +| Diagnostic | Trigger | Iteration | +|------------|---------|-----------| +| `TypeScopedMemberNotFound` | `T.x` where T is a type but `x` not in T's home module | prep.1 | +| `TypeScopedReceiverNotAType` | `X.y` where X is neither a known type nor a known module | prep.1 | +| `NewTypeNotConstructible` | `(new T args)` where T has no `new` def in its home module | prep.2 | +| `NewArgKindMismatch` | `(new T args)` where an arg is Type-positional where Value expected (or vice versa) | prep.2 | +| `ParamNotInRestrictedSet` | `Type::Con { name, args }` where `args[i]` violates the TypeDef's `param-in` for the corresponding var | prep.3 | + +`BareCrossModuleTypeRef` and `BadCrossModuleTypeRef` (pre-existing) +are repurposed in prep.1: they now fire when a type name resolves +through neither type-scoped lookup, nor an explicit import, nor a +kernel-tier auto-import. The semantic class of error remains "type +name not resolvable", but the suggested fix in the message +changes. + +## Testing strategy + +**Layer 1 — Schema drift** (`crates/ailang-core/tests/design_schema_drift.rs`): +- `module_kernel_flag_round_trips` — pins `Module.kernel = true` + serialises and deserialises with bit-identical bytes; `kernel: + false` is omitted from output. +- `typedef_param_in_round_trips` — pins `TypeDef.param_in` map + serialises with the `param-in` key (kebab); empty map omitted. +- `term_new_round_trips` — pins `Term::New { type_name, args }` + serialises with `t: "new"`, each arg with `kind: "type"|"value"`. + +**Layer 2 — Round-trip surface** (`crates/ailang-surface/tests/round_trip.rs`): +- Fixture for `(kernel)` in module header. +- Fixture for `(new T ...)` with mixed-kind args. +- Fixture for `(param-in (var t1 t2))` in TypeDef. +- All fixtures round-trip Form-A → JSON → Form-A bit-identical. + +**Layer 3 — Checker** (`crates/ailang-check/src/*.rs` in-source tests): +- `type_scoped_member_resolves` — `Maybe.from_maybe` resolves to + `std_maybe.from_maybe`'s def. +- `type_scoped_member_not_found` — `Maybe.bogus` emits diagnostic. +- `type_scoped_receiver_not_a_type` — `NotAType.x` emits diagnostic. +- `new_resolves_via_type_scope` — `(new Counter 42)` finds local + `new` def. +- `new_type_not_constructible` — `(new IntList ...)` (no `new` def + in IntList's home module) emits diagnostic. +- `new_arg_kind_mismatch_value_where_type` — `(new Series 3 (con Float))` + emits diagnostic. +- `param_in_accepts_allowed_type` — `(con StubT (con Int))` + type-checks. +- `param_in_rejects_disallowed_type` — `(con StubT (con Str))` + emits `ParamNotInRestrictedSet`. + +**Layer 4 — Workspace load** (`crates/ailang-core/tests/workspace_kernel.rs`, +new): +- Kernel-tier module's types are visible to a consumer without + any `(import ...)` declaration. +- Two kernel-tier modules with non-colliding names co-load. +- Explicit import overrides auto-import (precedence test). + +**Layer 5 — End-to-end via `ail check`** (`crates/ail/tests/e2e.rs`): +- The stub kernel module + a stub consumer checks clean. +- The `param-in` violation example produces the expected + diagnostic. + +**Layer 6 — Migrated std-library examples**: +- All migrated `.ail` examples (std_maybe_demo, std_list_demo, + etc.) check clean. Their `.ail.json` round-trip pins refreshed. + +## Acceptance criteria + +Milestone closes when: + +1. All four mechanisms (type-scoped namespacing, `Term::New`, + kernel-tier modules + auto-import, `param-in`) are implemented + and merged to main. +2. All five new diagnostics fire on their RED fixtures and do + not fire on green code. +3. The schema-drift pin ratifies `kernel`, `param-in`, `new`, + `NewArg` JSON tags. +4. The round-trip test exercises all new surface forms. +5. The stub kernel crate's module checks clean and is auto- + imported by a consumer module with no explicit import. +6. All 14-ish migrated `.ail` examples in `examples/` check + clean and round-trip to byte-identical Form-A. +7. Hash pins refreshed in both `crates/ailang-core/tests/hash_pin.rs` + and `crates/ailang-surface/tests/prelude_module_hash_pin.rs`, + each with an Honesty-Rule provenance comment. +8. The whitepaper `design/models/kernel-extensions.md` is + updated: sections describing prep.1, prep.2, prep.3 transition + from forward-looking ("will resolve…") to present-state + ("resolves…") where appropriate; STATUS header updated to + "Mechanisms milestone closed YYYY-MM-DD; Series milestone + pending." +9. The `design/INDEX.md` ledger entry's "design accepted + 2026-05-28; impl in progress" annotation is updated to reflect + the milestone close. +10. `bench/check.py` clean — no performance regression on the + existing benches (this milestone touches resolver / parser / + schema, not codegen or runtime; regression is unexpected + but bench is part of the close-out per audit discipline). + +## Out of scope (explicit) + +- The `RawBuf` base extension — kernel-tier module with Rust + codegen intercepts emitting LLVM IR for `new`/`get`/`set`/`size`, + element-type restriction via `param-in`. Future Gitea milestone + `raw-buf`. +- The `Series` library extension — kernel-tier `.ail` module + defining the Series ADT and its operations (push/at/len/ + total_count) in AILang itself, on top of RawBuf. Future Gitea + milestone `series`. +- Migration of `try_emit_primitive_instance_body` into a plugin + intercept registry. Happens in the `raw-buf` milestone when + the first base-extension consumer exists. +- LSP / MCP integration for `ail describe Series`. Out of scope + for all three milestones; future axis. +- Higher-kinded `param-in` (the restriction is currently + flat — type variable to set of named types; future variants + might restrict to "any type satisfying some structural + predicate", but that is not specified here). +- Type-scoped access on user types ≠ home-module defs (e.g. + cross-module-extension methods). Out of scope; the mechanism + is strictly "type T's home module's defs are accessible as + T.x". +- An auto-import precedence override syntax (the explicit-import + wins behaviour is implementation; no new author syntax is added + for it). +- Record-element support in RawBuf (the struct-of-arrays layout + for `Series Record`). The architecture accommodates it (see + whitepaper § "Forward axis: SoA for records") but it is a + later RawBuf-internal change that does not touch Series's + AILang code; out of scope for the three named milestones. + +## Iteration scope + +The plan that follows this spec carves the work into three +iterations: + +- **prep.1** — Type-scoped namespacing. Resolver change + 14 + example rewrites + 2 hash-pin refreshes. +- **prep.2** — `Term::New`. AST + surface + checker arg-kind + enforcement. +- **prep.3** — Kernel-tier modules + `param-in`. Schema + + workspace-load + checker enforcement + stub crate. + +Each iteration is independently shippable; main is green at every +iteration boundary.