MAIN-R: the if-join judges branches against EACH OTHER, never against the declared return context — a well-typed coproduct construction is refused, and the verdict depends on corpus scope

fixtures/if_join_pool_binding/closure_with_collision.dag

@@ -0,0 +1,21 @@
+module fixtures.if_join_pool_binding.closure_with_collision
+
+// THE RED ARM. Entry here puts BOTH modules in one closure and the compile REFUSES at
+// `declaring_module`'s if-expression:
+//
+//   if branches resolve to incompatible types:
+//     Coproduct(PoolSpecimenShape) vs Product(PoolSpecimenSquare)
+//
+// The refusal names `declaring_module`, which neither declares nor imports the competing type --
+// an innocent site. Note this module need not import the colliding SPELLING at all; importing any
+// other member of `colliding_module` is enough, because pool MEMBERSHIP is the variable.
+import fixtures.if_join_pool_binding.declaring_module { PoolSpecimenShape, pick_shape }
+import fixtures.if_join_pool_binding.colliding_module { PoolSpecimenSquare }
+
+fn refusing_use(c: Bool) -> PoolSpecimenShape {
+  pick_shape(c: c)
+}
+
+fn foreign_square() -> PoolSpecimenSquare {
+  PoolSpecimenSquare { s: 3 }
+}

fixtures/if_join_pool_binding/closure_without_collision.dag

@@ -0,0 +1,11 @@
+module fixtures.if_join_pool_binding.closure_without_collision
+
+// THE POSITIVE CONTROL, AND IT IS WHAT MAKES THE RED ARM DISCRIMINATING RATHER THAN MERELY RED.
+// Entry here reaches the SAME BYTES of `declaring_module` with `colliding_module` absent from the
+// closure, and the compile reports 0 blocking errors. Without this arm a reader could not tell a
+// refusal caused by pool membership from a refusal caused by the specimen being ill-typed.
+import fixtures.if_join_pool_binding.declaring_module { PoolSpecimenShape, pick_shape }
+
+fn accepting_use(c: Bool) -> PoolSpecimenShape {
+  pick_shape(c: c)
+}

fixtures/if_join_pool_binding/colliding_module.dag

@@ -0,0 +1,10 @@
+module fixtures.if_join_pool_binding.colliding_module
+
+// THE PERTURBATION, AND IT IS THE ONLY DIFFERENCE BETWEEN THE TWO CLOSURES. A standalone product
+// spelled the same as an ARM of another module's coproduct. This module is not on
+// `declaring_module`'s ancestor chain, does not import it, and is not imported by it.
+//
+// namespace-resolution-design.md section 13 (operator-ratified 2026-07-21, default
+// NamespaceOnlyY) decides an off-chain candidate as ZERO-ON-CHAIN and therefore UnresolvedType.
+// The type and variant-arm channel does not honour that: it binds here instead.
+type PoolSpecimenSquare { s: Int }

fixtures/if_join_pool_binding/declaring_module.dag

@@ -0,0 +1,20 @@
+module fixtures.if_join_pool_binding.declaring_module
+
+// THE SUBJECT. This module declares BOTH arms of its own coproduct and returns one arm per
+// if-branch, which is a well-typed inhabitant of the declared return in every closure. Nothing
+// here refers to any other module, and the file is BYTE-IDENTICAL across the two closures that
+// disagree about it -- that invariance is the whole instrument.
+//
+// A coproduct ARM is pool-visible corpus-wide while NOT being a local binding under its own
+// spelling, so `PoolSpecimenSquare` below misses local lookup and lands in the pool. When
+// `colliding_module` is present it binds THERE, the arm stops widening to its owner coproduct,
+// and the if-join then compares a widened arm against a bare product. Inside this module not even
+// the unlisted-import advisory fires, because the spelling is in `source_visible_names` here --
+// which is why the class is silent at the site that causes it.
+type PoolSpecimenShape
+  = PoolSpecimenCircle { r: Int }
+  | PoolSpecimenSquare { s: Int }
+
+fn pick_shape(c: Bool) -> PoolSpecimenShape {
+  if c { PoolSpecimenCircle { r: 1 } } else { PoolSpecimenSquare { s: 2 } }
+}