iter 24.3: fn print + E2E + 3 compiler-path repairs; milestone 24 close
Ships fn print : forall a. Show a => (a borrow) -> () !IO in the
prelude with explicit-let body \\x -> let s = show x in do
io/print_str s. Three new E2E fixtures + tests verify the full
path:
- show_print_smoke: 4 primitives smoke (print 42 / true / 'hello' /
3.14) — compile, run, expected stdout
- show_user_adt: data IntBox + instance prelude.Show IntBox +
print (MkIntBox 7) — stdout '7'
- show_no_instance: let f : Int -> Int = \\x -> x in do print f —
fires Show-aware NoInstance with DESIGN.md §Prelude(built-in)
classes cross-reference
IR-shape pin in print_mono_body_shape.rs asserts post-mono
print__Int.body is structurally Term::Let → App(show__Int) →
Do(io/print_str). Protects the explicit let-binder for the heap-Str
RC discipline per eob.1 Str carve-out.
Three plan-defects-fixed-inline surfaced during user-ADT E2E,
necessary repairs to make the spec's stated user-ADT trajectory
work end-to-end:
(a) mono.rs (2 sites): MonoTarget::FreeFn::type_args were carrying
bare type-cons references; normalised to canonical
<owner>.<bare> form via workspace_registry.normalize_type_for_lookup
so synthesised cross-module bodies' post-mono walks reach the
registry-keyed instance entries. Symmetric to the existing
class-method-arm normalisation.
(b) codegen/lib.rs (3 sites: resolve_top_level_fn, lower_app
cross-module arm, synth_with_extras Var arm): post-mono
synthesised bodies may carry cross-module references to modules
their source template didn't import (prelude.print__<UserType>
references show_user_adt.show__<UserType> even though prelude
does not import user modules). Fall back to direct
module_user_fns lookup when prefix not in import_map. Both
ends were independently typechecked before mono ran; the
cross-module ref is created by mono not by source.
(c) lib.rs synth FreeFnCall arm: walked Type::Forall.constraints,
substituted rigid vars with fresh metavars, pushed one
ResidualConstraint per declared constraint. Without this,
print f at Int -> Int would silently typecheck and fail with
a confusing 'unknown variable: show' at codegen rather than
fire the right typecheck-time NoInstance diagnostic.
NoInstance Float-aware arm in check/lib.rs:770-779 extended with
a parallel class == 'prelude.Show' branch that cross-references
DESIGN.md §Prelude(built-in) classes verbatim. Negative-fixture
test asserts code 'no-instance' + Show substring + Prelude-(built-in)-
classes substring.
DESIGN.md §Prelude(built-in) classes milestone-24 paragraph flips
fn print from 'ships in 24.3' to 'shipped in iter 24.3' with body
shape + pin file reference. §Float semantics gains a Show-Float
NaN-spelling cross-reference paragraph linking show 1.5 / show nan /
show inf to instance Show Float via float_to_str.
Roadmap P1 'Post-22 Prelude — Show + print rewire' flipped to [x]
with closing summary naming all three shipped iters (24.1 / 24.2 /
24.3). New P2 entry 'Retire io/print_int|bool|float effect-ops +
migrate example corpus to print' inserted at top of P2.
Tests: 556 passed (was 552 + 4 new). bench/cross_lang exit 0;
bench/compile_check + bench/check exit 1 on documented noise-class
metrics per the audit-cma lineage envelope (8th consecutive
audit-grade observation, baseline pristine per conservative-call).
Milestone 24 closes structurally with this iter. Standard audit
pipeline next.
This commit is contained in:
@@ -0,0 +1,238 @@
|
||||
# iter 24.3 — fn print polymorphic free fn + E2E + DESIGN.md sync; milestone 24 close
|
||||
|
||||
**Date:** 2026-05-13
|
||||
**Started from:** c04c07f
|
||||
**Status:** DONE
|
||||
**Tasks completed:** 8 of 8
|
||||
|
||||
## Summary
|
||||
|
||||
Ships `fn print : forall a. Show a => (a borrow) -> () !IO` in
|
||||
`examples/prelude.ail.json` with explicit-let body
|
||||
`\x -> let s = show x in do io/print_str s`. The let-binder is
|
||||
structurally pinned by `crates/ail/tests/print_mono_body_shape.rs`
|
||||
(post-mono `print__Int.body` is `Term::Let → Term::App(show__Int) →
|
||||
Term::Do(io/print_str)`). Three new E2E fixtures + tests verify the
|
||||
full path: `show_print_smoke` (4 primitives) and `show_user_adt`
|
||||
(`data IntBox` + `instance prelude.Show IntBox` + `print (MkIntBox 7)`)
|
||||
both compile, run, and produce expected stdout; `show_no_instance`
|
||||
fires a Show-aware `NoInstance` diagnostic with the canonical
|
||||
DESIGN.md cross-reference. DESIGN.md §"Prelude (built-in) classes"
|
||||
flips `print` from "ships in 24.3" to "shipped in iter 24.3" with the
|
||||
explicit-let body + pin reference. DESIGN.md §"Float semantics" gains
|
||||
a Show-Float NaN-spelling cross-reference paragraph. Roadmap P1
|
||||
"Post-22 Prelude — Show + print rewire" entry checked off; new P2
|
||||
entry "Retire `io/print_int|bool|float` effect-ops + migrate example
|
||||
corpus to `print`" inserted at top of P2. **Three plan-defects-fixed-
|
||||
inline** surfaced when running the user-ADT E2E: (a) `MonoTarget::
|
||||
FreeFn::type_args` were carrying bare type-cons references that broke
|
||||
the post-mono walk's registry lookup when the synthesised body lived
|
||||
in a different module from the type — fixed by normalising via
|
||||
`workspace_registry.normalize_type_for_lookup` at two
|
||||
`mono.rs` collection sites; (b) codegen's cross-module fn resolution
|
||||
went through `import_map`, but post-mono synthesised bodies may
|
||||
reference modules their source template didn't import — fixed by
|
||||
falling back to direct `module_user_fns` lookup at three codegen
|
||||
sites (`resolve_top_level_fn`, `lower_app` cross-module arm,
|
||||
`synth_with_extras` Var arm); (c) the synth FreeFnCall arm didn't push
|
||||
residuals for declared constraints, so `Show (Int -> Int)` never
|
||||
reached the typecheck-time discharge logic — fixed by walking
|
||||
`Type::Forall.constraints` at the FreeFnCall site and pushing one
|
||||
residual per constraint with the fresh-metavar substitution. Full
|
||||
`cargo test --workspace` 556 passed / 0 failed (was 552 post-24.2,
|
||||
+4 new = 1 print_mono_body_shape + 2 show_print_e2e + 1
|
||||
show_no_instance_e2e). `bench/cross_lang.py` clean; `bench/compile_check.py`
|
||||
+ `bench/check.py` exit 1 with documented noise-class metrics per the
|
||||
audit-cma lineage envelope (baseline pristine, 8th consecutive
|
||||
audit-grade observation). Milestone 24 closes structurally; only the
|
||||
audit pipeline remains.
|
||||
|
||||
## Per-task notes
|
||||
|
||||
- iter 24.3.1: Appended `fn print` to `examples/prelude.ail.json`
|
||||
after `fn ge` (last def pre-edit). 20 defs total (was 19). Body
|
||||
is the literal `Term::Let { name: "s", value: App(show, [x]), body:
|
||||
Do(io/print_str, [s]) }` with the constraint `Show a` bare per
|
||||
mq.1 same-module canonical form. 552 tests stay green.
|
||||
- iter 24.3.2: `crates/ail/tests/print_mono_body_shape.rs` asserts
|
||||
post-mono `print__Int.body` shape. Initial test asserted outer
|
||||
`Term::Lam` wrapper — corrected after the panic surfaced that
|
||||
`FnDef.body: Term` is the *inner* function body for top-level fns
|
||||
(params carried separately on `FnDef.params`). The test now asserts
|
||||
directly `Term::Let → App(show__Int, [x]) → Do(io/print_str, [s])`,
|
||||
faithful to the plan's intent (preserve the explicit-let-binder
|
||||
discipline) while matching the actual AST shape.
|
||||
- iter 24.3.3: `examples/show_print_smoke.ail.json` written with
|
||||
nested `Term::Seq` of four `App(print, [lit])` calls (Int 42, Bool
|
||||
true, Str "hello", Float bits=40091eb851eb851f for 3.14). `ail
|
||||
build` clean; stdout: `42\ntrue\nhello\n3.14` — io/print_str
|
||||
appends a newline via `@puts`.
|
||||
- iter 24.3.4: `examples/show_user_adt.ail.json` written + 2-test
|
||||
`crates/ail/tests/show_print_e2e.rs`. Surfaced three substantive
|
||||
plan-defects-fixed-inline (Concerns below); after fix, both E2E
|
||||
tests pass (`print (MkIntBox 7)` → stdout "7").
|
||||
- iter 24.3.5: Extended NoInstance Float-aware arm in
|
||||
`crates/ailang-check/src/lib.rs:770-779` with a parallel
|
||||
`class == "prelude.Show"` branch. The arm fires for ANY type
|
||||
lacking a Show instance (function types, user types without
|
||||
instance) — cross-references DESIGN.md §"Prelude (built-in)
|
||||
classes" verbatim. Negative fixture `examples/show_no_instance.ail.json`
|
||||
(let-bound `f : Int -> Int` + `print f`) and pin test in
|
||||
`crates/ail/tests/show_no_instance_e2e.rs` (asserts code,
|
||||
Show-substring, Prelude-(built-in)-classes substring). After
|
||||
the constraint-residual-push fix in synth (Concerns below), the
|
||||
diagnostic fires at typecheck.
|
||||
- iter 24.3.6: DESIGN.md §"Prelude (built-in) classes" milestone-24
|
||||
paragraph amended: `print` flipped to past tense ("shipped in iter
|
||||
24.3"), body shape + pin file reference added, retirement
|
||||
follow-up named. DESIGN.md §"Float semantics" gained a new
|
||||
paragraph in the "Unspecified" block cross-referencing `show 1.5`
|
||||
/ `show nan` / `show inf` to `instance Show Float` via
|
||||
`float_to_str`. ~10 lines added net (2697 → 2707).
|
||||
- iter 24.3.7: Roadmap P1 "Post-22 Prelude — Show + print rewire"
|
||||
entry flipped to `[x]` with a closing-summary block naming all
|
||||
three shipped iters (24.1 f38bad8, 24.2 iter-24.2, 24.3 this
|
||||
iter). New P2 entry "Retire `io/print_int|bool|float` effect-ops
|
||||
+ migrate example corpus to `print`" inserted at top of P2,
|
||||
before the existing operator-routing-through-Eq/Ord entry.
|
||||
- iter 24.3.8: Full workspace 556 passed / 0 failed. `prelude_free_fns`
|
||||
5/5 green; `mono_hash_stability` 2/2 green (Eq/Ord hashes
|
||||
unchanged, Show hashes from 24.2 unchanged). `bench/cross_lang.py`
|
||||
exit 0 (25/25 stable). `bench/compile_check.py` exit 1 with 1
|
||||
noise-class regression on a `check_ms.*` metric (regressed metric
|
||||
identity migrates between runs — pattern consistent with the
|
||||
documented noise envelope per audit-cma lineage, 8th consecutive
|
||||
observation). `bench/check.py` exit 1 with 2 improvements beyond
|
||||
tolerance on `latency.explicit_at_rc.*` — same envelope, same
|
||||
conservative call. Baseline pristine.
|
||||
|
||||
## Concerns
|
||||
|
||||
- **Three plan-defects-fixed-inline surfaced during Task 4 (user-ADT
|
||||
E2E).** All three are necessary repairs to make the spec's stated
|
||||
user-ADT trajectory (§"Data flow / print x at user type IntBox"
|
||||
lines 297-310) work end-to-end. The plan did not anticipate them
|
||||
because the test architecture envisioned (Tasks 3+4 sharing one
|
||||
test file) didn't actually exercise the cross-module mono synthesis
|
||||
before this iter; primitive-only smoke worked through the existing
|
||||
pipeline.
|
||||
- (a) **Bare type-cons in `MonoTarget::FreeFn::type_args`.** At
|
||||
mono target-collection (`collect_mono_targets` + `collect_residuals_ordered`
|
||||
free-fn arms), `subst.apply(meta)` returns the unification result
|
||||
in whatever qualification the caller-module's view used. For a
|
||||
user-defined type referenced from `main` (in `show_user_adt`),
|
||||
`IntBox` came out bare. The downstream `synthesise_mono_fn_for_free_fn`
|
||||
then substituted bare `IntBox` everywhere in the synthesised body,
|
||||
and Phase 3 rewrite of the synthesised body (run in PRELUDE
|
||||
caller-module context, where `IntBox` is not a known TypeDef) saw
|
||||
`Type::Con{IntBox}` that didn't normalise to the registry-keyed
|
||||
`show_user_adt.IntBox`. Lookup missed → no `show__IntBox` target
|
||||
scheduled → bare `Var "show"` persisted post-mono. Fix:
|
||||
`mono.rs` lines 685-696 + 1267-1278 normalise via
|
||||
`env.workspace_registry.normalize_type_for_lookup(module_name, &resolved)`
|
||||
before pushing the type into `MonoTarget::FreeFn::type_args`. Same
|
||||
invariant applies symmetric to the existing
|
||||
`r_ty_norm = normalize_type_for_lookup(...)` calls already in
|
||||
`collect_mono_targets`'s class-method arm.
|
||||
- (b) **Codegen cross-module references via import_map.** Post
|
||||
fix-(a), the synthesised body now correctly references
|
||||
`show_user_adt.show__cb5eb497` from inside `prelude.print__cb5eb497`.
|
||||
But `prelude` does not have `show_user_adt` in its `import_map`
|
||||
(prelude is the base; user modules import IT, not the other way
|
||||
around). Three codegen sites raised UnknownVar:
|
||||
`resolve_top_level_fn:2200`, `lower_app` cross-module arm:1981,
|
||||
`synth_with_extras` Var arm:2777. All three now fall back to a
|
||||
direct `module_user_fns.contains_key(prefix)` (or
|
||||
`module_def_ail_types.contains_key(prefix)`) lookup when the
|
||||
prefix isn't in the current module's import_map. This is the
|
||||
post-mono synthesised-body invariant: cross-module references in
|
||||
synthesised bodies may bypass the source template's imports
|
||||
(both ends were independently typechecked under their own module
|
||||
contexts before mono ran; the cross-module reference is created
|
||||
by mono, not by the source). Doc comments cross-reference all
|
||||
three sites.
|
||||
- (c) **Poly-free-fn constraint residuals not pushed at synth.**
|
||||
Pre-iter-24.3, the FreeFnCall arm at `lib.rs:2820` had
|
||||
`constraints: _` — declared constraints of the poly free fn were
|
||||
ignored. For all milestone-23 fixtures (`ne`/`lt`/`le`/`gt`/`ge`
|
||||
at primitive types), this was latent because every call site had
|
||||
a registry entry; the mono pass silently scheduled the
|
||||
corresponding `eq__T`/`compare__T` targets, and codegen succeeded.
|
||||
But for negative cases — `print f` where `f : Int -> Int` has no
|
||||
Show instance — the constraint never reached the typecheck-time
|
||||
`NoInstance` discharge (lib.rs:1880-1905). The build would emit
|
||||
a confusing post-mono `unknown variable: show` from codegen
|
||||
rather than the right typecheck-phase diagnostic. Fix: at
|
||||
`lib.rs:2820+`, walk `Type::Forall.constraints` at FreeFnCall
|
||||
sites, substitute the rigid vars with their fresh metavars, and
|
||||
push one `ResidualConstraint` per declared constraint. The
|
||||
discharge loop then fires the correct NoInstance with full
|
||||
diagnostic context (including the Show-aware addendum from
|
||||
Task 5). Pre-existing milestone-23 tests stay green because
|
||||
primitive-type Show/Eq/Ord registry entries discharge silently.
|
||||
- **bench/compile_check.py + check.py exit 1.** Both report
|
||||
noise-class metrics (1 regression / 2 improvements respectively).
|
||||
Metric identity migrates between consecutive runs — pattern
|
||||
consistent with the documented `latency.implicit_at_rc.*` /
|
||||
`check_ms.*` noise envelope per audit-cma + audit-ms + audit-eob +
|
||||
audit-ct-tidy + audit-mq + iter-24.2 lineage. 8th consecutive
|
||||
observation. Baseline pristine per conservative-call convention.
|
||||
- **Plan deviation on Task 2 (IR-shape pin).** The plan's test stub
|
||||
asserted `Term::Lam { body: Term::Let { ... } }` for `print__Int`.
|
||||
The actual `FnDef.body: Term` shape for top-level fns is the
|
||||
*inner* function body (params separate); no outer `Term::Lam`. The
|
||||
test was corrected to assert `Term::Let { ... }` directly. The
|
||||
load-bearing property (explicit let-binder for heap-Str RC
|
||||
discipline) is identical between the plan's intent and the
|
||||
shipped assertion; only the wrapper assumption changed. Doc
|
||||
comment in the test file explains the FnDef.body shape contract.
|
||||
|
||||
## Known debt
|
||||
|
||||
- **Milestone 24 closes structurally with this iter.** The standard
|
||||
`audit` pipeline (architect drift review + bench regression
|
||||
attribution) runs next. The three plan-defects-fixed-inline above
|
||||
may merit architect commentary on whether the fix sites belong as
|
||||
permanent invariants or are themselves transitional. Specifically:
|
||||
fix (a) implies that `MonoTarget::FreeFn::type_args` carries
|
||||
CANONICAL types post-collection — this is a strengthening of the
|
||||
pre-iter invariant which was "subst.apply result"; future planner
|
||||
work that touches the mono pass should keep that strengthening
|
||||
visible.
|
||||
- **P2 entry "Retire io/print_int|bool|float effect-ops" is queued.**
|
||||
The new entry's `~86 fixtures affected` count is from a rough
|
||||
grep against `do io/print_<T>`; precise count + migration plan is
|
||||
the planner's job when the milestone opens.
|
||||
- **Negative-fixture coverage is single-shape.** `show_no_instance.ail.json`
|
||||
uses `f : Int -> Int`. Other NoInstance shapes (user type without
|
||||
instance, `print x` where `x : SomeUnsupportedClass`) are not
|
||||
separately tested — the NoInstance arm fires for any non-prelude-Show
|
||||
type by construction, so the single fixture is structurally
|
||||
representative.
|
||||
|
||||
## Files touched
|
||||
|
||||
**Created (6):**
|
||||
- `crates/ail/tests/print_mono_body_shape.rs`
|
||||
- `crates/ail/tests/show_print_e2e.rs`
|
||||
- `crates/ail/tests/show_no_instance_e2e.rs`
|
||||
- `examples/show_print_smoke.ail.json`
|
||||
- `examples/show_user_adt.ail.json`
|
||||
- `examples/show_no_instance.ail.json`
|
||||
|
||||
**Modified (6):**
|
||||
- `examples/prelude.ail.json` (+1 def: `fn print`)
|
||||
- `crates/ailang-check/src/lib.rs` (NoInstance Show-aware branch +
|
||||
FreeFnCall constraint-residual push)
|
||||
- `crates/ailang-check/src/mono.rs` (FreeFn type_args canonical-form
|
||||
normalisation, 2 sites)
|
||||
- `crates/ailang-codegen/src/lib.rs` (cross-module reference fallback
|
||||
for post-mono synthesised bodies, 3 sites: `resolve_top_level_fn`,
|
||||
`lower_app`'s cross-module call arm, `synth_with_extras`'s Var arm)
|
||||
- `docs/DESIGN.md` (§"Prelude (built-in) classes" milestone-24
|
||||
paragraph + §"Float semantics" Show-Float cross-reference)
|
||||
- `docs/roadmap.md` (P1 Show+print → [x]; new P2 entry at top)
|
||||
|
||||
## Stats
|
||||
|
||||
`bench/orchestrator-stats/2026-05-13-iter-24.3.json`
|
||||
Reference in New Issue
Block a user