diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index 11c0379..62b33b1 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -1176,12 +1176,18 @@ fn check_in_workspace(
     ws: &Workspace,
     module_globals: &BTreeMap<String, ModuleGlobals>,
 ) -> Vec<CheckError> {
-    let mut env = Env::new();
-    builtins::install(&mut env);
+    let mut env = build_check_env(ws);
     let mut errors: Vec<CheckError> = Vec::new();
 
-    // Register type defs (local per module; cross-module ADT sharing is
-    // explicitly not part of 5b).
+    // Per-module overlay for `env.types` / `env.ctor_index`:
+    // `build_check_env` populates these workspace-flat for the
+    // mono pass, but `check_def` (specifically `Pattern::Ctor`'s
+    // local-first / imports-fallback resolution at the qualified
+    // type-name path) expects only THIS module's local entries.
+    // Clear and rebuild per-module, with the original fail-fast
+    // duplicate diagnostics in-band.
+    env.types.clear();
+    env.ctor_index.clear();
     for def in &m.defs {
         if let Def::Type(td) = def {
             if env.types.contains_key(&td.name) {
@@ -1205,79 +1211,31 @@ fn check_in_workspace(
                 }
                 env.ctor_index.insert(
                     c.name.clone(),
-                    CtorRef {
-                        type_name: td.name.clone(),
-                    },
+                    CtorRef { type_name: td.name.clone() },
                 );
             }
             env.types.insert(td.name.clone(), td.clone());
         }
     }
 
-    // Take local globals from the previously built table. Iter 22b.2:
-    // class methods sit in `g.class_methods` and reach the env through
-    // a separate channel in Tasks 9 / 10; here we only seed the HM
-    // monomorphic name table from `g.fns`.
+    // Per-module overlay for `globals`: `build_check_env` installed
+    // builtins operators workspace-flat; here we add this module's
+    // top-level fns from the previously built table.
     if let Some(g) = module_globals.get(&m.name) {
         for (n, t) in &g.fns {
             env.globals.insert(n.clone(), t.clone());
         }
     }
 
-    // Build import map: alias (or module name, if without alias) →
-    // module name. Conflicts are not allowed in the MVP: the same `as`
-    // clause twice would stand out and should surface as a duplicate
-    // symbol name — currently "last wins", because Iter 5b doesn't
-    // introduce a dedicated diagnostic for it; if needed later →
-    // `ambiguous-import` code.
+    // Per-module overlay for `imports`: alias-or-name -> module-name
+    // map for THIS module's import list.
     let mut import_map: BTreeMap<String, String> = BTreeMap::new();
     for imp in &m.imports {
         let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
         import_map.insert(key, imp.module.clone());
     }
     env.imports = import_map;
-    // Iter 22b.2: project to the legacy `IndexMap<String, Type>` shape
-    // so the cross-module qualified-var resolution path keeps its
-    // pre-22b.2 form. Class methods are not addressable through the
-    // qualified-var channel — they go through the per-module
-    // `class_methods` table consulted in the 22b.2 typecheck arms.
-    env.module_globals = module_globals
-        .iter()
-        .map(|(k, v)| (k.clone(), v.fns.clone()))
-        .collect();
-    env.module_types = build_module_types(ws);
     env.current_module = m.name.clone();
-    // Iter 22b.2 (Task 9): merge per-module class-method tables into a
-    // single workspace-wide map for [`synth`]'s `Term::Var` arm. Method
-    // names are unique workspace-wide (enforced by
-    // `workspace::build_registry`'s method-name-collision check), so
-    // the merge has no overwrites. Also walk every module's
-    // `Def::Class` to build the one-step superclass expansion table.
-    let mut class_methods: BTreeMap<String, ClassMethodEntry> = BTreeMap::new();
-    for g in module_globals.values() {
-        for (n, e) in &g.class_methods {
-            class_methods.insert(n.clone(), e.clone());
-        }
-    }
-    env.class_methods = class_methods;
-    let mut class_superclasses: BTreeMap<String, String> = BTreeMap::new();
-    for module in ws.modules.values() {
-        for def in &module.defs {
-            if let Def::Class(cd) = def {
-                if let Some(sc) = &cd.superclass {
-                    class_superclasses.insert(cd.name.clone(), sc.class.clone());
-                }
-            }
-        }
-    }
-    env.class_superclasses = class_superclasses;
-    // Iter 22b.2 (Task 10): thread the workspace-load-time instance
-    // registry into the env so `check_fn`'s concrete-residual path can
-    // look up `(class, type_hash)` keys for the no-instance check. The
-    // registry is the only field of `ws` consumed at typecheck time;
-    // cross-module name resolution uses `module_globals` / `module_types`
-    // built earlier in this function.
-    env.workspace_registry = ws.registry.clone();
 
     for def in &m.defs {
         if let Err(e) = check_def(def, &env) {