diff --git a/docs/specs/0053-fieldtest-kernel-extension-mechanics.md b/docs/specs/0053-fieldtest-kernel-extension-mechanics.md
new file mode 100644
index 0000000..1811116
--- /dev/null
+++ b/docs/specs/0053-fieldtest-kernel-extension-mechanics.md
@@ -0,0 +1,342 @@
+# Fieldtest — kernel-extension-mechanics — 2026-05-28
+
+**Status:** Draft — awaiting orchestrator triage
+**Author:** fieldtester (dispatched by fieldtest skill)
+
+## Scope
+
+The kernel-extension-mechanics milestone (commits `b586999`, `078c39a`,
+`9339279`, tidy `9d2e752`) ships four language-level mechanisms for
+plugin-style extension types: type-scoped namespacing
+(`TypeName.member`), the `(new T args)` term construct, kernel-tier
+modules with `(kernel)` auto-import flag, and `(param-in (a T1 T2 ...))`
+closed-set type-parameter restriction. The milestone touches the
+schema, surface parser/printer, checker, and workspace loader.
+Codegen for `Term::New` is explicitly out of scope (deferred to
+raw-buf). The stub crate `ailang-kernel-stub` ships as an
+auto-injected kernel-tier module purely as a ratifying fixture.
+
+## Examples
+
+### `examples/fieldtest/kem_1_list_running_sum.ail` — type-scoped namespacing cross-module
+- Builds a `List<Int>` via `term-ctor`, prints its length via
+  `(app List.length xs)` and its sum via `(app List.fold_left add 0 xs)`.
+  Imports `std_list` explicitly; bare `List`/`Int` in type slots.
+- Why fits: this is the spec's prep.1 canonical-form example over a
+  different home module and a function (fold_left) that takes a
+  lambda arg — a shape an LLM author naturally produces.
+- Outcome: `ail check` clean (`ok (48 symbols across 5 modules)`);
+  `ail run` prints `5\n15\n`. Required two local symlinks
+  (`std_list.ail`, `std_maybe.ail`) in `examples/fieldtest/`
+  because the loader resolves cross-module imports against the
+  entry file's directory — see Finding F2.
+
+### `examples/fieldtest/kem_2_counter_new.ail` — `(new T args)` term construct
+- The spec's literal prep.2 worked example (a local Counter ADT
+  with a `new` def and `(new Counter 42)` consumer).
+- Outcome: `ail check` clean (`ok (31 symbols across 3 modules)`).
+  `ail run` fails with the explicit codegen-deferral diagnostic
+  `internal: Term::New cannot be synthed at codegen — must be
+  desugared first; codegen support lands in the raw-buf milestone`.
+  Per spec § Architecture this is the explicit out-of-scope of the
+  milestone — recorded as a `working` finding (Finding F6).
+
+### `examples/fieldtest/kem_2b_min_repro.ail` — minimal repro for the same-module type-scoped-call bug
+- Same Counter shape minus the `new` def: one `value` projector,
+  one consumer site that calls `(app Counter.value c)` from
+  within Counter's home module.
+- Why fits: surfaced while extending kem_2 with a `value`
+  projector — turned out to be a clean repro of an axis-1 corner
+  the spec didn't carve out.
+- Outcome: `ail check` fails with
+  `[type-mismatch] main: type mismatch: expected
+  kem_2b_min_repro.Counter, got Counter`. Switching the call to
+  bare `(app value c)` makes the program check clean — see Finding F1.
+
+### `examples/fieldtest/kem_3_stub_consumer.ail` — kernel-tier auto-import in type position
+- A consumer that uses `(con StubT (con Int))` in a fn type
+  signature without `(import kernel_stub)`. The stub kernel module
+  is auto-injected by the workspace loader (`ail workspace` lists
+  it) and per spec § "Iteration prep.3" "the module's types are
+  accessible bare in type position".
+- Outcome: `ail check` fails with
+  `[unknown-module] unwrap_int: unknown module prefix
+  `kernel_stub` in qualified reference` (twice). Adding an explicit
+  `(import kernel_stub)` fails earlier with `[module-not-found]
+  expected at <sibling>/kernel_stub.ail.json` because the stub has
+  no on-disk file — see Finding F3.
+
+### `examples/fieldtest/kem_4_paramin_box_green.ail` — param-in restriction, accepting path
+- A user-defined `NumBox (vars a) (param-in (a Int Float))` ADT,
+  instantiated with `(con NumBox (con Int))`. Verifies the
+  param-in check is permissive when the type-arg is in the
+  allowed set.
+- Outcome: `ail check` clean; `ail run` prints `17\n`. See
+  Finding F7.
+
+### `examples/fieldtest/kem_4_paramin_box_red.ail` — param-in restriction, must-fail path
+- Same `NumBox` with `param-in (a Int Float)`, instantiated with
+  `(con NumBox (con Str))`. Expected diagnostic per spec table:
+  `ParamNotInRestrictedSet`.
+- Outcome: `ail check` fails with
+  `[param-not-in-restricted-set] unwrap_str: type-arg `Str` is
+  not in the restricted set for type-variable `a` of `NumBox``.
+  Diagnostic is precise — names the offending type, the
+  type-variable, and the TypeDef that owns the restriction. See
+  Finding F8.
+
+## Findings
+
+### [bug] F1 — Type-scoped call to a same-module def is rejected with a phantom-qualified type-mismatch
+- **Example:** `kem_2b_min_repro.ail` (minimal); also originally
+  surfaced in `kem_2_counter_new.ail` while drafting.
+- **What happened (verbatim):**
+  ```
+  $ ail check examples/fieldtest/kem_2b_min_repro.ail
+  error: [type-mismatch] main: type mismatch:
+      expected kem_2b_min_repro.Counter, got Counter
+  ```
+  Switching the call site from `(app Counter.value c)` to bare
+  `(app value c)` makes the same program check clean.
+- **Why it is a bug:** Per spec § "Iteration prep.1 — Type-scoped
+  namespacing" → "Canonical form decision": "Type-scoped form is
+  the canonical form for type-associated operations". The spec
+  does NOT carve out same-module calls as forbidden / different.
+  An LLM author who's just written `value` next to `data Counter`
+  in the same file will naturally reach for `Counter.value` from
+  inside main — the same way they spell every cross-module call
+  per Axis 1. The current resolver appears to produce a
+  qualified `<this-module>.Counter` for the return type of
+  `value` reached through `Counter.value`, but compares against
+  an unqualified `Counter` produced by the caller's local-scope
+  `value` lookup. The diagnostic itself is misleading — the two
+  types are the same, just written differently.
+- **Repro:** `ail check examples/fieldtest/kem_2b_min_repro.ail`.
+- **Recommended downstream action:** `debug` — write a RED test
+  that pins the same-module type-scoped-call expects-clean
+  behaviour, then `implement` mini-mode fixes the resolver to
+  treat `<this-module>.<Type>` and bare `<Type>` as one type.
+
+### [bug] F3 — Kernel-tier auto-import does not register the module as a valid qualifier prefix
+- **Example:** `kem_3_stub_consumer.ail`.
+- **What happened (verbatim):**
+  ```
+  $ ail check examples/fieldtest/kem_3_stub_consumer.ail
+  error: [unknown-module] unwrap_int: unknown module prefix
+      `kernel_stub` in qualified reference
+  error: [unknown-module] main: unknown module prefix
+      `kernel_stub` in qualified reference
+  ```
+  `ail workspace examples/fieldtest/kem_3_stub_consumer.ail` lists
+  `kernel_stub` as a loaded module with 1 def. Adding an explicit
+  `(import kernel_stub)` fails earlier with
+  `[module-not-found] expected at
+  /home/brummel/dev/ailang/examples/fieldtest/kernel_stub.ail.json`
+  — the stub has no on-disk manifest, it is built into the
+  compiler.
+- **Why it is a bug:** Per spec § "Iteration prep.3 — Kernel-tier
+  modules + param-in" the kernel-tier `Module.kernel: true` flag
+  promises: "The module's top-level defs are accessible bare in
+  every other module of the workspace, with no `(import ...)`
+  declaration required. The module's types are accessible bare in
+  type position." Prelude's free fns (`print`, `lt`, ...) do
+  satisfy that promise — `prelude_free_fns.rs` ratifies it. But
+  the stub kernel module's TypeDef `StubT`, referenced bare in a
+  type slot, is qualified by the pre-pass to `kernel_stub.StubT`,
+  and the resolver then rejects `kernel_stub` as an unknown module
+  prefix. The auto-import mechanism is asymmetric: it scopes
+  the names but does not register the kernel module as a
+  resolvable qualifier. Two layers (the pre-pass that qualifies
+  bare type names, and the resolver that validates qualified
+  module prefixes) disagree on whether kernel-tier modules count.
+  The shipped kernel_stub TypeDef appears effectively unreachable
+  from any consumer.
+- **Repro:** `ail check examples/fieldtest/kem_3_stub_consumer.ail`.
+- **Recommended downstream action:** `debug` — write a RED test
+  that a consumer using `(con StubT (con Int))` (or `(con
+  kernel_stub.StubT (con Int))` explicitly) checks clean; then
+  `implement` mini-mode either teaches the resolver to recognise
+  every kernel-tier module as an implicit qualifier, or teaches
+  the workspace pre-pass to leave bare references to kernel-tier
+  types un-qualified.
+
+### [bug] F4 — Spec's prep.3 worked consumer cannot compile against the actual shipped stub
+- **Example:** observed via probe (see § Examples kem_3 narrative);
+  not a standalone fixture because F3 already blocks the type
+  signature.
+- **What happened (verbatim):**
+  ```
+  $ cat /tmp/stub_consumer.ail
+  (module stub_consumer
+    (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)))))))
+  $ ail check /tmp/stub_consumer.ail
+  error: [new-type-not-constructible] main: type `StubT` is not
+      constructible: home module `kernel_stub` declares no `new` def
+  ```
+- **Why it is a bug:** Spec § "Iteration prep.3" → "Worked author
+  example — kernel-tier stub module" specifies the stub as a
+  TypeDef PLUS a `(fn new ...)` def, and the immediately following
+  "Worked consumer" exercises `(new StubT 42)`. The shipped stub
+  (per `ail describe --workspace … StubT`) has only the TypeDef
+  with one ctor `Stub` — no `new` fn. The implementation diverged
+  from the spec's stub design; the consumer-side worked example
+  the spec promises no longer compiles. The diagnostic the
+  resolver emits is excellent (precise, names the home module,
+  names the missing def) — that part is `working` and is
+  separately recorded as F5.
+- **Repro:** see narrative.
+- **Recommended downstream action:** `ratify` — either add the
+  `new` def to the stub (the spec's design) and refresh the
+  STUB_AIL constant + drift pin, or amend the design model and
+  spec to say "the stub has only a TypeDef; consumers must use
+  `term-ctor`" (which is also a coherent reading because the
+  stub's purpose is to exercise auto-import + param-in, not
+  `Term::New`). Either reading restores spec/ship coherence; the
+  current state has a drift.
+
+### [working] F5 — `NewTypeNotConstructible` diagnostic is precise
+- **Example:** observed via the F4 probe.
+- **What happened:** The diagnostic
+  `[new-type-not-constructible] main: type `StubT` is not
+  constructible: home module `kernel_stub` declares no `new` def`
+  names the offending type, the home module, and the missing def
+  in one sentence. An LLM author reading this routes correctly to
+  one of two natural next actions: add a `new` def, or use a
+  different construction path. Worth recording as a win: prep.2's
+  diagnostic is doing its job.
+- **Recommended downstream action:** carry-on.
+
+### [working] F6 — Term::New codegen-deferral diagnostic names the future milestone
+- **Example:** `kem_2_counter_new.ail` via `ail run`.
+- **What happened:**
+  ```
+  Error: module `kem_2_counter_new`: def `main`: internal:
+      Term::New cannot be synthed at codegen — must be
+      desugared first; codegen support lands in the raw-buf
+      milestone
+  ```
+- **Why a win:** The spec explicitly carves codegen out of scope
+  for this milestone. The error message explicitly names the
+  future milestone (`raw-buf`) where codegen support will land.
+  An LLM author sees the message and routes correctly: "this is
+  expected at this stage, the path forward is the raw-buf
+  milestone" — no guessing, no false leads. The contrast with the
+  phantom-qualified mismatch (F1) is sharp: F6 is what a precise
+  out-of-scope diagnostic looks like.
+- **Recommended downstream action:** carry-on.
+
+### [working] F7 — param-in accepts allowed type silently and end-to-end
+- **Example:** `kem_4_paramin_box_green.ail`.
+- **What happened:** `(con NumBox (con Int))` where
+  `NumBox`'s `param-in` is `(a Int Float)` checks clean; the
+  program also builds and runs (`ail run` prints `17`). The
+  param-in mechanism is data-driven from the TypeDef as spec
+  promises — nothing in the checker mentions `NumBox` specifically,
+  same enforcement path that fires `ParamNotInRestrictedSet` on
+  the RED case. A user TypeDef gets the same treatment as the
+  built-in stub, confirming the generic data-driven story.
+- **Recommended downstream action:** carry-on.
+
+### [working] F8 — ParamNotInRestrictedSet diagnostic is precise
+- **Example:** `kem_4_paramin_box_red.ail`.
+- **What happened:** Diagnostic
+  `[param-not-in-restricted-set] unwrap_str: type-arg `Str` is
+  not in the restricted set for type-variable `a` of `NumBox``
+  names the type-arg, the type-variable, and the TypeDef. An LLM
+  author reading this routes correctly to either (a) change the
+  type-arg to one in the allowed set or (b) extend the
+  TypeDef's `param-in`. The message does NOT name the allowed
+  set explicitly — that would make it a one-line full-context
+  diagnostic; recorded as a potential future polish in F9.
+- **Recommended downstream action:** carry-on.
+
+### [friction] F2 — Loader's sibling-only module resolution makes the fieldtest dir awkward
+- **Example:** `kem_1_list_running_sum.ail` and its symlinked
+  `std_list.ail` / `std_maybe.ail` in `examples/fieldtest/`.
+- **What happened (verbatim):**
+  ```
+  $ ail check examples/fieldtest/kem_1_list_running_sum.ail
+  error: [module-not-found] module `std_list` not found
+      (expected at /home/brummel/dev/ailang/examples/fieldtest/std_list.ail.json)
+  ```
+  The same consumer module sitting in `examples/` checks clean;
+  inside `examples/fieldtest/` it does not, because the loader
+  resolves `(import std_list)` against the entry file's directory.
+- **Why friction (not bug):** The loader behaviour is consistent
+  with its existing one-directory-per-workspace model; the spec
+  doesn't promise multi-directory loading. But the
+  fieldtest_examples path is `examples/fieldtest/` per the project
+  profile — every cross-module fixture either has to be entirely
+  self-contained (no `(import std_*)`) or pull in symlinks to
+  files in `examples/`. That tax falls on every future fieldtest.
+  An LLM author writing a new program for the project would hit
+  the same wall.
+- **Secondary friction:** the error message lists only the
+  `.ail.json` path even though the loader does in fact look for
+  both `.ail` and `.ail.json` (the existing `examples/` tree has
+  no `.ail.json` files for `std_list`, yet check there works). A
+  user reading the diagnostic would conclude they need to author
+  a `.ail.json` — a wrong reading.
+- **Recommended downstream action:** `plan` — small tidy iteration:
+  (a) loader looks up modules through a workspace-config search
+  path (analogous to `examples/` itself), so fixtures can sit
+  outside the canonical example directory without symlinks;
+  AND/OR (b) diagnostic message updated to list both expected
+  paths and to suggest the workspace config addition. Either
+  half-fix removes the symlink-as-workaround pattern.
+
+### [spec_gap] F9 — `unit` literal: design model uses it, checker rejects it
+- **Example:** `kem_4_paramin_box_red.ail` first draft (before fix).
+- **What happened:**
+  ```
+  ; before fix
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body unit))
+  ; resulting diagnostic:
+  ;   [unbound-var] main: unknown identifier: `unit`
+  ```
+  `design/models/0007-kernel-extensions.md` line 80 uses `unit` as
+  a value literal of type `Unit`. The checker treats it as a
+  Term::Var lookup and emits `[unbound-var]`. The fix in
+  `kem_4_paramin_box_red.ail` was to replace the body with
+  `(do io/print_str "")` — a small awkwardness for any
+  "intentionally empty effectful main" pattern.
+- **Why spec_gap (not bug):** The whitepaper and design ledger
+  may simply have been imprecise — there's no language contract
+  pinning `unit` as a value literal. But the design model uses
+  it as if it were canonical; an LLM author reading
+  `design/models/0007` will reach for it.
+- **Recommended downstream action:** `ratify` or
+  `tighten the design ledger` — either add `unit` as the
+  canonical Unit-value literal (a one-line resolver change) and
+  document it, or remove the usage from
+  `design/models/0007-kernel-extensions.md` and replace with the
+  canonical idiom. The current state has the model and the
+  surface disagreeing.
+
+## Recommendation summary
+
+| Finding | Class | Recommended action |
+|---|---|---|
+| F1 | bug | debug → implement (resolver: equate `<this>.T` with bare `T`) |
+| F2 | friction | plan (tidy iteration: loader search path + diagnostic) |
+| F3 | bug | debug → implement (auto-import registers module as qualifier) |
+| F4 | bug | debug or ratify (stub: add `new` def, OR amend spec) |
+| F5 | working | carry-on |
+| F6 | working | carry-on |
+| F7 | working | carry-on |
+| F8 | working | carry-on |
+| F9 | spec_gap | ratify OR tighten design model |
+
+### Concerns / blockers
+
+None. The two bugs (F1, F3) are diagnosis-clear and have minimal
+repros in the working tree. F4 is a spec/ship coherence call —
+either reading is coherent; needs an orchestrator decision.
diff --git a/examples/fieldtest/kem_1_list_running_sum.ail b/examples/fieldtest/kem_1_list_running_sum.ail
new file mode 100644
index 0000000..5ad8901
--- /dev/null
+++ b/examples/fieldtest/kem_1_list_running_sum.ail
@@ -0,0 +1,36 @@
+; Fieldtest kem.1 (Axis 1, type-scoped namespacing) — a consumer of
+; std_list that drives several List.<fn> calls from one main. The
+; LLM-natural shape is to spell every type-associated op with the
+; type-name prefix (`List.length`, `List.fold_left`, `List.map`),
+; not the module qualifier. Bare `List`/`Int` in type positions; bare
+; ctor names `Cons`/`Nil` because the type is in scope via
+; `(import std_list)`. The cycle's worked example for axis 1 is the
+; std_maybe_demo migration; this example is the same shape over
+; List<Int>, exercising a different home module and a function
+; (fold_left) that takes a lambda — the LLM-natural shape there is to
+; keep the lambda inline at the call site.
+
+(module kem_1_list_running_sum
+
+  (import std_list)
+
+  (fn add
+    (doc "Plain Int addition. Used as the (b, a) -> b arg to List.fold_left.")
+    (type (fn-type (params (con Int) (con Int)) (ret (con Int))))
+    (params acc x)
+    (body (app + acc x)))
+
+  (fn main
+    (doc "Build a List<Int> of [1,2,3,4,5], print its length (5), then its sum (15).")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let xs
+        (term-ctor List Cons 1
+        (term-ctor List Cons 2
+        (term-ctor List Cons 3
+        (term-ctor List Cons 4
+        (term-ctor List Cons 5
+        (term-ctor List Nil))))))
+        (seq (seq (app print (app List.length xs)) (do io/print_str "\n"))
+             (seq (app print (app List.fold_left add 0 xs)) (do io/print_str "\n")))))))
diff --git a/examples/fieldtest/kem_2_counter_new.ail b/examples/fieldtest/kem_2_counter_new.ail
new file mode 100644
index 0000000..e3c13b7
--- /dev/null
+++ b/examples/fieldtest/kem_2_counter_new.ail
@@ -0,0 +1,34 @@
+; Fieldtest kem.2 (Axis 2, (new T args) term construct) — derived
+; from the spec's prep.2 § "Iteration prep.2 — `new` term construct"
+; worked example, kept literally identical to that example so the
+; outcome speaks to the spec's own promise.
+;
+; Outcome:
+;   - `ail check` clean (the construct elaborates).
+;   - `ail run` fails with the codegen-deferral error
+;     "Term::New cannot be synthed at codegen — must be desugared
+;     first; codegen support lands in the raw-buf milestone".
+;     Per spec § Architecture this is the explicit out-of-scope of
+;     the milestone; recorded as a `working` finding (the diagnostic
+;     correctly names the future milestone and is precise enough that
+;     an LLM author can route to the right next step).
+
+(module kem_2_counter_new
+
+  (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)
+            (seq (app print x) (do io/print_str "\n"))))))))
diff --git a/examples/fieldtest/kem_2b_min_repro.ail b/examples/fieldtest/kem_2b_min_repro.ail
new file mode 100644
index 0000000..97b0cf3
--- /dev/null
+++ b/examples/fieldtest/kem_2b_min_repro.ail
@@ -0,0 +1,22 @@
+; Minimal repro of the same-module type-scoped call bug.
+; Calling `(app Counter.value c)` from within Counter's home
+; module raises [type-mismatch] expected `kem_2b_min_repro.Counter`,
+; got `Counter` — even though `value` belongs to *this* module.
+; Switching to bare `(app value c)` works.
+
+(module kem_2b_min_repro
+
+  (data Counter
+    (ctor MkCounter (con Int)))
+
+  (fn value
+    (type (fn-type (params (con Counter)) (ret (con Int))))
+    (params c)
+    (body (match c (case (pat-ctor MkCounter x) x))))
+
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let c (term-ctor Counter MkCounter 41)
+        (app print (app Counter.value c))))))
diff --git a/examples/fieldtest/kem_3_stub_consumer.ail b/examples/fieldtest/kem_3_stub_consumer.ail
new file mode 100644
index 0000000..22b3dd6
--- /dev/null
+++ b/examples/fieldtest/kem_3_stub_consumer.ail
@@ -0,0 +1,51 @@
+; Fieldtest kem.3 (Axis 3, kernel-tier modules + auto-import) — a
+; consumer that references `kernel_stub`'s TypeDef without an
+; `(import kernel_stub)` declaration. Per spec § "Iteration prep.3":
+;
+;   - The module's top-level defs are accessible bare in every other
+;     module of the workspace, with no `(import ...)` declaration
+;     required.
+;   - The module's types are accessible bare in type position.
+;
+; Outcome: `ail check` fails with
+;
+;     [unknown-module] unwrap_int: unknown module prefix
+;     `kernel_stub` in qualified reference
+;
+; The workspace pre-pass rewrites bare `StubT` to qualified
+; `kernel_stub.StubT` (correct per prep.1's `qualify_workspace_term`);
+; but the resolver does not accept `kernel_stub` as a valid module
+; prefix because the consumer has no explicit `(import kernel_stub)`.
+; That is, the qualification pre-pass and the auto-import scope are
+; not cooperating — the auto-import does NOT add the kernel module
+; to the resolver's known-prefixes set.
+;
+; Workarounds attempted:
+;
+;   - Adding `(import kernel_stub)`: fails earlier with
+;     [module-not-found] expected at <sibling>/kernel_stub.ail.json
+;     — the kernel stub has no on-disk file, it is built into the
+;     compiler binary.
+;   - Bare `StubT` everywhere: same outcome as above (the pre-pass
+;     qualifies it before the resolver sees it).
+;
+; Prelude's bare fns (`print`, `lt`, etc.) DO work — prelude_free_fns
+; ratifies that. So the bug is specifically about TypeDefs in type
+; position for kernel-tier modules other than prelude. The shipped
+; kernel_stub TypeDef appears unreachable from any consumer in
+; practice.
+
+(module kem_3_stub_consumer
+
+  (fn unwrap_int
+    (doc "Project the Int back out of a StubT<Int>. Bare `StubT` in the type slot exercises the kernel-tier auto-import — and currently fails to resolve.")
+    (type (fn-type (params (con StubT (con Int))) (ret (con Int))))
+    (params s)
+    (body (match s (case (pat-ctor Stub x) x))))
+
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let s (term-ctor StubT Stub 7)
+        (seq (app print (app unwrap_int s)) (do io/print_str "\n"))))))
diff --git a/examples/fieldtest/kem_4_paramin_box_green.ail b/examples/fieldtest/kem_4_paramin_box_green.ail
new file mode 100644
index 0000000..fa60ee0
--- /dev/null
+++ b/examples/fieldtest/kem_4_paramin_box_green.ail
@@ -0,0 +1,29 @@
+; Fieldtest kem.4-green (Axis 4, param-in restriction, accepting path).
+; User-defined `NumBox a` ADT restricts its type parameter to
+; {Int, Float}. The consumer uses `(con NumBox (con Int))` — Int is in
+; the allowed set, so check is clean.
+;
+; Per spec § "Iteration prep.3 — Kernel-tier modules + param-in":
+; the param-in restriction is a generic, data-driven check; nothing
+; in the checker mentions any specific extension. So a user TypeDef
+; can declare it just as the stub kernel_stub.StubT does.
+
+(module kem_4_paramin_box_green
+
+  (data NumBox (vars a)
+    (doc "An Int-or-Float container — param-in restriction on `a`.")
+    (param-in (a Int Float))
+    (ctor MkNumBox a))
+
+  (fn unwrap
+    (doc "Project the contained Int out of a NumBox<Int>.")
+    (type (fn-type (params (con NumBox (con Int))) (ret (con Int))))
+    (params b)
+    (body (match b (case (pat-ctor MkNumBox x) x))))
+
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let b (term-ctor NumBox MkNumBox 17)
+        (seq (app print (app unwrap b)) (do io/print_str "\n"))))))
diff --git a/examples/fieldtest/kem_4_paramin_box_red.ail b/examples/fieldtest/kem_4_paramin_box_red.ail
new file mode 100644
index 0000000..5e69250
--- /dev/null
+++ b/examples/fieldtest/kem_4_paramin_box_red.ail
@@ -0,0 +1,23 @@
+; Fieldtest kem.4-red (Axis 4, param-in restriction, must-fail path).
+; Same NumBox<a> with `param-in (a Int Float)`, but the consumer
+; instantiates it with `(con Str)` — Str is not in the allowed set.
+; Expected diagnostic per spec § Error handling table:
+; `ParamNotInRestrictedSet`.
+
+(module kem_4_paramin_box_red
+
+  (data NumBox (vars a)
+    (doc "Int-or-Float container — param-in restriction on `a`.")
+    (param-in (a Int Float))
+    (ctor MkNumBox a))
+
+  (fn unwrap_str
+    (doc "BAD: NumBox is restricted to {Int, Float}, but we ask for Str. Expected: ParamNotInRestrictedSet on the type signature.")
+    (type (fn-type (params (con NumBox (con Str))) (ret (con Str))))
+    (params b)
+    (body (match b (case (pat-ctor MkNumBox x) x))))
+
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body (do io/print_str ""))))
diff --git a/examples/fieldtest/std_list.ail b/examples/fieldtest/std_list.ail
new file mode 120000
index 0000000..b389ef8
--- /dev/null
+++ b/examples/fieldtest/std_list.ail
@@ -0,0 +1 @@
+../std_list.ail
\ No newline at end of file
diff --git a/examples/fieldtest/std_maybe.ail b/examples/fieldtest/std_maybe.ail
new file mode 120000
index 0000000..c9bff78
--- /dev/null
+++ b/examples/fieldtest/std_maybe.ail
@@ -0,0 +1 @@
+../std_maybe.ail
\ No newline at end of file