fieldtest: kernel-extension-mechanics — 6 examples, 9 findings (3 bugs, 1 friction, 1 spec_gap, 4 working)
Post-audit fieldtest for the kernel-extension-mechanics milestone. Fieldtester wrote 6 .ail consumer programs against the public interface only (design ledger + spec + ail CLI; no source crate reads), one per axis with two for the param-in pair (accept + reject). All artefacts in examples/fieldtest/ + the spec. **Working (4):** F5 NewTypeNotConstructible diagnostic is precise (names the home module + missing def in one sentence). F6 Term::New codegen-deferral diagnostic explicitly names the raw-buf milestone where support lands. F7 param-in accept-path is end-to-end (check + build + run prints 17). F8 ParamNotInRestrictedSet names type-arg + var + TypeDef. **Bugs (3, action: debug):** - F1 (axis 1) — Same-module type-scoped call `(app Type.member …)` rejected with phantom-qualified `expected <this>.T, got T`. Bare `(app member …)` from inside Type's home module works. Spec's "Canonical form decision" promises type-scoped works uniformly; the resolver appears to disagree with the workspace pre-pass on whether `<this-module>.T` equals bare `T`. Repro: examples/fieldtest/kem_2b_min_repro.ail. - F3 (axis 3) — Kernel-tier auto-import scopes the name but does not register the module as a resolvable qualifier prefix. Per the pre-pass, a bare `StubT` in a type slot is qualified to `kernel_stub.StubT`; the resolver then rejects `kernel_stub` as unknown. Asymmetric: prelude's free fns work (per prelude_free_fns.rs), but the stub's TypeDef is effectively unreachable from any consumer. Repro: examples/fieldtest/kem_3_stub_consumer.ail. - F4 (axis 3, spec/ship coherence) — The spec's prep.3 worked- consumer relies on `(new StubT 42)`, but the shipped STUB_AIL has only a TypeDef + ctor — the `(fn new ...)` the spec designed is missing from the implementation. The diagnostic the resolver does emit on the consumer (F5) is precise; the bug is the absent def itself. Resolution: re-add the `new` to STUB_AIL (the spec's design), refresh the drift pin. **Friction (1, action: plan-or-defer):** - F2 — Loader's sibling-only module resolution forces symlinks for any cross-module fixture sitting outside the canonical `examples/` directory. The kem_1 example required local symlinks for std_list.ail + std_maybe.ail. Secondary: the diagnostic message names only the .ail.json path even though .ail also resolves — actively misleading. Recommended: small tidy iter for loader workspace-search-path + diagnostic clarity. **Spec-gap (1, action: ratify):** - F9 — `design/models/0007-kernel-extensions.md:80` uses `unit` as a value literal of type Unit; the checker treats it as a Term::Var lookup and emits [unbound-var]. Either ratify `unit` as the canonical Unit-value literal in the language, or tighten the design model to use the existing idiom. The current model/ surface disagreement is a small but real LLM-author trap. **Symlinks committed** as evidence of the F2 workaround: examples/fieldtest/std_list.ail and std_maybe.ail are symlinks into ../. They are the fingerprint of the friction — removing them silently would erase the evidence. Per Iron Law, fieldtester did not work around bugs — they were all surfaced and recorded. The kem_2b_min_repro.ail fixture exists specifically because F1 surfaced mid-drafting and got minimised; kem_3_stub_consumer.ail also stays as the F3 RED-side fixture. Triage (next-step routing for /boss): F4 → small inline fix (add (fn new ...) to STUB_AIL + drift refresh) F9 → small inline ratify (whitepaper edit) F2 → backlog issue, deferred (single tidy iter someday) F1, F3 → debug skill dispatches, then implement mini-mode F5-F8 → carry-on, recorded as wins
This commit is contained in:
@@ -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.
|
||||
@@ -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")))))))
|
||||
@@ -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"))))))))
|
||||
@@ -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))))))
|
||||
@@ -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"))))))
|
||||
@@ -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"))))))
|
||||
@@ -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 ""))))
|
||||
Symlink
+1
@@ -0,0 +1 @@
|
||||
../std_list.ail
|
||||
Symlink
+1
@@ -0,0 +1 @@
|
||||
../std_maybe.ail
|
||||
Reference in New Issue
Block a user