# 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.