Brummel
832375f2ac
All 176 files in the four accumulating directories now use a zero-padded 4-digit counter prefix that reflects creation order (`NNNN-slug.md`). The counter is assigned per directory in strict git-log creation order; ties broken alphabetically by original name. The old `YYYY-MM-DD-` prefix on docs/specs/ and docs/plans/ files is dropped — the date is recoverable from git log and the counter carries the ordering. A file's counter is stable for the life of the file: never reassigned, never reused, never compacted. Deleted files retire their counter; subsequent files do not fill the gap. This is the property that lets cross-references stay literal — refs use the full filename including the counter (`design/contracts/0007-honesty-rule.md`) so they grep cleanly and resolve directly without a glob step. 313 cross-references updated across .md/.rs/.toml/.c/.json files (test pins, include_str! paths, design-INDEX entries, baseline notes, runtime C comments, inter-contract markdown links incl. bare basename and `../models/foo.md` forms). CLAUDE.md gets a new "File-naming convention" section spelling out the rule and rationale. skills/brainstorm/SKILL.md and skills/planner/SKILL.md updated so new spec/plan creation produces counter-prefixed names from the start. The full test suite (cargo test --workspace) passes.
628 lines
33 KiB
Markdown
628 lines
33 KiB
Markdown
# iter 24.tidy — close 5 actionable drift items from audit-24 — Implementation Plan
|
|
|
|
> **Parent spec:** `docs/journals/2026-05-13-audit-24.md` (the audit-24 drift report functions as the spec for this tidy iter — mirror of the `mq.tidy` pattern).
|
|
>
|
|
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement` to run this plan. Steps use `- [ ]` checkboxes for tracking.
|
|
|
|
**Goal:** Close the 5 actionable drift items audit-24 surfaced — documenting the three iter-24.3 strengthenings as load-bearing invariants in DESIGN.md, pinning the codegen import_map-fallback path with an integration test, asserting the dot-qualified-branch invariant for bare-name poly free fns, tightening the `unwrap_or_default()` method-name fallback to surface class-index drift, and extracting the duplicated `normalize_type_for_lookup` body into a single helper enforced by construction.
|
|
|
|
**Architecture:** This tidy iter is heterogeneous: one DESIGN.md doc-anchor (T1), two new integration test files (T2 + T3), one minimal-edit error-handling tightening (T4), one helper extraction across two `mono.rs` sites (T5), and one integration verification (T6). All five touch non-overlapping surfaces — the iter can be sequenced in any order, but the recommended order below ships the doc anchor first (lowest risk), refactors second (mechanical, T5), pins third (T2 + T3), tightens fourth (T4), verifies last (T6). No production semantic changes; the iter is documentation + test + refactor only.
|
|
|
|
**Tech Stack:** `docs/DESIGN.md` (one new subsection), `ailang-check` (one error-handling line + one helper extraction across two sites), two new `crates/ail/tests/*.rs` integration test files.
|
|
|
|
---
|
|
|
|
## Pre-flight notes (Boss-ratified post-recon)
|
|
|
|
**Recon-corrected line ranges.** Audit-24 named line ranges that recon verified post-iter-24.3:
|
|
- `mono.rs:687-696` → actual span is `:685-714` (full `for m in &fc.metas` loop).
|
|
- `mono.rs:1287-1294` → actual span is `:1284-1303` (full `.map(|m| ...)` collector).
|
|
- `check/lib.rs:2820-2865` → confirmed.
|
|
- `check/lib.rs:2852-2858` → confirmed, sits inside a `for c in constraints` loop emitting residuals (not nested in type-inference logic; structurally simple swap).
|
|
- `codegen/lib.rs:1980-2000, :2200-2244, :2776-2816` → confirmed; all three carry matching `// Iter 24.3:` comments naming each other (the iter-24.3 implementer already cross-referenced them).
|
|
|
|
**Boss decisions on recon-surfaced open questions:**
|
|
|
|
1. **T1 placement**: DESIGN.md has no top-level §"Monomorphisation" — it's a subsection of `## Decision 11: typeclasses` at line 1478 (`### Resolution and monomorphisation` at 1620). Insert a **new subsection** `### Cross-module references in synthesised bodies` between line 1693 (end of existing Monomorphisation paragraph) and line 1695 (`### Defaults and superclasses`). The new subsection groups the three iter-24.3 strengthenings as anchorable / citable invariants.
|
|
|
|
2. **T2 + T3 test placement**: Use **integration-style** tests in `crates/ail/tests/` (canonical pattern per `mono_xmod_qualified_ref.rs`, `mono_xmod_ctor_pattern.rs`). The codegen crate has rare in-crate tests (`crates/ailang-codegen/src/lib.rs:2990`, `escape.rs:477`); adding new `#[cfg(test)]` modules there would be inconsistent.
|
|
|
|
3. **T5 helper signature**: `apply_subst_and_normalize(env, module_name, m, subst) -> Option<Type>` — extracts only the common concrete-resolved arm. Each call site retains its own divergent rigid-var / unit-default policy: site 1 (`collect_mono_targets`) sets `has_rigid = true` + `break` when the helper returns `None` from a rigid path; site 2 (`collect_residuals_ordered`) returns `Type::unit()` when the helper returns `None`. The helper signature returning `Option<Type>` makes the divergence at the call sites explicit by construction.
|
|
|
|
**`Registry::normalize_type_for_lookup` signature** (from `crates/ailang-core/src/workspace.rs:127`):
|
|
```rust
|
|
pub fn normalize_type_for_lookup(&self, caller_module: &str, t: &Type) -> Type
|
|
```
|
|
|
|
---
|
|
|
|
## Files this plan creates or modifies
|
|
|
|
**Create:**
|
|
- `crates/ail/tests/codegen_import_map_fallback_pin.rs` — T2 pin: post-mono synthesised cross-module reference resolves via the import_map-fallback path.
|
|
- `crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` — T3 pin: bare-name poly-fn refs route through the dot-qualified branch (constraint-residual push fires).
|
|
|
|
**Modify:**
|
|
- `docs/DESIGN.md:1693-1695` — insert new subsection `### Cross-module references in synthesised bodies` documenting three iter-24.3 strengthenings.
|
|
- `crates/ailang-check/src/lib.rs:2852-2858` — replace `unwrap_or_default()` with explicit `.expect(...)`.
|
|
- `crates/ailang-check/src/mono.rs:685-714` + `:1284-1303` — replace duplicated normalization bodies with single helper call.
|
|
- `crates/ailang-check/src/mono.rs` (or a near anchor) — add the new `apply_subst_and_normalize` helper.
|
|
|
|
---
|
|
|
|
## Task 1: DESIGN.md — new subsection documenting iter-24.3 strengthenings
|
|
|
|
**Files:**
|
|
- Modify: `docs/DESIGN.md:1693-1695` — insert new subsection.
|
|
|
|
- [ ] **Step 1: Confirm DESIGN.md current state at the insertion point.**
|
|
|
|
Run: `sed -n '1690,1700p' docs/DESIGN.md`
|
|
|
|
Expected output: the end of the `### Resolution and monomorphisation` paragraph at line 1693, followed by line 1694 (likely blank), then `### Defaults and superclasses` at line 1695. If the structure differs (e.g. another subsection has been added since recon), adjust the insertion line.
|
|
|
|
- [ ] **Step 2: Insert the new subsection.**
|
|
|
|
Insert after line 1693 (after the closing paragraph of `### Resolution and monomorphisation`), before line 1695 (`### Defaults and superclasses`):
|
|
|
|
```markdown
|
|
|
|
### Cross-module references in synthesised bodies
|
|
|
|
The unified mono pass (per Decision 11's milestone-23.4 reorganisation)
|
|
synthesises mono symbols for polymorphic free fns and class-method
|
|
instances in the symbol's owner module — e.g. `print__Int` lives in
|
|
`prelude` (because `print` is defined in the prelude), but a
|
|
user-ADT call site `print (MkIntBox 7)` causes synthesis of
|
|
`prelude.print__IntBox` whose body references
|
|
`show_user_adt.show__IntBox` (the user instance lives in the
|
|
user-defining module per Decision 11 coherence). The synthesised body
|
|
crosses a module boundary the source template did not.
|
|
|
|
Three invariants make this work, all installed in milestone 24's iter
|
|
24.3 and worth keeping load-bearing:
|
|
|
|
1. **`MonoTarget::FreeFn::type_args` carries canonical types
|
|
post-collection.** At every site where `subst.apply(m)` produces a
|
|
concrete substitution that enters `MonoTarget::FreeFn::type_args`
|
|
(`crates/ailang-check/src/mono.rs::collect_mono_targets` and
|
|
`::collect_residuals_ordered`), the resolved `Type` must be passed
|
|
through `Registry::normalize_type_for_lookup(caller_module, &t)`
|
|
before being pushed. The downstream synthesised body's Phase 3
|
|
rewrite cursor (which runs in the OWNER module's context, not the
|
|
caller's) keys lookups in `Registry::entries` by the canonical
|
|
qualified form; a bare type-con reference at the type_args layer
|
|
silently drops the cross-module mono-symbol synthesis and leaves a
|
|
bare `Var "show"` post-mono that codegen later rejects with
|
|
`unknown variable`.
|
|
|
|
2. **Post-mono synthesised body cross-module references may bypass
|
|
the source template's `import_map`.** `prelude` does not import
|
|
user modules (the auto-injection runs one-way: user workspaces
|
|
import prelude, never the inverse). But a synthesised body for
|
|
`prelude.print__<UserType>` references `<user_module>.show__<UserType>`,
|
|
created by mono — not by the prelude source. Codegen's
|
|
cross-module name-resolution must accept this: at
|
|
`crates/ailang-codegen/src/lib.rs::resolve_top_level_fn` (Var-
|
|
resolution), `::lower_app`'s cross-module call arm, and
|
|
`::synth_with_extras`'s Var arm, the resolution first tries the
|
|
current module's `import_map`, then falls back to a direct
|
|
`module_user_fns` / `module_def_ail_types` lookup against the
|
|
prefix. Both ends were independently typechecked under their own
|
|
module contexts before mono ran; the cross-module reference is a
|
|
post-mono construct, not a source-language one.
|
|
|
|
3. **FreeFnCall synth pushes one residual per declared forall-
|
|
constraint.** At `crates/ailang-check/src/lib.rs`'s synth Var arm
|
|
for the `prefix.suffix` free-fn path, when the type is a
|
|
`Type::Forall { vars, constraints, body }`, instantiation produces
|
|
fresh metavars for the `vars` AND pushes one `ResidualConstraint`
|
|
per entry in `constraints` (with rigid vars substituted by the
|
|
freshly-generated metavars). The downstream discharge loop at
|
|
`check_fn`'s post-synth phase resolves each residual against the
|
|
workspace registry; if no instance satisfies the residual at the
|
|
unified concrete type, the `NoInstance` diagnostic fires at
|
|
typecheck (correctly), not at codegen (confusingly). Without the
|
|
residual push, milestone-23-shape negative cases (e.g. `print f`
|
|
where `f : Int -> Int`) silently typecheck and surface as
|
|
`unknown variable: show` from codegen instead of the right
|
|
typecheck-phase NoInstance Show.
|
|
|
|
The three invariants are lockstep partners: invariant (1) creates the
|
|
cross-module reference, invariant (2) makes codegen able to resolve
|
|
it, invariant (3) makes the typecheck-time discharge fire correctly
|
|
when no instance exists. A future refactor that loosens any one of
|
|
the three breaks the user-ADT trajectory; the test pins at
|
|
`crates/ail/tests/codegen_import_map_fallback_pin.rs` (invariant 2),
|
|
`crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` (invariant 3
|
|
+ lockstep), and the existing `crates/ail/tests/show_user_adt`
|
|
fixture (full trajectory) collectively protect the contract.
|
|
```
|
|
|
|
- [ ] **Step 3: Verify DESIGN.md still parses.**
|
|
|
|
Run: `wc -l docs/DESIGN.md`
|
|
|
|
Expected: line count grew by ~50-55 lines compared to post-iter-24.3 baseline (was at ~2707-2710 lines).
|
|
|
|
Run: `sed -n '1693,1755p' docs/DESIGN.md`
|
|
|
|
Expected: new `### Cross-module references in synthesised bodies` subsection visible, terminated by the existing `### Defaults and superclasses` header.
|
|
|
|
---
|
|
|
|
## Task 2: Codegen import_map-fallback path pin
|
|
|
|
**Files:**
|
|
- Create: `crates/ail/tests/codegen_import_map_fallback_pin.rs` — integration-style test.
|
|
|
|
- [ ] **Step 1: Read the canonical xmod-integration-test pattern.**
|
|
|
|
Run: `head -60 crates/ail/tests/mono_xmod_qualified_ref.rs`
|
|
|
|
Confirm: the file loads a workspace via `load_workspace`, runs `check_workspace` + `monomorphise_workspace`, then either inspects post-mono state OR runs `ail build` for full E2E. The pattern's signature features are: workspace from `examples/`, post-mono inspection assertions, doc-comment header naming the regression.
|
|
|
|
- [ ] **Step 2: Write the test file.**
|
|
|
|
Note: the existing `examples/show_user_adt.ail.json` fixture already exercises the import_map-fallback path end-to-end. The pin's job is to make the failure mode visible at unit-test granularity: when codegen tightens `resolve_top_level_fn` back to import_map-only, the pin fires with a localised assertion BEFORE the E2E reports a cryptic build failure.
|
|
|
|
```rust
|
|
//! Pin for the iter-24.3 codegen `import_map`-fallback path
|
|
//! (DESIGN.md §"Cross-module references in synthesised bodies"
|
|
//! invariant 2).
|
|
//!
|
|
//! Property protected: post-mono synthesised body cross-module
|
|
//! references resolve at codegen via the fallback to
|
|
//! `module_user_fns` / `module_def_ail_types` when the prefix is
|
|
//! NOT in the current module's `import_map`. Specifically, the
|
|
//! synthesised `prelude.print__<UserType>` body references
|
|
//! `<user_module>.show__<UserType>` even though `prelude` does not
|
|
//! import user modules.
|
|
//!
|
|
//! Failure mode this pin catches: a future codegen refactor
|
|
//! tightens `resolve_top_level_fn` or `lower_app`'s cross-module
|
|
//! arm or `synth_with_extras`'s Var arm back to `import_map`-only.
|
|
//! Without this pin, the regression surfaces only at the
|
|
//! `show_user_adt` E2E (which builds + runs a binary, slow to
|
|
//! bisect).
|
|
|
|
use ailang_check::{check_workspace, monomorphise_workspace};
|
|
use ailang_core::ast::{Def, Term};
|
|
use ailang_core::workspace::load_workspace;
|
|
use std::path::PathBuf;
|
|
|
|
fn fixture_path() -> PathBuf {
|
|
PathBuf::from(env!("CARGO_MANIFEST_DIR"))
|
|
.join("../../examples")
|
|
.join("show_user_adt.ail.json")
|
|
}
|
|
|
|
#[test]
|
|
fn synthesised_print_uses_user_module_show_via_fallback() {
|
|
// Step 1: workspace loads + typechecks clean.
|
|
let ws = load_workspace(&fixture_path()).expect("workspace loads");
|
|
let diags = check_workspace(&ws);
|
|
assert!(
|
|
diags.is_empty(),
|
|
"typecheck diagnostics in show_user_adt fixture: {diags:?}"
|
|
);
|
|
|
|
// Step 2: mono synthesis produces `prelude.print__<IntBox>` whose
|
|
// body references `show_user_adt.show__<IntBox>` (cross-module).
|
|
// The exact type-suffix is content-addressed; we look for a
|
|
// `Def::Fn` whose name starts with `print__` AND whose body
|
|
// contains a `Term::Var { name: "show_user_adt.<suffix>" }` (or
|
|
// analogous post-mono shape with the fully-qualified suffix).
|
|
let post_mono = monomorphise_workspace(&ws).expect("mono green");
|
|
let prelude_mod = post_mono
|
|
.modules
|
|
.get("prelude")
|
|
.expect("prelude post-mono module present");
|
|
|
|
let print_def = prelude_mod
|
|
.defs
|
|
.iter()
|
|
.find_map(|d| match d {
|
|
Def::Fn(f) if f.name.starts_with("print__") => Some(f),
|
|
_ => None,
|
|
})
|
|
.expect("synthesised print__<UserType> not found in prelude post-mono module");
|
|
|
|
// Step 3: recursively walk `print_def.body` looking for a Var
|
|
// whose name carries the `show_user_adt.` prefix (the cross-
|
|
// module reference invariant 2 protects).
|
|
fn contains_xmod_show_var(t: &Term) -> bool {
|
|
match t {
|
|
Term::Var { name } => {
|
|
name.starts_with("show_user_adt.") && name.contains("show__")
|
|
}
|
|
Term::Let { value, body, .. } => {
|
|
contains_xmod_show_var(value) || contains_xmod_show_var(body)
|
|
}
|
|
Term::App { fn: f, args } => {
|
|
contains_xmod_show_var(f) || args.iter().any(contains_xmod_show_var)
|
|
}
|
|
Term::Do { args, .. } => args.iter().any(contains_xmod_show_var),
|
|
Term::Lam { body, .. } => contains_xmod_show_var(body),
|
|
_ => false,
|
|
}
|
|
}
|
|
|
|
assert!(
|
|
contains_xmod_show_var(&print_def.body),
|
|
"synthesised print body should contain a `show_user_adt.<suffix>` Var \
|
|
referencing the user-module's show__<IntBox> mono symbol — \
|
|
this is the cross-module reference codegen resolves via the \
|
|
import_map-fallback path. Body: {:?}",
|
|
print_def.body
|
|
);
|
|
|
|
// Step 4: confirm prelude module's `imports` does NOT contain
|
|
// `show_user_adt` — the resolution at codegen time genuinely
|
|
// bypasses the source template's import_map.
|
|
let prelude_src = ws
|
|
.modules
|
|
.get("prelude")
|
|
.expect("prelude source module present");
|
|
assert!(
|
|
prelude_src
|
|
.imports
|
|
.iter()
|
|
.all(|imp| imp != "show_user_adt"),
|
|
"prelude must not import show_user_adt (the invariant is that \
|
|
codegen resolves the cross-module ref WITHOUT going through \
|
|
import_map). Got imports: {:?}",
|
|
prelude_src.imports
|
|
);
|
|
}
|
|
```
|
|
|
|
If the AST `Term` variants are named differently (e.g. `Term::Application` vs `Term::App`), adjust the pattern match. The load-bearing assertions are (a) the synthesised body contains a cross-module Var reference whose prefix is the user module, and (b) the prelude source-level module does not import the user module.
|
|
|
|
If the `WorkspaceModule` struct does not expose an `imports` field directly (recon did not verify this), the implementer adapts to the actual field name (could be `module_imports`, `deps`, or accessed via a method).
|
|
|
|
- [ ] **Step 3: Run the test.**
|
|
|
|
Run: `cargo test --workspace --no-fail-fast -p ail --test codegen_import_map_fallback_pin 2>&1 | tail -10`
|
|
|
|
Expected: `test result: ok. 1 passed`.
|
|
|
|
If the test fails with "synthesised print__<UserType> not found": the iter-24.3 mono synthesis path was inadvertently broken; the implementer should NOT just adjust the test — surface to Boss because invariant 1 from Task 1 is at risk.
|
|
|
|
If the test fails with "synthesised print body should contain a `show_user_adt.<suffix>` Var": the mono synthesis is producing the symbol but the body does not reference the user module — likely the iter-24.3 strengthening at `mono.rs::collect_mono_targets` was reverted or the test's recursive walker is missing a Term variant. Read the actual `print_def.body` shape from the failure message and adapt the walker.
|
|
|
|
---
|
|
|
|
## Task 3: Bare-name poly-fn dot-qualified-branch invariant pin
|
|
|
|
**Files:**
|
|
- Create: `crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` — integration-style test.
|
|
|
|
- [ ] **Step 1: Write the test file.**
|
|
|
|
The invariant per audit-24 [high-3]: "poly free fns always reach synth via the dot-qualified branch". For prelude poly fns (`ne`/`lt`/`le`/`gt`/`ge`/`print`), the auto-injected prelude path makes bare-name references resolve via the `prefix.suffix` synth arm internally. The pin asserts the observable consequence: calling a prelude poly fn by bare name AT A CONCRETE TYPE (where the constraint is satisfied) succeeds, AND calling it at a TYPE WITH NO INSTANCE fails with the NoInstance diagnostic (proving the constraint-residual push fired even via bare-name path).
|
|
|
|
This pin overlaps slightly with the existing `show_print_e2e` (positive) and `show_no_instance_e2e` (negative) tests — but those run via `ail build` / `check_workspace` on the show fixtures. The new pin uses a synthetic minimal fixture that exercises the bare-name path explicitly and asserts on the synth-level outcome (residual count or diagnostic presence) rather than full E2E.
|
|
|
|
```rust
|
|
//! Pin for the iter-24.3 FreeFnCall constraint-residual-push
|
|
//! invariant (DESIGN.md §"Cross-module references in synthesised
|
|
//! bodies" invariant 3).
|
|
//!
|
|
//! Property protected: bare-name references to polymorphic free fns
|
|
//! that resolve through the auto-injected-prelude path AT THE
|
|
//! DOT-QUALIFIED SYNTH BRANCH push residuals for the fn's declared
|
|
//! constraints. The discharge loop then fires `NoInstance` at
|
|
//! typecheck if no instance ships for the unified concrete type.
|
|
//!
|
|
//! Failure mode this pin catches: a future refactor changes the
|
|
//! prelude auto-injection resolution path so that bare-name `print`
|
|
//! reaches synth via a different branch (e.g. locals, env.module_globals
|
|
//! direct hit) that does NOT push residuals. Without this pin, the
|
|
//! regression surfaces as `unknown variable: show` from codegen for
|
|
//! the negative case — confusing diagnostic, hard to bisect.
|
|
|
|
use ailang_check::check_workspace;
|
|
use ailang_core::workspace::load_workspace;
|
|
use std::path::PathBuf;
|
|
|
|
fn fixture_path() -> PathBuf {
|
|
PathBuf::from(env!("CARGO_MANIFEST_DIR"))
|
|
.join("../../examples")
|
|
.join("show_no_instance.ail.json")
|
|
}
|
|
|
|
#[test]
|
|
fn bare_name_polyfn_fires_typecheck_no_instance_not_codegen_unknown_var() {
|
|
// The fixture calls `print f` bare-name (no `prelude.` qualifier)
|
|
// where `f : Int -> Int`. The auto-injected-prelude resolution
|
|
// must route this through the dot-qualified synth branch so that
|
|
// the `Show a` declared constraint of `print` produces a residual,
|
|
// and the discharge loop fires `no-instance`.
|
|
let ws = load_workspace(&fixture_path()).expect("workspace loads");
|
|
let diags = check_workspace(&ws);
|
|
|
|
// Exactly one `no-instance` diagnostic — proves:
|
|
// (a) the bare-name `print` resolved (was not "unknown variable")
|
|
// (b) the resolution reached the dot-qualified synth branch
|
|
// which pushes the declared-constraint residual
|
|
// (c) the discharge loop ran with the residual and fired the
|
|
// NoInstance because no `Show (Int -> Int)` instance exists.
|
|
let no_inst: Vec<_> = diags.iter().filter(|d| d.code == "no-instance").collect();
|
|
assert_eq!(
|
|
no_inst.len(),
|
|
1,
|
|
"expected exactly one 'no-instance' diagnostic — got {} (all diags: {diags:?})",
|
|
no_inst.len()
|
|
);
|
|
|
|
// No "unknown variable" or other codegen-grade errors at typecheck:
|
|
// if the residual push did NOT fire, the typecheck would pass
|
|
// silently and the error would only surface at codegen.
|
|
let unknown_vars: Vec<_> = diags
|
|
.iter()
|
|
.filter(|d| {
|
|
d.code == "unknown-variable"
|
|
|| d.message.contains("unknown variable")
|
|
|| d.code == "internal"
|
|
})
|
|
.collect();
|
|
assert!(
|
|
unknown_vars.is_empty(),
|
|
"expected zero 'unknown variable' or 'internal' diagnostics at typecheck — \
|
|
got {} (all diags: {diags:?}). If this fires, the bare-name `print` \
|
|
resolution bypassed the dot-qualified synth branch and the constraint \
|
|
residual was never pushed.",
|
|
unknown_vars.len()
|
|
);
|
|
}
|
|
```
|
|
|
|
The pin's load-bearing assertions are: (a) exactly one `no-instance` diagnostic fires (proving the residual push reached the discharge); (b) zero `unknown-variable` / `internal` diagnostics (proving the bare-name `print` resolved at typecheck rather than silently slipping through to codegen).
|
|
|
|
If the diagnostic `.code` field names differ (e.g. `no_instance` rather than `no-instance`, or `unknown_var` rather than `unknown-variable`), adjust to match what `crates/ail/tests/show_no_instance_e2e.rs` already uses (the iter-24.3 implementer verified that code).
|
|
|
|
- [ ] **Step 2: Run the test.**
|
|
|
|
Run: `cargo test --workspace --no-fail-fast -p ail --test polyfn_dot_qualified_branch_pin 2>&1 | tail -10`
|
|
|
|
Expected: `test result: ok. 1 passed`.
|
|
|
|
If `expected exactly one 'no-instance' diagnostic — got 0`: the FreeFnCall constraint-residual push at `check/lib.rs:2820-2865` was reverted or the bare-name resolution bypassed it. Surface to Boss because invariant 3 from Task 1 is at risk.
|
|
|
|
If `expected zero 'unknown variable' diagnostics`: the typecheck-time NoInstance is firing but ALSO an unknown-var is firing — the synthesised body's mono-symbol rewrite did not happen, suggesting invariant 1 (canonical-form `type_args`) is at risk.
|
|
|
|
---
|
|
|
|
## Task 4: Replace `unwrap_or_default()` with explicit `.expect(...)`
|
|
|
|
**Files:**
|
|
- Modify: `crates/ailang-check/src/lib.rs:2852-2858`.
|
|
|
|
- [ ] **Step 1: Read the current shape.**
|
|
|
|
Run: `sed -n '2846,2865p' crates/ailang-check/src/lib.rs`
|
|
|
|
Confirm: the `for c in constraints` loop contains a `.find_map` block producing `Option<String>` for the method name, with `.unwrap_or_default()` extracting it. The surrounding code constructs a `ResidualConstraint { class, type_, method, candidates: None }`.
|
|
|
|
- [ ] **Step 2: Swap the fallback.**
|
|
|
|
Use Edit tool to replace the `unwrap_or_default()` call with an explicit `.expect(...)` carrying the registry-coherence message:
|
|
|
|
Concretely (adapting to the actual `let method_name = ...` line shape at :2852):
|
|
|
|
```rust
|
|
let method_name = env
|
|
.class_methods
|
|
.iter()
|
|
.find_map(|((cls, m), _)| {
|
|
if *cls == c_class { Some(m.clone()) } else { None }
|
|
})
|
|
.expect(
|
|
"class_methods registry coherence — a declared constraint's \
|
|
class is missing from env.class_methods. The pre-pass \
|
|
`MissingClass` diagnostic should have rejected this earlier; \
|
|
reaching here means workspace-registry / class-index drift. \
|
|
Surface to debug skill rather than silently render NoInstance \
|
|
with an empty method name.",
|
|
);
|
|
```
|
|
|
|
The exact pattern of the `find_map` arm depends on the actual `class_methods` key type — the recon confirmed it's `(class_name: String, method_name: String) -> ClassMethodInfo`. If the iteration shape uses a different destructuring, adapt to match.
|
|
|
|
- [ ] **Step 3: Run the full workspace test to confirm no regression.**
|
|
|
|
Run: `cargo test --workspace --no-fail-fast 2>&1 | tail -5`
|
|
|
|
Expected: `test result: ok. 556 passed; 0 failed`.
|
|
|
|
If any test fails with the new `.expect(...)` panic message: the registry-coherence invariant was already being violated somewhere — the `unwrap_or_default()` was masking a real bug. Read the panic trace from the failure and decide:
|
|
- (a) the violation is in test fixture setup → fix the fixture
|
|
- (b) the violation is in production code → surface to Boss, this is a real registry/index drift bug
|
|
|
|
If 556 tests pass: the `.expect(...)` is a strict tightening; no regression.
|
|
|
|
---
|
|
|
|
## Task 5: Extract `apply_subst_and_normalize` helper
|
|
|
|
**Files:**
|
|
- Modify: `crates/ailang-check/src/mono.rs:685-714` + `:1284-1303` — replace duplicated bodies with helper calls.
|
|
- Modify: `crates/ailang-check/src/mono.rs` — add new helper definition near the existing `normalize_type_for_lookup` callers (or at the top of the file alongside other private helpers).
|
|
|
|
- [ ] **Step 1: Read both call sites.**
|
|
|
|
Run: `sed -n '685,716p' crates/ailang-check/src/mono.rs`
|
|
|
|
Confirm: this is site 1, the `for m in &fc.metas` loop in `collect_mono_targets`. The block has three branches: concrete → normalise + push; rigid → break + set `has_rigid`; otherwise → (default behaviour, possibly continue).
|
|
|
|
Run: `sed -n '1284,1305p' crates/ailang-check/src/mono.rs`
|
|
|
|
Confirm: this is site 2, the `.map(|m| ...)` collector. The block has two branches: concrete → normalise; otherwise → `Type::unit()`.
|
|
|
|
- [ ] **Step 2: Write the helper.**
|
|
|
|
Add the helper near the top of `mono.rs` (after the imports / type defs but before `collect_mono_targets`):
|
|
|
|
```rust
|
|
/// Apply the current substitution to a meta and, if the result is
|
|
/// fully concrete, normalise it to canonical-form for registry lookup.
|
|
///
|
|
/// Returns `Some(normalised)` if the meta resolves to a concrete type;
|
|
/// `None` if it does not (rigid var or unbound meta — the caller
|
|
/// decides the policy: break with `has_rigid = true` at the FreeFn
|
|
/// target-collection site, or `Type::unit()`-default at the residual-
|
|
/// ordering site).
|
|
///
|
|
/// Iter 24.tidy: extracted from two byte-identical call sites at
|
|
/// `collect_mono_targets` and `collect_residuals_ordered` per
|
|
/// audit-24's [medium-2] drift item. The byte-identity invariant
|
|
/// (Phase 2 synthesis name must match Phase 3 rewrite cursor's
|
|
/// lookup name) is now enforced by construction.
|
|
fn apply_subst_and_normalize(
|
|
env: &Env,
|
|
module_name: &str,
|
|
m: &MetaVar,
|
|
subst: &Subst,
|
|
) -> Option<Type> {
|
|
let resolved = subst.apply(m);
|
|
if crate::is_fully_concrete(&resolved) {
|
|
Some(env.workspace_registry.normalize_type_for_lookup(module_name, &resolved))
|
|
} else {
|
|
None
|
|
}
|
|
}
|
|
```
|
|
|
|
Adapt the parameter types to the actual signatures (`&Env`, `&MetaVar`, `&Subst`) — recon confirmed the funnel is `env.workspace_registry.normalize_type_for_lookup(module_name, &resolved)`. If `Env` is a different type name in this scope (e.g. `CheckEnv`, `WorkspaceState`), the implementer adapts.
|
|
|
|
If `Subst` is not in scope at the helper insertion point, the helper may need to live inside an impl block on the type that owns the substitution context, OR take it as `&Subst<...>`-generic if it's parametric.
|
|
|
|
- [ ] **Step 3: Replace site 1 (`collect_mono_targets`).**
|
|
|
|
Replace the existing `for m in &fc.metas { let resolved = subst.apply(m); ... }` block with:
|
|
|
|
```rust
|
|
for m in &fc.metas {
|
|
match apply_subst_and_normalize(env, module_name, m, subst) {
|
|
Some(normalised) => type_args.push(normalised),
|
|
None => {
|
|
if contains_rigid_var(&subst.apply(m)) {
|
|
has_rigid = true;
|
|
break;
|
|
}
|
|
// Unbound meta (neither concrete nor rigid): default policy
|
|
// is fall through to existing behaviour at this site.
|
|
// (The original code had no explicit `else` arm after the
|
|
// rigid check — the for loop simply continues to the next
|
|
// meta without pushing. The new shape preserves this.)
|
|
}
|
|
}
|
|
}
|
|
```
|
|
|
|
The exact policy after "neither concrete nor rigid" depends on the original code's pre-extraction behaviour — recon noted "site 1 sets has_rigid = true and breaks" for the rigid path but did not enumerate the unbound-meta path. The implementer reads the pre-extraction block and preserves whatever the original did (likely a `continue` without push).
|
|
|
|
- [ ] **Step 4: Replace site 2 (`collect_residuals_ordered`).**
|
|
|
|
Replace the existing `.map(|m| { let resolved = subst.apply(m); ... })` block with:
|
|
|
|
```rust
|
|
.map(|m| {
|
|
apply_subst_and_normalize(env, module_name, m, subst)
|
|
.unwrap_or_else(Type::unit)
|
|
})
|
|
```
|
|
|
|
The `unwrap_or_else(Type::unit)` preserves the existing fallback semantics for the non-concrete path.
|
|
|
|
- [ ] **Step 5: Run the full workspace test to confirm byte-identity preserved.**
|
|
|
|
Run: `cargo test --workspace --no-fail-fast 2>&1 | tail -5`
|
|
|
|
Expected: `test result: ok. 556 passed; 0 failed`.
|
|
|
|
The byte-identity invariant means the mono-symbol names produced post-extraction MUST match the names produced pre-extraction. If `mono_hash_stability::primitive_eq_ord_mono_symbol_hashes_stay_bit_identical` or `primitive_show_mono_symbol_hashes_stay_bit_identical` fail, the extraction inadvertently changed the normalisation form. Diagnose by running:
|
|
|
|
`cargo test --workspace --no-fail-fast -p ail --test mono_hash_stability 2>&1 | tail -15`
|
|
|
|
If hashes drifted: revert and re-do the extraction more carefully — the helper must produce byte-identical output to the inlined code it replaces.
|
|
|
|
---
|
|
|
|
## Task 6: Integration verification + bench
|
|
|
|
**Files:** none modified; verification-only.
|
|
|
|
- [ ] **Step 1: Full workspace test.**
|
|
|
|
Run: `cargo test --workspace --no-fail-fast 2>&1 | grep -E '^test result' | awk '{s+=$4; f+=$6} END {print "passed:", s, "failed:", f}'`
|
|
|
|
Expected: `passed: 558 failed: 0` — 556 from iter 24.3 + 2 new (codegen_import_map_fallback_pin + polyfn_dot_qualified_branch_pin).
|
|
|
|
If `failed` is non-zero, diagnose via `cargo test --workspace --no-fail-fast 2>&1 | grep -B2 FAILED | head -30`.
|
|
|
|
- [ ] **Step 2: Confirm milestone-24 specific tests stay green.**
|
|
|
|
Run: `cargo test --workspace --no-fail-fast 2>&1 | grep -E '(show_|print_).*FAILED|prelude_free_fns.*FAILED|mono_hash_stability.*FAILED|typeclass_22b.*FAILED|mq3.*FAILED' | head -10`
|
|
|
|
Expected: empty (no FAILED entries for these test groups).
|
|
|
|
- [ ] **Step 3: Bench scripts.**
|
|
|
|
Run: `bench/compile_check.py 2>&1 | tail -10`
|
|
|
|
Expected: exit 0 OR exit 1 with documented noise-class metrics per audit-24's 9th-consecutive-observation lineage.
|
|
|
|
Run: `bench/cross_lang.py 2>&1 | tail -10`
|
|
|
|
Expected: exit 0; 25/25 stable.
|
|
|
|
Run: `bench/check.py 2>&1 | tail -15`
|
|
|
|
Expected: exit 0 OR exit 1 with `latency.implicit_at_rc.*` / `latency.explicit_at_rc.*` / `bench_list_sum.bump_s` noise per the documented lineage. Conservative call: baseline pristine — extends the lineage to 10th consecutive observation if exit 1.
|
|
|
|
If any bench script exits non-zero on a metric NOT in the documented noise envelope, surface to Boss for audit-ratification or rebaseline.
|
|
|
|
- [ ] **Step 4: Write the per-iter journal.**
|
|
|
|
Path: `docs/journals/2026-05-13-iter-24.tidy.md`
|
|
|
|
Structure (matching mq.tidy journal pattern):
|
|
- `# iter 24.tidy — close 5 actionable drift items from audit-24`
|
|
- `**Date:** 2026-05-13`
|
|
- `**Started from:** 71dec14`
|
|
- `**Status:** DONE`
|
|
- `**Tasks completed:** 6 of 6`
|
|
- Summary paragraph
|
|
- Per-task notes (T1 placement + content; T2 pin observables; T3 pin observables; T4 expect message + any incidental fixture repairs; T5 helper signature + lockstep argument; T6 bench-lineage continuation)
|
|
- Concerns section (the recon-Boss reconciliation if any; the helper-extraction policy decision; any test-pin assertion approximations)
|
|
- Known debt (audit's [medium-3] negative-test coverage → P3; [low-1] bench sweep noise → carry-on)
|
|
- Files touched (list)
|
|
- Stats: `bench/orchestrator-stats/2026-05-13-iter-24.tidy.json`
|
|
|
|
Append the index line to `docs/journals/INDEX.md`:
|
|
`- 2026-05-13 — iter 24.tidy: close 5 actionable drift items from audit-24 (DESIGN.md doc-anchor + 2 codegen/synth pins + expect-tightening + helper extraction) → 2026-05-13-iter-24.tidy.md`
|
|
|
|
---
|
|
|
|
## Self-review checklist (planner Step 5)
|
|
|
|
**Spec coverage:**
|
|
- audit-24 [high-1] → Task 1 ✓
|
|
- audit-24 [high-2] → Task 2 ✓
|
|
- audit-24 [high-3] → Task 3 (documented-invariant path per Boss decision) ✓
|
|
- audit-24 [medium-1] → Task 4 ✓
|
|
- audit-24 [medium-2] → Task 5 ✓
|
|
- audit-24 [medium-3] → not in scope (defers to P3) — confirmed in carrier ✓
|
|
- audit-24 [low-1] → not in scope (carry-on) — confirmed in carrier ✓
|
|
- Integration verification → Task 6 ✓
|
|
|
|
**Placeholder scan:** the "If `Env` is a different type name in this scope" / "If `Subst` is not in scope" notes in Task 5 Step 2 are explicit adaptation instructions, not TBDs — the implementer reads the actual types and adapts. The "default policy is fall through to existing behaviour at this site" note in Task 5 Step 3 instructs the implementer to read the original code and preserve its semantics — also adaptation, not TBD. No genuine TBDs.
|
|
|
|
**Type consistency:** `apply_subst_and_normalize`, `normalize_type_for_lookup`, `class_methods`, `ResidualConstraint`, `MonoTarget::FreeFn::type_args`, `import_map`, `module_user_fns`, `module_def_ail_types`, `show__T`, `print__T`, `show_user_adt`, `prelude.Show`, `Type::Forall`, `Type::unit`, `Term::Var`/`Let`/`App`/`Do`/`Lam` — all consistent across tasks.
|
|
|
|
**Step granularity:** every step is a single discrete action (file read, single Edit, single test run, single command). The longest is Task 5 Step 3 (replace site 1 block) at ~5 minutes if the original code has subtle branching the helper must preserve.
|
|
|
|
**No commit steps:** none of the 6 tasks include `git commit`. The Boss commits at iter close per CLAUDE.md.
|