spec: env-construction unify — single source of truth for Env shape
This commit is contained in:
@@ -0,0 +1,242 @@
|
||||
# Env-construction unify — Design Spec
|
||||
|
||||
**Date:** 2026-05-10
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
|
||||
## Goal
|
||||
|
||||
Eliminate the structural drift between `check_in_workspace`
|
||||
(`crates/ailang-check/src/lib.rs`, near line 1059) and
|
||||
`mono::build_workspace_env` (`crates/ailang-check/src/mono.rs`,
|
||||
near line 367) — two paths that construct the same `Env` shape
|
||||
and have repeatedly diverged under feature pressure.
|
||||
|
||||
The empirical motivation is three consecutive bug fixes patching
|
||||
the same drift class at three different fields:
|
||||
|
||||
| Commit | Field forgotten by mono path | Iter |
|
||||
|--------|------------------------------|------|
|
||||
| `5c5180f` | `env.types`, `env.ctor_index` | 22c |
|
||||
| `13b36cc` | `env.globals` | post-22 debug |
|
||||
| `a9c685d` | `env.imports` | post-22 audit |
|
||||
|
||||
Each bug shipped as `ail check` passes / `ail build` fails with
|
||||
an env-table-miss in `monomorphise_workspace`. The pattern says a
|
||||
fourth field is one feature away.
|
||||
|
||||
## Architecture
|
||||
|
||||
A single source-of-truth function
|
||||
|
||||
```rust
|
||||
pub fn build_check_env(ws: &Workspace) -> Env
|
||||
```
|
||||
|
||||
in `crates/ailang-check/src/lib.rs` populates every workspace-flat
|
||||
`Env` field — that is, every field whose contents do not depend on
|
||||
a `current_module` overlay. Both existing entry points become thin
|
||||
consumers of this helper:
|
||||
|
||||
- `check_in_workspace` calls `build_check_env(ws)`, then applies
|
||||
the per-module overlay for the module it is checking
|
||||
(`current_module`, `globals` from `module_globals[m.name]`,
|
||||
`imports` from `m.imports`).
|
||||
- `mono::build_workspace_env` is a thin wrapper:
|
||||
`pub fn build_workspace_env(ws: &Workspace) -> Env { build_check_env(ws) }`.
|
||||
No additional seeding lives here. The per-module overlays in
|
||||
`collect_mono_targets` and `collect_residuals_ordered` (added in
|
||||
`13b36cc` and `a9c685d`) are already correctly placed at the
|
||||
per-fn call sites — they are not duplicated by this milestone,
|
||||
they stay where they are.
|
||||
|
||||
The split mirrors the semantic distinction:
|
||||
|
||||
- **Workspace-flat fields** are derivable from `Workspace` alone
|
||||
and do not change per call. They go in `build_check_env`.
|
||||
- **Per-module / per-fn overlay fields** depend on the call's
|
||||
`current_module` (or rigid vars). They stay at the call site.
|
||||
|
||||
After this refactor, when `synth` learns to read a new `Env`
|
||||
field, exactly one place needs the seeding edit.
|
||||
|
||||
## Components
|
||||
|
||||
**Files modified:**
|
||||
|
||||
- `crates/ailang-check/src/lib.rs` — adds
|
||||
`pub fn build_check_env(ws: &Workspace) -> Env`. Refactors
|
||||
`check_in_workspace` to call it and delete the now-duplicated
|
||||
inline seeding (effect_ops install, types, ctor_index,
|
||||
module_globals, module_types, class_methods,
|
||||
class_superclasses, workspace_registry, module_imports).
|
||||
`check_in_workspace` retains its per-module overlay logic
|
||||
(current_module, globals, imports for the module it is
|
||||
checking).
|
||||
- `crates/ailang-check/src/mono.rs` — `build_workspace_env`
|
||||
becomes a one-line wrapper around `build_check_env`. The
|
||||
drift-risk comment ("If `synth` starts reading a new `Env`
|
||||
field, update both paths") is deleted — there is no longer a
|
||||
pair of paths to keep in sync.
|
||||
|
||||
**Files added:**
|
||||
|
||||
- `crates/ailang-check/tests/env_construction_pin.rs` — a new
|
||||
integration test that pins the drift-shape invariant. See
|
||||
Testing strategy.
|
||||
|
||||
**Fields seeded by `build_check_env` (workspace-flat):**
|
||||
|
||||
- `effect_ops` — via `builtins::install`
|
||||
- `types` — workspace-flat from every `Def::Type`
|
||||
- `ctor_index` — workspace-flat from every `Def::Type`'s ctors
|
||||
- `module_globals` — per-module index built from
|
||||
`build_module_globals(ws)`
|
||||
- `module_types` — via `build_module_types(ws)`
|
||||
- `module_imports` — per-module index built from each
|
||||
`Workspace::modules.values().imports`
|
||||
- `class_methods` — workspace-merged from each module's
|
||||
`ModuleGlobals::class_methods`
|
||||
- `class_superclasses` — walk every `Def::Class` for
|
||||
`superclass`
|
||||
- `workspace_registry` — clone of `ws.registry`
|
||||
|
||||
**Fields not seeded by `build_check_env` (per-call overlay,
|
||||
applied by callers):**
|
||||
|
||||
- `current_module`
|
||||
- `globals`
|
||||
- `imports`
|
||||
- `rigid_vars`
|
||||
|
||||
## Data flow
|
||||
|
||||
```
|
||||
ws: &Workspace
|
||||
│
|
||||
▼
|
||||
build_check_env(ws) ─► Env (workspace-flat seeded)
|
||||
│
|
||||
├─► check_in_workspace(m: &Module):
|
||||
│ env.current_module = m.name
|
||||
│ seed env.globals from env.module_globals[m.name]
|
||||
│ build env.imports from m.imports
|
||||
│ run check on each Def in m
|
||||
│
|
||||
└─► mono::build_workspace_env(ws):
|
||||
return build_check_env(ws) verbatim
|
||||
(callers apply per-fn overlay)
|
||||
│
|
||||
▼
|
||||
collect_mono_targets / collect_residuals_ordered (per-fn):
|
||||
env.clone()
|
||||
env.current_module = module_name
|
||||
seed env.globals from env.module_globals[module_name]
|
||||
seed env.imports from env.module_imports[module_name]
|
||||
for v in fn rigids: env.rigid_vars.insert(v)
|
||||
run synth on body
|
||||
```
|
||||
|
||||
One construction; two consumers; per-fn overlays at the per-fn call sites.
|
||||
|
||||
## Error handling
|
||||
|
||||
No new error variants. The existing
|
||||
`build_module_globals(ws).expect(...)` call (used by
|
||||
`build_workspace_env` today) is a caller-contract panic that
|
||||
fires only if the mono pass is invoked on a workspace that has
|
||||
not passed typecheck — a programmer error, not a user error.
|
||||
That panic moves into `build_check_env` unchanged.
|
||||
|
||||
`build_check_env` has no fallible operations: every seeding step
|
||||
is a `clone` + `insert` into `BTreeMap` / `IndexMap`, all
|
||||
infallible.
|
||||
|
||||
User-facing diagnostics (`UnknownIdent`, `UnknownModule`,
|
||||
`UnknownType`, `UnknownCtor`) continue to fire at the same call
|
||||
sites in `synth`; the refactor changes the construction of `Env`,
|
||||
not its read paths.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
**Existing regression suite (drift class):** the three RED tests
|
||||
that pinned today's drift-class bugs run automatically and stay
|
||||
green:
|
||||
|
||||
- `crates/ail/tests/typeclass_22c.rs` — covers
|
||||
`env.types` / `env.ctor_index` (5c5180f).
|
||||
- `crates/ail/tests/mono_recursive_fn.rs` — covers
|
||||
`env.globals` (13b36cc).
|
||||
- `crates/ail/tests/mono_xmod_qualified_ref.rs` — covers
|
||||
`env.imports` (a9c685d).
|
||||
|
||||
If any of these regress after the refactor, the unify is broken
|
||||
and must not ship.
|
||||
|
||||
**New drift-shape pin test
|
||||
(`crates/ailang-check/tests/env_construction_pin.rs`):** a single
|
||||
integration test that:
|
||||
|
||||
1. Builds a representative class-bearing workspace fixture
|
||||
covering at least one `Def::Class`, one `Def::Instance`,
|
||||
one user ADT, and one cross-module import.
|
||||
2. Computes `env_a = build_check_env(&ws)` (the new helper).
|
||||
3. Computes `env_b` by running the inline construction the way
|
||||
`check_in_workspace` did pre-refactor — captured by reading
|
||||
the same code path and reproducing it inline in the test.
|
||||
(Practically: a small in-test helper that mirrors the
|
||||
pre-refactor seeding so the assertion has something to
|
||||
compare against.)
|
||||
4. Asserts that `env_a` and `env_b` agree on every workspace-flat
|
||||
field — same key-set, same per-key value (or, where types do
|
||||
not implement `PartialEq`, same key set).
|
||||
|
||||
The test serves as a tripwire: any future change that adds a new
|
||||
workspace-flat seed to one path but not the helper fails the
|
||||
test before it can ship a real bug.
|
||||
|
||||
**Bench gates:** `bench/check.py`, `bench/compile_check.py`,
|
||||
`bench/cross_lang.py` must each report 0 regressed. Performance
|
||||
of the refactor must be neutral — `build_check_env` is logically
|
||||
the same work as the pre-refactor inline.
|
||||
|
||||
**Workspace test suite:** `cargo test --workspace` must remain
|
||||
fully green (~344 tests).
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
1. `pub fn build_check_env(ws: &Workspace) -> Env` exists in
|
||||
`crates/ailang-check/src/lib.rs`.
|
||||
2. `mono::build_workspace_env` is a one-line wrapper: it calls
|
||||
`build_check_env(ws)` and returns the result. No inline
|
||||
seeding remains in this function.
|
||||
3. `check_in_workspace` calls `build_check_env(ws)` instead of
|
||||
inline workspace-flat seeding. Per-module overlay logic
|
||||
(current_module, globals, imports for the module being
|
||||
checked) remains.
|
||||
4. The drift-shape pin test
|
||||
(`crates/ailang-check/tests/env_construction_pin.rs`) is
|
||||
green.
|
||||
5. The three existing RED tests
|
||||
(`typeclass_22c`, `mono_recursive_fn`, `mono_xmod_qualified_ref`)
|
||||
remain green.
|
||||
6. `cargo test --workspace` is fully green.
|
||||
7. `bench/check.py`, `bench/compile_check.py`, `bench/cross_lang.py`
|
||||
each report 0 regressed.
|
||||
8. The `// Drift risk: this fn and `crate::check_in_workspace` both
|
||||
populate `crate::Env`. If `synth` starts reading a new `Env`
|
||||
field, update both paths.` comment in `mono.rs::build_workspace_env`
|
||||
is deleted (it no longer applies).
|
||||
|
||||
## Out of scope
|
||||
|
||||
- Pipeline-topology changes (e.g. moving the mono pass inside
|
||||
`check_workspace`). The pass-decomposition invariant — mono is
|
||||
post-typecheck / pre-codegen — stays.
|
||||
- Refactoring the per-module overlay shape. The
|
||||
`current_module` / `globals` / `imports` / `rigid_vars` overlay
|
||||
is semantically correct as it is and stays at the call site.
|
||||
- Primitive-name-set consolidation (still queued from 22-tidy).
|
||||
Different drift class, different milestone.
|
||||
- New env fields. This milestone preserves the current shape; it
|
||||
only changes who constructs it.
|
||||
Reference in New Issue
Block a user