diff --git a/crates/ailang-check/src/diagnostic.rs b/crates/ailang-check/src/diagnostic.rs
index dbba755..02bb31e 100644
--- a/crates/ailang-check/src/diagnostic.rs
+++ b/crates/ailang-check/src/diagnostic.rs
@@ -40,7 +40,6 @@
 //! - `module-name-mismatch` — workspace loader (Iter 5b, in the CLI path)
 //! - `module-hash-mismatch` — workspace loader (Iter 5b, in the CLI path)
 //! - `tail-call-not-in-tail-position` (Iter 14e, see Decision 8)
-//! - `ambiguous-ctor` — `ctx`: `{"ctor": "<n>", "candidates": ["m1.T", "m2.T"]}` (Iter 15a)
 //! - `use-after-consume` — `ctx`: `{"binder": "<n>"}` (Iter 18c.2);
 //!   carries non-empty [`Diagnostic::suggested_rewrites`] showing how to
 //!   spell the fix in form-A AILang.
diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index 1eecfa6..9a95b81 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -431,18 +431,6 @@ pub enum CheckError {
     #[error("call marked `tail` is not in tail position")]
     TailCallNotInTailPosition,
 
-    /// Iter 15a: a bare `Pattern::Ctor.ctor` did not resolve against the
-    /// current module's `ctor_index` and resolved against ctors in two
-    /// or more imported modules. The author must qualify the scrutinee
-    /// type so that ctor lookup is unambiguous (e.g. write
-    /// `(con std_maybe.Maybe (con Int))` for the scrutinee). Code:
-    /// `ambiguous-ctor`. `ctx`: `{"ctor": "<n>", "candidates": ["m1.T", "m2.T"]}`.
-    #[error("ambiguous constructor `{ctor}`: declared in {candidates:?}")]
-    AmbiguousCtor {
-        ctor: String,
-        candidates: Vec<String>,
-    },
-
     /// Iter 23.1.3: a bare `Term::Ctor.type_name` did not resolve
     /// against the current module's local `env.types` and resolved
     /// against type defs in two or more imported modules. The author
@@ -553,7 +541,6 @@ impl CheckError {
             CheckError::UnknownImport { .. } => "unknown-import",
             CheckError::InvalidDefName { .. } => "invalid-def-name",
             CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position",
-            CheckError::AmbiguousCtor { .. } => "ambiguous-ctor",
             CheckError::AmbiguousType { .. } => "ambiguous-type",
             CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body",
             CheckError::MissingConstraint { .. } => "missing-constraint",
@@ -593,9 +580,6 @@ impl CheckError {
             CheckError::InvalidDefName { name } => {
                 serde_json::json!({"name": name, "reason": "contains-dot"})
             }
-            CheckError::AmbiguousCtor { ctor, candidates } => {
-                serde_json::json!({"ctor": ctor, "candidates": candidates})
-            }
             CheckError::AmbiguousType { type_name, candidates } => {
                 serde_json::json!({"type_name": type_name, "candidates": candidates})
             }
@@ -1248,12 +1232,17 @@ fn check_in_workspace(
     let mut errors: Vec<CheckError> = Vec::new();
 
     // 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.
+    // `build_check_env` populates these workspace-flat, but the
+    // per-module pass needs only THIS module's local entries.
+    // Clear and rebuild so that:
+    //   - duplicate-type / duplicate-ctor detection (the in-band
+    //     errors below) sees only this module's defs;
+    //   - bare-name lookups (e.g. local `Term::Ctor` synth)
+    //     resolve against this module's types, not against the
+    //     workspace-flat union.
+    // Cross-module `Pattern::Ctor` resolution no longer touches
+    // this overlay — that path is type-driven via `expected` and
+    // consults `env.module_types` directly (ct.2.2).
     env.types.clear();
     env.ctor_index.clear();
     for def in &m.defs {
@@ -2494,9 +2483,9 @@ fn type_check_pattern(
             // TypeDef, qualified = explicit cross-module). Derive the
             // TypeDef from `expected` and find the ctor by name within
             // it; no env.ctor_index consult, no imports-walk.
-            let (resolved_type_name, resolved_td, resolved_owning_module) =
+            let (resolved_type_name, resolved_td, resolved_owning_module, scrutinee_args) =
                 match expected {
-                    Type::Con { name, args: _ } => {
+                    Type::Con { name, args } => {
                         if let Some((owner, suffix)) = name.split_once('.') {
                             let td = env
                                 .module_types
@@ -2509,7 +2498,7 @@ fn type_check_pattern(
                                         ty: ailang_core::pretty::type_to_string(expected),
                                     }
                                 })?;
-                            (name.clone(), td, Some(owner.to_string()))
+                            (name.clone(), td, Some(owner.to_string()), args.clone())
                         } else {
                             let td = env.types.get(name).cloned().ok_or_else(|| {
                                 CheckError::PatternTypeMismatch {
@@ -2517,7 +2506,7 @@ fn type_check_pattern(
                                     ty: ailang_core::pretty::type_to_string(expected),
                                 }
                             })?;
-                            (name.clone(), td, None)
+                            (name.clone(), td, None, args.clone())
                         }
                     }
                     _ => {
@@ -2527,21 +2516,12 @@ fn type_check_pattern(
                         });
                     }
                 };
-            // Validate the ctor exists in the resolved TypeDef.
-            if !resolved_td.ctors.iter().any(|c| &c.name == ctor) {
-                return Err(CheckError::UnknownCtorInPattern(ctor.clone()));
-            }
-            // expected is already validated as Type::Con above.
-            let scrutinee_args: Vec<Type> = match expected {
-                Type::Con { args, .. } => args.clone(),
-                _ => unreachable!("matched above"),
-            };
             let td = &resolved_td;
             let cdef = td
                 .ctors
                 .iter()
                 .find(|c| &c.name == ctor)
-                .expect("indexed ctor exists");
+                .ok_or_else(|| CheckError::UnknownCtorInPattern(ctor.clone()))?;
             if fields.len() != cdef.fields.len() {
                 return Err(CheckError::CtorArity {
                     ty: resolved_type_name.clone(),