spec: 23 (revised) — Eq/Ord prelude on unified mono pass
Re-brainstorm of milestone 23 after the original spec retired in iter gc.1. The original silently assumed polymorphic free fns are mono-specialised parallel to class methods; iter 23.4 BLOCKED three times on that seam. Revised spec corrects the architecture by committing to a unified typecheck-time mono pass (B1) — one specialiser for all Type::Forall Defs, codegen-time lower_polymorphic_call retired in same iter. First real run of the grounding-check agent (Step 7.5) shipped in gc.1: PASS, 15 assumptions ratified.
This commit is contained in:
@@ -0,0 +1,421 @@
|
||||
# 23 — Eq / Ord Prelude — Design Spec (revised)
|
||||
|
||||
**Date:** 2026-05-11
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
|
||||
**Supersedes:** `docs/specs/2026-05-10-23-eq-ord-prelude.md` (retired
|
||||
2026-05-11 in iter gc.1; commit `f6d4ba3`). Iter 23.1–23.3 shipped
|
||||
under the original spec and remain in effect; this revised spec
|
||||
re-frames the remaining work on a corrected architecture.
|
||||
|
||||
## Goal
|
||||
|
||||
Complete milestone 23 by shipping the five free top-level utility
|
||||
functions `ne`, `lt`, `le`, `gt`, `ge` in the auto-loaded prelude,
|
||||
plus the E2E and DESIGN.md amendments that close the Eq/Ord
|
||||
surface. Establish the partial-Eq/Ord story for `Float` as a lived
|
||||
reality: `Float` has neither instance, so polymorphic `eq x y` /
|
||||
`compare x y` over a Float fires `NoInstance` at typecheck — exactly
|
||||
what DESIGN.md §"Float semantics" prescribes.
|
||||
|
||||
The re-brainstorm exists because the original spec's architecture
|
||||
section silently assumed that polymorphic free fns with class
|
||||
constraints would be mono-specialised the same way class methods
|
||||
are. They are not — the typecheck-time mono pass
|
||||
(`crates/ailang-check/src/mono.rs`, iter 22b.3) operates only on
|
||||
class methods, while polymorphic free fns are specialised at codegen
|
||||
time by `crates/ailang-codegen/src/lib.rs::lower_polymorphic_call`
|
||||
(iter 12b). A polymorphic free fn whose body invokes class methods
|
||||
falls between the two passes. Iter 23.4 BLOCKED three times on this
|
||||
seam.
|
||||
|
||||
The corrected architecture unifies the two specialisers (see
|
||||
Architecture below) and ships the remaining free fns on top of
|
||||
the unified pass. The three iter-23.4 prep commits are classified:
|
||||
prep1 (linearity + checker bare-name) stays load-bearing, prep2 +
|
||||
prep3 (codegen bare-name fall-throughs) become provably dead and
|
||||
are rolled back in 23.4.
|
||||
|
||||
`Show`, operator routing, `print`-rewire, and the heap-Str ABI
|
||||
remain out of scope; each is its own milestone with substantive
|
||||
reasons (see "Out of scope" — unchanged from original spec).
|
||||
|
||||
## Architecture
|
||||
|
||||
The milestone no longer consumes the 22b.3 typeclass machinery
|
||||
unchanged. Four artefacts:
|
||||
|
||||
### 1. Mono-Pass unification (the corrected centrepiece)
|
||||
|
||||
`crates/ailang-check/src/mono.rs::monomorphise_workspace` is
|
||||
restructured into a single specialiser for every
|
||||
`Type::Forall`-quantified `Def::Fn` whose call sites supply
|
||||
fully-concrete substitutions. Two thin source-body entry points:
|
||||
|
||||
- **Class-method entry:** look up the resolved instance body via
|
||||
`Registry::entries[(class, type-hash)]`. Unchanged behaviour from
|
||||
iter 22b.3.
|
||||
- **Free-fn entry:** take the source body directly from the
|
||||
polymorphic `Def::Fn`, apply rigid-var substitution.
|
||||
|
||||
Shared core mechanics — identical for both arms — are: rigid-var
|
||||
substitution via `crate::substitute_rigids`, fixpoint loop (`mono.rs`
|
||||
line 88) that keeps collecting targets until a round adds nothing
|
||||
new, dedup cache keyed by `(name, type-hash)`, and the
|
||||
call-site-rewrite walker.
|
||||
|
||||
Output: synthesised `Def::Fn` entries with naming
|
||||
`<name>__<typesurfacename>` (extended to
|
||||
`<name>__<type1>__<type2>__…` for N-ary type vars in declaration
|
||||
order; concrete format is an Open commitment), appended to the
|
||||
defining module. The mono pass becomes the only specialiser; codegen
|
||||
sees no class machinery and no polymorphic call sites.
|
||||
|
||||
The current codegen-time specialiser is retired in the same iter:
|
||||
`crates/ailang-codegen/src/lib.rs::lower_polymorphic_call`,
|
||||
`module_polymorphic_fns` (the per-module FnDef map), and `mono_queue`
|
||||
(the deduplicated emission queue) are removed. All today's call
|
||||
sites of `lower_polymorphic_call` (lines 1944, 1972) become direct
|
||||
calls to mono symbols after the typecheck-mono walker has rewritten
|
||||
them.
|
||||
|
||||
### 2. Rollback of iter-23.4-prep2 + prep3
|
||||
|
||||
Two existing codegen bare-name fall-throughs were anticipatory
|
||||
patches for the prelude free fns:
|
||||
|
||||
- commit `a06159d` (prep2): codegen — bare-name fall-through to
|
||||
implicit-imported free fns.
|
||||
- commit `c42a0f5` (prep3): codegen — polymorphic-free-fn bare-name
|
||||
fall-through to implicit-imported modules.
|
||||
|
||||
After Mono unification, codegen never sees bare polymorphic free-fn
|
||||
names — the unified mono pass rewrites every call site to its mono
|
||||
symbol before codegen runs. The two patches are provably dead and
|
||||
are rolled back in 23.4. The rollback lands in the same iter as
|
||||
the unification so the codebase never carries the fall-throughs
|
||||
as visible-but-dead code.
|
||||
|
||||
The third iter-23.4-prep is kept:
|
||||
|
||||
- commit `8d39f13` (prep.1): linearity — register `Def::Class` method
|
||||
types in globals. Required independent of mono — linearity walks
|
||||
pre-mono.
|
||||
- commit `aef4ab8` (prep.2): check — bare-name fall-through to
|
||||
implicit-imported free fns. Required at typecheck time — bare `ne`
|
||||
must resolve to the prelude `Def::Fn` *before* mono can specialise.
|
||||
|
||||
### 3. Prelude AILang module
|
||||
|
||||
`examples/prelude.ail.json` already contains, from iters 23.1–23.3:
|
||||
the `Ordering` ADT, the `Eq` class with `Eq Int`/`Bool`/`Str`
|
||||
instances, the `Ord` class with `Ord Int`/`Bool`/`Str` instances.
|
||||
Iter 23.5 adds the five free fns:
|
||||
|
||||
- `ne : forall a. Eq a => (a borrow, a borrow) -> Bool`, body
|
||||
`not (eq x y)`.
|
||||
- `lt`, `le`, `gt`, `ge`: `forall a. Ord a => (a borrow, a borrow) -> Bool`,
|
||||
bodies pattern-matching `compare` against the appropriate
|
||||
`Ordering` shapes.
|
||||
|
||||
### 4. C-runtime functions
|
||||
|
||||
`runtime/str.c` shipped its two functions in iter 23.2 and 23.3:
|
||||
`ail_str_eq(a, b) -> bool` (byte-equality on constant-string layouts)
|
||||
and `ail_str_compare(a, b) -> i32` (lex comparison returning
|
||||
-1/0/+1). No further runtime work.
|
||||
|
||||
Existing primitive operators (`==`, `<`, `<=`, `>`, `>=`) remain
|
||||
primitive and per-type-routed at lowering, unchanged. Routing them
|
||||
through the class methods is the declared P2 follow-up; the
|
||||
redundancy between primitive `==` and class `eq x y` on
|
||||
Int/Bool/Str is acknowledged and ratified as transitional.
|
||||
|
||||
## Components (iterations)
|
||||
|
||||
| Iter | Status | Scope |
|
||||
|------|--------|-------|
|
||||
| 23.1 | shipped (2026-05-10) | `Ordering` ADT + prelude skeleton + auto-load via `check_workspace`. |
|
||||
| 23.2 | shipped (2026-05-10) | `class Eq` + `Eq Int/Bool/Str` + `ail_str_eq`. |
|
||||
| 23.3 | shipped (2026-05-10) | `class Ord extends Eq` + `Ord Int/Bool/Str` + `ail_str_compare`. |
|
||||
| 23.4-prep | shipped, **kept** | commits `8d39f13` (linearity registers `Def::Class` method types in globals) + `aef4ab8` (check bare-name fall-through to implicit-imported free fns). Both resolve names *before* mono; independent of B1. |
|
||||
| 23.4-prep2 / 23.4-prep3 | shipped, **rolled back in 23.4** | commits `a06159d` + `c42a0f5` — codegen bare-name fall-throughs. Provably dead after Mono unification. |
|
||||
| **23.4** (revised) | upcoming | **Mono-Pass unification.** Restructure `crates/ailang-check/src/mono.rs::monomorphise_workspace` into one specialiser with two source-body entry points (class-method via `Registry::entries`, free-fn direct). Extend `collect_mono_targets` to also produce targets for polymorphic free-fn calls with fully-concrete substitutions. Remove `lower_polymorphic_call` + `module_polymorphic_fns` + `mono_queue` from codegen. Rollback prep2 + prep3. Amend DESIGN.md §"Resolution and monomorphisation" to describe the pass as covering all `Type::Forall`-Defs. Tests: existing polymorphic fixtures (`poly_id`, `poly_apply`, `poly_box_proj`) green; new fixture `cmp_max_smoke` proves cross-cutting (`cmp_max : forall a. Ord a => (a, a) -> a` at Int synthesises both `cmp_max__Int` and nested `compare__Int` in one fixpoint). |
|
||||
| **23.5** (revised) | upcoming | **Prelude free fns + E2E.** Add `ne`/`lt`/`le`/`gt`/`ge` to `examples/prelude.ail.json`. E2E fixtures: (a) positive polymorphic helper at Int/Bool/Str, (b) negative — `eq f g` at Float typecheck-rejects with Float-aware diagnostic, (c) user-ADT — `IntBox` with `Eq`/`Ord` instances + polymorphic helper monomorphises to the user instance. Amend DESIGN.md §"Decision 11 / Prelude classes" — Eq/Ord shipped; the "Milestone 22 ships no built-in Prelude classes" wording stays as historical accuracy with a forward-pointing addendum. Roadmap: P1 Post-22 Prelude entry from `[~]` to `[x]` for Eq/Ord half; Show half stays. |
|
||||
|
||||
## Data flow
|
||||
|
||||
Two trajectories show the unification at work.
|
||||
|
||||
### Class-method call `(eq x y)` with `x : Int` (unchanged)
|
||||
|
||||
1. **Typecheck.** `eq` resolves to
|
||||
`forall a. Eq a => (a borrow, a borrow) -> Bool`. Constraint solver
|
||||
matches `Eq Int` against `instance Eq Int`; constraint
|
||||
discharged.
|
||||
2. **Mono (class-method entry).** `Registry::entries[(Eq, Int)]`
|
||||
lookup, body from `InstanceMethod`, rigid-var subst `a → Int`,
|
||||
synth `eq__Int`. Call site `eq x y` → `eq__Int x y`.
|
||||
3. **Codegen.** `eq__Int` lowers to `icmp eq i64` + `zext i1 i8`.
|
||||
|
||||
### Polymorphic free-fn call `(ne x y)` with `x : Int` (new with B1)
|
||||
|
||||
1. **Typecheck.** `ne` resolves to a polymorphic `Def::Fn` with
|
||||
`forall a. Eq a => (a borrow, a borrow) -> Bool`. Bare-name lookup
|
||||
reaches the prelude via prep1's `env.module_globals` fall-through.
|
||||
Constraint `Eq Int` discharged as above.
|
||||
2. **Mono (free-fn entry).** Body taken directly from
|
||||
`Def::Fn.body`, rigid-var subst `a → Int`, synth `ne__Int`. In
|
||||
the same fixpoint round, the body walker detects the nested
|
||||
`eq` call at concrete `Int` and schedules it as a class-method
|
||||
target. The next round synthesises `eq__Int` (or cache-hits).
|
||||
`ne__Int`'s body refers directly to `eq__Int`. Call site
|
||||
`ne x y` → `ne__Int x y`.
|
||||
3. **Codegen.** `ne__Int` lowers as any monomorphic fn would; the
|
||||
nested `eq__Int` is a direct call. No `lower_polymorphic_call`
|
||||
path involved — the codegen-time specialiser no longer exists.
|
||||
|
||||
The fixpoint loop in `monomorphise_workspace` (line 88) already
|
||||
iterates until a round adds nothing new. The change is in the
|
||||
target collector: it must additionally emit `MonoTarget`s for
|
||||
"call site to polymorphic free-fn `Def::Fn` with fully-concrete
|
||||
substitution", not only for class-constraint residuals.
|
||||
|
||||
## Error handling
|
||||
|
||||
Unchanged from original spec:
|
||||
|
||||
- **`NoInstance Eq Float` / `NoInstance Ord Float`** — fired at
|
||||
typecheck when class resolution selects Float. Diagnostic must
|
||||
cross-reference DESIGN.md §"Float semantics" so the LLM-author
|
||||
immediately learns the partial-Float story.
|
||||
- **`NoInstance Eq <UserType>` / `NoInstance Ord <UserType>`** —
|
||||
re-uses 22's existing diagnostic path.
|
||||
- **`OrphanInstance`** — Decision 11 unchanged. Prelude instances
|
||||
are non-orphan.
|
||||
|
||||
New categories under B1:
|
||||
|
||||
- **Polymorphic-free-fn specialisation failures** are
|
||||
`CheckError::Internal`. The mono pass runs post-typecheck, so
|
||||
every substitution must have been validated by then. A failure
|
||||
here is a caller-contract violation; mirrors the existing
|
||||
convention in `synthesise_mono_fn` (mono.rs line 549).
|
||||
- **Recursive polymorphic free fns with concrete substitutions** —
|
||||
the existing fixpoint loop closes transitively, same mechanism
|
||||
used for class-method bodies calling other class methods (e.g.
|
||||
`default ne x y = not (eq x y)`).
|
||||
- **Codegen-side errors remain not expected.** The unification
|
||||
reduces codegen's responsibility (removes
|
||||
`lower_polymorphic_call`), it does not expand it. Any
|
||||
fall-through that survives must be
|
||||
`CodegenError::Internal`-shaped per the iter-4.4 Floats precedent
|
||||
— never `unimplemented!()` panic.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
### 23.4 — Mono unification
|
||||
|
||||
- **Regression: existing polymorphic fixtures stay green.**
|
||||
`examples/poly_id.ail.json`, `examples/poly_apply.ail.json`,
|
||||
`examples/poly_box_proj.ail.json`, and every 22b.3 typeclass
|
||||
fixture must compile and run unchanged. These are the
|
||||
load-bearing proof that codegen-time specialisation was
|
||||
structurally replaceable.
|
||||
- **New: composition fixture.** `examples/cmp_max_smoke.ail.json`
|
||||
with `fn cmp_max : forall a. Ord a => (a, a) -> a` (body:
|
||||
`match compare x y with LT -> y | _ -> x`), invoked at Int. The
|
||||
test asserts that after mono, the workspace contains both
|
||||
`cmp_max__Int` and `compare__Int` as `Def::Fn`, both produced
|
||||
by the unified pass. This pins the cross-cutting case that
|
||||
iter-23.4-prep3 unsuccessfully tried to patch.
|
||||
- **Hash-stability of existing mono symbols.** `eq__Int`,
|
||||
`compare__Str`, and the four other already-synthesised symbols
|
||||
must produce identical bodies (and therefore identical hashes)
|
||||
under the unified pass. Pin test in the style of
|
||||
`crates/ailang-core/src/hash.rs::ct4_migrated_fixtures_have_canonical_form_hashes`.
|
||||
- **Rollback proof.** `cargo test --workspace` green after removal
|
||||
of `lower_polymorphic_call` + `module_polymorphic_fns` +
|
||||
`mono_queue`. No test relies on the removed symbols.
|
||||
- **Bench regression check.** `bench/check.py` /
|
||||
`bench/compile_check.py` re-run after 23.4. The mono pass does
|
||||
more work (two entry points, larger target sets per round); a
|
||||
measurable compile-time shift is expected and ratified per audit
|
||||
convention or rebaselined.
|
||||
|
||||
### 23.5 — Prelude free fns + E2E
|
||||
|
||||
- **Workspace tests per free fn:** `ne`, `lt`, `le`, `gt`, `ge`
|
||||
produce correct `Bool` on Int/Bool/Str, agree with their
|
||||
primitive-operator counterparts on a small smoke suite.
|
||||
- **Positive E2E** `examples/eq_ord_polymorphic.ail.json`:
|
||||
polymorphic helper invoked at three primitives, prints expected
|
||||
output, compiles and runs end-to-end.
|
||||
- **Negative E2E:** `eq f g` at Float typecheck-rejects with a
|
||||
Float-aware diagnostic; gold-standard test pins the message
|
||||
verbatim.
|
||||
- **User-ADT integration:** `examples/eq_ord_user_adt.ail.json` —
|
||||
`data IntBox = MkIntBox Int` + `instance Eq IntBox` +
|
||||
`instance Ord IntBox` + polymorphic helper monomorphises to the
|
||||
user instances.
|
||||
- **Round-trip:** prelude module + every new fixture passes
|
||||
Form-A parser + canonicaliser bit-stable.
|
||||
- **Bench regression check** at milestone close: the three bench
|
||||
scripts exit 0 or audit-ratified.
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
The milestone closes when:
|
||||
|
||||
1. **23.4 has landed:** `crates/ailang-check/src/mono.rs::monomorphise_workspace`
|
||||
synthesises both class-method and polymorphic-free-fn mono Defs
|
||||
in one fixpoint loop. `crates/ailang-codegen/src/lib.rs::lower_polymorphic_call` +
|
||||
`module_polymorphic_fns` + `mono_queue` are removed. Commits
|
||||
`a06159d` (prep2) + `c42a0f5` (prep3) are rolled back.
|
||||
2. **DESIGN.md §"Resolution and monomorphisation" amended:** the
|
||||
pass description covers all `Type::Forall`-quantified Defs, not
|
||||
only class methods.
|
||||
3. **23.5 has landed:** `examples/prelude.ail.json` contains `ne`,
|
||||
`lt`, `le`, `gt`, `ge` with correct constraint signatures and
|
||||
bodies.
|
||||
4. **DESIGN.md §"Decision 11 / Prelude classes" amended:** reflects
|
||||
Eq/Ord shipping in milestone 23; the "Milestone 22 ships no
|
||||
built-in Prelude classes" wording stays as historical accuracy
|
||||
with a forward-pointing addendum.
|
||||
5. **Tests pass:** `cargo test --workspace` green; existing
|
||||
polymorphic fixtures (`poly_id`, `poly_apply`, `poly_box_proj`)
|
||||
unchanged; new composition fixture (`cmp_max_smoke`) green; E2E
|
||||
fixtures from 23.5 green.
|
||||
6. **Bench regression ratified:** `bench/check.py && bench/compile_check.py && bench/cross_lang.py`
|
||||
exit 0 or audit-ratified with journal entry.
|
||||
7. **Surface acceptance from original spec:** a polymorphic helper
|
||||
`forall a. Ord a => (a, a) -> Bool` compiles, monomorphises at
|
||||
three primitive types, runs, and prints the expected output for
|
||||
at least Int and Str; the same helper on Float fires
|
||||
`NoInstance Ord Float` at typecheck with a Float-aware
|
||||
diagnostic.
|
||||
8. **Roadmap update:** P1 Post-22 Prelude entry from `[~]` to `[x]`
|
||||
for Eq/Ord half; Show half stays as a separate entry.
|
||||
|
||||
## Out of scope (deferred, with substantive rationale)
|
||||
|
||||
Unchanged from original spec:
|
||||
|
||||
- **`Show` typeclass.** Defers behind a heap-Str-ABI milestone.
|
||||
`instance Show Int` needs `int_to_str` to allocate a heap-Str —
|
||||
a runtime primitive AILang does not have today.
|
||||
- **Operator routing through `Eq` / `Ord`.** `==`, `<`, etc. stay
|
||||
primitive this milestone. Routing them through the class methods
|
||||
is the declared P2 todo, gated on bench rebaseline confirmation.
|
||||
- **`print`-rewire through `Show.show`.** Same heap-Str dependency.
|
||||
- **`Eq` / `Ord` on Float.** No instance per DESIGN.md §"Float
|
||||
semantics". A future iter exposing a partial
|
||||
`compare : Float -> Float -> Maybe Ordering` is a separate
|
||||
brainstorm.
|
||||
- **`deriving (Eq, Ord)` for user ADTs.** No auto-derivation.
|
||||
- **`Ord Ordering` instance.** Cute but no concrete demand.
|
||||
|
||||
New under B1 unification:
|
||||
|
||||
- **Higher-rank polymorphism.** Stays out of scope per DESIGN.md
|
||||
§"Polymorphism via Type::Forall" (line 2138-2140). The unified
|
||||
mono pass requires fully-concrete substitution at each call site;
|
||||
the same constraint as today, not weakened.
|
||||
- **Polymorphic constants** (`Type::Forall` on `ConstDef`). The mono
|
||||
pass operates on `Def::Fn`; `const_as_pseudo_fn` (mono.rs line
|
||||
261) is the only `ConstDef` bridge and stays unchanged.
|
||||
- **User-customisable mono-symbol naming.** The naming format is
|
||||
implementation-finalised in 23.4; no user-facing knob.
|
||||
|
||||
## Open commitments (23.4 / 23.5 implementer)
|
||||
|
||||
- **Mono-symbol naming for N-ary type vars.** Today's class-method
|
||||
naming `<method>__<typesurfacename>` is single-type-var.
|
||||
Polymorphic free fns can have N type vars (e.g. `poly_apply : forall a b.`).
|
||||
Default proposal: `<name>__<typename1>__<typename2>__…` in
|
||||
Forall-vars declaration order, hash-stable, covered by the
|
||||
canonical-type-names layer. Implementer may raise an alternative
|
||||
via `NEEDS_CONTEXT`.
|
||||
- **Target-collector heuristic.** `collect_mono_targets` (mono.rs
|
||||
line 422) today filters on residual class-constraints. For
|
||||
polymorphic free fns, the collector must additionally detect
|
||||
"call site to polymorphic free-fn `Def::Fn` with fully-concrete
|
||||
substitution, regardless of constraints". Implementer decides
|
||||
between extending the existing `synth`-residual path or adding a
|
||||
separate walker; both shapes are structurally viable.
|
||||
- **Original Free-Fn `Def::Fn` retention post-mono.** `Def::Class` /
|
||||
`Def::Instance` are kept in the workspace after mono (mono.rs
|
||||
line 40-42, for `ail describe`). Polymorphic Free-Fn `Def::Fn`s
|
||||
should be kept analogously — both the source-Def and the
|
||||
synthesised mono-Defs visible.
|
||||
- **Float-NoInstance diagnostic wording.** Implementer drafts a
|
||||
one-line Float-aware message; orchestrator reviews in
|
||||
spec-compliance phase.
|
||||
|
||||
## Known costs
|
||||
|
||||
- **23.4 mono refactor:** estimated +150 / −50 LOC in
|
||||
`crates/ailang-check/src/mono.rs` (target-collector extension,
|
||||
source-body entry points, naming helper).
|
||||
- **23.4 codegen cleanup:** estimated −200 LOC in
|
||||
`crates/ailang-codegen/src/lib.rs` (`lower_polymorphic_call`,
|
||||
`module_polymorphic_fns` fields, `mono_queue` machinery). Net
|
||||
code reduction expected.
|
||||
- **23.4 rollback:** `git revert a06159d c42a0f5` plus adaptation
|
||||
to the newly-dead code paths in codegen, estimated −80 LOC.
|
||||
- **23.5 prelude additions:** `examples/prelude.ail.json` +30-40
|
||||
lines (five free fns with Forall-constraint signatures and
|
||||
bodies). Three new E2E `.ail.json` fixtures, ~60 lines JSON.
|
||||
Diagnostic test ~20 lines Rust.
|
||||
- **Compile-time shift:** mono pass does more work (additional
|
||||
body walks over free fns, potentially larger fixpoint
|
||||
convergence). Quantified by `bench/compile_check.py` post-23.4;
|
||||
audit-ratified or rebaselined.
|
||||
- **DESIGN.md amendments:** §"Resolution and monomorphisation"
|
||||
(line 1513+) extends to cover polymorphic free fns; §"Decision
|
||||
11 / Prelude classes" (line 1659+) reflects Eq/Ord shipping.
|
||||
|
||||
## Load-bearing assumptions about current behaviour
|
||||
|
||||
Surfaced explicitly so the Step 7.5 grounding-check agent has a
|
||||
canonical list to ratify. Each assumption is something this spec
|
||||
relies on as currently-true.
|
||||
|
||||
1. `crates/ailang-check/src/mono.rs::monomorphise_workspace`
|
||||
today is the only typecheck-time specialiser, and it operates
|
||||
exclusively on class-method residuals (no free-fn handling).
|
||||
2. `crates/ailang-codegen/src/lib.rs::lower_polymorphic_call`
|
||||
today is the only codegen-time specialiser, and it operates
|
||||
exclusively on polymorphic free-fn calls (no class-method
|
||||
handling).
|
||||
3. The mono pass produces `Def::Fn` entries in the workspace; the
|
||||
codegen-time specialiser emits LLVM symbols without
|
||||
corresponding workspace Defs.
|
||||
4. `examples/prelude.ail.json` today contains no free fns (only
|
||||
ADT, classes, instances).
|
||||
5. Commits `a06159d` (prep2) and `c42a0f5` (prep3) added codegen
|
||||
bare-name fall-throughs that were anticipatory patches for the
|
||||
prelude free fns; they have no currently-active load-bearing
|
||||
case outside the still-not-shipped 23.4 free fns.
|
||||
6. Commit `8d39f13` (prep.1, linearity) and commit `aef4ab8`
|
||||
(prep.2, check bare-name) operate at typecheck / linearity time
|
||||
— before any mono pass — and are load-bearing for any prelude
|
||||
free-fn resolution regardless of mono architecture.
|
||||
7. `crates/ailang-codegen/src/lib.rs::lower_polymorphic_call` is
|
||||
invoked from two call sites today (lines 1944, 1972), both of
|
||||
which become direct mono-symbol calls after 23.4.
|
||||
8. `examples/poly_id.ail.json` and `examples/poly_apply.ail.json`
|
||||
today rely on the codegen-time specialiser path; under B1 they
|
||||
transition to the typecheck-time mono pass without surface
|
||||
behavioural change.
|
||||
9. The mono pass's fixpoint loop (mono.rs line 88) iterates until a
|
||||
round adds nothing new, and already supports transitive
|
||||
specialisation across nested class-method calls; the same
|
||||
mechanism handles a free-fn body whose specialisation triggers
|
||||
a class-method specialisation.
|
||||
10. The canonical-form layer (per
|
||||
`docs/specs/2026-05-10-canonical-type-names.md`, ct.4 closure)
|
||||
treats mono Defs as post-typecheck artefacts not in
|
||||
`CheckedModule.symbols`, so renaming or extending mono symbols
|
||||
does not affect surface-level hash pins.
|
||||
Reference in New Issue
Block a user