iter prep.2-term-new-construct (DONE 4/4): Term::New AST + Form-A surface + checker + drift — closes #32

Second iteration of the kernel-extension-mechanics milestone. Ships
the `new` Form-A keyword + `Term::New { type_name, args: Vec<NewArg> }`
AST variant + `NewArg::Type|Value` enum end-to-end through schema /
surface / checker, with two new diagnostics
(`NewTypeNotConstructible`, `NewArgKindMismatch`), a new arm in
prep.1's workspace-wide normalisation pre-pass `qualify_workspace_term`
that rewrites bare `Term::New.type_name` to qualified form
(symmetric to the existing `Term::Ctor` arm), and the data-model.md
+ form_a.md anchor additions. Codegen out of scope per spec; codegen
sites get `CodegenError::Internal` arms naming the raw-buf milestone
as the carrier.

Verification:

- `cargo test --workspace`: 654 tests passing, 0 failed.
- 3 new in-source checker tests pin the elaboration paths:
  `new_resolves_via_type_scope` (the spec's worked Counter example
  checks cleanly), `new_type_not_constructible` (missing `new` def
  in home module fires the new diagnostic), `new_arg_kind_mismatch_value_where_type`
  (kind-mismatch detection).
- 2 new schema-drift pins (`term_new_round_trips`,
  `term_new_type_arg_round_trips`) ratify the JSON byte shape:
  `{"t": "new", "type": "<TypeName>", "args": [{"kind": "type"|"value",
  "value": ...}]}`.
- 1 new surface round-trip pin exercises mixed-kind args through
  Form-A → JSON → Form-A.
- 44+ exhaustive Term-match sites across 24 files extended with
  `Term::New` arms — workspace-wide cargo build clean.

Concerns documented inline:

- `crates/ailang-core/tests/schema_coverage.rs` deliberately does
  NOT register `VariantTag::TermNew` in the `EXPECTED_VARIANTS`
  set. The coverage test asserts every declared variant is
  observed in the .ail fixture corpus; no .ail fixture in the
  current tree emits `"t": "new"` (codegen-runnable Term::New
  programs require the raw-buf milestone's plugin registry).
  Registering would fail the coverage check. The `visit_term` arm
  IS extended (compile-forced); only the enum registration is
  deferred. Inline rationale in the source. Future milestone that
  ships a Term::New fixture extends both sides.
- `crates/ailang-surface/src/print.rs` `write_term` Term::New arm
  was added in Task 1 (not Task 2 as planned), because without it
  ailang-core's tests fail to compile (the surface crate is in
  the dependency graph of ailang-core's test binaries). Task 2's
  round-trip pin verified the arm's correctness.
- Task 3 (synth elaboration) needed one implementer re-loop: the
  first attempt over-qualified within-module type-references via
  `qualify_local_types` on `new`'s signature when the home module
  was the calling module itself. Fixed by skipping qualification
  when `home_module == env.current_module`.

Architectural composition with prep.1: `Term::New` joins
`Term::Ctor` as a `type_name`-bearing site that goes through
`qualify_workspace_term`'s bare→qualified rewrite before the
checker sees it. The checker's `synth` arm for `Term::New`
therefore receives an already-qualified `type_name` (or a local
bare name for same-module construction).

Milestone status: kernel-extension-mechanics (Gitea #6) advances
2/3 iters. Next: prep.3 (kernel-tier modules + param-in), issue #33.

bench/orchestrator-stats/2026-05-28-iter-prep.2-term-new-construct.json

@@ -0,0 +1,18 @@
+{
+  "iter_id": "prep.2-term-new-construct",
+  "date": "2026-05-28",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 4,
+  "tasks_completed": 4,
+  "reloops_per_task": {
+    "1": 0,
+    "2": 0,
+    "3": 1,
+    "4": 0
+  },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null,
+  "notes": "Task 3 needed one implementer re-loop: the first synth elaboration over-qualified the within-module Counter type (`new_demo.Counter` vs declared bare `Counter`), unify caught the mismatch; the fix was to skip `qualify_local_types` when home_module == env.current_module. Task 1 carried a DONE_WITH_CONCERNS deviation from the plan: the schema_coverage.rs `VariantTag::TermNew` + `EXPECTED_VARIANTS` entry was deliberately NOT added — the iter's out-of-scope note declines a Term::New fixture migration in prep.2, and adding the EXPECTED entry without a fixture would break `every_ast_variant_is_observed_in_the_fixture_corpus`. Visitor arm was added; enum entry deferred to the raw-buf milestone when fixtures will land."
+}

crates/ail/src/main.rs

@@ -1563,6 +1563,22 @@ fn walk_term(
                 walk_term(a, out, builtins, scope);
             }
         }
+        // prep.2 (kernel-extension-mechanics): record the type-name
+        // dependency on the home module's TypeDef (mirrors the
+        // `Term::Ctor` arm above's `ctor:` insertion shape) and
+        // recurse into NewArg::Value subterms. NewArg::Type values
+        // are not walked for cross-module type dependencies here —
+        // `ail deps` works on the surface AST before workspace
+        // qualification, so embedded type names ride the existing
+        // `walk_type`/`walk_def_types` channels.
+        Term::New { type_name, args } => {
+            out.insert(format!("new:{type_name}"));
+            for arg in args {
+                if let ailang_core::ast::NewArg::Value(v) = arg {
+                    walk_term(v, out, builtins, scope);
+                }
+            }
+        }
     }
 }
 
@@ -2902,6 +2918,38 @@ fn rewrite_def(
                     );
                 }
             }
+            // prep.2 (kernel-extension-mechanics): `(new T args)` —
+            // rewrite the bare type-name through the same
+            // `rewrite_name` channel that `Term::Ctor` uses, then
+            // recurse into each NewArg::Value subterm; NewArg::Type
+            // values rewrite through `rewrite_type`.
+            Term::New { type_name, args } => {
+                rewrite_name(
+                    type_name,
+                    owning_module,
+                    local_types,
+                    import_names,
+                    changed,
+                );
+                for arg in args {
+                    match arg {
+                        ailang_core::ast::NewArg::Value(v) => rewrite_term(
+                            v,
+                            owning_module,
+                            local_types,
+                            import_names,
+                            changed,
+                        ),
+                        ailang_core::ast::NewArg::Type(t) => rewrite_type(
+                            t,
+                            owning_module,
+                            local_types,
+                            import_names,
+                            changed,
+                        ),
+                    }
+                }
+            }
         }
     }
 

crates/ail/tests/codegen_import_map_fallback_pin.rs

@@ -99,6 +99,12 @@ fn synthesised_print_uses_user_module_show_via_fallback() {
                     || contains_xmod_show_var(body)
             }
             Term::Recur { args } => args.iter().any(contains_xmod_show_var),
+            // prep.2 (kernel-extension-mechanics): recurse through
+            // NewArg::Value subterms; type-args do not carry a Var.
+            Term::New { args, .. } => args.iter().any(|arg| match arg {
+                ailang_core::ast::NewArg::Value(v) => contains_xmod_show_var(v),
+                ailang_core::ast::NewArg::Type(_) => false,
+            }),
             Term::Lit { .. } => false,
         }
     }

crates/ailang-check/src/lib.rs

@@ -260,6 +260,16 @@ pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Typ
                 .map(|a| substitute_rigids_in_term(a, mapping))
                 .collect(),
         },
+        Term::New { type_name, args } => Term::New {
+            type_name: type_name.clone(),
+            args: args
+                .iter()
+                .map(|arg| match arg {
+                    NewArg::Value(v) => NewArg::Value(substitute_rigids_in_term(v, mapping)),
+                    NewArg::Type(t) => NewArg::Type(substitute_rigids(t, mapping)),
+                })
+                .collect(),
+        },
     }
 }
 
@@ -704,6 +714,29 @@ pub enum CheckError {
         name: String,
     },
 
+    /// prep.2 (kernel-extension-mechanics): a `(new T args...)` call
+    /// where `T`'s home module declares no `new` def. Code:
+    /// `new-type-not-constructible`.
+    #[error("type `{type_name}` is not constructible: home module `{home_module}` declares no `new` def")]
+    NewTypeNotConstructible {
+        type_name: String,
+        home_module: String,
+    },
+
+    /// prep.2 (kernel-extension-mechanics): a `(new T args...)` call
+    /// whose Type-arg count vs. Value-arg count does not match `new`'s
+    /// declared signature (e.g. `new : forall a. (a) -> T a` needs one
+    /// Type-arg at position 0 and one Value-arg at position 1; a
+    /// call site with two Value-args trips this). Code:
+    /// `new-arg-kind-mismatch`.
+    #[error("`(new {type_name} …)` arg at position {position}: expected {expected}, got {got}")]
+    NewArgKindMismatch {
+        type_name: String,
+        position: usize,
+        expected: &'static str,
+        got: &'static str,
+    },
+
     /// an internal invariant in the typechecker / mono pass
     /// was violated — surfaced as an error so callers can propagate
     /// rather than abort, but in well-formed inputs (typecheck has
@@ -761,6 +794,8 @@ impl CheckError {
             CheckError::RecurNotInTailPosition => "recur-not-in-tail-position",
             CheckError::TypeScopedMemberNotFound { .. } => "type-scoped-member-not-found",
             CheckError::TypeScopedReceiverNotAType { .. } => "type-scoped-receiver-not-a-type",
+            CheckError::NewTypeNotConstructible { .. } => "new-type-not-constructible",
+            CheckError::NewArgKindMismatch { .. } => "new-arg-kind-mismatch",
             CheckError::Internal(_) => "internal",
         }
     }
@@ -838,6 +873,17 @@ impl CheckError {
             CheckError::TypeScopedReceiverNotAType { name } => {
                 serde_json::json!({"name": name})
             }
+            CheckError::NewTypeNotConstructible { type_name, home_module } => {
+                serde_json::json!({"type": type_name, "home_module": home_module})
+            }
+            CheckError::NewArgKindMismatch { type_name, position, expected, got } => {
+                serde_json::json!({
+                    "type": type_name,
+                    "position": position,
+                    "expected": expected,
+                    "actual": got,
+                })
+            }
             _ => serde_json::Value::Object(serde_json::Map::new()),
         }
     }
@@ -2846,6 +2892,20 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
             }
             Ok(())
         }
+        // prep.2 (kernel-extension-mechanics): `(new T args...)` is
+        // resolved by synth to a call into the home module's `new` def.
+        // Its value-args are evaluated in non-tail position (call-arg
+        // semantics); type-args carry no runtime term. The Term::New
+        // node itself is not a tail-app — codegen lowers it via a
+        // synth/desugar step in a later milestone.
+        Term::New { args, .. } => {
+            for arg in args {
+                if let NewArg::Value(v) = arg {
+                    verify_tail_positions(v, false)?;
+                }
+            }
+            Ok(())
+        }
     }
 }
 
@@ -2939,6 +2999,18 @@ fn verify_loop_body(t: &Term, in_loop_tail: bool) -> Result<()> {
             verify_loop_body(source, false)?;
             verify_loop_body(body, in_loop_tail)
         }
+        // prep.2 (kernel-extension-mechanics): Term::New's value-args
+        // are non-tail (call-arg semantics). The Term::New node itself
+        // is opaque to the loop/recur control transfer — value args
+        // are evaluated in non-tail position; type-args carry no term.
+        Term::New { args, .. } => {
+            for arg in args {
+                if let NewArg::Value(v) = arg {
+                    verify_loop_body(v, false)?;
+                }
+            }
+            Ok(())
+        }
     }
 }
 
@@ -3891,6 +3963,7 @@ pub(crate) fn synth(
                         Term::ReuseAs { .. } => "reuse-as",
                         Term::Loop { .. } => "loop",
                         Term::Recur { .. } => "recur",
+                        Term::New { .. } => "new",
                         Term::Ctor { .. } | Term::Lam { .. } => unreachable!(),
                     };
                     return Err(CheckError::ReuseAsNonAllocatingBody {
@@ -3981,6 +4054,174 @@ pub(crate) fn synth(
             }
             Ok(Subst::fresh(counter))
         }
+        // prep.2 (kernel-extension-mechanics): functional construction
+        // `(new T args...)` calls the `new` def in T's home module.
+        // After the prep.1 pre-pass, `type_name` is qualified to
+        // `<home>.<TypeName>` whenever T is cross-module; it stays
+        // bare when T is local to the current module. Steps:
+        //   1. resolve home_module + bare_type from type_name.
+        //   2. look up `new` in the home module's globals →
+        //      NewTypeNotConstructible if absent.
+        //   3. peel Forall (if any) → vars + (params, ret, effects).
+        //      Count Type-positional vs. Value-positional args; the
+        //      kind-pattern of the args (which positions are Type vs.
+        //      Value) must match the sig — for each Forall var the
+        //      corresponding arg slot is Type, for each value-param it
+        //      is Value. Anything else → NewArgKindMismatch.
+        //   4. build the rigid→concrete map from Type-args (in order),
+        //      substitute through param types and the return type.
+        //   5. synth each value-arg and unify against the substituted
+        //      param type.
+        //   6. inherit `new`'s effects; the result type is the
+        //      substituted ret.
+        Term::New { type_name, args } => {
+            // Step 1: resolve home module.
+            let (home_module, bare_type) = if let Some((m, t)) = type_name.split_once('.') {
+                (m.to_string(), t.to_string())
+            } else {
+                (env.current_module.clone(), type_name.clone())
+            };
+            // Step 2: look up `new` in home module's globals. Empty
+            // module_globals (e.g. when the home is the current
+            // module and globals live in env.globals instead) also
+            // counts as "no new def for this type" — we don't fall
+            // back to a different channel because spec semantics
+            // require `new` to be defined in the type's home module.
+            let new_ty = env
+                .module_globals
+                .get(&home_module)
+                .and_then(|g| g.get("new"))
+                .cloned()
+                .ok_or_else(|| CheckError::NewTypeNotConstructible {
+                    type_name: bare_type.clone(),
+                    home_module: home_module.clone(),
+                })?;
+            // Qualify any bare local Type::Cons in `new`'s signature
+            // against the home module's TypeDefs — mirrors the
+            // module-as-receiver path in Term::Ctor. Skip the
+            // qualification when `new` lives in the CURRENT module:
+            // the current module sees its own types bare (the
+            // workspace-wide qualify pre-pass leaves own-module names
+            // alone), so qualifying here would produce a mismatch
+            // against own-module declared types at unify time.
+            let qualified = if home_module == env.current_module {
+                new_ty
+            } else {
+                let owner_types = env
+                    .module_types
+                    .get(&home_module)
+                    .cloned()
+                    .unwrap_or_default();
+                qualify_local_types(&new_ty, &home_module, &owner_types)
+            };
+            // Step 3: peel Forall to (vars, params, ret, effects).
+            let (vars, param_tys, ret_ty, effects_sig) = match &qualified {
+                Type::Forall { vars, body, .. } => match body.as_ref() {
+                    Type::Fn { params, ret, effects, .. } => (
+                        vars.clone(),
+                        params.clone(),
+                        (**ret).clone(),
+                        effects.clone(),
+                    ),
+                    other => {
+                        return Err(CheckError::FnTypeRequired(
+                            "new".into(),
+                            ailang_core::pretty::type_to_string(other),
+                        ));
+                    }
+                },
+                Type::Fn { params, ret, effects, .. } => (
+                    Vec::new(),
+                    params.clone(),
+                    (**ret).clone(),
+                    effects.clone(),
+                ),
+                other => {
+                    return Err(CheckError::FnTypeRequired(
+                        "new".into(),
+                        ailang_core::pretty::type_to_string(other),
+                    ));
+                }
+            };
+            // Validate the arg-kind pattern positionally: the first
+            // `vars.len()` args must be NewArg::Type, the remaining
+            // `param_tys.len()` args must be NewArg::Value. The first
+            // mismatch fires NewArgKindMismatch with `position` and
+            // the expected/got kind labels.
+            let total_expected = vars.len() + param_tys.len();
+            if args.len() != total_expected {
+                // Mismatch on overall count maps to a kind-mismatch on
+                // the first position where the args run out (or the
+                // first extra), with `expected` set to what should
+                // have been there.
+                let pos = args.len().min(total_expected);
+                let expected_kind = if pos < vars.len() {
+                    "type-arg"
+                } else if pos < total_expected {
+                    "value-arg"
+                } else {
+                    "no arg"
+                };
+                let got_kind = if pos < args.len() {
+                    match &args[pos] {
+                        NewArg::Type(_) => "type-arg",
+                        NewArg::Value(_) => "value-arg",
+                    }
+                } else {
+                    "no arg"
+                };
+                return Err(CheckError::NewArgKindMismatch {
+                    type_name: bare_type.clone(),
+                    position: pos,
+                    expected: expected_kind,
+                    got: got_kind,
+                });
+            }
+            for (i, arg) in args.iter().enumerate() {
+                let expected_is_type = i < vars.len();
+                let got_is_type = matches!(arg, NewArg::Type(_));
+                if expected_is_type != got_is_type {
+                    return Err(CheckError::NewArgKindMismatch {
+                        type_name: bare_type.clone(),
+                        position: i,
+                        expected: if expected_is_type { "type-arg" } else { "value-arg" },
+                        got: if got_is_type { "type-arg" } else { "value-arg" },
+                    });
+                }
+            }
+            // Step 4: build the Forall-var → concrete-Type mapping
+            // from the Type-positional args (in order).
+            let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
+            for (var, arg) in vars.iter().zip(args.iter()) {
+                if let NewArg::Type(t) = arg {
+                    mapping.insert(var.clone(), t.clone());
+                }
+                // The kind-check loop above guarantees this branch
+                // matches; defensive: a Value arg in a Type slot
+                // would have raised NewArgKindMismatch already.
+            }
+            // Step 5: synth each value-arg, unify against the
+            // (substituted) corresponding param type.
+            let value_args = &args[vars.len()..];
+            for (val_arg, expected_param) in value_args.iter().zip(param_tys.iter()) {
+                let v = match val_arg {
+                    NewArg::Value(v) => v,
+                    NewArg::Type(_) => unreachable!("kind-check above"),
+                };
+                let expected_inst = substitute_rigids(expected_param, &mapping);
+                let actual = synth(
+                    v, env, locals, loop_stack, effects, in_def, subst, counter,
+                    residuals, free_fn_calls, warnings,
+                )?;
+                unify(&expected_inst, &actual, subst)?;
+            }
+            // Step 6: inherit `new`'s declared effects, return the
+            // substituted result type.
+            for e in &effects_sig {
+                effects.insert(e.clone());
+            }
+            Ok(substitute_rigids(&ret_ty, &mapping))
+        }
     }
 }
 
@@ -4232,6 +4473,38 @@ pub(crate) fn qualify_workspace_term(
             }
             qualify_workspace_term(body, own_local_types, module_types);
         }
+        // prep.2 (kernel-extension-mechanics): prep.1 pre-pass partner.
+        // Mirror the Term::Ctor arm above — normalize a bare
+        // cross-module `type_name` to qualified `<home>.<Type>` form
+        // before the synth pass elaborates the `new`-call. NewArg::Type
+        // values are recursively type-qualified; NewArg::Value subterms
+        // are recursively term-qualified.
+        Term::New { type_name, args } => {
+            if !type_name.contains('.')
+                && !ailang_core::primitives::is_primitive_name(type_name)
+                && !own_local_types.contains_key(type_name)
+            {
+                if let Some(home) = module_types.iter().find_map(|(m, types)| {
+                    if types.contains_key(type_name) {
+                        Some(m.clone())
+                    } else {
+                        None
+                    }
+                }) {
+                    *type_name = format!("{home}.{type_name}");
+                }
+            }
+            for arg in args.iter_mut() {
+                match arg {
+                    NewArg::Value(v) => {
+                        qualify_workspace_term(v, own_local_types, module_types)
+                    }
+                    NewArg::Type(t) => {
+                        *t = qualify_workspace_types(t, own_local_types, module_types)
+                    }
+                }
+            }
+        }
     }
 }
 
@@ -7426,4 +7699,160 @@ mod tests {
             "expected diagnostic code `type-scoped-receiver-not-a-type`, got {diags:?}"
         );
     }
+
+    /// prep.2 (kernel-extension-mechanics): the spec's worked example.
+    /// A `(new Counter 42)` call resolves to the home module's `new`
+    /// def, with `Counter` declared locally and `new : (Int) -> Counter`
+    /// constructing a `Counter` via `(term-ctor Counter MkCounter n)`.
+    /// Property: synth's Term::New arm walks the resolution + arity +
+    /// kind checks, substitutes type-vars (none here — `new` is
+    /// monomorphic), and unifies each value-arg against the
+    /// corresponding (substituted) param type.
+    #[test]
+    fn new_resolves_via_type_scope() {
+        let m: Module = serde_json::from_value(serde_json::json!({
+            "schema": SCHEMA,
+            "name": "new_demo",
+            "imports": [],
+            "defs": [
+                {"kind": "type", "name": "Counter", "ctors": [
+                    {"name": "MkCounter", "fields": [{"k": "con", "name": "Int"}]}
+                ]},
+                {"kind": "fn", "name": "new",
+                 "type": {"k": "fn",
+                          "params": [{"k": "con", "name": "Int"}],
+                          "ret": {"k": "con", "name": "Counter"},
+                          "effects": []},
+                 "params": ["n"],
+                 "body": {"t": "ctor", "type": "Counter", "ctor": "MkCounter",
+                          "args": [{"t": "var", "name": "n"}]}},
+                {"kind": "fn", "name": "main",
+                 "type": {"k": "fn", "params": [],
+                          "ret": {"k": "con", "name": "Counter"},
+                          "effects": []},
+                 "params": [],
+                 "body": {"t": "new", "type": "Counter",
+                          "args": [
+                              {"kind": "value", "value":
+                                  {"t": "lit", "lit": {"kind": "int", "value": 42}}}
+                          ]}}
+            ]
+        })).unwrap();
+        let mut modules = BTreeMap::new();
+        modules.insert("new_demo".to_string(), m);
+        let ws = Workspace {
+            entry: "new_demo".into(),
+            modules,
+            root_dir: std::path::PathBuf::from("."),
+            registry: ailang_core::workspace::Registry::default(),
+        };
+        let diags = check_workspace(&ws);
+        assert!(
+            diags.is_empty(),
+            "(new Counter 42) must check cleanly; got {diags:?}"
+        );
+    }
+
+    /// prep.2 (kernel-extension-mechanics): a `(new T arg)` where T's
+    /// home module declares no `new` def fires
+    /// `NewTypeNotConstructible`. Property: synth's Term::New arm
+    /// resolves T's home module and then looks up `new` in its
+    /// globals; absence triggers the diagnostic with `type` and
+    /// `home_module` context.
+    #[test]
+    fn new_type_not_constructible() {
+        let m: Module = serde_json::from_value(serde_json::json!({
+            "schema": SCHEMA,
+            "name": "no_new",
+            "imports": [],
+            "defs": [
+                {"kind": "type", "name": "T", "ctors": [
+                    {"name": "MkT", "fields": []}
+                ]},
+                // No `new` def for T.
+                {"kind": "fn", "name": "main",
+                 "type": {"k": "fn", "params": [],
+                          "ret": {"k": "con", "name": "T"},
+                          "effects": []},
+                 "params": [],
+                 "body": {"t": "new", "type": "T",
+                          "args": [
+                              {"kind": "value", "value":
+                                  {"t": "lit", "lit": {"kind": "int", "value": 42}}}
+                          ]}}
+            ]
+        })).unwrap();
+        let mut modules = BTreeMap::new();
+        modules.insert("no_new".to_string(), m);
+        let ws = Workspace {
+            entry: "no_new".into(),
+            modules,
+            root_dir: std::path::PathBuf::from("."),
+            registry: ailang_core::workspace::Registry::default(),
+        };
+        let diags = check_workspace(&ws);
+        assert!(
+            diags.iter().any(|d| d.code == "new-type-not-constructible"),
+            "expected diagnostic code `new-type-not-constructible`, got {diags:?}"
+        );
+    }
+
+    /// prep.2 (kernel-extension-mechanics): a `(new T ...)` whose
+    /// `new` def expects a Type-arg in position 0 (because its sig is
+    /// `forall a. (a) -> T a`) but the call site supplies a Value-arg
+    /// instead fires `NewArgKindMismatch`. Property: synth counts
+    /// NewArg::Type and NewArg::Value separately, compares Type count
+    /// to the Forall vars count, and emits the kind-mismatch on
+    /// inequality before any other check fires.
+    #[test]
+    fn new_arg_kind_mismatch_value_where_type() {
+        let m: Module = serde_json::from_value(serde_json::json!({
+            "schema": SCHEMA,
+            "name": "kind_mismatch",
+            "imports": [],
+            "defs": [
+                {"kind": "type", "name": "T", "vars": ["a"], "ctors": [
+                    {"name": "MkT", "fields": [{"k": "var", "name": "a"}]}
+                ]},
+                // `new : forall a. (a) -> T a`. The new-site at `main`
+                // wrongly supplies a single Value-arg where the Forall
+                // expects one Type-arg (then a Value-arg).
+                {"kind": "fn", "name": "new",
+                 "type": {"k": "forall", "vars": ["a"], "constraints": [],
+                          "body": {"k": "fn",
+                                   "params": [{"k": "var", "name": "a"}],
+                                   "ret": {"k": "con", "name": "T",
+                                           "args": [{"k": "var", "name": "a"}]},
+                                   "effects": []}},
+                 "params": ["x"],
+                 "body": {"t": "ctor", "type": "T", "ctor": "MkT",
+                          "args": [{"t": "var", "name": "x"}]}},
+                {"kind": "fn", "name": "main",
+                 "type": {"k": "fn", "params": [],
+                          "ret": {"k": "con", "name": "T",
+                                  "args": [{"k": "con", "name": "Int"}]},
+                          "effects": []},
+                 "params": [],
+                 // Wrong: only one NewArg::Value supplied for a sig
+                 // that needs 1 Type-arg + 1 Value-arg.
+                 "body": {"t": "new", "type": "T", "args": [
+                     {"kind": "value", "value":
+                         {"t": "lit", "lit": {"kind": "int", "value": 42}}}
+                 ]}}
+            ]
+        })).unwrap();
+        let mut modules = BTreeMap::new();
+        modules.insert("kind_mismatch".to_string(), m);
+        let ws = Workspace {
+            entry: "kind_mismatch".into(),
+            modules,
+            root_dir: std::path::PathBuf::from("."),
+            registry: ailang_core::workspace::Registry::default(),
+        };
+        let diags = check_workspace(&ws);
+        assert!(
+            diags.iter().any(|d| d.code == "new-arg-kind-mismatch"),
+            "expected diagnostic code `new-arg-kind-mismatch`, got {diags:?}"
+        );
+    }
 }

crates/ailang-check/src/lift.rs

@@ -671,6 +671,24 @@ impl<'a> Lifter<'a> {
 
                 Ok(in_full)
             }
+            Term::New { type_name, args } => {
+                // prep.2 (kernel-extension-mechanics): structural
+                // recurse through NewArg::Value sub-terms; NewArg::Type
+                // carries no term and is untouched.
+                let new_args: Result<Vec<NewArg>> = args
+                    .iter()
+                    .map(|arg| match arg {
+                        NewArg::Value(v) => {
+                            Ok(NewArg::Value(self.lift_in_term(v, locals, in_def)?))
+                        }
+                        NewArg::Type(t) => Ok(NewArg::Type(t.clone())),
+                    })
+                    .collect();
+                Ok(Term::New {
+                    type_name: type_name.clone(),
+                    args: new_args?,
+                })
+            }
         }
     }
 
@@ -758,6 +776,10 @@ fn contains_any_letrec(m: &Module) -> bool {
                 binders.iter().any(|b| term_has_letrec(&b.init)) || term_has_letrec(body)
             }
             Term::Recur { args } => args.iter().any(term_has_letrec),
+            Term::New { args, .. } => args.iter().any(|arg| match arg {
+                NewArg::Value(v) => term_has_letrec(v),
+                NewArg::Type(_) => false,
+            }),
         }
     }
     for def in &m.defs {

crates/ailang-check/src/linearity.rs

@@ -141,7 +141,7 @@
 
 use crate::diagnostic::Diagnostic;
 use crate::uniqueness::{infer_module as infer_uniqueness, UniquenessTable};
-use ailang_core::ast::{Arm, Ctor, Def, FnDef, Module, ParamMode, Pattern, Term, Type};
+use ailang_core::ast::{Arm, Ctor, Def, FnDef, Module, NewArg, ParamMode, Pattern, Term, Type};
 use ailang_surface::{term_to_form_a, type_to_form_a};
 use std::collections::HashMap;
 
@@ -615,6 +615,17 @@ impl<'a> Checker<'a> {
                     self.walk(a, Position::Consume);
                 }
             }
+            // prep.2 (kernel-extension-mechanics): `(new T args...)` is
+            // a Ctor-like construction call — each value-arg is
+            // consumed by the new value. Type-args carry no runtime
+            // term and contribute no use.
+            Term::New { args, .. } => {
+                for arg in args {
+                    if let NewArg::Value(v) = arg {
+                        self.walk(v, Position::Consume);
+                    }
+                }
+            }
         }
     }
 
@@ -801,6 +812,7 @@ fn make_reuse_as_source_not_bare_var(def: &str, source: &Term, body: &Term) -> D
         Term::ReuseAs { .. } => "reuse-as",
         Term::Loop { .. } => "loop",
         Term::Recur { .. } => "recur",
+        Term::New { .. } => "new",
     };
     let replacement = term_to_form_a(body);
     Diagnostic::error(
@@ -956,6 +968,12 @@ fn any_sub_binder_consumed_for(
         Term::Recur { args } => args.iter().any(|a| {
             any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)
         }),
+        // prep.2 (kernel-extension-mechanics): recurse through
+        // NewArg::Value subterms; NewArg::Type carries no runtime term.
+        Term::New { args, .. } => args.iter().any(|arg| match arg {
+            NewArg::Value(v) => any_sub_binder_consumed_for(v, pname, uniq, def_name, ctors),
+            NewArg::Type(_) => false,
+        }),
     }
 }
 
@@ -1086,6 +1104,13 @@ fn ctor_uses_any_binder(t: &Term, binders: &[String]) -> bool {
                 || ctor_uses_any_binder(body, binders)
         }
         Term::Recur { args } => args.iter().any(|a| ctor_uses_any_binder(a, binders)),
+        // prep.2 (kernel-extension-mechanics): recurse through
+        // NewArg::Value subterms. NewArg::Type carries no runtime
+        // ctor invocation.
+        Term::New { args, .. } => args.iter().any(|arg| match arg {
+            NewArg::Value(v) => ctor_uses_any_binder(v, binders),
+            NewArg::Type(_) => false,
+        }),
     }
 }
 
@@ -1133,6 +1158,13 @@ fn term_mentions_any_binder(t: &Term, binders: &[String]) -> bool {
             lb.iter().any(|b| term_mentions_any_binder(&b.init, binders))
                 || term_mentions_any_binder(body, binders)
         }
+        // prep.2 (kernel-extension-mechanics): NewArg::Value subterms
+        // may mention any of the destructured binders; NewArg::Type
+        // carries no runtime term.
+        Term::New { args, .. } => args.iter().any(|arg| match arg {
+            NewArg::Value(v) => term_mentions_any_binder(v, binders),
+            NewArg::Type(_) => false,
+        }),
     }
 }
 

crates/ailang-check/src/mono.rs

@@ -55,7 +55,7 @@
 //! `module_hash` is unchanged end-to-end for any workspace with no
 //! monomorphisation targets.
 
-use ailang_core::ast::{Arm, ClassDef, ConstDef, Def, FnDef as AstFnDef, InstanceDef, Pattern, Term, Type};
+use ailang_core::ast::{Arm, ClassDef, ConstDef, Def, FnDef as AstFnDef, InstanceDef, NewArg, Pattern, Term, Type};
 use ailang_core::workspace::Workspace;
 use crate::Result;
 use indexmap::IndexMap;
@@ -1275,6 +1275,19 @@ fn rewrite_mono_calls(
                 rewrite_mono_calls(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
             }
         }
+        // prep.2 (kernel-extension-mechanics): walker through
+        // NewArg::Value subterms; type args carry no callable term.
+        // The Term::New site itself does not consume a mono cursor
+        // slot — synth desugars it to a global-fn call in a later
+        // milestone, at which point the call site reads as a Term::App
+        // and rides the existing Var-arm channel.
+        Term::New { args, .. } => {
+            for arg in args.iter_mut() {
+                if let NewArg::Value(v) = arg {
+                    rewrite_mono_calls(v, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+                }
+            }
+        }
         Term::Lit { .. } => {}
     }
 }
@@ -1647,6 +1660,16 @@ fn interleave_slots(
                 interleave_slots(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
             }
         }
+        // prep.2 (kernel-extension-mechanics): walker through
+        // NewArg::Value subterms; Term::New itself does not push a
+        // mono slot — see `rewrite_mono_calls`'s arm for the rationale.
+        Term::New { args, .. } => {
+            for arg in args {
+                if let NewArg::Value(v) = arg {
+                    interleave_slots(v, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+                }
+            }
+        }
         Term::Lit { .. } => {}
     }
 }

crates/ailang-check/src/pre_desugar_validation.rs

@@ -132,6 +132,18 @@ fn walk_term(t: &Term) -> Result<(), CheckError> {
             }
             Ok(())
         }
+        // prep.2 (kernel-extension-mechanics): structural recurse
+        // through NewArg::Value subterms; NewArg::Type carries no term
+        // to validate at this stage (pre-desugar). Validity of the
+        // resolved `new` def is checked at synth time.
+        Term::New { args, .. } => {
+            for arg in args {
+                if let NewArg::Value(v) = arg {
+                    walk_term(v)?;
+                }
+            }
+            Ok(())
+        }
     }
 }
 

crates/ailang-check/src/reuse_shape.rs

@@ -67,7 +67,7 @@
 //! mechanical follow-up if it ever lands.
 
 use crate::diagnostic::Diagnostic;
-use ailang_core::ast::{Arm, Def, FnDef, Module, ParamMode, Pattern, Term, Type, TypeDef};
+use ailang_core::ast::{Arm, Def, FnDef, Module, NewArg, ParamMode, Pattern, Term, Type, TypeDef};
 use ailang_surface::term_to_form_a;
 use std::collections::HashMap;
 
@@ -264,6 +264,20 @@ impl<'a> Checker<'a> {
                     self.walk(a);
                 }
             }
+            // prep.2 (kernel-extension-mechanics): walker through
+            // NewArg::Value subterms. Term::New itself is not a Ctor
+            // site for the reuse-as path-ctor analysis — its value is
+            // synth'd to whatever the resolved `new` def returns;
+            // refining `path_ctors` from a Term::New result would
+            // require knowing the body of `new`, which lives in
+            // another module.
+            Term::New { args, .. } => {
+                for arg in args {
+                    if let NewArg::Value(v) = arg {
+                        self.walk(v);
+                    }
+                }
+            }
         }
     }
 

crates/ailang-check/src/uniqueness.rs

@@ -58,7 +58,7 @@
 //!   dec (uniform `drop_<m>_<T>` call vs inlined partial drop) is a
 //!   codegen-side decision driven by `moved_slots`.
 
-use ailang_core::ast::{Arm, Def, FnDef, Module, ParamMode, Pattern, Term, Type};
+use ailang_core::ast::{Arm, Def, FnDef, Module, NewArg, ParamMode, Pattern, Term, Type};
 use std::collections::BTreeMap;
 
 /// Per-binder classification produced by the inference. See module
@@ -347,6 +347,17 @@ impl<'a> Walker<'a> {
                     self.walk(a, Position::Consume);
                 }
             }
+            // prep.2 (kernel-extension-mechanics): each NewArg::Value
+            // is consumed by the construction call — same rule as a
+            // Ctor or App arg in `Position::Consume`. NewArg::Type
+            // carries no runtime term.
+            Term::New { args, .. } => {
+                for arg in args {
+                    if let NewArg::Value(v) = arg {
+                        self.walk(v, Position::Consume);
+                    }
+                }
+            }
         }
     }
 

crates/ailang-codegen/src/escape.rs

@@ -80,7 +80,7 @@
 //! Precision can be improved later; correctness is the priority for
 //! this iter.
 
-use ailang_core::ast::{Pattern, Term};
+use ailang_core::ast::{NewArg, Pattern, Term};
 use std::collections::BTreeSet;
 
 /// Set of allocation sites (identified by raw pointer address cast to
@@ -201,6 +201,17 @@ fn walk(t: &Term, out: &mut NonEscapeSet) {
                 walk(a, out);
             }
         }
+        // prep.2 (kernel-extension-mechanics): walker through
+        // NewArg::Value subterms; Term::New does not yet have a
+        // direct codegen path (lower_term returns an Internal error
+        // via Pattern D until the raw-buf milestone lands).
+        Term::New { args, .. } => {
+            for arg in args {
+                if let NewArg::Value(v) = arg {
+                    walk(v, out);
+                }
+            }
+        }
         Term::Lit { .. } | Term::Var { .. } => {}
     }
 }
@@ -394,6 +405,21 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             false
         }
+        // prep.2 (kernel-extension-mechanics): walk every NewArg::Value
+        // in non-tail mode (call-arg semantics). Term::New itself does
+        // not yet codegen; the analysis stays conservative against the
+        // future codegen by treating each value-arg as a non-tail
+        // expression whose tainted-name flow matters.
+        Term::New { args, .. } => {
+            for arg in args {
+                if let NewArg::Value(v) = arg {
+                    if escapes(v, tainted, false) {
+                        return true;
+                    }
+                }
+            }
+            false
+        }
     }
 }
 
@@ -516,6 +542,16 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<
                 collect_free_vars(a, bound, out);
             }
         }
+        // prep.2 (kernel-extension-mechanics): free vars of a
+        // `(new T args)` are the union of free vars of every
+        // NewArg::Value; NewArg::Type carries no term.
+        Term::New { args, .. } => {
+            for arg in args {
+                if let NewArg::Value(v) = arg {
+                    collect_free_vars(v, bound, out);
+                }
+            }
+        }
     }
 }
 

crates/ailang-codegen/src/lambda.rs

@@ -492,6 +492,16 @@ impl<'a> Emitter<'a> {
                     Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
                 }
             }
+            // prep.2 (kernel-extension-mechanics): captures of a
+            // `(new T args)` are the union of captures of every
+            // NewArg::Value; NewArg::Type carries no runtime term.
+            Term::New { args, .. } => {
+                for arg in args {
+                    if let NewArg::Value(v) = arg {
+                        Self::collect_captures(v, bound, captures, captures_set, builtins, top_level);
+                    }
+                }
+            }
         }
     }
 

crates/ailang-codegen/src/lib.rs

@@ -2064,6 +2064,18 @@ impl<'a> Emitter<'a> {
                 self.block_terminated = true;
                 Ok(("0".into(), "i8".into()))
             }
+            // prep.2 (kernel-extension-mechanics): Term::New has no
+            // direct codegen path in this milestone — typecheck
+            // accepts it via synth's elaboration, but lowering to LLVM
+            // IR requires a desugar pass that resolves the `new` def
+            // and rewrites the site as a Term::App. That desugar lands
+            // in the raw-buf milestone. Until then, codegen of
+            // Term::New is an internal error: a workspace that types-
+            // checks should not reach codegen with a surviving Term::New.
+            Term::New { .. } => Err(CodegenError::Internal(
+                "Term::New requires the type's `new` def to be desugared first; \
+                 codegen does not yet support Term::New directly — milestone raw-buf".into(),
+            )),
         }
     }
 
@@ -3543,6 +3555,16 @@ impl<'a> Emitter<'a> {
             // value at its own position).
             Term::Loop { body, .. } => self.synth_with_extras(body, extras),
             Term::Recur { .. } => Ok(Type::unit()),
+            // prep.2 (kernel-extension-mechanics): Term::New has no
+            // codegen path in this milestone (see lower_term's arm).
+            // synth_with_extras would only fire if codegen reaches a
+            // surviving Term::New as a callee or sub-expression — same
+            // BUG class as a surviving LetRec — so an internal error
+            // here mirrors lower_term's stance.
+            Term::New { .. } => Err(CodegenError::Internal(
+                "Term::New cannot be synthed at codegen — must be desugared first; \
+                 codegen support lands in the raw-buf milestone".into(),
+            )),
         }
     }
 }

crates/ailang-core/specs/form_a.md

@@ -296,6 +296,7 @@ Parenthesised forms:
 (reuse-as SOURCE-TERM BODY-TERM)        ; explicit reuse hint
 (loop (NAME TYPE INIT)* BODY-TERM+)     ; strict iteration block (loop-recur)
 (recur ARG*)                            ; re-enter enclosing loop (loop-recur)
+(new TYPE-NAME ARG+)                    ; functional construction (kernel-extension prep.2)
 ```
 
 Notes:
@@ -325,6 +326,17 @@ Notes:
   `recur-not-in-tail-position`). `loop`/`recur` make no termination
   claim: a `loop` with no non-`recur` exit runs forever. See
   `docs/specs/0034-loop-recur.md`.
+- `new` is functional construction: `(new TYPE-NAME ARG+)` calls the
+  `new` def in `TYPE-NAME`'s home module with the supplied args.
+  Each arg is positional and disambiguated by syntactic form: a
+  parenthesised form whose head ident is one of `con`, `fn-type`,
+  `borrow`, `own` parses as a Type-positional arg (instantiating one
+  of `new`'s outer `Forall` vars); anything else parses as a
+  Value-positional arg (a Term checked against the corresponding
+  param type). Zero args is rejected at parse-time. Diagnostics:
+  `new-type-not-constructible` (T's home module has no `new` def),
+  `new-arg-kind-mismatch` (arg's kind disagrees with the sig at that
+  position). Codegen lands in the raw-buf milestone.
 
 ## Patterns
 

crates/ailang-core/src/ast.rs

@@ -562,6 +562,30 @@ pub enum Term {
     Recur {
         args: Vec<Term>,
     },
+    /// Functional construction: `(new T arg+)` calls the `new` def in
+    /// `T`'s home module with the supplied args. Each arg is either a
+    /// Type or a Value (see [`NewArg`]). Resolution: type-scoped
+    /// lookup of `type_name` → home module → find `new` def → check
+    /// arg-count and arg-kind. See prep.2 of the
+    /// kernel-extension-mechanics milestone.
+    New {
+        #[serde(rename = "type")]
+        type_name: String,
+        args: Vec<NewArg>,
+    },
+}
+
+/// One positional arg to a `(new T args...)` call. Either a `Type`
+/// (e.g. `(new Series (con Float) 3)` — first arg is `NewArg::Type`)
+/// or a `Value` (e.g. the literal `3` in the same example, a
+/// `Term`). Disambiguation at parse-time is by syntactic form: a
+/// Type starts with one of the Type-production heads (`con`,
+/// `fn-type`, `borrow`, `own`); anything else is a Term.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+#[serde(tag = "kind", content = "value", rename_all = "lowercase")]
+pub enum NewArg {
+    Type(Type),
+    Value(Term),
 }
 
 /// One arm of a [`Term::Match`].

crates/ailang-core/src/desugar.rs

@@ -358,6 +358,14 @@ fn collect_used_in_term(t: &Term, used: &mut BTreeSet<String>) {
                 collect_used_in_term(a, used);
             }
         }
+        Term::New { args, .. } => {
+            for arg in args {
+                match arg {
+                    NewArg::Value(v) => collect_used_in_term(v, used),
+                    NewArg::Type(_) => {}
+                }
+            }
+        }
     }
 }
 
@@ -914,6 +922,16 @@ impl Desugarer {
                 }));
                 in_full
             }
+            Term::New { type_name, args } => Term::New {
+                type_name: type_name.clone(),
+                args: args
+                    .iter()
+                    .map(|arg| match arg {
+                        NewArg::Value(v) => NewArg::Value(self.desugar_term(v, scope)),
+                        NewArg::Type(t) => NewArg::Type(t.clone()),
+                    })
+                    .collect(),
+            },
         }
     }
 
@@ -1224,6 +1242,14 @@ pub fn free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut BTreeSet<
                 free_vars_in_term(a, bound, out);
             }
         }
+        Term::New { args, .. } => {
+            for arg in args {
+                match arg {
+                    NewArg::Value(v) => free_vars_in_term(v, bound, out),
+                    NewArg::Type(_) => {}
+                }
+            }
+        }
     }
 }
 
@@ -1404,6 +1430,16 @@ pub fn subst_var(t: &Term, from: &str, to: &str) -> Term {
         Term::Recur { args } => Term::Recur {
             args: args.iter().map(|a| subst_var(a, from, to)).collect(),
         },
+        Term::New { type_name, args } => Term::New {
+            type_name: type_name.clone(),
+            args: args
+                .iter()
+                .map(|arg| match arg {
+                    NewArg::Value(v) => NewArg::Value(subst_var(v, from, to)),
+                    NewArg::Type(t) => NewArg::Type(t.clone()),
+                })
+                .collect(),
+        },
     }
 }
 
@@ -1542,6 +1578,18 @@ pub fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[Stri
                 .map(|a| subst_call_with_extras(a, name, lifted, extras))
                 .collect(),
         },
+        Term::New { type_name, args } => Term::New {
+            type_name: type_name.clone(),
+            args: args
+                .iter()
+                .map(|arg| match arg {
+                    NewArg::Value(v) => {
+                        NewArg::Value(subst_call_with_extras(v, name, lifted, extras))
+                    }
+                    NewArg::Type(t) => NewArg::Type(t.clone()),
+                })
+                .collect(),
+        },
     }
 }
 
@@ -1603,6 +1651,10 @@ pub fn find_non_callee_use(t: &Term, name: &str) -> Option<Term> {
         Term::Recur { args } => {
             args.iter().find_map(|a| find_non_callee_use(a, name))
         }
+        Term::New { args, .. } => args.iter().find_map(|arg| match arg {
+            NewArg::Value(v) => find_non_callee_use(v, name),
+            NewArg::Type(_) => None,
+        }),
     }
 }
 
@@ -1649,6 +1701,10 @@ mod tests {
                 binders.iter().any(|b| any_nested_ctor(&b.init)) || any_nested_ctor(body)
             }
             Term::Recur { args } => args.iter().any(any_nested_ctor),
+            Term::New { args, .. } => args.iter().any(|arg| match arg {
+                NewArg::Value(v) => any_nested_ctor(v),
+                NewArg::Type(_) => false,
+            }),
         }
     }
 
@@ -1678,6 +1734,10 @@ mod tests {
                 binders.iter().any(|b| any_let_rec(&b.init)) || any_let_rec(body)
             }
             Term::Recur { args } => args.iter().any(any_let_rec),
+            Term::New { args, .. } => args.iter().any(|arg| match arg {
+                NewArg::Value(v) => any_let_rec(v),
+                NewArg::Type(_) => false,
+            }),
         }
     }
 
@@ -2816,6 +2876,10 @@ mod tests {
                 binders.iter().any(|b| any_lit_pattern(&b.init)) || any_lit_pattern(body)
             }
             Term::Recur { args } => args.iter().any(any_lit_pattern),
+            Term::New { args, .. } => args.iter().any(|arg| match arg {
+                NewArg::Value(v) => any_lit_pattern(v),
+                NewArg::Type(_) => false,
+            }),
         }
     }
 

crates/ailang-core/src/workspace.rs

@@ -27,7 +27,7 @@
 //! with different content, and by the CLI for stable per-module
 //! identifiers.
 
-use crate::ast::{ClassDef, Def, InstanceDef, Module, Term, Type};
+use crate::ast::{ClassDef, Def, InstanceDef, Module, NewArg, Term, Type};
 use crate::canonical;
 use crate::Error as CoreError;
 use std::collections::{BTreeMap, BTreeSet, HashSet};
@@ -1269,6 +1269,15 @@ where
             }
             Ok(())
         }
+        Term::New { args, .. } => {
+            for arg in args {
+                match arg {
+                    NewArg::Type(t) => walk_type(t, f)?,
+                    NewArg::Value(v) => walk_term_embedded_types(v, f)?,
+                }
+            }
+            Ok(())
+        }
     }
 }
 
@@ -1403,6 +1412,15 @@ where
             }
             Ok(())
         }
+        Term::New { type_name, args } => {
+            f(type_name)?;
+            for arg in args {
+                if let NewArg::Value(v) = arg {
+                    walk_term(v, f)?;
+                }
+            }
+            Ok(())
+        }
     }
 }
 

crates/ailang-core/tests/design_schema_drift.rs

@@ -16,7 +16,7 @@
 
 use ailang_core::ast::{
     ClassDef, ClassMethod, Constraint, ConstDef, Ctor, Def, FnDef, InstanceDef,
-    InstanceMethod, Literal, Pattern, ParamMode, Suppress, Term, Type, TypeDef,
+    InstanceMethod, Literal, NewArg, Pattern, ParamMode, Suppress, Term, Type, TypeDef,
 };
 
 const DATA_MODEL: &str = include_str!("../../../design/contracts/0002-data-model.md");
@@ -158,6 +158,13 @@ fn design_md_anchors_every_term_variant() {
             r#""t": "recur""#,
             Term::Recur { args: vec![] },
         ),
+        (
+            r#""t": "new""#,
+            Term::New {
+                type_name: "T".into(),
+                args: vec![],
+            },
+        ),
     ];
 
     for (anchor, term) in exemplars {
@@ -179,6 +186,7 @@ fn design_md_anchors_every_term_variant() {
             Term::ReuseAs { .. } => "reuse-as",
             Term::Loop { .. } => "loop",
             Term::Recur { .. } => "recur",
+            Term::New { .. } => "new",
         };
         assert!(
             anchor_in_jsonc_block(DATA_MODEL, anchor),
@@ -539,4 +547,85 @@ fn design_md_anchors_nested_struct_keys() {
     }
 }
 
+/// prep.2 (kernel-extension-mechanics): pin the JSON byte-shape of
+/// `Term::New` with a single `NewArg::Value`. Property protected:
+/// the tag is `t: "new"`, the type-name field is serialised as
+/// `"type"` (not `"type_name"` or any camelCase variant), the args
+/// list serialises each `NewArg::Value` as `{kind: "value", value:
+/// <Term JSON>}`, and the whole shape round-trips through
+/// `serde_json` without information loss. A future edit that
+/// re-renames any of these keys breaks the pin and the data-model
+/// document must be updated in lockstep.
+#[test]
+fn term_new_round_trips() {
+    let t = Term::New {
+        type_name: "Counter".into(),
+        args: vec![NewArg::Value(Term::Lit {
+            lit: Literal::Int { value: 42 },
+        })],
+    };
+    let json = serde_json::to_value(&t).expect("serialise Term::New");
+    assert_eq!(json["t"], "new", "Term discriminator must be `t: \"new\"`");
+    assert_eq!(json["type"], "Counter", "type_name must serialise as `\"type\"`");
+    let args = json["args"].as_array().expect("args must be an array");
+    assert_eq!(args.len(), 1);
+    assert_eq!(
+        args[0]["kind"], "value",
+        "NewArg::Value discriminator must be `kind: \"value\"`"
+    );
+    assert!(
+        args[0]["value"].is_object(),
+        "value-arg's payload is the inlined Term JSON object"
+    );
+    let recovered: Term =
+        serde_json::from_value(json).expect("Term::New round-trips through serde");
+    match recovered {
+        Term::New { type_name, args } => {
+            assert_eq!(type_name, "Counter");
+            assert_eq!(args.len(), 1);
+            assert!(matches!(args[0], NewArg::Value(_)));
+        }
+        other => panic!("expected Term::New after round-trip, got {other:?}"),
+    }
+}
+
+/// prep.2 (kernel-extension-mechanics): pin the JSON byte-shape of
+/// `NewArg::Type` (a Type-positional arg). Property protected: the
+/// inner `value` carries a full `Type` JSON object (here a
+/// `(k = "con", name = "Float")`), and the round-trip preserves both
+/// the discriminator and the embedded Type's own discriminator. A
+/// future edit that changes `NewArg`'s serde tag/content shape (or
+/// renames `kind`/`value`) breaks the pin in lockstep with the
+/// data-model document.
+#[test]
+fn term_new_type_arg_round_trips() {
+    let t = Term::New {
+        type_name: "Series".into(),
+        args: vec![
+            NewArg::Type(Type::Con {
+                name: "Float".into(),
+                args: vec![],
+            }),
+            NewArg::Value(Term::Lit {
+                lit: Literal::Int { value: 3 },
+            }),
+        ],
+    };
+    let json = serde_json::to_value(&t).expect("serialise Term::New with mixed args");
+    let args = json["args"].as_array().expect("args must be an array");
+    assert_eq!(args.len(), 2);
+    assert_eq!(args[0]["kind"], "type", "first arg is a Type-positional");
+    assert_eq!(args[0]["value"]["k"], "con", "Type-arg's value carries the Type tag");
+    assert_eq!(args[0]["value"]["name"], "Float");
+    assert_eq!(args[1]["kind"], "value", "second arg is a Value-positional");
+    let recovered: Term =
+        serde_json::from_value(json).expect("mixed Term::New round-trips through serde");
+    if let Term::New { args, .. } = recovered {
+        assert!(matches!(args[0], NewArg::Type(Type::Con { ref name, .. }) if name == "Float"));
+        assert!(matches!(args[1], NewArg::Value(_)));
+    } else {
+        panic!("expected Term::New after round-trip");
+    }
+}
+
 

crates/ailang-core/tests/schema_coverage.rs

@@ -22,7 +22,7 @@ use std::collections::HashSet;
 use std::path::PathBuf;
 
 use ailang_core::ast::{
-    Def, InstanceMethod, Literal, Module, ParamMode, Pattern, Term, Type,
+    Def, InstanceMethod, Literal, Module, NewArg, ParamMode, Pattern, Term, Type,
 };
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -246,6 +246,21 @@ fn visit_term(t: &Term, observed: &mut HashSet<VariantTag>) {
                 visit_term(a, observed);
             }
         }
+        Term::New { args, .. } => {
+            // prep.2 (kernel-extension-mechanics): functional construction.
+            // The variant is intentionally NOT added to `VariantTag` /
+            // `EXPECTED_VARIANTS` in prep.2 — no .ail fixture in the
+            // current corpus emits `"t": "new"` (per the iter's
+            // out-of-scope note), so an EXPECTED entry would fail the
+            // coverage check. A future milestone that ships a Term::New
+            // fixture extends both the enum and the expected list.
+            for arg in args {
+                match arg {
+                    NewArg::Type(t) => visit_type(t, observed),
+                    NewArg::Value(v) => visit_term(v, observed),
+                }
+            }
+        }
     }
 }
 

crates/ailang-core/tests/spec_drift.rs

@@ -12,7 +12,7 @@
 //! Once the variant is matched, the test asserts the spec mentions it.
 
 use ailang_core::ast::{
-    ConstDef, Ctor, Def, FnDef, Literal, Pattern, Suppress, Term, Type, TypeDef,
+    ConstDef, Ctor, Def, FnDef, Literal, NewArg, Pattern, Suppress, Term, Type, TypeDef,
 };
 use ailang_core::FORM_A_SPEC;
 
@@ -125,6 +125,15 @@ fn spec_mentions_every_term_variant() {
             "(recur",
             Term::Recur { args: vec![] },
         ),
+        (
+            "(new",
+            Term::New {
+                type_name: "T".into(),
+                args: vec![NewArg::Value(Term::Lit {
+                    lit: Literal::Int { value: 0 },
+                })],
+            },
+        ),
     ];
 
     for (anchor, term) in exemplars {
@@ -148,6 +157,7 @@ fn spec_mentions_every_term_variant() {
             Term::ReuseAs { .. } => "reuse-as",
             Term::Loop { .. } => "loop",
             Term::Recur { .. } => "recur",
+            Term::New { .. } => "new",
         };
         assert!(
             FORM_A_SPEC.contains(anchor),

crates/ailang-prose/src/lib.rs

@@ -25,7 +25,7 @@
 
 use ailang_core::ast::{
     ClassDef, ClassMethod, ConstDef, Ctor, Def, FnDef, Import, InstanceDef, InstanceMethod,
-    Literal, Module, ParamMode, Pattern, Suppress, Term, Type, TypeDef,
+    Literal, Module, NewArg, ParamMode, Pattern, Suppress, Term, Type, TypeDef,
 };
 
 /// Render a [`Module`] as human-readable prose.
@@ -934,6 +934,26 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, ow
             }
             out.push(')');
         }
+        Term::New { type_name, args } => {
+            // prep.2 (kernel-extension-mechanics): functional construction
+            // `new T(args...)`. Form-B render is positional and uses
+            // square brackets for Type-positional args, parens for
+            // Value-positional args, mirroring the Form-A `(con T)` vs
+            // bare-term distinction at re-parse time.
+            out.push_str("new ");
+            out.push_str(type_name);
+            out.push('(');
+            for (i, arg) in args.iter().enumerate() {
+                if i > 0 {
+                    out.push_str(", ");
+                }
+                match arg {
+                    NewArg::Type(t) => write_type(out, t, owning_module),
+                    NewArg::Value(v) => write_term(out, v, level, owning_module),
+                }
+            }
+            out.push(')');
+        }
     }
 }
 
@@ -1127,6 +1147,13 @@ fn count_free_var(name: &str, t: &Term) -> usize {
         Term::Recur { args } => {
             args.iter().map(|a| count_free_var(name, a)).sum()
         }
+        Term::New { args, .. } => args
+            .iter()
+            .map(|arg| match arg {
+                NewArg::Value(v) => count_free_var(name, v),
+                NewArg::Type(_) => 0,
+            })
+            .sum(),
     }
 }
 
@@ -1277,6 +1304,16 @@ fn subst_var_with_term(t: &Term, name: &str, replacement: &Term) -> Term {
                 .map(|a| subst_var_with_term(a, name, replacement))
                 .collect(),
         },
+        Term::New { type_name, args } => Term::New {
+            type_name: type_name.clone(),
+            args: args
+                .iter()
+                .map(|arg| match arg {
+                    NewArg::Value(v) => NewArg::Value(subst_var_with_term(v, name, replacement)),
+                    NewArg::Type(t) => NewArg::Type(t.clone()),
+                })
+                .collect(),
+        },
     }
 }
 

crates/ailang-surface/src/parse.rs

@@ -1241,6 +1241,7 @@ impl<'a> Parser<'a> {
                     "reuse-as" => self.parse_reuse_as(),
                     "loop" => self.parse_loop(),
                     "recur" => self.parse_recur(),
+                    "new" => self.parse_new(),
                     other => {
                         let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
                         Err(ParseError::Production {
@@ -1249,7 +1250,7 @@ impl<'a> Parser<'a> {
                                 "unknown term head `{other}`; expected one of \
                                 `app`, `tail-app`, `lam`, `let`, `let-rec`, `if`, `match`, `do`, \
                                 `tail-do`, `seq`, `term-ctor`, `clone`, `reuse-as`, \
-                                `loop`, `recur`, `lit-unit`"
+                                `loop`, `recur`, `new`, `lit-unit`"
                             ),
                             pos,
                         })
@@ -1627,6 +1628,7 @@ impl<'a> Parser<'a> {
                     | "reuse-as"
                     | "loop"
                     | "recur"
+                    | "new"
             )
         }
 
@@ -1685,6 +1687,52 @@ impl<'a> Parser<'a> {
         Ok(Term::Recur { args })
     }
 
+    /// prep.2 (kernel-extension-mechanics): `(new TYPE-NAME ARG+)` —
+    /// functional construction. Calls the `new` def in `TYPE-NAME`'s
+    /// home module with the supplied args. Each arg is positional and
+    /// disambiguated at parse-time by its syntactic form:
+    /// - a parenthesised form whose head ident is one of the
+    ///   Type-production keywords (`con`, `fn-type`, `borrow`, `own`)
+    ///   parses as a `NewArg::Type` via [`parse_type`];
+    /// - anything else (a parenthesised term form, or a bare token —
+    ///   integer / float / string / ident) parses as a `NewArg::Value`
+    ///   via [`parse_term`].
+    ///
+    /// Requires ≥ 1 arg — a zero-arg `(new T)` shape is rejected at
+    /// parse time so a misspelled type name surfaces as a parse error
+    /// rather than as a downstream synth-time mystery.
+    fn parse_new(&mut self) -> Result<Term, ParseError> {
+        let head_pos = self.peek().map(|t| t.span.start).unwrap_or(0);
+        self.expect_lparen("new-term")?;
+        self.expect_keyword("new")?;
+        let type_name = self.expect_ident("new-term type name")?;
+        let mut args: Vec<ailang_core::ast::NewArg> = Vec::new();
+        while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
+            // Look at the next form: a parenthesised Type-production
+            // head is a Type-arg; everything else is a Term-arg.
+            let is_type_arg = matches!(
+                self.peek_head_ident(),
+                Some("con") | Some("fn-type") | Some("borrow") | Some("own")
+            );
+            if is_type_arg {
+                let t = self.parse_type()?;
+                args.push(ailang_core::ast::NewArg::Type(t));
+            } else {
+                let v = self.parse_term()?;
+                args.push(ailang_core::ast::NewArg::Value(v));
+            }
+        }
+        self.expect_rparen("new-term")?;
+        if args.is_empty() {
+            return Err(ParseError::Production {
+                production: "new-term",
+                message: "`(new T ...)` requires at least one arg".into(),
+                pos: head_pos,
+            });
+        }
+        Ok(Term::New { type_name, args })
+    }
+
     // ---- patterns -------------------------------------------------------
 
     fn parse_pattern(&mut self) -> Result<Pattern, ParseError> {

crates/ailang-surface/src/print.rs

@@ -9,7 +9,7 @@
 
 use ailang_core::ast::{
     Arm, ClassDef, ClassMethod, Constraint, ConstDef, Ctor, Def, FnDef, Import, InstanceDef,
-    InstanceMethod, Literal, Module, ParamMode, Pattern, SuperclassRef, Suppress, Term,
+    InstanceMethod, Literal, Module, NewArg, ParamMode, Pattern, SuperclassRef, Suppress, Term,
     Type, TypeDef,
 };
 
@@ -594,6 +594,24 @@ fn write_term(out: &mut String, t: &Term, level: usize) {
             }
             out.push(')');
         }
+        Term::New { type_name, args } => {
+            // prep.2 (kernel-extension-mechanics): functional construction
+            // `(new T arg+)`. Each arg is either a Type or a Term;
+            // disambiguation on re-parse is by syntactic form (head
+            // keyword in the `con` / `fn-type` / `borrow` / `own` set
+            // → Type; otherwise → Term). Both forms write through the
+            // existing `write_type` / `write_term`.
+            out.push_str("(new ");
+            out.push_str(type_name);
+            for arg in args {
+                out.push(' ');
+                match arg {
+                    NewArg::Type(t) => write_type(out, t),
+                    NewArg::Value(v) => write_term(out, v, level),
+                }
+            }
+            out.push(')');
+        }
     }
 }
 

crates/ailang-surface/tests/round_trip.rs

@@ -140,6 +140,36 @@ fn parse_then_print_then_parse_is_idempotent_on_every_ail_fixture() {
     eprintln!("parse→print→parse idempotency ok for {passed} .ail fixtures");
 }
 
+/// prep.2 (kernel-extension-mechanics): pins the Form-A round-trip for
+/// `(new T <type-arg> <value-arg>)`. The fixture exercises the
+/// `parse_new` dispatcher + the `write_term` Term::New arm, including
+/// the Type-vs-Value arg disambiguation on the parser side (head
+/// keyword `con` → NewArg::Type; bare integer → NewArg::Value).
+///
+/// Inline rather than `examples/*.ail` because no existing fixture
+/// uses `Term::New` and the iter's out-of-scope note explicitly
+/// declines a fixture migration in prep.2 (the construct will only
+/// see real fixtures once raw-buf's codegen lands).
+#[test]
+fn round_trip_term_new_mixed_args() {
+    // (new Series (con Float) 3) — a Type-positional arg followed by
+    // a Value-positional arg. The body lives inside an otherwise
+    // minimal module shell that the printer emits in canonical form.
+    let form_a = "(module new_demo\n  (data Series\n    (ctor MkSeries (con Int)))\n  (fn new\n    (type (fn-type (params (con Int)) (ret (con Series))))\n    (params n)\n    (body (term-ctor Series MkSeries n)))\n  (fn main\n    (type (fn-type (params) (ret (con Series))))\n    (params)\n    (body (new Series (con Float) 3))))";
+    let parsed_once = ailang_surface::parse(form_a)
+        .expect("Form-A round-trip fixture must parse");
+    let printed = ailang_surface::print(&parsed_once);
+    let parsed_twice = ailang_surface::parse(&printed).expect("print(parse(x)) must re-parse");
+    let bytes_a = ailang_core::canonical::to_bytes(&parsed_once);
+    let bytes_b = ailang_core::canonical::to_bytes(&parsed_twice);
+    assert_eq!(
+        bytes_a, bytes_b,
+        "Term::New round-trip parse→print→parse is not idempotent.\nfirst:  {}\nprint:  {printed}\nsecond: {}",
+        String::from_utf8_lossy(&bytes_a),
+        String::from_utf8_lossy(&bytes_b),
+    );
+}
+
 /// Parse-determinism (post-form-a-default-authoring §C3): for every
 /// well-formed `.ail` text `t`, `parse(t)` produces the same canonical
 /// bytes every invocation. Loader is a pure function of input — no

design/contracts/0002-data-model.md

@@ -176,6 +176,32 @@ narrative — defaults, superclasses, diagnostics — lives in
 // enclosing loop (enforced at typecheck, `recur-not-in-tail-position`).
 { "t": "recur",
   "args": [ Term, ... ] }
+
+// new: functional construction. Resolves `type` via type-scoped
+// lookup to its home module, then calls the home module's `new`
+// def with the supplied args. Each arg is a `NewArg` (see below).
+// Type-args (kind = "type") instantiate the `new` def's outer
+// `Forall` vars in declaration order; Value-args (kind = "value")
+// are checked against the (substituted) param types. Strictly
+// additive (no `skip_serializing_if`; pre-existing fixtures hash
+// bit-identically — none carry the tag). See prep.2 of the
+// kernel-extension-mechanics milestone.
+{ "t": "new",
+  "type": "<TypeName>",
+  "args": [ NewArg, ... ] }
+```
+
+**`NewArg`** (one positional arg to a `(new T args...)` call):
+
+```jsonc
+// Type-positional arg: instantiates one of `new`'s outer Forall
+// vars. The inner `value` carries a full `Type` JSON object.
+{ "kind": "type",  "value": Type }
+
+// Value-positional arg: a `Term` checked against the corresponding
+// substituted param type of `new`. The inner `value` carries a
+// full `Term` JSON object.
+{ "kind": "value", "value": Term }
 ```
 
 In the MVP, `do` is only a direct call to a built-in effect op (no