Files
AILang/docs/specs/0052-kernel-extension-mechanics.md
T
Brummel 46c9aabf00 plan: prep.1 type-scoped namespacing — 5-task atomic resolver + 12-fixture migration (refs #31)
The plan covers the first iteration of the kernel-extension-mechanics
milestone: type-scoped `<TypeName>.<member>` resolution in
`ailang-check`, narrowed `BareCrossModuleTypeRef` /
`BadCrossModuleTypeRef` diagnostics in `ailang-core::workspace`,
two new `CheckError` variants, CLI diagnostic-message rewording,
and atomic rewrite of 12 `.ail` example fixtures from `std_X.Y` to
the type-scoped form. Five tasks, each unit-of-review.

Includes a spec correction (same commit because plan recon
surfaced it): the prep.1 Blast Radius previously claimed
`hash_pin.rs` + `prelude_module_hash_pin.rs` refreshes and a
`design_schema_drift.rs` pin addition. Plan-recon walked every
test crate (per the schema-camelcase-fix hash-pin-blast-radius
lesson) and found:
  * neither hash-pin file pins any fixture in prep.1's migration
    set — refresh is empty;
  * type-scoped resolution is a checker-only change (no new JSON
    tags, no AST shape change) — the drift pin belongs to prep.2
    (`Term::New`) and prep.3 (`kernel: true` + `param-in`), not
    prep.1.

Spec section 'Blast radius' and the 'Iteration scope' summary now
reflect the recon-cleared reality.
2026-05-28 14:04:01 +02:00

30 KiB

Kernel extension mechanics — Design Spec

Date: 2026-05-28 Status: Draft — awaiting user spec review Authors: Brummel (orchestrator) + Claude Reference: design/models/0007-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 — <TypeName>.<member> 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 (12 with cross-module refs, plus the three defining modules with no refs): ct_2_bare_cross_module.ail, ct_3b_bad_qualified_known_module.ail, nested_pat.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_demo.ail, std_pair_demo.ail. Each rewritten from std_X.Y to Y (type-scoped) where Y is type-associated. The three defining modules std_either.ail, std_maybe.ail, std_pair.ail contain no cross-module references and need no body changes (intra-module refs are bare today already). ct_2_bare_cross_module.ail's role flips semantically: it stays RED (the unimported bare type case still fires BareCrossModuleTypeRef under the narrowed rule), but the diagnostic message it asserts is the new one.
  • No corresponding .ail.json fixtures. None of the 15 spec-named .ail files have a sibling .ail.json round-trip pin in the tree.
  • Source-side reference in crates/ailang-{check,codegen,surface}/src/ and crates/ail/tests/e2e.rs (7 files): doc-comments and test-helper code mentioning std_X.Y vocabulary update to type-scoped vocabulary. Production type-resolution logic is the new code. The specific sites are enumerated in the prep.1 plan.
  • CLI diagnostic renderer + assertion update: crates/ail/src/main.rs:1249-1278 (the BareCrossModuleTypeRef and BadCrossModuleTypeRef translation arms) and crates/ail/tests/ct1_check_cli.rs:154 (an assertion on the old "ail migrate-canonical-types" hint string) move with the diagnostic-message narrowing.

No hash-pin or schema-drift work in prep.1. The hash-pin audit across every test crate (per the hash-pin blast-radius audit lesson from schema-camelcase-fix) is mandatory and was performed during prep.1's plan recon. Result: crates/ailang-core/tests/hash_pin.rs pins sum.ail, list.ail, ordering_match.ail, test_22b1_dup_a.ail, test_22b1_dup_classmod.ail — none of which contain std_X.Y references; crates/ailang-surface/tests/prelude_module_hash_pin.rs pins prelude.ail — also no std_X.Y references. No pin refresh applies to prep.1. The prelude_module_hash_pin.rs refresh happens in prep.3 when kernel: true lands on the prelude module. Schema-drift pins in crates/ailang-core/tests/design_schema_drift.rs also do not apply: type-scoped resolution is a checker change with no new JSON tags, no new enum variants, no AST shape changes. The drift pins for this milestone land in prep.2 (new t: "new" tag, new NewArg JSON) and prep.3 (new kernel, param-in schema attrs).

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) 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:

pub enum Term {
    // ...
    New {
        type_name: TypeName,
        args: Vec<NewArg>,
    },
}

pub enum NewArg {
    Type(Type),
    Value(Term),
}

Serialised JSON:

{ "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<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))))

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 IntInt ∈ {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:

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<String, BTreeSet<TypeName>>,
}

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<a> 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_resolvesMaybe.from_maybe resolves to std_maybe.from_maybe's def.
  • type_scoped_member_not_foundMaybe.bogus emits diagnostic.
  • type_scoped_receiver_not_a_typeNotAType.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/0007-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 + 12 example rewrites + diagnostic-message narrowing + ct1_check_cli assertion update. No hash-pin or drift-test work (audit cleared during plan recon; pins live in prep.2/3).
  • prep.2Term::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.