diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs
index bc6cf66d..dc5c201f 100644
--- a/src/ccl/ccl_utils.rs
+++ b/src/ccl/ccl_utils.rs
@@ -797,27 +797,127 @@ pub fn bare_predicate_of_fn(base: &Type, predicate: Expr) -> Expr {
     Expr::apply(elem, predicate).with_ty(Type::Base(BaseType::Bool))
 }
 
-/// Re-point every [`TypedExprNode::Cast`]'s `target` type slot at the cast
-/// node's own `expr.ty`. A cast's recorded type *is* its target type, so the
-/// two are equal by construction — but the `target` carries its **own**
-/// immutable refinement-predicate `Rc`, and lambda elimination rebuilds the
-/// predicate on `expr.ty` without touching `target`, so they drift apart. The
-/// post-pass `typecheck` reconstructs a cast from its `target`
-/// ([`cast_target_refinement`]) and compares against the recorded `expr.ty`;
-/// re-syncing after that pass keeps the match exact.
-///
-/// Only lambda elimination needs it. Inlining and planning each ran it too, and
-/// removing those calls changes no test — a whole-tree repair after a pass is
-/// weaker than writing both copies at the rewrite, which is what
-/// [`sync_cast_target_kind`] does for the arrow kind.
-pub fn sync_cast_targets(expr: &mut Expr) {
-    if matches!(expr.node, TypedExprNode::Cast { .. }) {
-        let ty = expr.ty.clone();
-        if let TypedExprNode::Cast { target, .. } = &mut expr.node {
-            *target = ty;
+/// Restore every [`TypedExprNode::Cast`]'s canonical type split after a
+/// rebuild pass: the `target` keeps its **born** refinements on the rebuilt view's
+/// shape and bases; the node type carries the value's domain refinements ∪ born
+/// ([`canonical_cast_ty`] — the same rule coalesce applies). Bottom-up, so a
+/// cast value that is itself a cast presents its canonical type to its parent.
+///
+/// A pass that rebuilds node types wholesale (lambda elimination's composition
+/// typing, `simplify`'s rule rewrites, planning's point-free compilation)
+/// re-derives `expr.ty` from surrounding term structure — and where inference
+/// left route-dependent types in eq-blind slots (a lambda param annotation,
+/// say), that re-derivation is route-dependent too. Installing the rebuilt
+/// view wholesale into `target` (the previous behaviour) therefore made a
+/// cast's *refinements* route-dependent — the defect the coalesce-time
+/// canonicalization retired — while dropping the view's refinements from `expr.ty`
+/// left the recorded type disagreeing with the post-pass typecheck's
+/// reconstruction (value-refinements ∪ target-refinements). Deriving both slots from
+/// the term repairs both at once.
+pub fn canonicalize_cast_types(expr: &mut Expr) {
+    expr.walk_children_mut(canonicalize_cast_types);
+    match &expr.node {
+        TypedExprNode::Cast { .. } => {
+            let view = expr.ty.clone();
+            if let TypedExprNode::Cast { value, target } = &mut expr.node {
+                let born = std::mem::replace(target, Type::Hole);
+                *target = canonical_cast_ty(&born, None, view.clone());
+                expr.ty = canonical_cast_ty(&born, Some(&value.ty), view);
+            }
         }
+        // A chain's type is derived from its ends (`emit_compose`): the domain
+        // comes from the head, the codomain from the tail. A head cast whose
+        // domain was just canonicalized owes the chain its domain — the
+        // post-pass typecheck's reconcile is exact on domain refinements (a
+        // recorded domain may be neither wider nor narrower than the derived
+        // one, by contravariance meeting the covariant reconcile), so the
+        // recorded chain type must follow.
+        //
+        // Follow only where the difference is *refinements on the same base* — the
+        // one thing cast canonicalization moves — and only on the domain. A
+        // structurally different recorded end, or a codomain refined beyond
+        // the tail's (a conditional leg's realization pin, planning's
+        // `refine_codomain`), is a deliberate statement this pass has no
+        // license to rewrite; overwriting one miscompiles (observed: a
+        // comprehension over a conditional summing the unfiltered extent).
+        // The kind and Pi name stay recorded for the same reason (`Data`
+        // pins, dependent binders).
+        TypedExprNode::Compose(elts) => {
+            if let Some(head) = elts.first()
+                && matches!(head.node, TypedExprNode::Cast { .. })
+                && let Some(head_dom) = head.ty.domain()
+                && let Type::Fun { domain, .. } = &mut expr.ty
+                && **domain != head_dom
+                && domain.peel_refinements() == head_dom.peel_refinements()
+            {
+                **domain = head_dom;
+            }
+        }
+        _ => {}
     }
-    expr.walk_children_mut(sync_cast_targets);
+}
+
+/// The canonical type of a `Cast` node: the `view`'s shape and bases (the
+/// coalesced view at inference time; the rebuilt type after a rebuild pass),
+/// carrying the refinements the **term** determines — the value's own domain refinements
+/// plus the `born` target's refinement set. Inference and the rebuild passes
+/// resolve a cast's bases; they do not decide its refinements.
+///
+/// A cast is an *assertion*: `cast(value, {𝐷 | 𝑝} ⇒ 𝑉)` asserts exactly `𝑝` on
+/// top of whatever its value already established, and both parts are fixed by
+/// the term — the born refinements when the cast was written (lowering's filter, a
+/// group-by's key equation), the value's refinements by the value's own type, which
+/// is already canonical by induction (both callers walk bottom-up). The graph
+/// view of the same position accumulates the same union on the ordinary route
+/// — the upcast `value <: target` is how the value's refinements flow in — but
+/// *which* refinements an occurrence's variable accumulates depends on the route
+/// bounds took through the graph: an embedded copy of a cast (a comprehension
+/// source cloned into a filter predicate) has its own variable, and under an
+/// adversarial bound order it coalesces bare, or decorated with a sibling
+/// layer's filter. Installing the view wholesale (the previous behaviour)
+/// therefore made a cast's *identity* route-dependent — which refinement
+/// equality, deliberately cast-target-aware, then refused to dedup. Deriving
+/// the refinements from the term instead is route-independent and agrees with the
+/// view on every deterministic route.
+///
+/// When the view's refinements already equal the term-derived set, the view is
+/// installed wholesale — preserving the predicate-`Rc` sharing between the
+/// target and the node type that planning's compile-once relies on.
+/// `value_ty: None` computes the canonical *target* (born refinements alone);
+/// `Some` computes the canonical node *type* (value's domain refinements ∪ born).
+pub(crate) fn canonical_cast_ty(born: &Type, value_ty: Option<&Type>, view: Type) -> Type {
+    let born_refinements = match born.domain() {
+        Some(d) => d.refinements().to_vec(),
+        None => return view,
+    };
+    let Some(view_dom) = view.domain() else {
+        return view;
+    };
+    // The term-determined refinement set: value's domain refinements (type position
+    // only) ∪ born refinements.
+    let mut canon_refinements: RefinementSet = value_ty
+        .and_then(|t| t.domain())
+        .map(|d| d.refinements().to_vec())
+        .unwrap_or_default()
+        .into_iter()
+        .collect();
+    canon_refinements.extend(born_refinements);
+    let view_refinements = view_dom.refinements();
+    let same = canon_refinements.len() == view_refinements.len()
+        && view_refinements
+            .iter()
+            .all(|r| canon_refinements.contains(r));
+    if same {
+        return view;
+    }
+    let cod = view
+        .codomain()
+        .expect("a type with a domain has a codomain");
+    Type::fun_like(
+        &view,
+        Type::refined(view_dom.peel_refinements().clone(), canon_refinements),
+        cod,
+    )
 }
 
 /// Carry a re-typed node's [`FunKind`](crate::ccl::ty::FunKind) onto its `target`,
diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md
index 26d9513c..d0eeec0a 100644
--- a/src/ccl/design/type-inference.md
+++ b/src/ccl/design/type-inference.md
@@ -525,10 +525,15 @@ place. A pass that processes a predicate at one occurrence must therefore reach
 threads a memo keyed on the original predicate's identity so occurrences that
 shared one term are re-pointed at the same rebuild (the immutable replacement
 for "mutate the shared cell, every alias observes it"). One consequence worth
-naming: a `Cast`'s `target` type slot is the cast's recorded type, so passes
-that rebuild a predicate on `expr.ty` re-sync the `target` to it
-(`ccl_utils::sync_cast_targets`) — the post-inference check reconstructs a cast
-from its `target`.
+naming: a `Cast`'s `target` slot carries the cast's **born** refinements (the
+assertion), never a copy of the recorded type — a pass that rebuilds node types
+restores the canonical split afterwards (`ccl_utils::canonicalize_cast_types`:
+`target` = born refinements on the rebuilt view's bases, `expr.ty` = value-refinements ∪
+born) rather than overwriting `target` with `expr.ty`. The post-inference check
+reconstructs a cast as value-refinements ∪ target-refinements, and a wholesale overwrite
+satisfied that check only by making the cast's refinement *identity* track whatever
+route-dependent type the rebuild derived — the arrival-order defect the
+canonical split retires (see the coalesce-time rule at `canonical_cast_ty`).
 
 #### Sharing is an invariant, not an optimization detail
 
diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs
index 7584b606..655820be 100644
--- a/src/ccl/infer/solve.rs
+++ b/src/ccl/infer/solve.rs
@@ -19,7 +19,7 @@
 // (`coalesce_node` ↔ `specialize_use`) over one shared [`CoalesceCtx`], so they
 // live in a single module.
 
-use crate::ccl::ccl_utils::PredMemo;
+use crate::ccl::ccl_utils::{PredMemo, canonical_cast_ty};
 use crate::ccl::infer::InferError;
 use crate::ccl::infer::emit::read_through;
 use crate::ccl::infer::solver::{
@@ -1539,19 +1539,26 @@ fn coalesce_node_inner(expr: &mut Expr, level: Level, ctx: &mut CoalesceCtx) {
     // (`specialize_lambda_domain`).
     refresh_lambda_param_slot(expr);
 
-    // A `Cast`'s `target` is the inferred cast type — exactly `expr.ty`. Point
-    // it at the fully-resolved `expr.ty` (sharing the resolved refinement `Rc`),
-    // so the cast's domain refinement carries a concrete base (lowering left it
-    // a `Hole`) and shares one predicate term with the result. Planning then
-    // compiles that one predicate once and the post-inference check reconstructs
-    // the cast from a `target` that matches what the producer supplies. (The
-    // pre-materialization `coalesce_type_predicates(target)` in the `Cast` arm
-    // resolved the predicate in scope — e.g. a generalized use inside it — but
-    // against the lowered `Hole` base; this overwrite installs the concrete one.)
+    // A `Cast`'s `target` and its `expr.ty` converge on the **canonical cast
+    // type**: the coalesced view's *shape and bases*, carrying the refinements the
+    // *term* determines — the value's own domain refinements plus the target's born
+    // refinements (see `canonical_cast_ty`). Both slots share one `Type`, so
+    // planning compiles one predicate term and the post-inference check
+    // reconstructs the cast from a `target` that matches the recorded type.
     if matches!(expr.node, TypedExprNode::Cast { .. }) {
-        let cast_ty = expr.ty.clone();
-        if let TypedExprNode::Cast { target, .. } = &mut expr.node {
-            *target = cast_ty;
+        let view = expr.ty.clone();
+        if let TypedExprNode::Cast { value, target } = &mut expr.node {
+            // The *target* keeps exactly its born refinements (the assertion); the
+            // node *type* is the value's refinements joined with them (what the
+            // assertion yields on this value). Keeping the two distinct is
+            // load-bearing for the post-inference check, which recomputes the
+            // type as value-refinements ∪ target-refinements: a target that also carried
+            // the value's refinements would double-book them, and any divergence
+            // between the value's copy and the target's copy of one refinement
+            // would surface as a duplicated refinement in the recomputation.
+            let born = std::mem::replace(target, Type::Hole);
+            *target = canonical_cast_ty(&born, None, view.clone());
+            expr.ty = canonical_cast_ty(&born, Some(&value.ty), view);
         }
     }
 }
diff --git a/src/ccl/lambda_elim.rs b/src/ccl/lambda_elim.rs
index edf6a7e4..7ee1e068 100644
--- a/src/ccl/lambda_elim.rs
+++ b/src/ccl/lambda_elim.rs
@@ -93,11 +93,12 @@ pub fn run(expr: Expr) -> Result<Expr, LambdaElimError> {
     // → simplify (→ planning) sub-pipeline when a refined type is iterated
     // (`planning::compile_refinement_predicates`).
     let mut simplified = simplify(point_free);
-    // Predicate rewrites during elimination/simplification rebuild the
-    // immutable predicate on each node's `expr.ty`; re-sync every `Cast`'s
-    // `target` slot to its `expr.ty` so the post-pass typecheck's
-    // reconstruction matches the recorded type.
-    crate::ccl::ccl_utils::sync_cast_targets(&mut simplified);
+    // Elimination and simplification rebuild node types from surrounding term
+    // structure; restore each `Cast`'s canonical split (`target` = born
+    // refinements, `expr.ty` = value-refinements ∪ born on the rebuilt view) so the
+    // post-pass typecheck's reconstruction matches the recorded type without
+    // making the cast's refinements route-dependent.
+    crate::ccl::ccl_utils::canonicalize_cast_types(&mut simplified);
     Ok(simplified)
 }
 
diff --git a/src/ccl/planning/predicates.rs b/src/ccl/planning/predicates.rs
index bc16de1c..62fdefbb 100644
--- a/src/ccl/planning/predicates.rs
+++ b/src/ccl/planning/predicates.rs
@@ -8,6 +8,7 @@
 //! op-conversion lowering consume.
 
 use super::*;
+use crate::ccl::RefinementSet;
 
 // Predicate compilation is a predicate-*rebuilding* pass like any other, so it
 // memoizes with the shared [`ccl_utils::PredMemo`] — including its keepalive
@@ -109,10 +110,47 @@ fn term_mentions_pair_binder(e: &Expr) -> bool {
 /// case the per-`Rc` memo keeps shared occurrences equal despite `lambda_elim`'s
 /// `__pair` minting (see [`PredMemo`]).
 pub(crate) fn compile_refinement_predicates(expr: &mut Expr, memo: &PredMemo<Type>) {
+    // A `Cast`'s target refinements are assertions on the cast's *value*: the
+    // checker types them with `__elem` bound at the value's domain (see
+    // `emit_cast`), which carries the value's own refinements. Compile them against
+    // that same base — a target holds only the cast's *born* refinements, so
+    // deriving the element type from the target alone would stamp `__elem`
+    // bare and fail the checker's argument edge against a predicate function
+    // whose domain the value's refinements narrow.
+    if let TypedExprNode::Cast { value, target } = &mut expr.node {
+        let value_dom = value.ty.domain();
+        compile_cast_target(target, value_dom, memo);
+        compile_predicates_in_type(&mut expr.ty, memo);
+        compile_refinement_predicates(value, memo);
+        return;
+    }
     expr.walk_type_slots_mut(|ty| compile_predicates_in_type(ty, memo));
     expr.walk_children_mut(|child| compile_refinement_predicates(child, memo));
 }
 
+/// Compile a cast target's domain refinements against the value's domain (the
+/// assertion base — see [`compile_refinement_predicates`]), then the rest of
+/// the target generically. The top-level domain refinement must not be
+/// revisited by the generic walk: recompiling it against the target's bare
+/// base would re-stamp `__elem` with the narrower context lost.
+fn compile_cast_target(target: &mut Type, value_dom: Option<Type>, memo: &PredMemo<Type>) {
+    if let Type::Fun {
+        domain, codomain, ..
+    } = target
+    {
+        if let Type::Refinement(base, refinements) = domain.as_mut() {
+            let assert_base = value_dom.unwrap_or_else(|| (**base).clone());
+            compile_refinements(refinements, &assert_base, memo);
+            compile_predicates_in_type(base, memo);
+        } else {
+            compile_predicates_in_type(domain, memo);
+        }
+        compile_predicates_in_type(codomain, memo);
+    } else {
+        compile_predicates_in_type(target, memo);
+    }
+}
+
 /// The point-free predicate function `p : base ⇒ Bool` underlying a refinement's
 /// bare predicate `__elem ▷ p` (the inverse of [`ccl_utils::bare_predicate_of_fn`]).
 /// Fast-pathed when the bare predicate is already that single application;
@@ -129,54 +167,59 @@ pub(crate) fn fn_of_bare_predicate(base: &Type, bare: &Expr) -> Expr {
 
 fn compile_predicates_in_type(ty: &mut Type, memo: &PredMemo<Type>) {
     if let Type::Refinement(base, refinements) = ty {
-        // Each refinement is compiled against the element type it sees in the
-        // restrict pipeline planning will build for this domain — the base
-        // narrowed by the refinements applied before it. `wrap_with_iterate` builds
-        // that pipeline from the same application order, so the compiled
-        // predicates and the pipeline's types agree.
-        //
-        // Indexed by physical position (`application_elem_types`), because the
-        // rewrite below walks the set in place and the application order is a
-        // *permutation* of the physical one.
-        let elem_tys = crate::ccl::application_elem_types(refinements.as_slice(), base);
-        refinements.rewrite_each(|i, refinement| {
-            let base_ctx = elem_tys[i].clone();
-            memo.rebuild(refinement, &base_ctx, |bare| {
-                // Normalize the bare predicate to `__elem ▷ p` with `p` point-free:
-                // recover the predicate function and re-wrap it. This keeps the stored
-                // predicate in the single bare form while pinning a point-free core, so
-                // the iterate/restrict producers (built from the same `p`) carry a
-                // structurally-identical refinement to the cast demand they satisfy.
-                let p = fn_of_bare_predicate(&base_ctx, bare);
-                let mut compiled = ccl_utils::bare_predicate_of_fn(&base_ctx, p);
-                // The compiled predicate's own sub-expressions can carry *nested*
-                // refinements (a filter over an already-filtered source: the inner
-                // refinement rides a sub-expression's type slot inside this predicate).
-                // `Type::walk_children_mut` below does not descend into a predicate term,
-                // so compile those here, sharing the memo.
-                compile_refinement_predicates(&mut compiled, memo);
-                // The producer/consumer refinement match (`sum`'s domain vs. its feed, a
-                // compose adjacency) compares *distinct* predicate `Rc`s — the memo only
-                // dedups occurrences sharing one `Rc`. That match rests on compilation
-                // being a deterministic value function, which requires that lambda
-                // elimination's freshly-minted `__pair` (`Uid::fresh()`) never survive
-                // into the compared *term*. It legitimately survives as a `Fun.name` Pi
-                // binder in a type slot (which `eq_refinement_predicate` is type-blind
-                // to), so the check is term-only. Assert that load-bearing invariant
-                // rather than leaving it argued.
-                debug_assert!(
-                    !term_mentions_pair_binder(&compiled),
-                    "a `__pair` binder survived into a compiled predicate term, \
-                 breaking the value-function property the structural \
-                 producer/consumer match relies on: {}",
-                    symbolic(&compiled)
-                );
-                *bare = compiled;
-                true
-            });
-        });
+        let base = base.clone();
+        compile_refinements(refinements, &base, memo);
     }
     // Recurse into structural type children (refinement base, function
     // domain/codomain, tuple/record/variant elements).
     ty.walk_children_mut(|child| compile_predicates_in_type(child, memo));
 }
+
+/// Compile each refinement of a set against the element type it sees in the restrict
+/// pipeline planning will build for this domain — `base` narrowed by the refinements
+/// applied before it. `wrap_with_iterate` builds that pipeline from the same
+/// application order, so the compiled predicates and the pipeline's types
+/// agree. For a cast target's refinements, `base` is the cast value's domain (the
+/// assertion base — see [`compile_refinement_predicates`]).
+fn compile_refinements(refinements: &mut RefinementSet, base: &Type, memo: &PredMemo<Type>) {
+    // Indexed by physical position (`application_elem_types`), because the
+    // rewrite below walks the set in place and the application order is a
+    // *permutation* of the physical one.
+    let elem_tys = crate::ccl::application_elem_types(refinements.as_slice(), base);
+    refinements.rewrite_each(|i, refinement| {
+        let base_ctx = elem_tys[i].clone();
+        memo.rebuild(refinement, &base_ctx, |bare| {
+            // Normalize the bare predicate to `__elem ▷ p` with `p` point-free:
+            // recover the predicate function and re-wrap it. This keeps the stored
+            // predicate in the single bare form while pinning a point-free core, so
+            // the iterate/restrict producers (built from the same `p`) carry a
+            // structurally-identical refinement to the cast demand they satisfy.
+            let p = fn_of_bare_predicate(&base_ctx, bare);
+            let mut compiled = ccl_utils::bare_predicate_of_fn(&base_ctx, p);
+            // The compiled predicate's own sub-expressions can carry *nested*
+            // refinements (a filter over an already-filtered source: the inner
+            // refinement rides a sub-expression's type slot inside this predicate).
+            // `Type::walk_children_mut` below does not descend into a predicate term,
+            // so compile those here, sharing the memo.
+            compile_refinement_predicates(&mut compiled, memo);
+            // The producer/consumer refinement match (`sum`'s domain vs. its feed, a
+            // compose adjacency) compares *distinct* predicate `Rc`s — the memo only
+            // dedups occurrences sharing one `Rc`. That match rests on compilation
+            // being a deterministic value function, which requires that lambda
+            // elimination's freshly-minted `__pair` (`Uid::fresh()`) never survive
+            // into the compared *term*. It legitimately survives as a `Fun.name` Pi
+            // binder in a type slot (which `eq_refinement_predicate` is type-blind
+            // to), so the check is term-only. Assert that load-bearing invariant
+            // rather than leaving it argued.
+            debug_assert!(
+                !term_mentions_pair_binder(&compiled),
+                "a `__pair` binder survived into a compiled predicate term, \
+                 breaking the value-function property the structural \
+                 producer/consumer match relies on: {}",
+                symbolic(&compiled)
+            );
+            *bare = compiled;
+            true
+        });
+    });
+}
diff --git a/src/ccl/simplify.rs b/src/ccl/simplify.rs
index 7798f0ee..c5610309 100644
--- a/src/ccl/simplify.rs
+++ b/src/ccl/simplify.rs
@@ -480,6 +480,16 @@ fn try_pairwise_in_compose(
     // a rewrite that overwrote them with a type derived from the surrounding term
     // would make the assertion track its own consumer.
     crate::ccl::ccl_utils::sync_cast_target_kind(expr);
+    // Nor may the collapsed node inherit the chain's interface type wholesale: a
+    // cast's refinements are term-determined (its type is the value's domain refinements ∪
+    // the target's born refinements), while the chain's recorded type was derived from
+    // neighbour types — which can be route-dependent where inference left
+    // route-dependent slots. Keep the chain's shape and bases, restore the
+    // term-determined refinements, reading a `target` whose kind now matches.
+    if let TypedExprNode::Cast { value, target } = &expr.node {
+        let view = expr.ty.clone();
+        expr.ty = crate::ccl::ccl_utils::canonical_cast_ty(target, Some(&value.ty), view);
+    }
     expr.user_annotation = user_annotation;
     true
 }
diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs
index fde06db2..9dc8e09b 100644
--- a/src/ccl/ty.rs
+++ b/src/ccl/ty.rs
@@ -2700,14 +2700,18 @@ mod tests {
     /// still holds both, because collapsing them would let refinement-deficit
     /// matching accept an unsatisfied demand.
     ///
-    /// A pass that decides a cast's refinements from route-dependent context can
-    /// mint such a pair out of *one* refinement, and dedup then correctly refuses to
-    /// collapse it — which surfaces as a recorded type disagreeing with its
-    /// recomputation while printing the same. No corpus program reaches that pair
-    /// (instrumenting [`RefinementSet::insert`] for a member rendering alike without
-    /// being `eq` counts zero in both physical orders, because a refinement's binding
-    /// is its index rather than its spelling), so the hazard is in the pass rather
-    /// than in the equality pinned here, and closing it is a separate change.
+    /// A pass that decides a cast's refinements from route-dependent context would
+    /// mint such a pair out of *one* refinement, and dedup would then correctly refuse
+    /// to collapse it — surfacing as a recorded type disagreeing with its
+    /// recomputation while printing the same. No pass does: a cast's refinements are
+    /// term-determined
+    /// ([`ccl_utils::canonical_cast_ty`](crate::ccl::ccl_utils::canonical_cast_ty) /
+    /// [`ccl_utils::canonicalize_cast_types`](crate::ccl::ccl_utils::canonicalize_cast_types)),
+    /// pinned by `a_cast_target_does_not_carry_its_value_s_refinements`. Nor is the
+    /// pair otherwise reachable: instrumenting [`RefinementSet::insert`] for a member
+    /// rendering alike without being `eq` counts zero over the corpus in both physical
+    /// orders, because a refinement's binding is its index rather than its spelling.
+    /// So the hazard was in the pass, not in the equality this pins.
     #[test]
     fn cast_target_vintages_render_alike_but_do_not_dedup() {
         // Two casts of one value, differing *only* in their targets' domain
diff --git a/tests/predicate_sharing.rs b/tests/predicate_sharing.rs
index ebb79b91..b97a763b 100644
--- a/tests/predicate_sharing.rs
+++ b/tests/predicate_sharing.rs
@@ -36,6 +36,7 @@
 //! lineage-redesign doc, §12.4(9); rationale in `ccl/design/type-inference.md`.
 
 use cambra::ccl::ccl_utils::{distinct_predicate_rcs, reachable_refinements};
+use cambra::ccl::context::{GlobalContext, compile_program};
 use cambra::ccl::infer::{TypeInferenceContext, infer};
 use cambra::ccl::lower::{LoweringContext, lower_stmts};
 use cambra::ccl::symbolic::symbolic;
@@ -106,6 +107,68 @@ fn assert_no_split(code: &str) {
 /// misses the binder slots and cast targets happens to cost nothing. At two
 /// levels, a filter predicate reachable only through a `Cast.target` appears —
 /// and that is the slot `lambda_elim` and operator conversion read it from.
+/// **A cast's `target` carries only the cast's own refinements.** The value's
+/// refinements belong on the node's *type*, which the post-inference check
+/// recomputes as value-refinements ∪ target-refinements — so a `target` that also
+/// carried the value's would double-book each one.
+///
+/// The minimal exhibit is a nested filter. `coalesce_node` used to overwrite a
+/// `Cast`'s `target` with the occurrence's coalesced view, which carries the
+/// value's filter alongside the cast's own, and three rebuild passes then did the
+/// same from route-dependent types; the inner cast came out with two refinements
+/// where one is its own. Measured over the corpus, the overwrite differed from the
+/// term-determined set at 14 cast sites in either physical refinement order.
+///
+/// A duplicate is currently absorbed rather than observed, because the two copies
+/// of the value's refinement are `eq` and a `RefinementSet` deduplicates them. It
+/// stops being absorbed as soon as they are not — `eq_refinement_predicate`
+/// compares a cast's target predicate, so two vintages of one refinement do not
+/// dedup, and the recomputation then disagrees with the recorded type while
+/// printing the same. This asserts the disjointness rather than that surface,
+/// because the disjointness is what the passes can break and what no fuzz reaches.
+#[test]
+fn a_cast_target_does_not_carry_its_value_s_refinements() {
+    let mut ctx = GlobalContext::default();
+    let consumer: Box<dyn cambra::interpreter::Consumer> = Box::new(|| {});
+    let compiled = compile_program(
+        &mut ctx,
+        "[a for a in [b for b in [1, 2, 3, 4] if b < 3] if a < 3]",
+        consumer,
+    )
+    .expect("the nested filter compiles");
+
+    let mut casts = 0;
+    let mut doubled = Vec::new();
+    fn walk(e: &Expr, casts: &mut usize, doubled: &mut Vec<String>) {
+        if let TypedExprNode::Cast { target, value } = &e.node {
+            *casts += 1;
+            let refs_of = |t: &Type| -> Vec<Refinement> {
+                t.domain()
+                    .map(|d| d.refinements().to_vec())
+                    .unwrap_or_default()
+            };
+            let (target_refs, value_refs) = (refs_of(target), refs_of(&value.ty));
+            for r in &target_refs {
+                if value_refs.contains(r) {
+                    doubled.push(symbolic(&r.predicate));
+                }
+            }
+        }
+        e.walk_children(&mut |c| walk(c, casts, doubled));
+    }
+    walk(&compiled.ast, &mut casts, &mut doubled);
+
+    assert!(
+        casts >= 2,
+        "the exhibit needs the nested cast pair; found {casts} cast(s)"
+    );
+    assert!(
+        doubled.is_empty(),
+        "{} cast target(s) carry a refinement the value already establishes: {doubled:?}",
+        doubled.len()
+    );
+}
+
 #[test]
 fn nested_comprehension_shares_predicate_rcs() {
     assert_no_split(