diff --git a/docs/specs/2026-05-10-env-construction-unify.md b/docs/specs/2026-05-10-env-construction-unify.md
new file mode 100644
index 0000000..3779039
--- /dev/null
+++ b/docs/specs/2026-05-10-env-construction-unify.md
@@ -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.