diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6bd59f03b..40a619e6a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -158,6 +158,19 @@ jobs:
         # step, which is worth paying to keep the next one from doing the same.
         run: DEEP_TYPECHECK=1 CAMBRA_PROVENANCE_GATE=1 ./ci.sh test
 
+      - name: Test (reversed refinement order)
+        if: steps.filter.outputs.code == 'true' && (success() || failure())
+        # A refinement set is unordered by contract, but two classes of
+        # order-dependence survive a compile-clean rewrite and only running the
+        # suite both ways exercises them: a consumer that iterates the set and
+        # lets the order reach something observable, and a dedup that keeps the
+        # first-inserted of two `eq`-equal refinements whose predicate terms carry
+        # different embedded type slots. Nothing in the type system catches
+        # either, so an unrun knob would rot exactly as an uncompiled feature
+        # does. The env var is read at *runtime*, so this reuses the binaries
+        # the step above already built.
+        run: CAMBRA_REFINEMENT_ORDER=reverse ./ci.sh test
+
         # 4. Success Signal for noops
       - name: No-op for docs
         if: steps.filter.outputs.code == 'false'
diff --git a/ci.sh b/ci.sh
index c08feb697..e63bcc69f 100755
--- a/ci.sh
+++ b/ci.sh
@@ -39,6 +39,14 @@ ci_clippy_lib() { cargo clippy --lib -- -D warnings; }
 # `deep-typecheck` feature). The GitHub workflow sets it so automated runs keep
 # exercising that check; it stays off for a bare local `./ci.sh` because it is
 # superlinear on nested comprehensions (that cost is why it is gated).
+#
+# `CAMBRA_REFINEMENT_ORDER=reverse` (read at runtime, debug builds only) flips
+# the physical order of every refinement set. The workflow runs the suite
+# both ways: set semantics makes that order meaningless by contract, but a
+# consumer that lets it become observable — or a dedup keeping the
+# first-inserted of two `eq`-equal refinements — compiles clean either way. Same
+# argument as `ci_clippy_serde`: a configuration nothing runs is a
+# configuration that rots.
 ci_test() { cargo test -q ${DEEP_TYPECHECK:+--features deep-typecheck}; }
 ci_doc() {
   RUSTDOCFLAGS="-A warnings -D rustdoc::broken_intra_doc_links" \
diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs
index 313537d82..d7c964c19 100644
--- a/src/ccl/ccl_utils.rs
+++ b/src/ccl/ccl_utils.rs
@@ -7,7 +7,8 @@ use std::rc::Rc;
 use crate::ccl::scope::{ScopedItem, for_each_scoped_item};
 use crate::ccl::{
     BaseType, BinOpKind, Branch, Builtin, Expr, F_FIRE_SUFFIX, F_WRITES, FieldKey, Lit, LogicKind,
-    Name, PredicateId, Refinement, Type, TypedExprNode, UnaryOpKind, V_ABORT, V_COMMIT,
+    Name, PredicateId, Refinement, RefinementSet, Type, TypedExprNode, UnaryOpKind, V_ABORT,
+    V_COMMIT,
 };
 
 /// The `commit` selector field of the **intermediate** decision record the two
@@ -285,12 +286,14 @@ pub(crate) fn debug_assert_no_iteration_markers_in_type(ty: &Type) {
             || e.fold_children(false, |acc, c| acc || expr_has_marker(c))
     }
     fn go(ty: &Type) {
-        if let Type::Refinement(_, r) = ty {
-            debug_assert!(
-                !expr_has_marker(&r.predicate),
-                "iteration/restrict marker leaked into a refinement predicate: {}",
-                crate::ccl::symbolic::symbolic(&r.predicate)
-            );
+        if let Type::Refinement(_, refinements) = ty {
+            for r in refinements {
+                debug_assert!(
+                    !expr_has_marker(&r.predicate),
+                    "iteration/restrict marker leaked into a refinement predicate: {}",
+                    crate::ccl::symbolic::symbolic(&r.predicate)
+                );
+            }
         }
         ty.walk_children(go);
     }
@@ -532,12 +535,12 @@ pub fn make_restrict(predicate: Expr, upstream: Expr) -> Expr {
     // capability yields a capability.
     //
     // The refinement is built **without** `refine_with`'s trivially-true
-    // degeneracy: the caller emits one `restrict` per refinement layer the site
-    // declared, so dropping a layer here would leave the source producing a bare
-    // extent while the site — and the body's `cast` — still demand the refined
-    // one. A layer that is vacuous is the site's business, not this constructor's.
-    let refined_dom = Type::Refinement(
-        Box::new(domain.clone()),
+    // degeneracy: the caller emits one `restrict` per refinement the site declared,
+    // so dropping one here would leave the source producing a bare extent while the
+    // site — and the body's `cast` — still demand the refined one. A vacuous
+    // refinement is the site's business, not this constructor's.
+    let refined_dom = Type::refined_one(
+        domain.clone(),
         Refinement::born(Rc::new(bare_predicate_of_fn(&domain, predicate.clone()))),
     );
     let refined_stream = Type::fun_like(&upstream_ty, refined_dom, value_ty);
@@ -682,16 +685,21 @@ pub fn make_cast(value: Expr, target_ty: Type) -> Expr {
 /// [`TypedExprNode::Cast`]'s `target` to reattach the refinement to the
 /// reconstructed `groupby` lambda.  (Inference does not need it: it types the
 /// cast as the upcast `value_ty <: target` and lets the solver carry the
-/// refinement.) The returned `Refinement` shares the predicate's `Rc<Expr>` with
+/// refinement.) The returned refinements share their predicates' `Rc<Expr>`s with
 /// `target`.
-pub fn cast_target_refinement(target: &Type) -> Option<Refinement> {
+///
+/// The whole [`RefinementSet`] is returned rather than a single refinement: a target
+/// is *built* carrying one predicate ([`refined_data_fun`]), but the domain it
+/// unifies against may contribute more, and a caller reattaching "the cast's
+/// refinement" wants all of what the target demands.
+pub fn cast_target_refinement(target: &Type) -> Option<RefinementSet> {
     let Type::Fun { domain, .. } = target else {
         return None;
     };
-    let Type::Refinement(_, refinement) = domain.as_ref() else {
+    let Type::Refinement(_, refinements) = domain.as_ref() else {
         return None;
     };
-    Some(refinement.clone())
+    Some(refinements.clone())
 }
 
 /// Build a function type whose domain is `base_domain` wrapped in a fresh
@@ -707,7 +715,7 @@ pub fn cast_target_refinement(target: &Type) -> Option<Refinement> {
 /// inference fills them in by unifying against the value being cast.
 pub fn refined_data_fun(base_domain: Type, predicate: Expr, codomain: Type) -> Type {
     Type::data_fun(
-        Type::Refinement(Box::new(base_domain), Refinement::born(Rc::new(predicate))),
+        Type::refined_one(base_domain, Refinement::born(Rc::new(predicate))),
         codomain,
     )
 }
@@ -815,7 +823,7 @@ pub fn sync_cast_targets(expr: &mut Expr) {
 /// Carry a re-typed node's [`FunKind`](crate::ccl::ty::FunKind) onto its `target`,
 /// when that node is a [`TypedExprNode::Cast`].
 ///
-/// A cast's `target` states the claims the cast asserts, and those are the cast's
+/// A cast's `target` states the refinements the cast asserts, and those are the cast's
 /// own — a rewrite must not overwrite them with a type derived from the
 /// surrounding term. The `FunKind` is different: nothing asserts it
 /// independently, `emit_cast` reads it off `target` to type the node, and so the
@@ -825,7 +833,7 @@ pub fn sync_cast_targets(expr: &mut Expr) {
 /// sub-expressions (`simplify`'s collapse rules). Such a rewrite writes the
 /// position's type onto the survivor, and where the survivor is a cast that
 /// re-kinds it — `⟨id, const 𝑥⟩ ≫ apply` collapsing to a `𝑥` that is a collection
-/// standing in a morphism position. Only the kind moves; the claims stay the
+/// standing in a morphism position. Only the kind moves; the refinements stay the
 /// cast's.
 pub(crate) fn sync_cast_target_kind(expr: &mut Expr) {
     if matches!(expr.node, TypedExprNode::Cast { .. }) {
@@ -845,7 +853,7 @@ pub(crate) fn refine_with(base: Type, predicate: &Expr) -> Type {
         return base;
     }
     let bare = bare_predicate_of_fn(&base, predicate.clone());
-    Type::Refinement(Box::new(base), Refinement::born(Rc::new(bare)))
+    Type::refined_one(base, Refinement::born(Rc::new(bare)))
 }
 
 /// Is `bare` the trivially-true predicate in **bare** form, `__elem ▷ (true ▷ const)`?
@@ -871,10 +879,7 @@ pub fn refine_with_bare(base: Type, bare_predicate: &Expr) -> Type {
     if is_trivially_true_bare_predicate(bare_predicate) {
         return base;
     }
-    Type::Refinement(
-        Box::new(base),
-        Refinement::born(Rc::new(bare_predicate.clone())),
-    )
+    Type::refined_one(base, Refinement::born(Rc::new(bare_predicate.clone())))
 }
 
 /// Count free occurrences of `name` in `expr`, including occurrences in
@@ -1171,10 +1176,12 @@ pub fn walk_refined_predicates<F>(ty: &Type, visited: &mut HashSet<PredicateId>,
 where
     F: FnMut(&Expr, &mut HashSet<PredicateId>),
 {
-    if let Type::Refinement(_, refinement) = ty
-        && visited.insert(refinement.predicate_id())
-    {
-        f(&refinement.predicate, visited);
+    if let Type::Refinement(_, refinements) = ty {
+        for refinement in refinements {
+            if visited.insert(refinement.predicate_id()) {
+                f(&refinement.predicate, visited);
+            }
+        }
     }
     ty.walk_children(|child| walk_refined_predicates(child, visited, f));
 }
@@ -1513,12 +1520,14 @@ impl TermMemo {
 /// refinement, i.e. whether sharing was split (see `tests/predicate_sharing.rs`).
 pub fn reachable_refinements(expr: &Expr) -> Vec<Refinement> {
     fn in_type(ty: &Type, out: &mut Vec<Refinement>, seen: &mut HashSet<PredicateId>) {
-        if let Type::Refinement(_, r) = ty
-            && seen.insert(r.predicate_id())
-        {
-            out.push(r.clone());
-            // A predicate's own subexpressions carry further refinements.
-            in_expr(&r.predicate, out, seen);
+        if let Type::Refinement(_, refinements) = ty {
+            for r in refinements {
+                if seen.insert(r.predicate_id()) {
+                    out.push(r.clone());
+                    // A predicate's own subexpressions carry further refinements.
+                    in_expr(&r.predicate, out, seen);
+                }
+            }
         }
         ty.walk_children(|c| in_type(c, out, seen));
     }
@@ -1575,8 +1584,10 @@ where
     F: FnMut(&mut Expr, &PredMemo<C>) -> bool,
 {
     let mut changed = false;
-    if let Type::Refinement(_, refinement) = ty {
-        changed |= memo.rebuild(refinement, context, |pred| f(pred, memo));
+    if let Type::Refinement(_, refinements) = ty {
+        refinements.rewrite_each(|_, refinement| {
+            changed |= memo.rebuild(refinement, context, |pred| f(pred, memo));
+        });
     }
     ty.walk_children_mut(|child| changed |= walk_refined_predicates_mut(child, memo, context, f));
     changed
diff --git a/src/ccl/channelize.rs b/src/ccl/channelize.rs
index fa881b79d..3d5b1c1a4 100644
--- a/src/ccl/channelize.rs
+++ b/src/ccl/channelize.rs
@@ -1728,10 +1728,10 @@ fn collect_free_vars(expr: &Expr, out: &mut HashSet<Name>) {
 /// as "no references"; callers run between passes when no predicate
 /// is being walked elsewhere, so the under-count is safe in practice.
 fn collect_free_vars_in_type(ty: &Type, out: &mut HashSet<Name>) {
-    if let Type::Refinement(_, refinement) = ty {
-        // Refinement predicates are themselves CCL expressions; recurse into
-        // them through `collect_free_vars` so their own type-position
-        // predicates and shadowing are handled consistently.
+    // Refinement predicates are themselves CCL expressions; recurse into them
+    // through `collect_free_vars` so their own type-position predicates and
+    // shadowing are handled consistently.
+    for refinement in ty.refinements() {
         collect_free_vars(&refinement.predicate, out);
     }
     ty.walk_children(|child| collect_free_vars_in_type(child, out));
@@ -1967,31 +1967,14 @@ fn copair_type(feeds: &[Expr]) -> Type {
 /// `PartialEq`), and the skeletons must already agree — the caller's
 /// `debug_assert` states that invariant.
 fn join_refinements(a: &Type, b: &Type) -> Type {
-    let mut layers: Vec<Refinement> = Vec::new();
-    let mut cur = a;
-    while let Type::Refinement(inner, r) = cur {
-        if type_carries_refinement(b, r) {
-            layers.push(r.clone());
-        }
-        cur = inner;
-    }
-    // Innermost-first, so the outermost layer of `a` ends up outermost again.
-    layers
-        .into_iter()
-        .rev()
-        .fold(cur.clone(), |acc, r| Type::Refinement(Box::new(acc), r))
-}
-
-/// Whether `ty`'s own refinement layers include `refinement`.
-fn type_carries_refinement(ty: &Type, refinement: &Refinement) -> bool {
-    let mut cur = ty;
-    while let Type::Refinement(inner, r) = cur {
-        if r == refinement {
-            return true;
-        }
-        cur = inner;
-    }
-    false
+    Type::refined(
+        a.peel_refinements().clone(),
+        a.refinements()
+            .iter()
+            .filter(|r| b.refinements().contains(r))
+            .cloned()
+            .collect(),
+    )
 }
 
 /// Peel outer `Refinement` wrappers off a type, returning the underlying type.
@@ -2665,12 +2648,7 @@ fn extract_for_defer_impl(
                     let refined = if matches!(&pred.node, TypedExprNode::Lit(Lit::Bool(true))) {
                         unit_ty.clone()
                     } else {
-                        Type::Refinement(
-                            Box::new(unit_ty.clone()),
-                            Refinement {
-                                predicate: Rc::new(pred),
-                            },
-                        )
+                        Type::refined_one(unit_ty.clone(), Refinement::born(Rc::new(pred)))
                     };
                     for v in branch_feeds {
                         feeds.push(Expr::lambda("__unused", refined.clone(), v.clone()));
@@ -2977,7 +2955,7 @@ mod tests {
         let pred = var("outer_n");
         let refinement = Refinement::born(Rc::new(pred));
         let annotated = Expr::var(Name::raw("__chan")).with_user_annotation(Type::fun(
-            Type::Refinement(Box::new(Type::Hole), refinement),
+            Type::refined_one(Type::Hole, refinement),
             Type::Hole,
         ));
 
@@ -3003,7 +2981,7 @@ mod tests {
         let typed = Expr::lit(Lit::Unit).with_ty(Type::Fun {
             name: None,
             kind: crate::ccl::ty::FunKind::Compute,
-            domain: Box::new(Type::Refinement(Box::new(Type::Hole), refinement)),
+            domain: Box::new(Type::refined_one(Type::Hole, refinement)),
             codomain: Box::new(Type::Hole),
         });
         let mut free: HashSet<Name> = HashSet::new();
diff --git a/src/ccl/context.rs b/src/ccl/context.rs
index 015822406..61dd49207 100644
--- a/src/ccl/context.rs
+++ b/src/ccl/context.rs
@@ -838,14 +838,16 @@ pub(crate) fn predicate_id_collisions(expr: &Expr) -> Vec<(NodeId, &'static str)
         e.walk_children(|c| ids_of(c, out));
     }
     fn from_ty(t: &Type, acc: &mut HashMap<usize, HashSet<NodeId>>) {
-        if let Type::Refinement(_, r) = t {
-            let key = Rc::as_ptr(&r.predicate) as usize;
-            if let std::collections::hash_map::Entry::Vacant(slot) = acc.entry(key) {
-                let mut s = HashSet::new();
-                ids_of(&r.predicate, &mut s);
-                slot.insert(s);
+        if let Type::Refinement(_, rs) = t {
+            for r in rs.iter() {
+                let key = Rc::as_ptr(&r.predicate) as usize;
+                if let std::collections::hash_map::Entry::Vacant(slot) = acc.entry(key) {
+                    let mut s = HashSet::new();
+                    ids_of(&r.predicate, &mut s);
+                    slot.insert(s);
+                }
+                from_expr_ty(&r.predicate, acc);
             }
-            from_expr_ty(&r.predicate, acc);
         }
         t.walk_children(|c| from_ty(c, acc));
     }
@@ -910,8 +912,12 @@ pub(crate) fn collect_tree_ids(expr: &Expr) -> std::collections::HashSet<NodeId>
     use crate::ccl::ty::Type;
 
     fn from_ty(t: &Type, acc: &mut std::collections::HashSet<NodeId>) {
-        if let Type::Refinement(_, r) = t {
-            from_expr(&r.predicate, acc);
+        if let Type::Refinement(_, refinements) = t {
+            // Every refinement's predicate rides the slot, so every one of them
+            // carries ids the projections must explain.
+            for r in refinements.iter() {
+                from_expr(&r.predicate, acc);
+            }
         }
         t.walk_children(|c| from_ty(c, acc));
     }
diff --git a/src/ccl/design/optimization.md b/src/ccl/design/optimization.md
index 5153a8d0d..86350e378 100644
--- a/src/ccl/design/optimization.md
+++ b/src/ccl/design/optimization.md
@@ -137,7 +137,7 @@ When the lambda-elimination rule 7 rewrites a `Let` inside a lambda body, the bo
 1. **Keyed-aggregate rewrite** (`recognize_groupby_sites` / `convert_groupby_pointful`) — recognises the **pointful** dependent-refinement source `const(cast(c)) : (k) ⇒ ({i | i ▷ c ▷ key == k} ⇒ V)` that lambda elimination emits for `[sum(g) for g in groupby(xs, key_fn)]` and folds the partition dispatch through `converse`.
 2. **Iteration-site materialization** (`insert_iterate_markers`) — a single walk that visits every position where op-conversion would compile with `input=None`.  At each site the pass picks the best implementation strategy:
    - **Hash join** (`try_hash_join_rewrite` → `convert_loop_join` → `plan_loop_join` → `join_plan_to_expr`) when the site's domain is a refined tuple whose predicate decomposes into equality join conditions.  The emitted chain is itself iteration-bearing at its leaves (each `JoinPlan::Loop` emits `Apply(true ▷ const, Iterate)`), so no further marker is added.
-   - **Iterate-then-restricts chain** (`wrap_with_iterate`'s fallback) — build the iteration source by *applying* one `restrict(p)` per refinement layer (innermost first) to a chain-head `Apply(true ▷ const, Iterate)`, then compose the value-producing body onto it, when the hash-join recogniser doesn't match.  `restrict` is a function transformer `(𝐷 ⇒ 𝑇) ⇒ ({𝑑: 𝐷 \| 𝑝(𝑑)} ⇒ 𝑇)` — applied, not composed — so each layer narrows the domain while preserving the value `𝑇`, and the chain stays well-typed (its honest second-order type would make a morphism-`Compose` ill-typed; `typecheck` rejects that).
+   - **Iterate-then-restricts chain** (`wrap_with_iterate`'s fallback) — build the iteration source by *applying* one `restrict(p)` per refinement, in `ccl::application_order`, to a chain-head `Apply(true ▷ const, Iterate)`, then compose the value-producing body onto it, when the hash-join recogniser doesn't match.  `restrict` is a function transformer `(𝐷 ⇒ 𝑇) ⇒ ({𝑑: 𝐷 \| 𝑝(𝑑)} ⇒ 𝑇)` — applied, not composed — so each stage narrows the domain while preserving the value `𝑇`, and the chain stays well-typed (its honest second-order type would make a morphism-`Compose` ill-typed; `typecheck` rejects that).
 
 Hash-join planning is the *specialised* strategy at an iteration site; the uniform iterate-then-restricts chain is the default.
 
@@ -229,7 +229,7 @@ This transformation reduces the domain iteration complexity and allows the runti
 
 For the full description of the input-policy split that this pass mirrors, see the [Operator Conversion section in `interpreter/design-operators.md`](/src/interpreter/design-operators.md#operator-conversion-interpreteroperator_conversionrs).  The short version:
 
-- **Input-internalising arms** in op-conversion (`Sum`, `Max`, `Converse`, `MapDomain`, `Uncurry`, `FlattenDomain`, `PermuteDomain`, `Copair` / `DisjointJoin`, `FinalOrDefault` stream side, `Loop` source, value-position `Record` fields, the catch-all `Apply`) compile their argument with `input=None`.  Each such argument is an iteration site and gets a chain-head `Apply(true ▷ const, Iterate)` as its source, with one `restrict(p)` *applied* per refinement layer.
+- **Input-internalising arms** in op-conversion (`Sum`, `Max`, `Converse`, `MapDomain`, `Uncurry`, `FlattenDomain`, `PermuteDomain`, `Copair` / `DisjointJoin`, `FinalOrDefault` stream side, `Loop` source, value-position `Record` fields, the catch-all `Apply`) compile their argument with `input=None`.  Each such argument is an iteration site and gets a chain-head `Apply(true ▷ const, Iterate)` as its source, with one `restrict(p)` *applied* per refinement.
 - **Input-threading arms** (`Const`, `Zip`, `Map`, `Restrict` itself, and the `Var` / `Let` / `Compose` infrastructure) accept `input=Some(upstream)` and pass it through, so their children inherit the surrounding iteration and are not iteration sites.
 - **The program root** and each function-typed field of a trailing sink-bound `Record` are iteration sites by *subscription*: the user-supplied consumer (or `SinkConsumer`) subscribes to the result, expecting an iterated stream.
 - **Each function-typed bound expression in the top-level `Let` chain** is wrapped because op-conversion's `Let` arm compiles `bound_expr` *unconditionally* (`operator_conversion.rs`, `let bound_op = convert_impl(bound_expr, …)?`), whether or not `body` references the binding — a non-iteration-bearing function-typed bound expr would otherwise reach an `input=None` arm and error (e.g. the `List` arm's "list literal reached op-conversion without an input").  This is a mechanical requirement of eager compilation, not subscription.  One consequence: a dead iterable binding (`let x = [1, 2, 3] in 42`) is eagerly compiled and iterate-wrapped rather than eliminated — making iteration use-driven so the wrap becomes unnecessary is tracked by [#232](https://github.com/cambra-dev/Cambra/issues/232).
@@ -238,7 +238,7 @@ At each iteration site, `wrap_with_iterate` first tries the specialised hash-joi
 
 When the hash-join rewrite doesn't fire, the chain that `wrap_with_iterate` emits is:
 - A single chain-head `Apply(true ▷ const, Iterate)` over the unrefined base domain — op-conversion compiles this to a bare `IterateExtent` (no filter tile, since the predicate is trivially true).
-- One `restrict(p)` *applied* per refinement layer, innermost-first.  Each `restrict` is a function transformer applied to the source it narrows — not a morphism composed with it — so `make_restrict` keeps the term well-typed (its honest second-order type makes a morphism-`Compose` ill-typed; `typecheck` rejects that).  Op-conversion compiles each applied `restrict` to a `Restrict` tile fed the previous step's tile as `input=Some(_)`.
+- One `restrict(p)` *applied* per refinement, in `ccl::application_order`.  Each `restrict` is a function transformer applied to the source it narrows — not a morphism composed with it — so `make_restrict` keeps the term well-typed (its honest second-order type makes a morphism-`Compose` ill-typed; `typecheck` rejects that).  Op-conversion compiles each applied `restrict` to a `Restrict` tile fed the previous step's tile as `input=Some(_)`.
 - The value-producing body is then composed onto that source (`source ≫ body`) as a genuine CCC morphism.
 
 For an unrefined site, the source is just the chain-head iterate.  For a refined site `{D | p}`, it's `iterate ▷ (p ▷ restrict)`.  For nested `{{D | p_inner} | p_outer}`, it's `iterate ▷ (p_inner ▷ restrict) ▷ (p_outer ▷ restrict)` — matching the goldens in `tests/compilation_pipeline/`.
diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md
index 75790ab9e..a5ae4be1e 100644
--- a/src/ccl/design/type-inference.md
+++ b/src/ccl/design/type-inference.md
@@ -281,7 +281,7 @@ Vanilla algebraic subtyping makes a `let`-bound function polymorphic by **freshe
 
 **How Cambra applies this — and then lowers it.** A `let` binding a *function definition* (`should_generalize`) is typed one level deeper (`in_let_rhs`) and generalized into a `PolyScheme` at the binding level (`scoped_let`); each `Var` use then `instantiate`s a fresh copy, exactly the freshening above. Because every pass after inference is monomorphic, the generalized binding is lowered to concrete code **inside the coalesce walk** (integrated monomorphization): the walk carries a scope of *specialization frames* — one per in-scope generalized `let`, plus shadow markers for every other binder — and a use of a generalized binding specializes at first visit (`specialize_use`). By coalesce time the constraint graph is *complete* (emission saw the whole program), so a use's instantiation is fully determined when the bottom-up walk reaches it: the walk resolves it off the live graph, and on a memo miss clones the definition (`freshen_expr_type_slots` freshens an independent copy — uniformly over terms and types, so a refinement predicate's slots and the suspended-substitution payloads riding the copied bound edges are renamed in the same traversal as every other slot), **pins the clone two-way to the use's live instantiation type**, coalesces the clone re-entrantly *in the definition site's scope* (entries pushed between definition and use are suspended, so a same-named binder introduced in between cannot capture the clone's references), renames the use to a synthetic `Mono` name (`Name::mono`) carrying the source binding plus a globally-fresh uid, and stamps the specialization's resolved type on it. When the `let`'s body walk completes, the node rebuilds itself as the chain of demanded specializations (`coalesce_generalized_let`), running the §6.2 `let`-closing discharge per spliced layer; a binding never demanded is resolved for its diagnostics and then dropped as dead code (see [Typechecking a never-called definition](#typechecking-a-never-called-definition)). Uses that instantiate the definition identically share one clone — the memo is keyed on a `SpecKey`, taken from the use's live type before its pin, and an entry stores the key of the use that minted it (see [Keying a specialization](#keying-a-specialization)). The definition's own subtree is never coalesced in place *while it has clones*: its quantified variables have no use-site bounds, so coalescing it would both produce an under-determined type and overwrite the bound-bearing `InferVar`s the clones freshen from. A definition with no clones is the never-called case above, where neither objection applies.
 
-Specializing *during* the walk — rather than splicing after it — is load-bearing twice over. First, every parent derives its type from concrete children on the first pass: in particular a parent `Apply`'s dependent-codomain discharge forces against the specialization's resolved predicate terms, so parent types are never re-derived from a second, graph-unreachable copy of the discharge logic. Second, chained polymorphism (a generalized UDF used only inside *another* generalized definition, poly-calls-poly) needs no special ordering: the inner use is reached only inside an outer clone's re-entrant walk, after that clone's pin has driven the use's instantiation concrete, and the inner binding's frame is still in scope below the outer's. The ordering invariant that makes in-walk specialization sound: **specialization may only add bounds to variables the walk has not yet read** — a use's pin touches its own instantiation variables (read right after, at its own stamp), the clone's fresh variables (read only inside the clone's walk), and otherwise deposits only α-copies of demands the instantiation already made at emit; `coalesce_node`'s `Apply` arm coalesces function before argument to keep even those copies behind the read front. The invariant is **checked explicitly, not just argued**: the walk logs every graph read as a `(var-laden type, resolution)` pair (the snapshot shares the live `InferVar`s), and `assert_reads_stable` re-resolves each against the *final* graph at end of pass, requiring the structural skeleton — bases, ranges, shapes, refinement-layer count, with under-determined positions wildcarded and predicate *content* deferred to `check_scope_valid` / the post-inference reconcile — to be unchanged. A pin that retroactively altered an already-read variable's resolution trips it by name (debug builds; free in release). Refinement layers count because a refinement is lattice content like a record field, so a bound determines it as much as it determines the base; the **one** read that excludes them is a use's own instantiation resolution, where the pin that immediately follows the read is itself what moves the refinements (`ReadPurpose::Instantiation`). That is sound because the read's consumers are refinement-insensitive — it seeds the clone's channel-domain pairings and blames a resolution failure — and, in particular, *sharing does not ride on it*: that is the `SpecKey`'s job, and a key consults both bound directions precisely so it does not depend on which polarity a rendering would have picked. The read's *skeleton* is still held fixed — a stale one would pair channel domains wrong. The contravariant-domain coalescing of §2 — the opposite-polarity fallback plus `coalesce_node`'s per-morphism domain specialization (projections and lambdas) — is the monomorphic coalescing rule for those vars; it is sound because every variable reaching coalesce is monomorphically determined (§1).
+Specializing *during* the walk — rather than splicing after it — is load-bearing twice over. First, every parent derives its type from concrete children on the first pass: in particular a parent `Apply`'s dependent-codomain discharge forces against the specialization's resolved predicate terms, so parent types are never re-derived from a second, graph-unreachable copy of the discharge logic. Second, chained polymorphism (a generalized UDF used only inside *another* generalized definition, poly-calls-poly) needs no special ordering: the inner use is reached only inside an outer clone's re-entrant walk, after that clone's pin has driven the use's instantiation concrete, and the inner binding's frame is still in scope below the outer's. The ordering invariant that makes in-walk specialization sound: **specialization may only add bounds to variables the walk has not yet read** — a use's pin touches its own instantiation variables (read right after, at its own stamp), the clone's fresh variables (read only inside the clone's walk), and otherwise deposits only α-copies of demands the instantiation already made at emit; `coalesce_node`'s `Apply` arm coalesces function before argument to keep even those copies behind the read front. The invariant is **checked explicitly, not just argued**: the walk logs every graph read as a `(var-laden type, resolution)` pair (the snapshot shares the live `InferVar`s), and `assert_reads_stable` re-resolves each against the *final* graph at end of pass, requiring the structural skeleton — bases, ranges, shapes, refinement-set cardinality, with under-determined positions wildcarded and predicate *content* deferred to `check_scope_valid` / the post-inference reconcile — to be unchanged. A pin that retroactively altered an already-read variable's resolution trips it by name (debug builds; free in release). The refinement count is part of the skeleton because a refinement is lattice content like a record field, so a bound determines it as much as it determines the base; the **one** read that excludes them is a use's own instantiation resolution, where the pin that immediately follows the read is itself what moves the refinements (`ReadPurpose::Instantiation`). That is sound because the read's consumers are refinement-insensitive — it seeds the clone's channel-domain pairings and blames a resolution failure — and, in particular, *sharing does not ride on it*: that is the `SpecKey`'s job, and a key consults both bound directions precisely so it does not depend on which polarity a rendering would have picked. The read's *skeleton* is still held fixed — a stale one would pair channel domains wrong. The contravariant-domain coalescing of §2 — the opposite-polarity fallback plus `coalesce_node`'s per-morphism domain specialization (projections and lambdas) — is the monomorphic coalescing rule for those vars; it is sound because every variable reaching coalesce is monomorphically determined (§1).
 
 #### Typechecking a never-called definition
 
@@ -477,9 +477,9 @@ analysis over an algebraic-subtyping system, including where it stops being
 possible, at the cyclic flow of polymorphic recursion.)
 
 **Specializing precisely is the correct rule, not a budget choice.** A refinement
-layer on an iterated domain is *compiled* — `planning::iterate` emits one
-`restrict(p)` filter per layer — so a refinement is code, and two clones pinned to
-different refinements are genuinely different code. Since every literal carries its
+on an iterated domain is *compiled* — `planning::iterate` emits one `restrict(p)`
+filter per refinement, in `application_order` — so a refinement is code, and two
+clones pinned to different refinements are genuinely different code. Since every literal carries its
 own singleton ([A literal is refined by its own value](#a-literal-is-refined-by-its-own-value)),
 the practical rule is one specialization per distinct argument tuple. `inline`
 beta-reduces scalar UDFs, so the cost lands on collection-producing ones, which it
@@ -742,10 +742,27 @@ Singletons are *not* erased after inference. They are ordinary refinements and r
 
 A **refined type** `{T | p}` carries a *set* of [`Refinement`]s, and the lattice treats each as a black box: it accumulates them and matches them by identity, never reasoning about what they imply (the predicate's logical content is real and used by the runtime, just opaque *here*). It is a fourth structural dimension on `CompactType`, width-subtyped exactly like records: **`{b₁ | S₁} <: {b₂ | S₂}` iff `b₁ <: b₂` and `S₂ ⊆ S₁ ∪ refinements(b₁)`** — more refinements ⇒ subtype. So `{T | p, q} <: {T | p}` and `{T | p} <: T`, but `{T | q} ⊀ {T | p}`. Refinements match by **type-blind structural equality of their predicate terms** (`Refinement`'s `PartialEq` / `eq_refinement_predicate`) — *not* by predicate implication (`{T | x > 0} ⊀ {T | x > -1}`). Structural matching makes refinement identity agnostic to *where* a predicate was constructed (join planning re-mints `{D | p}` at every marker it emits — `make_iterate` / `make_restrict` / `refine_with` — and must match the structurally-identical contract recorded elsewhere on the tree) and to in-place type resolution (copies of one predicate along a monomorphization descent line differ only in their inferred-type slots); a pointer-equal predicate `Rc` short-circuits as the fast path, since a refinement that merely flows around shares its `Rc`. The refinement set merges with the *same polarity rule as `rec`* (positive ⇒ intersect, negative ⇒ union) and is carried verbatim through simplification (refinements are positional, never folded into a variable's identity, so co-occurrence merging can't move or drop them).
 
+##### The set is the representation, not just the reading
+
+`Type::Refinement` carries a `RefinementSet` — unordered, deduplicated, with set-semantic `Eq`/`Hash` — and `Type::refined` is the sole constructor, establishing two invariants: the set is non-empty, and the base is never itself a refinement. Nested layers flatten, so `{{𝑇 | 𝑝} | 𝑞}` is *unrepresentable* and "which layer is outermost" cannot be asked.
+
+That question previously had an answer, and the answer was constraint **arrival order**: two refined upper bounds meeting at one variable produced `{{𝑇 | 𝑞} | 𝑝}` or `{{𝑇 | 𝑝} | 𝑞}` depending on which arrived first. Subtyping never cared — the deficit machinery above already compares layers as a set — but `Type`'s derived equality did, and structural equality is load-bearing wherever a type is an **identity**: the trivial-equality short-circuit in `constrain_go`, cache keys, `SpecKey`, and the recorded-vs-recomputed walls. One `Vec` was serving three incompatible readings — a set to subtyping, a stack to planning, an identity to the walls.
+
+Flattening is sound because every refinement at a position restricts the same underlying element: a refinement narrows *which* values inhabit a type, it does not change them, so an outer refinement's `__elem` ranges over exactly the values an inner one does. Canonically *sorting* the `Vec` was tried and rejected: it pins the ambiguity rather than deleting it, and it denies planning the freedom to apply refinements in whatever order it likes.
+
+##### Materializing a refinement set is a pipeline, and a pipeline is ordered
+
+The set is unordered as a *fact about a value*. Materializing it is not: planning emits one `restrict` per refinement, and stage 𝑘 reads elements already narrowed by stages 1..𝑘-1, so its element type is the base narrowed by the refinements applied before it — not the bare base. Planning therefore **chooses** an order.
+
+Which order is free (any of them yields a well-typed pipeline for the same final domain, and a cost model could pick the cheapest filter first); choosing *differently in two places* is not, since the types along the pipeline and the predicates compiled for it must agree. `ccl::application_order` is the single place that choice is made, and it keys on the refinements' **content** — their rendered predicates — never on the set's physical order, so the built term is reproducible however the refinements happened to accumulate.
+
+The chosen order is a **permutation** of the physical one, and that is the trap: a site rewriting refinements *in place* walks them physically, and zipping the application order's types onto that walk pairs refinements with the wrong element type — silently, since the two sequences have equal length. `application_elem_types` does the permutation explicitly and is what such a site uses.
+
+Two classes of order-dependence survive a compile-clean rewrite of this kind: a consumer that *iterates* the set and lets the order reach something observable, and a dedup that keeps the first-inserted of two `eq`-equal members whose type-blind-equal predicate terms carry different embedded type slots. `CAMBRA_REFINEMENT_ORDER=reverse` (debug builds only) flips the set's physical order globally, and CI runs the suite both ways — an unrun knob rots exactly as an uncompiled feature does. The variable is read at runtime, so the reversed pass reuses the binaries the ordinary one built.
 
 **A refinement never changes a type's shape.** It is a claim about the value at a position, not part of the structure carrying it, so `{(𝐷 ⇒ 𝑉) | 𝑝}` *is* a function and `{Mut(𝑉, 𝐷) | 𝑝}` *is* a mutable variable. Every rule that dispatches on or destructures a shape therefore looks *through* the outer layers first — `Type::peel_refinements`, and the handle accessors `Type::mut_value_type` / `as_feed` / `is_handle` built on it, which are what the typing rules and the second-class `Mut` discipline both ask "is this a mutable variable?" with. It is the same claim-versus-structure distinction a trait obligation draws when it reads a base off an operand ([Refinements are transparent](#refinements-are-transparent)): what narrowing consumes is the structure, and the refinement rides along untouched.
 
-A refinement is **required**, so `constrain_subtype` is strict for *concrete* bases: an unrefined concrete value does **not** flow into a refined position (`T ⊀ {T | p}`), and `{T | q} ⊀ {T | p}`. The one subtlety is the `S₂ ⊆ S₁ ∪ refinements(b₁)` clause: when the subtype side's base `b₁` is an **inference variable**, it can still acquire the deficit `S₂ \ S₁`, so the solver flows `b₁ <: {b₂ | S₂ \ S₁}` onto the variable rather than rejecting (the refinement analog of how the record/function arms thread structure through a variable base; it fails later iff the variable resolves to a concrete base lacking those refinements). This is what lets a value that is *already* refined be cast to acquire a further refinement — `{D | p} ⇒ V <: {?a | q} ⇒ V` records `?a <: {D | p}`, stacking `q` over `p` (nested list-comprehension filters). Acquiring a refinement on a *concrete* value is still an *explicit* operation, not subsumption: the explicit `Cast` node from [PR #218](https://github.com/cambra-dev/Cambra/pull/218) (an upcast — `value <: target` — written `cast({D | r} ⇒ V, value)`) makes refinement-acquisition explicit, and the interpreter compiles a refinement on a **collection domain** to a runtime `Restrict`/`Filter` at the iteration boundary (the `Iterate`/`Restrict` arms of `operator_conversion`, where `extent_of` strips the domain refinement into a `Restrict`). The predicate `Expr` of each refinement is inferred/coalesced like any other sub-tree (annotation-borne predicates via `emit_annotation_predicates` / `coalesce_type_predicates`).
+A refinement is **required**, so `constrain_subtype` is strict for *concrete* bases: an unrefined concrete value does **not** flow into a refined position (`T ⊀ {T | p}`), and `{T | q} ⊀ {T | p}`. The one subtlety is the `S₂ ⊆ S₁ ∪ refinements(b₁)` clause: when the subtype side's base `b₁` is an **inference variable**, it can still acquire the deficit `S₂ \ S₁`, so the solver flows `b₁ <: {b₂ | S₂ \ S₁}` onto the variable rather than rejecting (the refinement analog of how the record/function arms thread structure through a variable base; it fails later iff the variable resolves to a concrete base lacking those refinements). This is what lets a value that is *already* refined be cast to acquire a further refinement — `{D | p} ⇒ V <: {?a | q} ⇒ V` records `?a <: {D | p}`, so the position carries both `p` and `q` (nested list-comprehension filters). Acquiring a refinement on a *concrete* value is still an *explicit* operation, not subsumption: the explicit `Cast` node from [PR #218](https://github.com/cambra-dev/Cambra/pull/218) (an upcast — `value <: target` — written `cast({D | r} ⇒ V, value)`) makes refinement-acquisition explicit, and the interpreter compiles a refinement on a **collection domain** to a runtime `Restrict`/`Filter` at the iteration boundary (the `Iterate`/`Restrict` arms of `operator_conversion`, where `extent_of` strips the domain refinement into a `Restrict`). The predicate `Expr` of each refinement is inferred/coalesced like any other sub-tree (annotation-borne predicates via `emit_annotation_predicates` / `coalesce_type_predicates`).
 
 **Refinements in the post-inference check.** The post-inference structural check (`infer::check`, reimplemented on the same structural rules as emission via the `Typing` trait — see §2, *The post-inference check*) is **strict and refinement-aware throughout** — it does not strip refinements before its width-subtyping checks. It runs `constrain_subtype` in two places, both fully refinement-aware:
 
@@ -909,7 +926,7 @@ Once constraints are resolved (Pass 2), `coalesce_compact` resolves each node's
 
 * **Products:** dense `Index` keys become `Type::Tuple`; `Name` keys become `Type::Record`; a sparse `Index` product (an open/under-determined position) coalesces to a fresh `Type::Infer` rather than a concrete product. **No keys at all become `Unit`** — the product of zero fields, which has exactly one representation (see [docs/chl-spec.md](../../../docs/chl-spec.md#66-the-empty-product-is-unit)); `Type::Tuple([])` and `Type::Record([])` are invalid. The empty case has no keys to tell positional from named keying, so without the collapse each site picks a spelling arbitrarily — here on `rec.is_empty()`, in `product` on a vacuously-all-`Name` test — and two spellings for one type fail to reconcile at the consistency wall, which compares a node's recorded type against one rebuilt from its children.
 * **Variants:** materialize into `Type::Variant(Vec<(FieldKey, Type)>)` with tags in `BTreeMap` order. A variant payload sits at a record-field-like position, so it inherits that position's polarity and coalesces by the same rule as a record field value. An all-`Index` variant pretty-prints as a bare `A | B | C`. Arm *order* is a presentation detail and nothing depends on it: arms are keyed by tag everywhere downstream — in a `Type::Variant`, in a runtime union column, and in `variant_project`/`variant_wrap` — so a variant a pass constructs by hand (the writer decision variant ``{`commit{𝑃} | `abort}``) and the same variant materialized by the solver in sorted order are interchangeable.
-* **Refinements:** the refinement set carried at a position is re-wrapped as nested `Type::Refinement` layers around the materialized inner type (in first-insertion order — deterministic and, since consumers strip at all depths, order-independent).
+* **Refinements:** the refinement set carried at a position is re-attached to the materialized inner type through `Type::refined`, which is one `Type::Refinement` node holding the whole set — there are no layers to order. An empty set (and the `None` a non-value contribution carries) yields the bare type.
 * **Incompatible bounds:** if a variable accumulates multiple distinct concrete primitives (e.g. `Int` and `String`) with no tag to discriminate them, the solver emits an `IncompatibleBounds` error. A *tagged* sum is unaffected — ``{`i{Int} | `s{String}}`` is a single `Variant`, not a primitive collision.
 * **Recursive types:** the algorithm has no occurs check. With one-way Apply edges a self-application like `λx. x x` produces no cyclic bound graph — it types cleanly (MLsub would give `(α ∧ (α ⇒ β)) ⇒ β`; Cambra drops the unconstrained `α` leg and infers `(?a ⇒ ?b) ⇒ ?c`, an unapplied-lambda type carrying `Infer`s), while *misusing* one (`(λy. y y)(1)`) still fails with `ExpectedFunction`. Should a residual cyclic bound graph ever form, `coalesce_compact` rejects it with a `RecursiveType` error — a defensive check; no current emission path produces one.
 
diff --git a/src/ccl/expr.rs b/src/ccl/expr.rs
index f6942e803..ca6b8bc15 100644
--- a/src/ccl/expr.rs
+++ b/src/ccl/expr.rs
@@ -2052,7 +2052,7 @@ pub struct Pattern {
     /// then a reserved spelling nothing can refer to. [`Self::empty_payload`] carries
     /// what the source said about the payload's type; the presence of this does not.
     pub binding: TypedBinding,
-    /// Whether the arm claims the tag carries **nothing**: the surface `` case
+    /// Whether the arm asserts the tag carries **nothing**: the surface `` case
     /// `tag: ``, as against `` case `tag(_): ``, which has a payload it does not read.
     ///
     /// The claim is about the type, so it is a constraint rather than a formality.
diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs
index a330822b1..a45ba8c07 100644
--- a/src/ccl/infer/api.rs
+++ b/src/ccl/infer/api.rs
@@ -1253,7 +1253,7 @@ fn collect_type_errors(
             collect_type_errors(value, context_sym, strictness, errors, seen_refinements);
             collect_type_errors(domain, context_sym, strictness, errors, seen_refinements);
         }
-        Type::Refinement(inner, refinement) => {
+        Type::Refinement(inner, refinements) => {
             // Walk each predicate term only once: a predicate term shared by
             // `Rc` across occurrences (its own type slots can carry the same
             // refinement) is a DAG, so this dedups it. (Immutable predicates
@@ -1265,8 +1265,15 @@ fn collect_type_errors(
             // [`crate::ccl::ccl_utils::walk_refined_predicates`]). This site
             // doesn't share the helper because it mixes per-node error checks
             // with the refinement walk.
-            if seen_refinements.insert(refinement.predicate_id()) {
-                collect_expr_errors(&refinement.predicate, strictness, errors, seen_refinements);
+            for refinement in refinements {
+                if seen_refinements.insert(refinement.predicate_id()) {
+                    collect_expr_errors(
+                        &refinement.predicate,
+                        strictness,
+                        errors,
+                        seen_refinements,
+                    );
+                }
             }
             collect_type_errors(inner, context_sym, strictness, errors, seen_refinements);
         }
diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs
index 6958436a5..de043bb56 100644
--- a/src/ccl/infer/context.rs
+++ b/src/ccl/infer/context.rs
@@ -253,10 +253,9 @@ impl InferCtx {
             // Refinements ride the lattice: keep the wrapper, normalize the
             // inner (so a `Refinement(Hole, r)` source annotation becomes
             // `Refinement(?fresh, r)` rather than losing the refinement).
-            Type::Refinement(inner, r) => Type::Refinement(
-                Box::new(self.normalize_annotation_in(inner, telescope)),
-                r.clone(),
-            ),
+            Type::Refinement(inner, r) => {
+                Type::refined(self.normalize_annotation_in(inner, telescope), r.clone())
+            }
             // Structural types are already solver-ready; recurse to
             // normalize any nested holes/refinements. A named function's binder
             // is in scope in its codomain — the annotation's own Pi
@@ -330,7 +329,7 @@ impl InferCtx {
             // `unit`: a singleton adds nothing to a one-inhabitant base.
             return base;
         };
-        Type::Refinement(Box::new(base), Refinement::sharing(&predicate))
+        Type::refined_one(base, Refinement::sharing(&predicate))
     }
 }
 
diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs
index 631bf9281..3f5044309 100644
--- a/src/ccl/infer/emit.rs
+++ b/src/ccl/infer/emit.rs
@@ -369,11 +369,11 @@ pub(super) fn emit_annotation_predicates<C: Typing>(
         // `BoundedHole` here: recurse into the bound, or a predicate written inside one
         // (`x <: {Int | p}`) never gets typed.
         Type::BoundedHole(bound) => emit_annotation_predicates(bound, ctx),
-        Type::Refinement(inner, r) => {
-            // The annotation's refinement is bare over REFINEMENT_BINDER, just
+        Type::Refinement(inner, refinements) => {
+            // The annotation's refinements are bare over REFINEMENT_BINDER, just
             // like a cast target's — bind the element over the refined base and
             // check `Bool`.
-            emit_bare_predicate(r, inner, ctx)?;
+            refinements.try_rewrite_each(|_, r| emit_bare_predicate(r, inner, ctx))?;
             emit_annotation_predicates(inner, ctx)
         }
         Type::Fun {
@@ -547,9 +547,9 @@ fn complete_annotation(ann: &Type, inferred: &Type) -> Type {
         // refinement itself is the user's claim and is kept. `peel_refinements`
         // on the inferred side because its own refinements describe the *value*,
         // and this is filling in a *shape*.
-        (Type::Refinement(base, r), _) => Type::Refinement(
-            Box::new(complete_annotation(base, inferred.peel_refinements())),
-            r.clone(),
+        (Type::Refinement(base, refinements), _) => Type::refined(
+            complete_annotation(base, inferred.peel_refinements()),
+            refinements.clone(),
         ),
         // The binder and kind come from the *annotation*, per the rule
         // above: a kind is something an annotation can state (`List(T)` is a data
@@ -740,13 +740,12 @@ pub(super) fn emit_cast<C: Typing>(
     // it on the `target` slot is what carries the typed predicate onto the
     // syntactic node; the result domain below then clones the typed refinement.
     if let Type::Fun { domain, .. } = target
-        && let Type::Refinement(_, r) = domain.as_mut()
+        && let Type::Refinement(_, refinements) = domain.as_mut()
     {
-        emit_bare_predicate(r, &d, ctx)?;
+        refinements.try_rewrite_each(|_, r| emit_bare_predicate(r, &d, ctx))?;
     }
-    let refinement = cast_target_refinement(target);
-    let domain = match refinement {
-        Some(r) => Type::Refinement(Box::new(d), r),
+    let domain = match cast_target_refinement(target) {
+        Some(refinements) => Type::refined(d, refinements),
         None => d,
     };
     // A cast re-views the value *at* `target`, so the result carries `target`'s
diff --git a/src/ccl/infer/mod.rs b/src/ccl/infer/mod.rs
index 1c39295a1..f6dfb0cf9 100644
--- a/src/ccl/infer/mod.rs
+++ b/src/ccl/infer/mod.rs
@@ -382,7 +382,7 @@ pub(super) fn lit_base(lit: &Lit) -> Type {
 /// literal takes [`lit_base`] — refining *it* too would not terminate.
 pub fn lit_singleton(lit: &Lit) -> Type {
     match singleton_predicate(lit) {
-        Some(predicate) => Type::Refinement(Box::new(lit_base(lit)), Refinement::born(predicate)),
+        Some(predicate) => Type::refined_one(lit_base(lit), Refinement::born(predicate)),
         None => lit_base(lit),
     }
 }
@@ -602,10 +602,7 @@ pub(crate) mod test_helpers {
             BinOpKind::Compare(CompareKind::Greater),
             rhs,
         );
-        Type::Refinement(
-            Box::new(Type::Base(BaseType::Int)),
-            Refinement::born(Rc::new(pred)),
-        )
+        Type::refined_one(Type::Base(BaseType::Int), Refinement::born(Rc::new(pred)))
     }
 
     /// Walk `expr`, counting `Let` bindings minted by specialization (their
diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs
index f6aed01d5..7497af637 100644
--- a/src/ccl/infer/solve.rs
+++ b/src/ccl/infer/solve.rs
@@ -300,7 +300,7 @@ fn assert_reads_stable(reads: &[ReadRecord]) {
 /// **bounds on inference variables**, so this checks the *structural skeleton* a
 /// bound determines — bases, ranges, sources, Pi binder names,
 /// function/product/variant shape, and, for a [`ReadPurpose::Stamp`] read, the
-/// *number* of refinement layers at each position. A refinement is lattice content
+/// *number* of refinements at each position. A refinement is lattice content
 /// like a record field, so a bound determines it as much as it determines the
 /// base: one appearing on — or vanishing from — a variable an earlier read
 /// consumed is exactly the staleness this guards, and with every literal
@@ -325,7 +325,7 @@ fn assert_reads_stable(reads: &[ReadRecord]) {
 ///   or leaving without depending on term identity, which legitimately churns.
 #[cfg(debug_assertions)]
 fn types_agree_modulo_unread(read: &Type, now: &Type, refinements: bool) -> bool {
-    // Peel refinement layers, counting them. The *base* under the refinements is
+    // Peel the refinements, counting them. The *base* under the refinements is
     // what recurses structurally; predicate content is out of scope (above).
     fn peel<'t>(mut t: &'t Type, layers: &mut usize) -> &'t Type {
         while let Type::Refinement(inner, _) = t {
@@ -410,7 +410,7 @@ fn types_agree_modulo_unread(read: &Type, now: &Type, refinements: bool) -> bool
 }
 
 /// The history half of [`types_agree_modulo_unread`], split out because it must run
-/// **before** the refinement-layer comparison (see the call site).
+/// **before** the refinement-count comparison (see the call site).
 ///
 /// Two histories of *different* kinds never agree — an `Overwrite` and a `Feed` are
 /// distinct handles even if their read views coincidentally line up. Rejecting that
@@ -426,7 +426,7 @@ fn types_agree_modulo_unread(read: &Type, now: &Type, refinements: bool) -> bool
 /// `channelize` erases to the concrete channel domain by substitution; the `ChanDom`
 /// arm agrees it by name.
 ///
-/// A **handle's own** outer refinement layers are peeled and not counted, unlike
+/// A **handle's own** outer refinements are peeled and not counted, unlike
 /// everywhere else in this comparison. They cannot be: the two sides here are legally a
 /// handle and its read view, which sit at different depths, so there is no layer count
 /// to compare. Only the handle side is peeled — the read view carries the value's own
@@ -1613,14 +1613,16 @@ fn coalesce_type_predicates(ty: &mut Type, level: Level, ctx: &mut CoalesceCtx)
                 "Type::BoundedHole reached the solver; `normalize_annotation` must erase it"
             )
         }
-        Type::Refinement(inner, r) => {
+        Type::Refinement(inner, refinements) => {
             // A handle clone, so `ctx` stays freely borrowable for the rebuild —
             // which re-enters this same memo through `coalesce_node` →
             // `coalesce_type_predicates`.
             let memo = ctx.pred_memo.clone();
-            memo.rebuild(r, &(), |pred| {
-                coalesce_node(pred, level, ctx);
-                true
+            refinements.rewrite_each(|_, r| {
+                memo.rebuild(r, &(), |pred| {
+                    coalesce_node(pred, level, ctx);
+                    true
+                });
             });
             coalesce_type_predicates(inner, level, ctx);
         }
@@ -2173,7 +2175,7 @@ pub(super) fn specialize_lambda_domain(lambda: &mut Expr, input: &Type) {
         return;
     }
     // Split the coalesced function type into its outer (function-level)
-    // refinement layers and the `Fun` shape.
+    // refinements and the `Fun` shape.
     let mut fn_layers = Vec::new();
     let mut cur = lambda.ty.clone();
     while let Type::Refinement(inner, r) = cur {
@@ -2189,7 +2191,7 @@ pub(super) fn specialize_lambda_domain(lambda: &mut Expr, input: &Type) {
     else {
         return;
     };
-    // Peel the domain's refinement layers down to the base `input` replaces.
+    // Peel the domain's refinements down to the base `input` replaces.
     let mut dom_layers = Vec::new();
     let mut base = *dom;
     while let Type::Refinement(inner, r) = base {
@@ -2211,9 +2213,7 @@ pub(super) fn specialize_lambda_domain(lambda: &mut Expr, input: &Type) {
         .into_iter()
         .rev()
         .filter(|r| !input_refinements.contains(&r))
-        .fold(recovered_input(&base, input), |acc, r| {
-            Type::Refinement(Box::new(acc), r)
-        });
+        .fold(recovered_input(&base, input), Type::refined);
     lambda.ty = fn_layers.into_iter().rev().fold(
         // Preserve the Pi binder: specialization rewrites only the domain
         // *shape*; a dependent codomain still refers to the same binder.
@@ -2223,7 +2223,7 @@ pub(super) fn specialize_lambda_domain(lambda: &mut Expr, input: &Type) {
             domain: Box::new(new_dom),
             codomain: cod,
         },
-        |acc, r| Type::Refinement(Box::new(acc), r),
+        Type::refined,
     );
     // The param slot was derived from the pre-specialization domain during the
     // lambda's own `coalesce_node`; re-derive it from the rewritten one.
@@ -2276,9 +2276,9 @@ mod tests {
         // Refinements are built here rather than via `refined_int`, which is
         // `debug_assertions`-only: the rule under test is not.
         let refined = |inner: Type| {
-            Type::Refinement(
-                Box::new(inner),
-                Refinement::born(std::rc::Rc::new(TypedExpr::lit(Lit::Bool(true)))),
+            Type::refined(
+                inner,
+                Refinement::born(std::rc::Rc::new(TypedExpr::lit(Lit::Bool(true)))).into(),
             )
         };
         let int = Type::Base(BaseType::Int);
@@ -2358,7 +2358,7 @@ mod tests {
         };
         let refinement = Refinement::born(std::rc::Rc::new(TypedExpr::lit(Lit::Bool(true))));
         let on_the_handle =
-            |t: Type| Type::Refinement(Box::new(t), Refinement::sharing(&refinement.predicate));
+            |t: Type| Type::refined_one(t, Refinement::sharing(&refinement.predicate));
 
         for (read, now) in [
             // handle vs its read view: the refined value sits one layer deeper.
@@ -2490,7 +2490,7 @@ mod tests {
         // Three uses, three distinct instantiations. Every literal carries its own
         // singleton, so the two `Int` uses instantiate `f` at *different* refined
         // types and get a specialization each — and that is the intended rule, not
-        // a shortfall: a refinement layer on an iterated domain is compiled (one
+        // a shortfall: a refinement on an iterated domain is compiled (one
         // `restrict` filter per layer), so refinements are code and two clones
         // pinned to different ones are genuinely different code.
         let f = TypedExpr::lambda("x", Type::Hole, TypedExpr::var("x"));
diff --git a/src/ccl/infer/solver/coalesce.rs b/src/ccl/infer/solver/coalesce.rs
index bf89faf16..b529ea4ce 100644
--- a/src/ccl/infer/solver/coalesce.rs
+++ b/src/ccl/infer/solver/coalesce.rs
@@ -291,15 +291,8 @@ fn coalesce_compact_go(ct: &CompactType, polarity: bool) -> Result<Type, Coalesc
         }
     };
 
-    // Re-wrap the refinements carried at this position. `extent_of`
-    // strips refinements at every depth and composes the resulting
-    // `Restrict`s, so the wrap order is semantically irrelevant;
-    // first-insertion order in the `Vec` makes it stable.
-    let out = ct
-        .refinements
-        .iter()
-        .fold(inner, |acc, r| Type::Refinement(Box::new(acc), r.clone()));
-    Ok(out)
+    // Re-attach the refinements carried at this position.
+    Ok(Type::refined(inner, ct.refinements.clone()))
 }
 
 /// Dissolve a position's feed `history_slot` into its other contributions when
@@ -772,6 +765,42 @@ mod tests {
         assert_eq!(out, ty);
     }
 
+    #[test]
+    fn refinements_meeting_at_one_variable_do_not_depend_on_arrival_order() {
+        // Two refined upper bounds meet at one variable. As nested layers the
+        // result was `{{Int | q} | p}` or `{{Int | p} | q}` by which arrived
+        // first; subtyping was indifferent either way (deficit matching compares
+        // refinements as a set), but `Type`'s equality was not, and structural
+        // equality is load-bearing where a type is an *identity*: the
+        // trivial-equality short-circuit, cache keys, and the
+        // recorded-vs-recomputed walls. One unordered set makes the two orders
+        // build the same type, so this asserts plain equality rather than
+        // equality after a canonical sort.
+        let coalesce_with_order = |first: &Type, second: &Type| {
+            let v = fresh_var(0);
+            constrain_subtype(&v, first, &mut ConstrainCache::new()).unwrap();
+            constrain_subtype(&v, second, &mut ConstrainCache::new()).unwrap();
+            coalesce_compact(&simplify_type(compact_type(&v))).unwrap()
+        };
+        let (p, q) = (
+            refined(prim(BaseType::Int), 1),
+            refined(prim(BaseType::Int), 2),
+        );
+        let a = coalesce_with_order(&p, &q);
+        let b = coalesce_with_order(&q, &p);
+        assert_eq!(a, b, "refinements must not depend on arrival order");
+        // Both survived: the meet of two refined upper bounds carries each
+        // side's restriction, so this is a two-member set and not one order
+        // winning.
+        assert_eq!(
+            a.refinements().len(),
+            2,
+            "expected both refinements, got {a}"
+        );
+        // Rendering is order-stable too, so a diagnostic cannot leak the order.
+        assert_eq!(format!("{a}"), format!("{b}"));
+    }
+
     #[test]
     fn var_constrained_to_refined_coalesces_refined() {
         // A fresh var equated to a refined type (both bounds) must coalesce
diff --git a/src/ccl/infer/solver/compact.rs b/src/ccl/infer/solver/compact.rs
index 504f8b6a7..1ea2e2fd9 100644
--- a/src/ccl/infer/solver/compact.rs
+++ b/src/ccl/infer/solver/compact.rs
@@ -13,7 +13,7 @@ use smol_str::SmolStr;
 
 use crate::ccl::subst::{RefinementScope, Subst};
 use crate::ccl::{
-    BaseType, HistoryKind, InferVarId, Name, Openness, Refinement, Type, fresh_infer_var_id,
+    BaseType, HistoryKind, InferVarId, Name, Openness, RefinementSet, Type, fresh_infer_var_id,
 };
 
 use crate::ccl::FieldKey;
@@ -289,15 +289,14 @@ pub struct CompactType {
     /// `Data ⊔ Data` join accumulated alternatives via [`union_domains`]), and the
     /// codomain. Recursively merged with polarity flip on the domain.
     pub fun: Option<CompactFun>,
-    /// Refinement contributions at this position. A set with `==`
-    /// membership (deduplicated by [`Refinement`]'s structural `PartialEq`),
-    /// stored as a `Vec` in first-insertion order. A refinement-set is
-    /// width-subtyped exactly like `rec`: more refinements ⇒ subtype
-    /// (`{T | p, q} <: {T | p}`), so at positive polarity the sets are
-    /// *intersected* and at negative *unioned* (see
-    /// [`CompactType::merge`]). The stored [`Refinement`] is the payload
-    /// carried to coalesce.
-    pub refinements: Vec<Refinement>,
+    /// Refinement contributions at this position — the same
+    /// [`RefinementSet`](crate::ccl::RefinementSet) the materialized `Type`
+    /// carries, so flattening and coalescing agree on what a refinement set *is*
+    /// rather than each keeping its own bag. A refinement set is width-subtyped
+    /// exactly like `rec`: more refinements ⇒ subtype (`{T | p, q} <: {T | p}`), so
+    /// at positive polarity the sets are *intersected* and at negative
+    /// *unioned* (see [`CompactType::merge`]).
+    pub refinements: RefinementSet,
     /// History-handle `(value, domain, kind)`, if a [`Type::History`]
     /// contributed here — a mutable variable (`kind: Overwrite`) or a feed channel
     /// (`kind: Feed`).
@@ -474,19 +473,13 @@ impl CompactType {
     /// position the value reliably carries only the refinements *both*
     /// sides guarantee; at a negative position a consumer that may
     /// impose either set imposes their union.
-    fn merge_refinements(pol: bool, lhs: Vec<Refinement>, rhs: Vec<Refinement>) -> Vec<Refinement> {
+    fn merge_refinements(pol: bool, lhs: RefinementSet, rhs: RefinementSet) -> RefinementSet {
         if pol {
             // The types are being unioned, so the refinements should be intersected.
-            lhs.into_iter().filter(|r| rhs.contains(r)).collect()
+            lhs.intersect(&rhs)
         } else {
             // The types are being intersected, so the refinements should be unioned.
-            let mut out = lhs;
-            for r in rhs {
-                if !out.contains(&r) {
-                    out.push(r);
-                }
-            }
-            out
+            lhs.union(&rhs)
         }
     }
 
@@ -778,14 +771,14 @@ fn compact_go(
         // application's argument) before the refinement lands in the position.
         // The predicate is an immutable term, so a non-vacuous force builds a
         // fresh predicate from the (freshened) bound's content directly.
-        Type::Refinement(inner, r) => {
+        Type::Refinement(inner, refinements) => {
             let mut ct = compact_go(inner, pol, subst_acc, parents, st);
-            let r = subst_acc.force_refinement(r);
-            // References to the walk's enclosing binders become indices
-            // before the refinement is compared or stored.
-            let r = st.scope.close(&r);
-            if !ct.refinements.contains(&r) {
-                ct.refinements.push(r);
+            for r in refinements {
+                let r = subst_acc.force_refinement(r);
+                // References to the walk's enclosing binders become indices
+                // before the refinement is compared or stored.
+                let r = st.scope.close(&r);
+                ct.refinements.insert(r);
             }
             ct
         }
@@ -1054,11 +1047,7 @@ fn compact_go(
                     // so both hold of it.
                     if let Some(primary) = bound.take() {
                         recovered.vars.extend(primary.vars);
-                        for r in primary.refinements {
-                            if !recovered.refinements.contains(&r) {
-                                recovered.refinements.push(r);
-                            }
-                        }
+                        recovered.refinements.extend(primary.refinements);
                     }
                     bound = Some(recovered);
                 }
@@ -1274,8 +1263,8 @@ mod refinement_closing_tests {
             name: Some(Name::raw(binder)),
             kind: FunKind::Data,
             domain: Box::new(Type::UIntRange(3)),
-            codomain: Box::new(Type::Refinement(
-                Box::new(Type::Base(BaseType::Int)),
+            codomain: Box::new(Type::refined_one(
+                Type::Base(BaseType::Int),
                 Refinement::born(dep_pred(binder)),
             )),
         }
@@ -1309,18 +1298,23 @@ mod refinement_closing_tests {
             b.without_pi_names(),
             "α-variant bound merge must be arrival-order-independent"
         );
-        // The α-copies collapsed: one refinement layer, spelled as the index,
-        // nothing dangling.
+        // The α-copies collapsed: one refinement, spelled as the index, nothing
+        // dangling.
         let Type::Fun { codomain, .. } = &a else {
             panic!("expected a function, got {a}");
         };
-        let Type::Refinement(base, r) = &**codomain else {
-            panic!("expected exactly one refinement layer, got {codomain}");
+        let Type::Refinement(base, refinements) = &**codomain else {
+            panic!("expected a refined codomain, got {codomain}");
         };
         assert!(
             !matches!(&**base, Type::Refinement(..)),
-            "the two α-copies of one constraint must dedup to one layer, got {codomain}"
+            "a refinement's base is never itself refined under `RefinementSet`, got {codomain}"
         );
+        let Some(r) = refinements.sole() else {
+            panic!(
+                "the two α-copies of one constraint must dedup to one refinement, got {codomain}"
+            );
+        };
         assert!(
             crate::ccl::subst::type_free_vars(&a).is_empty(),
             "no refinement may dangle on a free binder name: {a}"
@@ -1353,8 +1347,8 @@ mod refinement_closing_tests {
                 name: Some(Name::raw("y")),
                 kind: FunKind::Data,
                 domain: Box::new(Type::UIntRange(4)),
-                codomain: Box::new(Type::Refinement(
-                    Box::new(Type::Base(BaseType::Int)),
+                codomain: Box::new(Type::refined_one(
+                    Type::Base(BaseType::Int),
                     Refinement::born(dep_pred(referenced)),
                 )),
             }),
diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs
index 03094ac7e..ef2f5f3c4 100644
--- a/src/ccl/infer/solver/constrain.rs
+++ b/src/ccl/infer/solver/constrain.rs
@@ -22,7 +22,8 @@ use smol_str::SmolStr;
 use crate::ccl::subst::Subst;
 use crate::ccl::ty::FunKind;
 use crate::ccl::{
-    BaseType, Bound, HistoryKind, InferVar, InferVarId, Level, Name, Refinement, Type,
+    BaseType, Bound, HistoryKind, InferVar, InferVarId, Level, Name, Refinement, RefinementSet,
+    Type,
 };
 
 use super::traits::{Trait, link_watches, notify_lower};
@@ -1018,8 +1019,8 @@ fn constrain_go_impl(
         // refinement on a concrete value is an explicit `Restrict`, not
         // subsumption.
         (Type::Refinement(..), _) | (_, Type::Refinement(..)) => {
-            let (lbase, lrefs) = peel_refinements(lhs);
-            let (rbase, rrefs) = peel_refinements(rhs);
+            let (lbase, lrefs) = (lhs.peel_refinements(), lhs.refinements());
+            let (rbase, rrefs) = (rhs.peel_refinements(), rhs.refinements());
             // The refinements rhs requires that no transported lhs layer
             // matches (by `Refinement`'s structural `PartialEq`). Each side's
             // refinements are forced through its own morphism into the ambient frame
@@ -1028,10 +1029,10 @@ fn constrain_go_impl(
             // carries `sr` for them.
             let lrefs_in_ambient: Vec<Refinement> =
                 lrefs.iter().map(|l| sl.force_refinement(l)).collect();
-            let deficit: Vec<&Refinement> = rrefs
+            let deficit: RefinementSet = rrefs
                 .iter()
-                .copied()
                 .filter(|r| !lrefs_in_ambient.contains(&sr.force_refinement(r)))
+                .cloned()
                 .collect();
             if deficit.is_empty() {
                 // lhs's explicit layers already supply every refinement rhs requires.
@@ -1040,7 +1041,7 @@ fn constrain_go_impl(
                 // Variable base: flow the deficit onto it (`b₁ <: {b₂ | deficit}`)
                 // rather than rejecting; it fails later iff the variable
                 // resolves to a concrete base lacking those refinements.
-                let demanded = wrap_refinements(rbase, &deficit);
+                let demanded = Type::refined(rbase.clone(), deficit);
                 constrain_go(lbase, &demanded, sl, sr, cache)
             } else {
                 Err(ConstrainError::Mismatch {
@@ -1057,30 +1058,6 @@ fn constrain_go_impl(
     }
 }
 
-/// Peel all outer [`Type::Refinement`] layers, returning the bare base type
-/// and the refinements carried by the peeled layers (outermost first).
-fn peel_refinements(ty: &Type) -> (&Type, Vec<&Refinement>) {
-    let mut refs = Vec::new();
-    let mut cur = ty;
-    while let Type::Refinement(inner, r) = cur {
-        refs.push(r);
-        cur = inner;
-    }
-    (cur, refs)
-}
-
-/// Re-wrap `base` in the given [`Type::Refinement`] layers (passed
-/// outermost-first), preserving their order.
-///
-/// Used by [`constrain_subtype`]'s refinement arm to rebuild the deficit
-/// refinement `{rbase | S₂ \ S₁}` from the rhs's own layers, so the kept refinements
-/// retain their real [`crate::ccl::Refinement`] payloads (predicate `Rc`s).
-fn wrap_refinements(base: &Type, refs: &[&Refinement]) -> Type {
-    refs.iter().rev().fold(base.clone(), |acc, r| {
-        Type::Refinement(Box::new(acc), (*r).clone())
-    })
-}
-
 /// Give an extrusion proxy the same trait obligations as the variable it
 /// approximates.
 ///
@@ -1161,10 +1138,9 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac
                 .collect(),
             *openness,
         ),
-        Type::Refinement(inner, r) => Type::Refinement(
-            Box::new(extrude(inner, pol, target_level, cache)),
-            r.clone(),
-        ),
+        Type::Refinement(inner, r) => {
+            Type::refined(extrude(inner, pol, target_level, cache), r.clone())
+        }
         // Invariant payload: polarity is meaningless under invariance, so
         // both children are extruded with two-way proxies (a history is read
         // *and* written) instead of the polar one-way approximation below.
@@ -1402,7 +1378,8 @@ mod tests {
                     TypedExpr::var(Name::elem()),
                     BinOpKind::Compare(CompareKind::Equals),
                     TypedExpr::var(referenced.clone()),
-                ))),
+                )))
+                .into(),
             )
         };
         // Construction closes the reference into `#0`.
@@ -1505,8 +1482,8 @@ mod tests {
         // (`Refinement: PartialEq`).
         use crate::ccl::{Lit, TypedExpr};
         let mk = || {
-            Type::Refinement(
-                Box::new(prim(BaseType::Int)),
+            Type::refined_one(
+                prim(BaseType::Int),
                 Refinement::born(Rc::new(TypedExpr::lit(Lit::Bool(true)))),
             )
         };
@@ -1525,8 +1502,8 @@ mod tests {
         // not one of them.
         use crate::ccl::{Lit, TypedExpr};
         let refined_dom = || {
-            Type::Refinement(
-                Box::new(Type::UIntRange(3)),
+            Type::refined_one(
+                Type::UIntRange(3),
                 Refinement {
                     predicate: Rc::new(TypedExpr::lit(Lit::Bool(true))),
                 },
@@ -1611,8 +1588,8 @@ mod tests {
         use std::collections::hash_map::DefaultHasher;
         use std::hash::{Hash, Hasher};
         let mk = || {
-            Type::Refinement(
-                Box::new(prim(BaseType::Int)),
+            Type::refined_one(
+                prim(BaseType::Int),
                 Refinement::born(Rc::new(TypedExpr::lit(Lit::Bool(true)))),
             )
         };
@@ -1639,8 +1616,8 @@ mod tests {
         );
 
         // A structurally *different* predicate must not collapse into it.
-        let c = Type::Refinement(
-            Box::new(prim(BaseType::Int)),
+        let c = Type::refined_one(
+            prim(BaseType::Int),
             Refinement::born(Rc::new(TypedExpr::lit(Lit::Bool(false)))),
         );
         assert_ne!(a, c, "distinct predicates must stay distinct");
@@ -2218,8 +2195,8 @@ mod tests {
         let Type::Fun { domain, .. } = ty else {
             panic!("expected fun, got {ty}");
         };
-        let Type::Refinement(_, r) = domain.as_ref() else {
-            panic!("expected refined domain, got {domain}");
+        let [r] = domain.refinements() else {
+            panic!("expected a singly-refined domain, got {domain}");
         };
         crate::ccl::symbolic::symbolic(&r.predicate)
     }
@@ -2238,10 +2215,7 @@ mod tests {
             "k",
             prim(BaseType::Int),
             Type::fun(
-                Type::Refinement(
-                    Box::new(prim(BaseType::Int)),
-                    gt_refinement(TypedExpr::var("k")),
-                ),
+                Type::refined_one(prim(BaseType::Int), gt_refinement(TypedExpr::var("k"))),
                 prim(BaseType::Int),
             ),
         );
@@ -2272,10 +2246,7 @@ mod tests {
             "k",
             prim(BaseType::Int),
             Type::fun(
-                Type::Refinement(
-                    Box::new(prim(BaseType::Int)),
-                    gt_refinement(TypedExpr::var("k")),
-                ),
+                Type::refined_one(prim(BaseType::Int), gt_refinement(TypedExpr::var("k"))),
                 prim(BaseType::Int),
             ),
         );
@@ -2312,10 +2283,7 @@ mod tests {
             "k",
             prim(BaseType::Int),
             Type::fun(
-                Type::Refinement(
-                    Box::new(prim(BaseType::Int)),
-                    gt_refinement(TypedExpr::var("k")),
-                ),
+                Type::refined_one(prim(BaseType::Int), gt_refinement(TypedExpr::var("k"))),
                 prim(BaseType::Int),
             ),
         )
diff --git a/src/ccl/infer/solver/mod.rs b/src/ccl/infer/solver/mod.rs
index 4a151b8ca..d21376cfe 100644
--- a/src/ccl/infer/solver/mod.rs
+++ b/src/ccl/infer/solver/mod.rs
@@ -181,7 +181,7 @@ pub(crate) mod test_helpers {
     pub(crate) fn refined(base: Type, marker: i64) -> Type {
         use crate::ccl::{Lit, TypedExpr};
         let r = Refinement::born(Rc::new(TypedExpr::lit(Lit::Int(marker))));
-        Type::Refinement(Box::new(base), r)
+        Type::refined_one(base, r)
     }
 
     /// Helper: build a `Type::Variant({tag: payload, ...})` with named
diff --git a/src/ccl/infer/solver/scheme.rs b/src/ccl/infer/solver/scheme.rs
index cfbdf41de..ef9abee3f 100644
--- a/src/ccl/infer/solver/scheme.rs
+++ b/src/ccl/infer/solver/scheme.rs
@@ -225,7 +225,7 @@ fn freshen_level(ty: &Type) -> Level {
         Type::Infer(v) => v.level,
         _ => 0,
     };
-    if let Type::Refinement(_, r) = ty {
+    for r in ty.refinements() {
         lvl = lvl.max(predicate_level(&r.predicate));
     }
     ty.walk_children(|c| lvl = lvl.max(freshen_level(c)));
@@ -328,15 +328,18 @@ pub fn freshen_above(
             domain: Box::new(freshen_above(lim, domain, target, cache)),
             kind: *kind,
         },
-        Type::Refinement(inner, r) => Type::Refinement(
-            Box::new(freshen_above(lim, inner, target, cache)),
+        Type::Refinement(inner, refinements) => Type::refined(
+            freshen_above(lim, inner, target, cache),
             // Faithfully freshen the predicate's own type slots through the same
             // `cache`, so a specialization's predicate is a proper freshen
             // instance — its slots are the clone's fresh variables, driven
             // concrete by the use's pin — rather than sharing the definition's
             // unresolved ones. Immutable predicate terms are acyclic, so this
             // cannot loop.
-            freshen_refinement_predicate(lim, r, target, cache),
+            refinements
+                .iter()
+                .map(|r| freshen_refinement_predicate(lim, r, target, cache))
+                .collect(),
         ),
         Type::Infer(tv) => {
             if let Some(existing) = cache.vars.get(&tv.uid) {
@@ -748,8 +751,8 @@ mod tests {
             TypedExpr::lit(crate::ccl::Lit::Bool(true))
                 .with_ty(Type::Infer(Rc::clone(&quantified))),
         );
-        let refined_domain = Type::Refinement(
-            Box::new(Type::UIntRange(3)), // ground base: hides the predicate's level
+        let refined_domain = Type::refined_one(
+            Type::UIntRange(3), // ground base: hides the predicate's level
             Refinement::sharing(&predicate),
         );
         let ty = Type::Fun {
@@ -770,7 +773,7 @@ mod tests {
         let Type::Fun { domain, .. } = &fresh else {
             panic!("expected a function type");
         };
-        let Type::Refinement(_, r) = &**domain else {
+        let [r] = domain.refinements() else {
             panic!("expected the refinement to survive freshening");
         };
         let Type::Infer(v) = &r.predicate.ty else {
diff --git a/src/ccl/infer/solver/spec_key.rs b/src/ccl/infer/solver/spec_key.rs
index 2e5dcf718..cd89bec49 100644
--- a/src/ccl/infer/solver/spec_key.rs
+++ b/src/ccl/infer/solver/spec_key.rs
@@ -402,15 +402,17 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView
         // dependent-application discharge lands in the key as the predicate the
         // clone will actually carry — that is use-specific information, and two
         // uses discharging different arguments *should* key apart.
-        Type::Refinement(inner, r) => {
+        Type::Refinement(inner, refinements) => {
             let mut k = key_go(inner, pol, subst_acc, ctx);
-            let r = subst_acc.force_refinement(r);
-            // Closed against the walk's enclosing binders, as in `compact_go`: the
-            // key stores the index-spelled refinement, so α-variant instantiations
-            // key together.
-            let r = ctx.scope.close(&r);
-            if !k.refinements.contains(&r) {
-                k.refinements.push(r);
+            for r in refinements {
+                let r = subst_acc.force_refinement(r);
+                // Closed against the walk's enclosing binders, as in `compact_go`:
+                // the key stores the index-spelled refinement, so α-variant
+                // instantiations key together.
+                let r = ctx.scope.close(&r);
+                if !k.refinements.contains(&r) {
+                    k.refinements.push(r);
+                }
             }
             k
         }
@@ -605,14 +607,8 @@ mod tests {
 
     #[test]
     fn refinement_sets_compare_order_insensitively() {
-        let a = Type::Refinement(
-            Box::new(Type::Refinement(Box::new(int()), refined(1))),
-            refined(2),
-        );
-        let b = Type::Refinement(
-            Box::new(Type::Refinement(Box::new(int()), refined(2))),
-            refined(1),
-        );
+        let a = Type::refined_one(Type::refined_one(int(), refined(1)), refined(2));
+        let b = Type::refined_one(Type::refined_one(int(), refined(2)), refined(1));
         assert_eq!(spec_key(&a), spec_key(&b));
     }
 
@@ -879,8 +875,8 @@ mod refinement_closing_tests {
             name: Some(Name::raw(binder)),
             kind: FunKind::Data,
             domain: Box::new(Type::UIntRange(3)),
-            codomain: Box::new(Type::Refinement(
-                Box::new(Type::Base(crate::ccl::BaseType::Int)),
+            codomain: Box::new(Type::refined_one(
+                Type::Base(crate::ccl::BaseType::Int),
                 Refinement::born(dep_pred(binder)),
             )),
         }
@@ -922,8 +918,8 @@ mod refinement_closing_tests {
                 name: Some(Name::raw("y")),
                 kind: FunKind::Data,
                 domain: Box::new(Type::UIntRange(4)),
-                codomain: Box::new(Type::Refinement(
-                    Box::new(Type::Base(crate::ccl::BaseType::Int)),
+                codomain: Box::new(Type::refined_one(
+                    Type::Base(crate::ccl::BaseType::Int),
                     Refinement::born(dep_pred(referenced)),
                 )),
             }),
@@ -936,8 +932,8 @@ mod refinement_closing_tests {
         // A free name that binds to no enclosing function stays a name and stays
         // distinct from every index: distinct enclosing binders outside the
         // walked type key apart too.
-        let free = Type::Refinement(
-            Box::new(Type::Base(crate::ccl::BaseType::Int)),
+        let free = Type::refined_one(
+            Type::Base(crate::ccl::BaseType::Int),
             Refinement::born(dep_pred("outer")),
         );
         let bound = {
diff --git a/src/ccl/infer/solver/traits.rs b/src/ccl/infer/solver/traits.rs
index 9122f8a89..eb17c0d6f 100644
--- a/src/ccl/infer/solver/traits.rs
+++ b/src/ccl/infer/solver/traits.rs
@@ -866,7 +866,7 @@ struct Place {
     reqs: Vec<(Rc<TraitObligation>, u8)>,
 }
 
-/// Strip every refinement layer, as [`offered`] does: `{𝑇 | 𝑝}` constrains a place
+/// Strip every refinement, as [`offered`] does: `{𝑇 | 𝑝}` constrains a place
 /// exactly as `𝑇` does, so structure underneath a refinement is still structure.
 fn peel_refinements(ty: &Type) -> &Type {
     let mut cur = ty;
@@ -1532,8 +1532,8 @@ mod tests {
     /// emission an operand is usually still a variable with nothing to strip.
     #[test]
     fn a_refinement_narrows_as_its_base() {
-        let refined = Type::Refinement(
-            Box::new(Type::Base(BaseType::String)),
+        let refined = Type::refined_one(
+            Type::Base(BaseType::String),
             crate::ccl::Refinement::born(Rc::new(crate::ccl::TypedExpr::lit(
                 crate::ccl::Lit::Bool(true),
             ))),
diff --git a/src/ccl/infer_var.rs b/src/ccl/infer_var.rs
index d545c2036..fb83d7050 100644
--- a/src/ccl/infer_var.rs
+++ b/src/ccl/infer_var.rs
@@ -696,8 +696,8 @@ mod tests {
         use crate::ccl::{Lit, Name, Refinement, TypedExpr, subst::Subst};
         use std::rc::Rc as StdRc;
         let dep = |referenced: &str| {
-            Type::Refinement(
-                Box::new(Type::Base(BaseType::Int)),
+            Type::refined_one(
+                Type::Base(BaseType::Int),
                 Refinement::born(StdRc::new(TypedExpr::binop(
                     TypedExpr::var(Name::elem()),
                     crate::ccl::BinOpKind::Compare(crate::ccl::CompareKind::Equals),
@@ -734,8 +734,8 @@ mod tests {
     fn recording_an_open_bound_is_an_internal_error() {
         use crate::ccl::{Name, Refinement, TypedExpr};
         use std::rc::Rc as StdRc;
-        let dep = Type::Refinement(
-            Box::new(Type::Base(BaseType::Int)),
+        let dep = Type::refined_one(
+            Type::Base(BaseType::Int),
             Refinement::born(StdRc::new(TypedExpr::var(Name::fresh("escaped")))),
         );
         let holder = InferVar::fresh(0);
@@ -758,8 +758,8 @@ mod tests {
     fn a_raw_gap_is_an_internal_error() {
         use crate::ccl::{Name, Refinement, TypedExpr};
         use std::rc::Rc as StdRc;
-        let dep = Type::Refinement(
-            Box::new(Type::Base(BaseType::Int)),
+        let dep = Type::refined_one(
+            Type::Base(BaseType::Int),
             Refinement::born(StdRc::new(TypedExpr::var(Name::raw("a")))),
         );
         let holder = InferVar::fresh(0);
diff --git a/src/ccl/inline.rs b/src/ccl/inline.rs
index 45d96609a..9725bb712 100644
--- a/src/ccl/inline.rs
+++ b/src/ccl/inline.rs
@@ -580,15 +580,7 @@ fn is_name_in_function_position(expr: &Expr, name: &Name) -> bool {
 /// equality. Anything subtler is exactly what should trip the assert and get a real
 /// `restrict` lift.
 fn refinement_discharged_by(arg_ty: &Type, param_ty: &Type) -> bool {
-    fn layers(mut ty: &Type) -> Vec<&Refinement> {
-        let mut out = Vec::new();
-        while let Type::Refinement(inner, r) = ty {
-            out.push(r);
-            ty = inner;
-        }
-        out
-    }
-    let demanded = layers(param_ty);
+    let demanded = param_ty.refinements();
     if demanded.is_empty() {
         return true;
     }
@@ -600,11 +592,11 @@ fn refinement_discharged_by(arg_ty: &Type, param_ty: &Type) -> bool {
     // survive on the bare `Var` for the phase to find the read. Comparing the stamp
     // against the parameter would ask a handle to entail a fact about a value. See
     // `src/ccl/design/mutability.md`, "`Mut` is a CCL type".
-    let mut supplied = layers(arg_ty);
+    let mut supplied: Vec<&Refinement> = arg_ty.refinements().iter().collect();
     if let Some(value) = arg_ty.mut_value_type() {
-        supplied.extend(layers(value));
+        supplied.extend(value.refinements());
     }
-    demanded.iter().all(|d| supplied.contains(d))
+    demanded.iter().all(|d| supplied.contains(&d))
 }
 
 // ---------------------------------------------------------------------------
@@ -669,7 +661,7 @@ mod tests {
             name: None,
             kind: FunKind::Compute,
             domain: Box::new(Type::Base(BaseType::Int)),
-            codomain: Box::new(Type::Refinement(Box::new(inner_fun), refinement)),
+            codomain: Box::new(Type::refined_one(inner_fun, refinement)),
         };
         assert!(should_inline(&ty));
     }
diff --git a/src/ccl/lambda_elim.rs b/src/ccl/lambda_elim.rs
index 21ec4820c..bfddbde9a 100644
--- a/src/ccl/lambda_elim.rs
+++ b/src/ccl/lambda_elim.rs
@@ -1627,7 +1627,7 @@ fn elim_lambdas_impl(ctx: &mut ElimContext, expr: Expr) -> Result<Expr, LambdaEl
             let source_domain = target_elim.ty.domain().unwrap();
             let source_codomain = target_elim.ty.codomain().unwrap();
             let refinement = Refinement::born(Rc::new(pred_on_source));
-            let refined_domain = Type::Refinement(Box::new(source_domain), refinement);
+            let refined_domain = Type::refined_one(source_domain, refinement);
             // A **domain-only** rewrite of the source, so it keeps the source's
             // own function type: `fun_like`, not a bare `Type::fun`, which would rebuild
             // a collection as a capability (`src/ccl/design/type-inference.md`,
@@ -2047,7 +2047,7 @@ mod tests {
         // a dedicated AST field. `substitute` must descend through the type
         // (via `substitute_in_type`) into the predicate body.
         let refinement = Refinement::born(Rc::new(refinement_pred));
-        let refined_param = Type::Refinement(Box::new(int_ty()), refinement);
+        let refined_param = Type::refined_one(int_ty(), refinement);
         let expr = Expr::lambda("x", int_ty(), Expr::var("x").with_ty(int_ty()))
             .with_ty(fun_ty(refined_param, int_ty()));
 
@@ -2058,9 +2058,9 @@ mod tests {
         // Extract the refinement predicate from the result's domain type to
         // verify substitution descended into it.
         let pred_after_subst = match &result.ty {
-            Type::Fun { domain, .. } => match domain.as_ref() {
-                Type::Refinement(_, r) => (*r.predicate).clone(),
-                other => panic!("expected refined domain, got {other}"),
+            Type::Fun { domain, .. } => match domain.refinements() {
+                [r] => (*r.predicate).clone(),
+                _ => panic!("expected a singly-refined domain, got {domain}"),
             },
             other => panic!("expected function type, got {other}"),
         };
@@ -2179,7 +2179,7 @@ mod tests {
 
         // Uncorrelated refinement (a Bool constant predicate) on the param.
         let refinement = Refinement::born(Rc::new(Expr::lit(Lit::Bool(true)).with_ty(bool_ty)));
-        let refined_y_ty = Type::Refinement(Box::new(int_ty()), refinement);
+        let refined_y_ty = Type::refined_one(int_ty(), refinement);
         let body = var("y").with_ty(int_ty());
 
         // Eliminate λ y → y over the refined domain.
@@ -2234,10 +2234,7 @@ mod tests {
 
         // Tuple([Int, {Int | __elem > x}]): the predicate rides only the second
         // component, so `any`-vs-`all` is observable.
-        let tuple_ty = Type::Tuple(vec![
-            int_ty(),
-            Type::Refinement(Box::new(int_ty()), refinement),
-        ]);
+        let tuple_ty = Type::Tuple(vec![int_ty(), Type::refined_one(int_ty(), refinement)]);
 
         // Lit(42) typed with the tuple above — the expression node itself has no
         // free vars, so both answers come entirely from `is_free_in_type`.
diff --git a/src/ccl/lower/stmts.rs b/src/ccl/lower/stmts.rs
index 2f8356006..061c9f16c 100644
--- a/src/ccl/lower/stmts.rs
+++ b/src/ccl/lower/stmts.rs
@@ -1162,11 +1162,16 @@ pub(super) fn lower_type_expr(
         // `Bool` term with `__elem` free — the same shape a singleton or a
         // `groupby` refinement carries. Discharge of the predicate is the
         // solver's structural refinement subsumption; this only builds the type.
+        //
+        // A written base that is itself a refinement (`{{Int where p} where q}`)
+        // merges into one set rather than nesting: the two predicates restrict
+        // the same element, so the nesting the source spells carries nothing the
+        // set does not.
         ChlExpr::BraceRefinement { base, predicate } => {
             let base_ty = lower_type_expr(base, ctx)?;
             let pred = ctx.with_in_refinement_predicate(|ctx| lower_expr(predicate, ctx))?;
-            Ok(Type::Refinement(
-                Box::new(base_ty),
+            Ok(Type::refined_one(
+                base_ty,
                 crate::ccl::Refinement::born(Rc::new(pred)),
             ))
         }
@@ -1894,10 +1899,12 @@ x";
     // Nested refinement: both levels' `_` resolve to `__elem`, and the
     // save/restore of `in_refinement_predicate` around the inner annotation
     // keeps the flag from leaking — the outer `_` still lowers to `__elem`
-    // after the inner predicate closes.
+    // after the inner predicate closes. The two written levels land as one
+    // refinement set: both predicates restrict the same element, so the source's
+    // nesting carries nothing the set does not.
     #[case(
         "x: { {Int where _ != 1} where _ != 0} = 5\nx",
-        "{{Int | __elem != 1} | __elem != 0}"
+        "{Int | __elem != 0, __elem != 1}"
     )]
     fn test_lower_refinement_annotation(#[case] code: &str, #[case] expected_ty: &str) {
         use crate::ccl::{Type, TypedExprNode};
diff --git a/src/ccl/planning/groupby.rs b/src/ccl/planning/groupby.rs
index 7e30d137f..f43a4b3a6 100644
--- a/src/ccl/planning/groupby.rs
+++ b/src/ccl/planning/groupby.rs
@@ -7,6 +7,7 @@
 //! [`emit_groupby`].
 
 use super::*;
+use crate::ccl::Refinement;
 use crate::ccl::ty::FunKind;
 
 /// Recognize group-by sites and rewrite them to the bucketize chain.
@@ -143,29 +144,19 @@ fn rewrite_groupby_source(head: &Expr) -> Option<Expr> {
     else {
         return None;
     };
-    let Type::Refinement(idx_ty, refinement) = refined_dom.as_ref() else {
-        return None;
-    };
-    // The bare predicate binds the implicit REFINEMENT_BINDER as the element:
-    //   pred = (__elem ▷ c ▷ key) == <key binder>
-    let pred = &*refinement.predicate;
-    let TypedExprNode::BinOp {
-        left,
-        op: BinOpKind::Compare(CompareKind::Equals),
-        right,
-    } = &pred.node
-    else {
-        return None;
-    };
-    // Identify which side is the element-extraction `__elem ▷ c ▷ key` and which
-    // is the free key binder (a `Var` not bound by the element).
-    let extract = if side_extracts_element(left) && is_free_var(right) {
-        left
-    } else if side_extracts_element(right) && is_free_var(left) {
-        right
-    } else {
+    let Type::Refinement(idx_ty, refinements) = refined_dom.as_ref() else {
         return None;
     };
+    // Find the refinement that *is* the grouping equation, by its shape. The domain
+    // may carry other refinements (an ordinary filter on the grouped collection);
+    // they are not this rewrite's to consume, so they ride along on the index
+    // type below. Nothing distinguishes the grouping refinement positionally — the
+    // set is unordered — which is exactly why the recognizer asks what a refinement
+    // *says* rather than where it sits.
+    let (key_eq, extract) = refinements
+        .iter()
+        .enumerate()
+        .find_map(|(i, r)| groupby_key_extraction(r).map(|e| (i, e)))?;
     // extract = r ▷ c ▷ key = Apply { argument: Apply { argument: Var(r), .. }, function: key }
     let TypedExprNode::Apply {
         function: key_expr,
@@ -198,7 +189,17 @@ fn rewrite_groupby_source(head: &Expr) -> Option<Expr> {
     // makes the crossing safe; `groupby_recognition_lifts_the_key_without_aliasing`
     // pins the property rather than the mechanism.
     let key_pf = lambda_elim::run((**key_expr).clone()).ok()?;
-    let value_idx_ty = (**idx_ty).clone();
+    // Every refinement except the consumed grouping equation stays on the index
+    // domain — dropping them here would silently discard a filter.
+    let value_idx_ty = Type::refined(
+        (**idx_ty).clone(),
+        refinements
+            .iter()
+            .enumerate()
+            .filter(|(i, _)| *i != key_eq)
+            .map(|(_, r)| r.clone())
+            .collect(),
+    );
     let keys =
         compose((**c).clone(), key_pf).with_ty(Type::fun(value_idx_ty.clone(), (**key_ty).clone()));
     let grouped_values = emit_groupby(
@@ -213,6 +214,29 @@ fn rewrite_groupby_source(head: &Expr) -> Option<Expr> {
     Some(grouped_values)
 }
 
+/// Read a refinement as a group-by key equation, yielding its element-extraction
+/// side: the bare predicate binds the implicit `REFINEMENT_BINDER` as the
+/// element, so the grouping refinement reads `(__elem ▷ c ▷ key) == <key binder>` —
+/// one side extracting from the element, the other a free key binder.
+fn groupby_key_extraction(r: &Refinement) -> Option<&Expr> {
+    let TypedExprNode::BinOp {
+        left,
+        op: BinOpKind::Compare(CompareKind::Equals),
+        right,
+    } = &r.predicate.node
+    else {
+        return None;
+    };
+    let (left, right) = (left.as_ref(), right.as_ref());
+    if side_extracts_element(left) && is_free_var(right) {
+        Some(left)
+    } else if side_extracts_element(right) && is_free_var(left) {
+        Some(right)
+    } else {
+        None
+    }
+}
+
 /// Is `e` the element-extraction `__elem ▷ c ▷ key` — an application whose
 /// innermost argument is the refinement element binder?
 fn side_extracts_element(e: &Expr) -> bool {
diff --git a/src/ccl/planning/iterate.rs b/src/ccl/planning/iterate.rs
index 6fff411a9..eac44a9c8 100644
--- a/src/ccl/planning/iterate.rs
+++ b/src/ccl/planning/iterate.rs
@@ -33,9 +33,9 @@ use super::*;
 ///    so no extra marker is added.
 /// 2. **Iterate-then-restricts chain** (the [`wrap_with_iterate`]
 ///    fallback) — build the source by *applying* one `restrict(p)`
-///    filter per refinement layer (innermost first) to a chain-head
-///    `Apply(true ▷ const, Iterate)`, then compose the body onto it:
-///    `(iterate ▷ (p_inner ▷ restrict) ▷ … ▷ (p_outer ▷ restrict)) ≫
+///    filter per refinement, in [`crate::ccl::application_order`], to a
+///    chain-head `Apply(true ▷ const, Iterate)`, then compose the body
+///    onto it: `(iterate ▷ (p₁ ▷ restrict) ▷ … ▷ (pₙ ▷ restrict)) ≫
 ///    body`.  Each `restrict` *applies* to its upstream (it is a
 ///    function transformer, not a composed morphism — see
 ///    [`make_restrict`]).  Unrefined sites get just the chain-head
@@ -394,8 +394,7 @@ pub(super) fn wrap_with_iterate(expr: &mut Expr) {
     let Some(domain_ty) = expr.ty.domain() else {
         return;
     };
-    // The recording names the site being wrapped. The predicate `fresh_copy` below lands
-    // as a `Copy` of the term it lifts out of the type.
+    // The recording names the site being wrapped.
     //
     // These rows reach no table in a normal compile: `compile_program` calls
     // `planning::run` outside every pass scope it opens, so they land only under
@@ -405,47 +404,35 @@ pub(super) fn wrap_with_iterate(expr: &mut Expr) {
         "planning.iterate",
         provenance::Nature::Machinery,
     );
-    // Walk every nested `Type::Refinement` layer (innermost ⊇ outermost,
-    // each layer's predicate must hold), collecting the predicates
-    // outer-to-inner; reverse to inner-to-outer.  Then emit a uniform
-    // chain: one chain-head `iterate(true)` over the unrefined base
-    // (op-conversion's `IterateExtent`), followed by one
-    // `restrict(p_inner)`, `restrict(p_next)`, … per refinement layer,
-    // narrowing the domain layer by layer.  Unrefined sites get just
-    // the iterate.
-    // Recover each layer's point-free predicate function from its bare
-    // `__elem ▷ p` form — that is what `make_restrict` filters with (the
-    // refinement type it then re-stamps stays bare).
-    let mut preds: Vec<Expr> = Vec::new();
-    let mut current = &domain_ty;
-    while let Type::Refinement(base, refinement) = current {
-        // Lifting a predicate out of a *type* and into the term tree: one
-        // predicate `Rc` reached from two iteration sites would otherwise land
-        // twice. `fn_of_bare_predicate` already returns an owned, freshened term
-        // on both its paths — the fast path clones the function subterm, the slow
-        // path η-expands and runs `lambda_elim` — so the lift is already a
-        // distinct node-set and needs no second copy here. (It needed one when
-        // `Clone` preserved ids; the trailing `fresh_copy()` was load-bearing
-        // then, and cloning again now would duplicate a whole tree per
-        // refinement layer for nothing.)
-        preds.push(fn_of_bare_predicate(base.as_ref(), &refinement.predicate));
-        current = base.as_ref();
-    }
-    preds.reverse();
+    // Every refinement at the position must hold, so each becomes a filter and
+    // the pipeline narrows stage by stage.  `application_order` picks the order —
+    // any is correct for the same final domain, and choosing it in one place is
+    // what makes the predicates compiled for this pipeline agree with its types.
+    // The chain is uniform: one chain-head `iterate(true)` over the unrefined base
+    // (op-conversion's `IterateExtent`), then one `restrict(pₖ)` per refinement.
+    // Unrefined sites get just the iterate.
+    let base = domain_ty.peel_refinements();
     let body = take(expr);
-    // Build the iteration source by applying one `restrict(p)` per
-    // refinement layer (innermost first) to a chain-head `iterate(true)`
-    // over the unrefined base.  Each `restrict` is a function transformer
-    // *applied* to its upstream (not composed): `make_restrict` narrows
-    // the domain layer by layer while preserving the codomain, so `source`
-    // ends with type `{{…{D | p_inner} …} | p_outer} ⇒ D` — the full
-    // refinement on the domain.  The value-producing `body` is then
+    // Build the iteration source by applying one `restrict(p)` per refinement to a
+    // chain-head `iterate(true)` over the unrefined base.  Each `restrict` is a
+    // function transformer *applied* to its upstream (not composed):
+    // `make_restrict` narrows the domain by one refinement while preserving the
+    // codomain, so `source` ends with type `{D | p₁, …, pₙ} ⇒ D` — the site's
+    // full refinement set on the domain.  The value-producing `body` is then
     // composed onto that source as a genuine CCC morphism.
+    //
+    // Each refinement's predicate function is recovered from its bare `__elem ▷ p`
+    // form against the element type that stage of the pipeline actually sees —
+    // the base narrowed by the refinements applied before it (`application_order`,
+    // which `compile_predicates_in_type` walks identically so the compiled
+    // predicates match these stages). Any order of the refinements yields a
+    // well-typed pipeline for the same final domain; the order is planning's to
+    // choose, which is what lets the refinement set itself stay unordered.
     let site_ty = body.ty.clone();
-    let source = preds.into_iter().fold(
-        make_iterate(trivially_true_predicate(current.clone())),
-        |upstream, pred| make_restrict(pred, upstream),
-    );
+    let mut source = make_iterate(trivially_true_predicate(base.clone()));
+    for (r, elem_ty) in crate::ccl::application_order(domain_ty.refinements(), base) {
+        source = make_restrict(fn_of_bare_predicate(&elem_ty, &r.predicate), source);
+    }
     // An iteration source produces the refined extent it iterates, so its
     // codomain is the *site's* refined domain `{D | p}`, mirroring
     // `make_iterate`'s `{D | p} ⇒ {D | p}` symmetry. Surfacing the refinement
@@ -875,12 +862,13 @@ mod tests {
 
     #[test]
     fn test_wrap_with_iterate_nested_refinements_emits_chain() {
-        // `{{D | p_inner} | p_outer} ⇒ Int` builds the iteration source by
-        // *applying* one restrict per refinement layer (inner first) to a
-        // chain-head trivially-true iterate, then composes `body` onto it:
-        //   restrict(p_outer)(restrict(p_inner)(iterate(true))) ≫ body.
-        // So the outermost application narrows by `p_outer`, its upstream
-        // narrows by `p_inner`, and the innermost upstream is the iterate.
+        // `{D | p₁, p₂} ⇒ Int` builds the iteration source by *applying* one
+        // restrict per refinement, in `application_order`, to a chain-head
+        // trivially-true iterate, then composes `body` onto it:
+        //   restrict(p₂)(restrict(p₁)(iterate(true))) ≫ body.
+        // So the outermost application narrows by the last refinement in that
+        // order, its upstream by the first, and the innermost upstream is the
+        // iterate.
         let int = int_ty();
         let inner_pred = var("p_inner").with_ty(fun_ty(Type::UIntRange(3), bool_ty()));
         let outer_pred = var("p_outer").with_ty(fun_ty(Type::UIntRange(3), bool_ty()));
diff --git a/src/ccl/planning/join.rs b/src/ccl/planning/join.rs
index 5e4f22e00..e721095e7 100644
--- a/src/ccl/planning/join.rs
+++ b/src/ccl/planning/join.rs
@@ -718,20 +718,13 @@ fn join_plan_to_expr(plan: &JoinPlan, types: &[Type]) -> Expr {
         JoinPlan::Loop { arms, predicate } => {
             let base_iteration = (|| {
                 if arms.len() == 1 {
-                    if let Type::Refinement(base_ty, refinement) = &types[arms[0]] {
-                        // `convert_loop_join` only reads the predicate (it
-                        // builds a new expr), so borrow the immutable term
-                        // rather than clone it.
-                        let pred = &*refinement.predicate;
-                        trace!("Attempting loop join conversion inside iteration");
-                        if let Some(transformed) = convert_loop_join(base_ty, pred) {
-                            trace!(
-                                "Converted iteration to {} : {}",
-                                symbolic(&transformed),
-                                transformed.ty
-                            );
-                            return transformed;
-                        }
+                    if let Some(transformed) = convert_refinement_to_join(&types[arms[0]]) {
+                        trace!(
+                            "Converted iteration to {} : {}",
+                            symbolic(&transformed),
+                            transformed.ty
+                        );
+                        return transformed;
                     }
                     make_iterate(trivially_true_predicate(types[arms[0]].clone()))
                 } else {
@@ -1031,6 +1024,36 @@ fn convert_loop_join(base_ty: &Type, refinement: &Expr) -> Option<Expr> {
     Some(result)
 }
 
+/// Compile **one** of a refined domain's refinements into a join, leaving the others
+/// as ordinary restrictions on the domain the join reads.
+///
+/// Any refinement may be the join condition — the set is unordered, so there is no
+/// "the" predicate to read — and the first that [`convert_loop_join`] accepts
+/// wins. That also gives planning latitude it could not have while refinements were
+/// a chain: when several are joinable, which one becomes the join is a free
+/// choice a cost model may later make, and the rest remain filters either way.
+/// `None` for an unrefined domain or when no refinement forms a join.
+fn convert_refinement_to_join(domain_ty: &Type) -> Option<Expr> {
+    let Type::Refinement(base, refinements) = domain_ty else {
+        return None;
+    };
+    trace!("Attempting loop join conversion inside iteration");
+    refinements.iter().enumerate().find_map(|(i, r)| {
+        let rest = Type::refined(
+            (**base).clone(),
+            refinements
+                .iter()
+                .enumerate()
+                .filter(|(j, _)| *j != i)
+                .map(|(_, c)| c.clone())
+                .collect(),
+        );
+        // `convert_loop_join` only reads the predicate (it builds a new expr),
+        // so borrow the immutable term rather than clone it.
+        convert_loop_join(&rest, &r.predicate)
+    })
+}
+
 /// Try the hash-join rewrite at an iteration site whose domain is `domain_ty`.
 ///
 /// Called from [`super::iterate::wrap_with_iterate`] before its iterate-then-restricts
@@ -1054,17 +1077,11 @@ fn convert_loop_join(base_ty: &Type, refinement: &Expr) -> Option<Expr> {
 /// the BFS order of that spanning tree.  For now, predicates must be
 /// expressed as conjunctions of single-arm equality conditions.
 pub(super) fn try_hash_join_rewrite(expr: &mut Expr, domain_ty: &Type) -> bool {
-    let Type::Refinement(base, refinement) = domain_ty else {
-        return false;
-    };
-    // `convert_loop_join` only reads the predicate (it builds a new expr), so
-    // borrow the immutable term rather than clone it.
-    let pred = &*refinement.predicate;
     trace!(
         "Attempting hash-join rewrite at iteration site: {}",
         symbolic(expr),
     );
-    let Some(transformed) = convert_loop_join(base, pred) else {
+    let Some(transformed) = convert_refinement_to_join(domain_ty) else {
         trace!("Hash-join pattern did not match");
         return false;
     };
diff --git a/src/ccl/planning/mod.rs b/src/ccl/planning/mod.rs
index b89a3ec13..1afd8aa66 100644
--- a/src/ccl/planning/mod.rs
+++ b/src/ccl/planning/mod.rs
@@ -68,10 +68,10 @@ pub(crate) use predicates::fn_of_bare_predicate;
 ///    join conditions.  Emitted as a `JoinPlan::Hash` / `JoinPlan::Loop`
 ///    tree compiled to a CCL chain whose leaves are iteration-bearing.
 /// 2. **Iterate-then-restricts chain** otherwise — build the source by
-///    *applying* one `restrict(p)` filter per refinement layer (innermost
-///    first) to a chain-head `Apply(true ▷ const, Iterate)`, then compose
-///    the value-producing body onto it: `(iterate ▷ (p_inner ▷ restrict)
-///    ▷ … ▷ (p_outer ▷ restrict)) ≫ body`.  Each `restrict` *applies* to
+///    *applying* one `restrict(p)` filter per refinement, in
+///    [`crate::ccl::application_order`], to a chain-head
+///    `Apply(true ▷ const, Iterate)`, then compose the value-producing body
+///    onto it: `(iterate ▷ (p₁ ▷ restrict) ▷ … ▷ (pₙ ▷ restrict)) ≫ body`.  Each `restrict` *applies* to
 ///    its upstream — it is a function transformer, not a morphism composed
 ///    with the source (its honest type makes the composed form ill-typed;
 ///    see [`make_restrict`]).  Unrefined sites get just the chain-head
@@ -298,7 +298,7 @@ pub(crate) mod test_helpers {
     /// predicate.  The predicate must have type `base ⇒ Bool` so the
     /// refinement is well-formed.
     pub(crate) fn refined_ty(base: Type, predicate: Expr) -> Type {
-        Type::Refinement(Box::new(base), Refinement::born(Rc::new(predicate)))
+        Type::refined_one(base, Refinement::born(Rc::new(predicate)))
     }
 
     /// Build an `Apply { argument, function: <builtin> }` whose function
diff --git a/src/ccl/planning/predicates.rs b/src/ccl/planning/predicates.rs
index 6bcbff756..bc16de1cc 100644
--- a/src/ccl/planning/predicates.rs
+++ b/src/ccl/planning/predicates.rs
@@ -128,40 +128,52 @@ 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, refinement) = ty {
-        let base_ctx = (**base).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, \
+    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
+                    symbolic(&compiled)
+                );
+                *bare = compiled;
+                true
+            });
         });
     }
     // Recurse into structural type children (refinement base, function
diff --git a/src/ccl/simplify.rs b/src/ccl/simplify.rs
index c27613b5e..bcc623dc9 100644
--- a/src/ccl/simplify.rs
+++ b/src/ccl/simplify.rs
@@ -555,7 +555,7 @@ fn try_pairwise_in_compose(
     // A `Cast` states its `FunKind` twice — on the node and on `target`, which is
     // where its typing rule reads it — so writing the position's type above
     // without the second copy leaves the node contradicting itself. Only the kind
-    // is carried across: the `target`'s *claims* are the cast's own assertion, and
+    // is carried across: the `target`'s refinements are the cast's own assertion, and
     // 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);
diff --git a/src/ccl/subst.rs b/src/ccl/subst.rs
index 2fca858ad..e1326f33a 100644
--- a/src/ccl/subst.rs
+++ b/src/ccl/subst.rs
@@ -941,7 +941,7 @@ impl Subst {
                 restricted.rewrite_type_go(codomain, memo);
             }
 
-            Type::Refinement(base, r) => {
+            Type::Refinement(base, refinements) => {
                 // The refinement implicitly binds REFINEMENT_BINDER in its bare
                 // predicate, so the substitution acts *under* that binder.
                 let restricted = self.shadow(&Name::elem());
@@ -951,25 +951,27 @@ impl Subst {
                 // served to an occurrence inside it (and a vacuous decision made
                 // inside is never served outside). That is what makes threading one
                 // memo across binder crossings correct — see `PredMemo`.
-                memo.rebuild(r, &restricted, |pred| {
-                    if !restricted.0.keys().any(|k| is_free(k, pred)) {
-                        // Vacuous: no substituted binder occurs free here, so report
-                        // no change and keep the origin `Rc` — a predicate this
-                        // substitution merely walks past stays shared with its other
-                        // occurrences (mirroring `force_refinement`'s transport
-                        // path). Memoizing the decision also makes this `is_free`
-                        // scan run once per distinct predicate, not per occurrence.
-                        return false;
-                    }
-                    restricted.rewrite_expr_go(pred, memo);
-                    // Keep the predicate marker-free: a substituted collection may
-                    // carry a term-tree `iterate` marker that must not leak into a
-                    // type (see `strip_iterate_markers` and the `force_refinement`
-                    // twin). Only the rewritten path needs it — a marker arrives
-                    // *through* the substitution, so the vacuous path above, which
-                    // rewrites nothing and keeps the origin `Rc`, has none to strip.
-                    *pred = strip_iterate_markers(pred);
-                    true
+                refinements.rewrite_each(|_, r| {
+                    memo.rebuild(r, &restricted, |pred| {
+                        if !restricted.0.keys().any(|k| is_free(k, pred)) {
+                            // Vacuous: no substituted binder occurs free here, so report
+                            // no change and keep the origin `Rc` — a predicate this
+                            // substitution merely walks past stays shared with its other
+                            // occurrences (mirroring `force_refinement`'s transport
+                            // path). Memoizing the decision also makes this `is_free`
+                            // scan run once per distinct predicate, not per occurrence.
+                            return false;
+                        }
+                        restricted.rewrite_expr_go(pred, memo);
+                        // Keep the predicate marker-free: a substituted collection may
+                        // carry a term-tree `iterate` marker that must not leak into a
+                        // type (see `strip_iterate_markers` and the `force_refinement`
+                        // twin). Only the rewritten path needs it — a marker arrives
+                        // *through* the substitution, so the vacuous path above, which
+                        // rewrites nothing and keeps the origin `Rc`, has none to strip.
+                        *pred = strip_iterate_markers(pred);
+                        true
+                    });
                 });
                 self.rewrite_type_go(base, memo);
             }
@@ -1168,12 +1170,18 @@ impl Subst {
                 }
             }
 
-            Type::Refinement(base, r) => {
+            Type::Refinement(base, refinements) => {
                 // The refinement implicitly binds REFINEMENT_BINDER in its bare
                 // predicate; `force_refinement` shadows it before rewriting.
                 // Substituting the predicate changes its meaning, so it builds a
                 // fresh predicate `Rc` rather than sharing the original's.
-                Type::Refinement(Box::new(self.apply_type(base)), self.force_refinement(r))
+                Type::refined(
+                    self.apply_type(base),
+                    refinements
+                        .iter()
+                        .map(|r| self.force_refinement(r))
+                        .collect(),
+                )
             }
 
             Type::Tuple(ts) => Type::Tuple(ts.iter().map(|t| self.apply_type(t)).collect()),
@@ -1321,15 +1329,17 @@ fn collect_type_fv(
                 collect_type_fv(codomain, bnd, visited, out)
             });
         }
-        Type::Refinement(base, r) => {
+        Type::Refinement(base, refinements) => {
             // Walk each predicate term at most once (a term shared by `Rc`
             // across occurrences is a DAG — dedup, not cycle-breaking). The
             // refinement binds the implicit REFINEMENT_BINDER over `base`, so it
             // is bound — not free — inside the predicate.
-            if visited.insert(r.predicate_id()) {
-                with_binders(bound, [Name::elem()], |bnd| {
-                    collect_expr_fv(&r.predicate, bnd, visited, out)
-                });
+            for r in refinements {
+                if visited.insert(r.predicate_id()) {
+                    with_binders(bound, [Name::elem()], |bnd| {
+                        collect_expr_fv(&r.predicate, bnd, visited, out)
+                    });
+                }
             }
             collect_type_fv(base, bound, visited, out);
         }
@@ -1406,10 +1416,12 @@ pub fn name_spelled_stored_binders(ty: &Type) -> Vec<Binder> {
             out.push(b.clone());
         }
         match ty {
-            Type::Refinement(base, r) => {
+            Type::Refinement(base, rs) => {
                 go(base, out, visited);
-                if visited.insert(r.predicate_id()) {
-                    expr_go(&r.predicate, out, visited);
+                for r in rs.iter() {
+                    if visited.insert(r.predicate_id()) {
+                        expr_go(&r.predicate, out, visited);
+                    }
                 }
             }
             _ => ty.walk_children(|c| go(c, out, visited)),
@@ -1600,9 +1612,9 @@ impl<'a> PiWalk<'a> {
                 self.ty(domain, depth);
                 self.ty(codomain, depth + 1);
             }
-            Type::Refinement(base, r) => {
+            Type::Refinement(base, refinements) => {
                 self.ty(base, depth);
-                self.refinement(r, depth);
+                refinements.rewrite_each(|_, r| self.refinement(r, depth));
             }
             Type::Tuple(ts) => ts.iter_mut().for_each(|t| self.ty(t, depth)),
             Type::Record(fs) => fs.iter_mut().for_each(|(_, t)| self.ty(t, depth)),
@@ -1744,10 +1756,11 @@ pub fn references_enclosing_function(ty: &Type) -> bool {
             // reached at two depths is two questions. Keying on identity alone
             // answers the second from the first and reports a dependent
             // codomain as independent — the index would then lose its binder.
-            Type::Refinement(base, r) => {
-                (visited.insert((r.predicate_id(), depth))
-                    && expr_scan(&r.predicate, depth, visited))
-                    || ty_scan(base, depth, visited)
+            Type::Refinement(base, refinements) => {
+                refinements.iter().any(|r| {
+                    visited.insert((r.predicate_id(), depth))
+                        && expr_scan(&r.predicate, depth, visited)
+                }) || ty_scan(base, depth, visited)
             }
             Type::Tuple(ts) => ts.iter().any(|t| ty_scan(t, depth, visited)),
             Type::Record(fs) => fs.iter().any(|(_, t)| ty_scan(t, depth, visited)),
@@ -1949,11 +1962,11 @@ mod tests {
         use std::rc::Rc;
         // y : {_ | k > 0} — `k` appears only in the type slot's predicate.
         let slot_ref = Refinement::born(Rc::new(gt(var("k"), int(0))));
-        let e = var("y").with_ty(Type::Refinement(Box::new(Type::Hole), slot_ref.clone()));
+        let e = var("y").with_ty(Type::refined_one(Type::Hole, slot_ref.clone()));
         let dis = Subst::discharge("k", int(5));
 
         let out = dis.apply_expr(&e);
-        let Type::Refinement(_, out_ref) = &out.ty else {
+        let [out_ref] = out.ty.refinements() else {
             panic!("type slot preserved");
         };
         assert_eq!(
@@ -1973,7 +1986,7 @@ mod tests {
         let forced = dis.force_refinement(&outer);
         assert!(!Rc::ptr_eq(&forced.predicate, &outer.predicate));
         let forced_pred = &*forced.predicate;
-        let Type::Refinement(_, nested) = &forced_pred.ty else {
+        let [nested] = forced_pred.ty.refinements() else {
             panic!("nested refinement preserved");
         };
         assert_eq!(*nested.predicate, gt(int(5), int(0)));
@@ -2009,7 +2022,7 @@ mod tests {
     #[test]
     fn scenario_f_context_check() {
         let pred = TypedExpr::lambda("y", Type::Hole, gt(var("y"), var("k")));
-        let bad = Type::Refinement(Box::new(Type::infer()), Refinement::born(Rc::new(pred)));
+        let bad = Type::refined_one(Type::infer(), Refinement::born(Rc::new(pred)));
         let only_x: BTreeSet<Binder> = [Name::raw("x")].into_iter().collect();
         let only_k: BTreeSet<Binder> = [Name::raw("k")].into_iter().collect();
         assert!(!scope_gaps(&bad, |n| only_x.contains(n)).is_empty());
@@ -2053,12 +2066,12 @@ mod tests {
     #[test]
     fn apply_type_discharges_refinement_predicate() {
         let r = Refinement::born(Rc::new(gt(var("i"), var("k"))));
-        let ty = Type::fun(Type::Refinement(Box::new(Type::infer()), r), Type::infer());
+        let ty = Type::fun(Type::refined_one(Type::infer(), r), Type::infer());
         let out = Subst::discharge("k", int(5)).apply_type(&ty);
         let Type::Fun { domain, .. } = &out else {
             panic!("expected fun");
         };
-        let Type::Refinement(_, r2) = domain.as_ref() else {
+        let [r2] = domain.refinements() else {
             panic!("expected refinement domain");
         };
         assert_eq!(*r2.predicate, gt(var("i"), int(5)));
@@ -2073,7 +2086,7 @@ mod tests {
     fn apply_type_shadows_pi_binder() {
         let refined = |pred: TypedExpr| {
             Type::fun(
-                Type::Refinement(Box::new(Type::infer()), Refinement::born(Rc::new(pred))),
+                Type::refined_one(Type::infer(), Refinement::born(Rc::new(pred))),
                 Type::infer(),
             )
         };
@@ -2091,7 +2104,7 @@ mod tests {
             panic!()
         };
         assert_eq!(
-            *r2.predicate,
+            *r2.sole().expect("one refinement").predicate,
             gt(var("i"), TypedExpr::var(Name::pi_bound_bare(0)))
         );
 
@@ -2110,9 +2123,7 @@ mod tests {
         let Type::Fun { domain, .. } = codomain.as_ref() else {
             panic!()
         };
-        let Type::Refinement(_, r2) = domain.as_ref() else {
-            panic!()
-        };
+        let [r2] = domain.refinements() else { panic!() };
         assert_eq!(*r2.predicate, gt(var("i"), var("k")));
     }
 
@@ -2271,8 +2282,8 @@ mod rewrite_tests {
         let shared = Rc::new(gt(var("k"), int(0)));
         // Two refinement occurrences sharing one predicate term, both inside a
         // single type (a function's domain and codomain).
-        let dom = Type::Refinement(Box::new(Type::Hole), Refinement::sharing(&shared));
-        let cod = Type::Refinement(Box::new(Type::Hole), Refinement::sharing(&shared));
+        let dom = Type::refined_one(Type::Hole, Refinement::sharing(&shared));
+        let cod = Type::refined_one(Type::Hole, Refinement::sharing(&shared));
         let mut e = var("y").with_ty(Type::fun(dom, cod));
 
         Subst::discharge("k", int(5)).rewrite_expr(&mut e);
@@ -2283,10 +2294,10 @@ mod rewrite_tests {
         else {
             panic!("function type preserved");
         };
-        let Type::Refinement(_, rd) = domain.as_ref() else {
+        let [rd] = domain.refinements() else {
             panic!("domain refinement preserved");
         };
-        let Type::Refinement(_, rc) = codomain.as_ref() else {
+        let [rc] = codomain.refinements() else {
             panic!("codomain refinement preserved");
         };
         assert_eq!(
@@ -2544,13 +2555,13 @@ mod locally_nameless_tests {
     /// `{Int | <pred>}` — the predicate need not be `Bool`-typed for these
     /// structural tests.
     fn refined(pred: TypedExpr) -> Type {
-        Type::Refinement(Box::new(int()), Refinement::born(Rc::new(pred)))
+        Type::refined_one(int(), Refinement::born(Rc::new(pred)))
     }
     fn predicate_of(ty: &Type) -> &TypedExpr {
-        let Type::Refinement(_, r) = ty else {
+        let Type::Refinement(_, refinements) = ty else {
             panic!("expected a refinement, got {ty}");
         };
-        &r.predicate
+        &refinements.sole().expect("one refinement").predicate
     }
     fn is_pi_bound(e: &TypedExpr, k: u32) -> bool {
         matches!(&e.node, TypedExprNode::Var(n) if n.pi_bound_index() == Some(k))
@@ -2678,17 +2689,17 @@ mod locally_nameless_tests {
         let k = Name::fresh("k");
         let shared = Rc::new(TypedExpr::var(k.clone()));
         let untouched = Rc::new(TypedExpr::lit(Lit::Int(1)));
-        let slot = |r: &Rc<TypedExpr>| Type::Refinement(Box::new(int()), Refinement::sharing(r));
+        let slot = |r: &Rc<TypedExpr>| Type::refined_one(int(), Refinement::sharing(r));
         let ty = Type::Tuple(vec![slot(&shared), slot(&shared), slot(&untouched)]);
         let closed = close_pi_binder(&k, &ty);
         let Type::Tuple(ts) = &closed else {
             panic!("closing preserves the tuple");
         };
         let pred_rc = |t: &Type| {
-            let Type::Refinement(_, r) = t else {
+            let Type::Refinement(_, refinements) = t else {
                 panic!("expected refinement");
             };
-            Rc::clone(&r.predicate)
+            Rc::clone(&refinements.sole().expect("one refinement").predicate)
         };
         assert!(
             Rc::ptr_eq(&pred_rc(&ts[0]), &pred_rc(&ts[1])),
@@ -2733,7 +2744,7 @@ mod locally_nameless_tests {
     #[test]
     fn the_dependence_test_is_per_position_not_per_predicate() {
         let shared = Rc::new(TypedExpr::var(Name::pi_bound_bare(0)));
-        let slot = || Type::Refinement(Box::new(int()), Refinement::sharing(&shared));
+        let slot = || Type::Refinement(Box::new(int()), Refinement::sharing(&shared).into());
         // Under a function the index is one crossing short of the enclosing
         // one, so that position does not reference it; beside the function it
         // does.
diff --git a/src/ccl/symbolic.rs b/src/ccl/symbolic.rs
index f7e1a2c71..8ca8d6759 100644
--- a/src/ccl/symbolic.rs
+++ b/src/ccl/symbolic.rs
@@ -935,9 +935,9 @@ in x"
     #[case(
         Expr::lambda(
             "x",
-            Type::Refinement(
-                Box::new(Type::Base(BaseType::Int)),
-                Refinement::born(Rc::new(Expr::lit(Lit::Bool(true)))),
+            Type::refined_one(
+                Type::Base(BaseType::Int),
+                Refinement::born(Rc::new(Expr::lit(Lit::Bool(true))))
             ),
             Expr::var("x"),
         ),
diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs
index 9948ebe0b..e9bcc6118 100644
--- a/src/ccl/ty.rs
+++ b/src/ccl/ty.rs
@@ -597,8 +597,15 @@ pub enum Type {
     /// the part this type commits to — see that type for why a sum needs the
     /// distinction where a record does not.
     Variant(Vec<(FieldKey, Type)>, Openness),
-    /// A refinement of another type
-    Refinement(Box<Type>, Refinement),
+    /// A base type narrowed by the conjunction of a [`RefinementSet`]'s refinements.
+    ///
+    /// **Invariants**, both established by [`Type::refined`] (which every
+    /// construction site should go through rather than building this variant
+    /// directly): the set is non-empty, and the base is not itself a
+    /// `Refinement` — nested layers flatten into one set, so `{{𝑇 | 𝑝} | 𝑞}` is
+    /// unrepresentable and the question "which layer is outermost" cannot be
+    /// asked. See [`RefinementSet`] for why that question had no good answer.
+    Refinement(Box<Type>, RefinementSet),
     /// Pre-inference placeholder stamped by lowering on every new node.
     ///
     /// Invariant: every `Hole` must be eliminated by the end of inference.
@@ -953,16 +960,24 @@ fn fmt_type(
         // and spelling it out puts one in front of the reader at every literal.
         // Every other refinement prints in the general form.
         //
-        // The predicate renders inside `binders`, so a reference to an
-        // enclosing function prints as that function's binder name.
-        Type::Refinement(t, r) => match singleton_value(ty) {
+        // Refinements render comma-separated (`{Int | p, q}`) — a conjunction.
+        // Sorted, because the set is unordered: a rendering must not depend
+        // on which order refinements happened to be inserted in, or a diagnostic
+        // (or a test comparing rendered types) would see a difference that
+        // the type system says is not there.
+        //
+        // Each refinement renders inside `binders`, so a reference to an enclosing
+        // function prints as that function's binder name.
+        Type::Refinement(t, refinements) => match singleton_value(ty) {
             Some(lit) => write!(f, "{}@{}", at(t, binders), symbolic::symbolic(lit)),
-            None => write!(
-                f,
-                "{{{} | {}}}",
-                at(t, binders),
-                symbolic::symbolic_under(&r.predicate, binders)
-            ),
+            None => {
+                let mut rendered: Vec<String> = refinements
+                    .iter()
+                    .map(|r| symbolic::symbolic_under(&r.predicate, binders))
+                    .collect();
+                rendered.sort();
+                write!(f, "{{{} | {}}}", at(t, binders), rendered.join(", "))
+            }
         },
         Type::Hole => write!(f, "_"),
         // A hole with an identity renders as one: `_#0` and `_#1` are distinct
@@ -994,13 +1009,11 @@ fn fmt_type(
 /// rule that handles refinements handles this one unchanged — and this recognizes
 /// the shape just well enough to print it as what it means.
 fn singleton_value(ty: &Type) -> Option<&TypedExpr> {
-    let Type::Refinement(base, r) = ty else {
+    let Type::Refinement(_, refinements) = ty else {
         return None;
     };
-    // Exactly one layer: a further-refined singleton is not one.
-    if matches!(base.as_ref(), Type::Refinement(..)) {
-        return None;
-    }
+    // Exactly one refinement: a base carrying further restrictions is not a singleton.
+    let r = refinements.sole()?;
     let TypedExprNode::BinOp {
         left,
         op: crate::ccl::BinOpKind::Compare(crate::ccl::CompareKind::Equals),
@@ -1247,7 +1260,45 @@ impl Type {
         }
     }
 
-    /// Look through every outer [`Type::Refinement`] layer, returning the bare
+    /// Build `base` narrowed by `refinements` — **the** way to construct a
+    /// [`Type::Refinement`], establishing both of its invariants.
+    ///
+    /// Empty `refinements` yields `base` unrefined (a position claiming nothing is
+    /// its base type), and a `base` that is already refined has its refinements
+    /// merged in rather than stacked on top, so refinement sets never nest.
+    /// Flattening is sound because every refinement at a position restricts the same
+    /// underlying element: a refinement narrows which values inhabit a type, it
+    /// does not change them, so an outer refinement's [`REFINEMENT_BINDER`] ranges
+    /// over exactly the values the inner one does.
+    pub fn refined(base: Type, refinements: RefinementSet) -> Type {
+        if refinements.is_empty() {
+            return base;
+        }
+        match base {
+            Type::Refinement(inner, existing) => {
+                Type::Refinement(inner, existing.union(&refinements))
+            }
+            bare => Type::Refinement(Box::new(bare), refinements),
+        }
+    }
+
+    /// [`Type::refined`] with a single refinement — the common case at a site that
+    /// mints one predicate.
+    pub fn refined_one(base: Type, refinement: Refinement) -> Type {
+        Type::refined(base, RefinementSet::one(refinement))
+    }
+
+    /// The refinements carried at this position — empty for an unrefined type, so a
+    /// caller can compare or filter what two positions demand without
+    /// case-splitting on whether either is refined.
+    pub fn refinements(&self) -> &[Refinement] {
+        match self {
+            Type::Refinement(_, refinements) => refinements.as_slice(),
+            _ => &[],
+        }
+    }
+
+    /// Look through the [`Type::Refinement`] wrapper, returning the bare
     /// structural type underneath. Borrowing and non-allocating; refinements
     /// nested inside the structure are left in place.
     ///
@@ -1261,11 +1312,12 @@ impl Type {
     /// is a different operation: it *drops* refinements rather than looking past them,
     /// allocates, and is only meaningful on a resolved type.
     pub fn peel_refinements(&self) -> &Type {
-        let mut cur = self;
-        while let Type::Refinement(inner, _) = cur {
-            cur = inner;
+        match self {
+            // One layer suffices: `Type::refined` flattens, so a refinement's
+            // base is never itself refined.
+            Type::Refinement(inner, _) => inner,
+            other => other,
         }
-        cur
     }
 
     /// The value type of the mutable variable this denotes, or `None` if it is not
@@ -1389,8 +1441,8 @@ impl Type {
                     .collect(),
                 *openness,
             ),
-            Type::Refinement(base, r) => {
-                Type::Refinement(Box::new(base.without_pi_names()), r.clone())
+            Type::Refinement(base, refinements) => {
+                Type::refined(base.without_pi_names(), refinements.clone())
             }
             Type::History {
                 value,
@@ -1756,14 +1808,25 @@ fn eq_cast_target_predicates(
         ccl_utils::cast_target_refinement(t2),
     ) {
         (None, None) => true,
-        (Some(r1), Some(r2)) => {
-            if Rc::ptr_eq(&r1.predicate, &r2.predicate) {
-                return true;
-            }
-            // Under the *enclosing* pairing: a nested predicate may reference a
-            // binder the outer predicate introduced (a comprehension inside a
-            // filter), and that reference resolves by position like any other.
-            eq_refinement_predicate_go(&r1.predicate, &r2.predicate, pairs)
+        // Set equality, whose member comparison is `Refinement`'s own, run
+        // **under the enclosing pairing**: a nested predicate may reference a
+        // binder the outer predicate introduced (a comprehension inside a
+        // filter), and that reference resolves by position like any other, so
+        // the comparison cannot start a fresh pairing the way
+        // `RefinementSet`'s own `PartialEq` does. Deduplicated on both sides
+        // ([`RefinementSet::insert`]), so equal cardinality plus one-way
+        // containment is mutual containment — the same argument that impl
+        // makes. The mutual recursion terminates on tree shape: predicates are
+        // acyclic `Rc<TypedExpr>`s, so a cast target cannot contain the term
+        // comparing it.
+        (Some(s1), Some(s2)) => {
+            s1.len() == s2.len()
+                && s1.iter().all(|r1| {
+                    s2.iter().any(|r2| {
+                        Rc::ptr_eq(&r1.predicate, &r2.predicate)
+                            || eq_refinement_predicate_go(&r1.predicate, &r2.predicate, pairs)
+                    })
+                })
         }
         _ => false,
     }
@@ -2073,6 +2136,320 @@ impl std::hash::Hash for Refinement {
     }
 }
 
+/// The refinements carried at one refined position: an **unordered set** of
+/// [`Refinement`]s, deduplicated by their structural [`PartialEq`].
+///
+/// A refined type narrows its base by the *conjunction* of these refinements, and
+/// conjunction is commutative, idempotent, and associative — so a set is the
+/// honest carrier and a chain of nested `{{𝑇 | 𝑝} | 𝑞}` layers was not. That
+/// chain gave one representation three incompatible readings: a *set* to
+/// subtyping (the deficit machinery compares layers as a set), a *stack* to
+/// planning (whichever layer sat outermost drove which restrict it built), and
+/// an *identity* to `SpecKey` and the recorded-vs-recomputed walls (`Type`'s
+/// derived equality is position-sensitive). Layers accumulated in constraint
+/// *arrival* order, so the stack reading made typing depend on the order two
+/// bounds happened to meet at a variable. Set semantics deletes the degree of
+/// freedom rather than pinning it to a canonical order: there is no position to
+/// read, so planning is free to apply predicates in whatever order it likes
+/// (cheapest filter first, say) without changing an identity.
+///
+/// The invariant, maintained by [`insert`](Self::insert) and relied on by
+/// [`PartialEq`]: **no two members are equal**. Given that, mutual containment
+/// reduces to equal length plus one-way containment.
+#[derive(Debug, Clone, Default)]
+pub struct RefinementSet(Vec<Refinement>);
+
+/// Whether to build refinement sets in reversed physical order — the
+/// order-independence **stress knob**, driven by `CAMBRA_REFINEMENT_ORDER=reverse`.
+///
+/// Set semantics makes the backing `Vec`'s order meaningless by contract, but
+/// two classes of order-dependence survive a representation change that the
+/// type system cannot catch: a consumer that *iterates* the set and lets the
+/// order reach something observable, and a dedup that keeps the
+/// first-inserted of two `eq`-equal members whose (type-blind-equal) predicate
+/// terms carry different embedded type slots. Flipping the physical order
+/// globally and re-running the suite is the only way to exercise both. Reading
+/// it once into a `LazyLock` keeps the check to a cached bool, and it is
+/// `debug_assertions`-only so a release compiler cannot be perturbed by the
+/// environment.
+#[cfg(debug_assertions)]
+fn stress_reversed() -> bool {
+    static REVERSED: std::sync::LazyLock<bool> = std::sync::LazyLock::new(|| {
+        std::env::var("CAMBRA_REFINEMENT_ORDER").as_deref() == Ok("reverse")
+    });
+    *REVERSED
+}
+
+#[cfg(not(debug_assertions))]
+fn stress_reversed() -> bool {
+    false
+}
+
+impl RefinementSet {
+    /// The empty set — an unrefined position.
+    pub fn new() -> Self {
+        RefinementSet(Vec::new())
+    }
+
+    /// The singleton set carrying one refinement.
+    pub fn one(r: Refinement) -> Self {
+        RefinementSet(vec![r])
+    }
+
+    /// Add a refinement, keeping the set deduplicated. Returns whether it was new.
+    ///
+    /// A refinement already present is dropped rather than replacing the incumbent:
+    /// the two are equal as *restrictions* ([`eq_refinement_predicate`]), and
+    /// keeping the incumbent preserves whatever predicate `Rc` sharing the
+    /// position already had.
+    pub fn insert(&mut self, r: Refinement) -> bool {
+        if self.0.contains(&r) {
+            return false;
+        }
+        if stress_reversed() {
+            self.0.insert(0, r);
+        } else {
+            self.0.push(r);
+        }
+        true
+    }
+
+    /// Add every refinement of `other`.
+    pub fn extend(&mut self, other: impl IntoIterator<Item = Refinement>) {
+        for r in other {
+            self.insert(r);
+        }
+    }
+
+    /// The union of two sets — the position carries every refinement either side
+    /// imposes.
+    /// This is the *meet* of the refined types (a narrower value satisfies
+    /// more), so it is what a negative-polarity merge performs.
+    pub fn union(mut self, other: &RefinementSet) -> Self {
+        self.extend(other.iter().cloned());
+        self
+    }
+
+    /// The intersection — only the refinements *both* sides guarantee, which is
+    /// what a value known to be one of two things reliably carries (the
+    /// positive-polarity merge, and the *join* of the refined types).
+    pub fn intersect(&self, other: &RefinementSet) -> Self {
+        RefinementSet(
+            self.0
+                .iter()
+                .filter(|r| other.contains(r))
+                .cloned()
+                .collect(),
+        )
+    }
+
+    pub fn contains(&self, r: &Refinement) -> bool {
+        self.0.contains(r)
+    }
+
+    pub fn as_slice(&self) -> &[Refinement] {
+        &self.0
+    }
+
+    pub fn is_empty(&self) -> bool {
+        self.0.is_empty()
+    }
+
+    pub fn len(&self) -> usize {
+        self.0.len()
+    }
+
+    pub fn iter(&self) -> std::slice::Iter<'_, Refinement> {
+        self.0.iter()
+    }
+
+    /// Rewrite every refinement's predicate in place, then re-establish the dedup
+    /// invariant.
+    ///
+    /// The passes that rewrite predicates — substitution forcing, predicate
+    /// compilation, binder conversion, node typing — cannot change *which*
+    /// positions are refined, but they can make two distinct refinements **equal**:
+    /// a substitution mapping two binders onto one term, or a compilation
+    /// normalizing two spellings of one predicate. The set would then hold a
+    /// duplicate, and [`PartialEq`] reads cardinality, so two sets equal as sets
+    /// would compare unequal — and a set is an identity at the trivial-equality
+    /// short-circuit, at cache keys, and at the recorded-vs-recomputed walls.
+    /// Re-deduplicating after the walk is what makes the invariant hold by
+    /// construction instead of being re-argued at each of the eight rewrite sites.
+    ///
+    /// No program in the suite reaches a collapsing rewrite, in either physical
+    /// order; the dedup is what would notice one starting to, and
+    /// `a_rewrite_that_collapses_two_refinements_leaves_a_set` reaches it directly.
+    ///
+    /// The closure sees each refinement's **physical** index, for a caller pairing
+    /// per-position context onto the walk ([`application_elem_types`]).
+    pub fn rewrite_each(&mut self, mut f: impl FnMut(usize, &mut Refinement)) {
+        let outcome = self.try_rewrite_each(|i, r| {
+            f(i, r);
+            Ok::<(), std::convert::Infallible>(())
+        });
+        debug_assert!(outcome.is_ok(), "an infallible rewrite cannot fail");
+    }
+
+    /// [`rewrite_each`](Self::rewrite_each) for a rewrite that can fail. The
+    /// dedup runs whether or not the walk completed, so a set is never left
+    /// holding a duplicate on the error path.
+    pub fn try_rewrite_each<E>(
+        &mut self,
+        mut f: impl FnMut(usize, &mut Refinement) -> Result<(), E>,
+    ) -> Result<(), E> {
+        let mut outcome = Ok(());
+        for (i, r) in self.0.iter_mut().enumerate() {
+            if let Err(e) = f(i, r) {
+                outcome = Err(e);
+                break;
+            }
+        }
+        if self.0.len() > 1 {
+            let mut kept = Vec::with_capacity(self.0.len());
+            for r in self.0.drain(..) {
+                if !kept.contains(&r) {
+                    kept.push(r);
+                }
+            }
+            self.0 = kept;
+        }
+        outcome
+    }
+
+    /// The sole refinement, or `None` if the set does not hold exactly one.
+    ///
+    /// For the positions built with exactly one predicate by construction — a
+    /// `cast` target's domain refinement, a literal singleton's pin — where
+    /// "the" refinement is a real notion rather than a position in a chain.
+    pub fn sole(&self) -> Option<&Refinement> {
+        match self.0.as_slice() {
+            [r] => Some(r),
+            _ => None,
+        }
+    }
+}
+
+/// Walk `refinements` in **application order**: each refinement paired with the type its
+/// element has at the point that refinement applies — `base` narrowed by every refinement
+/// applied before it.
+///
+/// A refinement set is unordered as a *fact* about a value, but materializing it is a
+/// pipeline — planning emits one `restrict` per refinement — and a pipeline is
+/// sequential: stage 𝑘 reads elements already narrowed by stages 1..𝑘-1, so its
+/// element type is not the bare base. Planning therefore *chooses* an order here.
+/// Which order is free (any of them yields a well-typed pipeline for the same
+/// final domain, and a cost model could pick the cheapest filter first); what is
+/// not free is choosing *differently* in two places, since the types along the
+/// pipeline and the predicates compiled for it must agree. Every site that
+/// lowers or types that pipeline goes through this function, so they agree by
+/// construction rather than by coincidence.
+pub fn application_order<'a>(
+    refinements: &'a [Refinement],
+    base: &'a Type,
+) -> impl Iterator<Item = (&'a Refinement, Type)> + 'a {
+    // Planning's chosen order is a deterministic function of the refinements'
+    // *content* — their rendered predicates — never of the set's physical
+    // (insertion) order, which carries no meaning. Any order yields a correct
+    // pipeline; choosing one that ignores insertion order keeps the built term
+    // reproducible however the refinements happened to accumulate, and matches the
+    // order `Display` renders a refinement set in. A cost model is free to replace
+    // this key (cheapest filter first) without touching identity.
+    let mut ordered: Vec<&Refinement> = refinements.iter().collect();
+    // `sort_by_cached_key`, not `sort_by_key`: rendering a predicate walks its whole
+    // term tree and allocates, and `sort_by_key` recomputes the key at every
+    // comparison.
+    ordered.sort_by_cached_key(|r| symbolic::symbolic(&r.predicate));
+    let mut narrowed = RefinementSet::new();
+    ordered.into_iter().map(move |r| {
+        let elem_ty = Type::refined(base.clone(), narrowed.clone());
+        narrowed.insert(r.clone());
+        (r, elem_ty)
+    })
+}
+
+/// [`application_order`]'s element types, indexed by each refinement's **physical**
+/// position in `refinements`.
+///
+/// For the sites that rewrite refinements *in place* and so must walk the set in its
+/// own order. The application order is a permutation of the physical one, so
+/// zipping [`application_order`]'s types straight onto a physical-order walk
+/// pairs refinements with the wrong element type whenever the two orders differ —
+/// silently, since both sequences have the same length. This does the
+/// permutation explicitly.
+pub fn application_elem_types(refinements: &[Refinement], base: &Type) -> Vec<Type> {
+    let mut out = vec![base.clone(); refinements.len()];
+    for (r, elem_ty) in application_order(refinements, base) {
+        // `application_order` borrows the very slice it was handed, so pointer
+        // identity locates the refinement exactly — `PartialEq` would not, being
+        // type-blind and therefore able to match a sibling.
+        let idx = refinements
+            .iter()
+            .position(|c| std::ptr::eq(c, r))
+            .expect("application_order yields borrows into `refinements`");
+        out[idx] = elem_ty;
+    }
+    out
+}
+
+impl PartialEq for RefinementSet {
+    /// Set equality. Sound as stated because both sides are deduplicated
+    /// ([`insert`](RefinementSet::insert)), so equal cardinality plus one-way
+    /// containment is mutual containment.
+    fn eq(&self, other: &Self) -> bool {
+        self.0.len() == other.0.len() && self.0.iter().all(|r| other.0.contains(r))
+    }
+}
+
+impl Eq for RefinementSet {}
+
+impl std::hash::Hash for RefinementSet {
+    /// Order-insensitive, as [`PartialEq`] demands: each member's hash is
+    /// folded in with a commutative operation. `wrapping_add` rather than
+    /// `XOR` because XOR lets two hash-colliding members cancel to the empty
+    /// set's hash; the length is mixed in for the same reason.
+    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
+        let mut combined: u64 = 0;
+        for r in &self.0 {
+            let mut h = std::collections::hash_map::DefaultHasher::new();
+            std::hash::Hash::hash(r, &mut h);
+            combined = combined.wrapping_add(std::hash::Hasher::finish(&h));
+        }
+        std::hash::Hash::hash(&self.0.len(), state);
+        std::hash::Hash::hash(&combined, state);
+    }
+}
+
+impl FromIterator<Refinement> for RefinementSet {
+    fn from_iter<I: IntoIterator<Item = Refinement>>(iter: I) -> Self {
+        let mut out = RefinementSet::new();
+        out.extend(iter);
+        out
+    }
+}
+
+impl IntoIterator for RefinementSet {
+    type Item = Refinement;
+    type IntoIter = std::vec::IntoIter<Refinement>;
+    fn into_iter(self) -> Self::IntoIter {
+        self.0.into_iter()
+    }
+}
+
+impl<'a> IntoIterator for &'a RefinementSet {
+    type Item = &'a Refinement;
+    type IntoIter = std::slice::Iter<'a, Refinement>;
+    fn into_iter(self) -> Self::IntoIter {
+        self.0.iter()
+    }
+}
+
+impl From<Refinement> for RefinementSet {
+    fn from(r: Refinement) -> Self {
+        RefinementSet::one(r)
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -2239,6 +2616,48 @@ mod tests {
         );
     }
 
+    /// [`application_elem_types`] permutes, it does not zip.
+    ///
+    /// [`application_order`] walks refinements in *content* order; a site that
+    /// rewrites refinements in place walks them in *physical* order. Both sequences
+    /// have the same length, so zipping one onto the other pairs refinements with
+    /// the wrong element type silently whenever the orders differ. Built here
+    /// with physical order deliberately the reverse of content order.
+    #[test]
+    fn application_elem_types_follow_the_refinement_not_the_position() {
+        let refinement = |name: &str| {
+            Refinement::born(Rc::new(TypedExpr::binop(
+                TypedExpr::var(name),
+                BinOpKind::Compare(CompareKind::Equals),
+                TypedExpr::lit(Lit::Int(1)),
+            )))
+        };
+        // Physical order [b, a]; content order sorts to [a, b].
+        let (a, b) = (refinement("a"), refinement("b"));
+        let refinements = vec![b.clone(), a.clone()];
+        let base = Type::Base(BaseType::Int);
+
+        let by_position = application_elem_types(&refinements, &base);
+        let by_content: Vec<Type> = application_order(&refinements, &base)
+            .map(|(_, t)| t)
+            .collect();
+
+        // `a` applies first, so it sees the bare base; `b` sees the base
+        // narrowed by `a`. Indexed physically, that is [narrowed, bare].
+        assert_eq!(by_position[1], base, "`a` (physical index 1) applies first");
+        assert_eq!(
+            by_position[0],
+            Type::refined(base.clone(), RefinementSet::one(a)),
+            "`b` (physical index 0) applies second, under `a`"
+        );
+        // The naive zip would have handed `b` the bare base — the two
+        // sequences are genuinely different, so this test has teeth.
+        assert_ne!(
+            by_position, by_content,
+            "physical and content order must differ here, or this pins nothing"
+        );
+    }
+
     /// Two predicates that each contain a [`TypedExprNode::Cast`] and differ
     /// only in the *target's* domain-refinement predicate denote different
     /// refinements: the nested filter is semantic, not inference metadata, so
@@ -2275,6 +2694,89 @@ mod tests {
         );
     }
 
+    /// A rewrite that makes two refinements equal leaves a *set*, not a bag.
+    ///
+    /// [`RefinementSet::rewrite_each`]'s callers rewrite predicates in place, and a
+    /// substitution mapping two binders onto one term collapses two refinements into
+    /// one. `PartialEq` reads cardinality, so a surviving duplicate would make two
+    /// sets equal as sets compare unequal.
+    #[test]
+    fn a_rewrite_that_collapses_two_refinements_leaves_a_set() {
+        let eq_to = |name: &str| {
+            Refinement::born(Rc::new(TypedExpr::binop(
+                TypedExpr::var(crate::ccl::Name::elem()),
+                BinOpKind::Compare(CompareKind::Equals),
+                TypedExpr::var(crate::ccl::Name::raw(name)),
+            )))
+        };
+        let mut set = RefinementSet::new();
+        set.insert(eq_to("x"));
+        set.insert(eq_to("y"));
+        assert_eq!(set.len(), 2, "two distinct predicates, two refinements");
+
+        // The collapsing rewrite: both binder references become `z`.
+        set.rewrite_each(|_, r| *r = eq_to("z"));
+
+        assert_eq!(
+            set.len(),
+            1,
+            "the collapsed pair is one refinement: {set:?}"
+        );
+        assert_eq!(
+            set,
+            RefinementSet::one(eq_to("z")),
+            "and equals the set built with one insert"
+        );
+    }
+
+    /// The same equality from the other side: two cast-target vintages that
+    /// render identically stay two refinements.
+    ///
+    /// [`eq_refinement_predicate`] compares a cast's target predicate because
+    /// that predicate is a semantic filter rather than inference metadata
+    /// (pinned above by `refinement_eq_distinguishes_cast_target_predicates`).
+    /// A resolved `ty` slot makes the rendering elide the target, so the two
+    /// vintages are indistinguishable in a diagnostic — and a [`RefinementSet`]
+    /// 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.
+    #[test]
+    fn cast_target_vintages_render_alike_but_do_not_dedup() {
+        // Two casts of one value, differing *only* in their targets' domain
+        // refinement — the shape a discharge mints at two comprehension depths.
+        let vintage = |marker: i64| {
+            let target = ccl_utils::refined_data_fun(
+                Type::Base(BaseType::Int),
+                TypedExpr::lit(Lit::Int(marker)),
+                Type::Base(BaseType::Int),
+            );
+            Refinement::born(Rc::new(
+                ccl_utils::make_cast(TypedExpr::lit(Lit::Int(0)), target)
+                    .with_ty(Type::Base(BaseType::Int)),
+            ))
+        };
+        let (a, b) = (vintage(1), vintage(2));
+        assert_eq!(
+            symbolic::symbolic(&a.predicate),
+            symbolic::symbolic(&b.predicate),
+            "the two vintages must be indistinguishable in the rendering"
+        );
+        assert_ne!(a, b, "cast-target predicates distinguish the two vintages");
+
+        let mut set = RefinementSet::new();
+        set.insert(a);
+        set.insert(b);
+        assert_eq!(set.len(), 2, "vintages do not dedup: {set:?}");
+    }
+
     /// A shape test looks *through* a refinement: a refined mutable variable is still
     /// one and a refined channel is still a channel. Nothing in the pipeline
     /// wraps a handle today — a handle type is built structurally rather than
@@ -2284,7 +2786,7 @@ mod tests {
     #[test]
     fn handle_accessors_see_through_a_refinement() {
         let refinement = Refinement::born(Rc::new(TypedExpr::lit(Lit::Bool(true))));
-        let refine = |t: Type| Type::Refinement(Box::new(t), refinement.clone());
+        let refine = |t: Type| Type::refined_one(t, refinement.clone());
         let int = Type::Base(BaseType::Int);
         let mut_var = Type::History {
             value: Box::new(int.clone()),
@@ -2504,7 +3006,8 @@ mod tests {
                 TypedExpr::var(crate::ccl::Name::elem()),
                 BinOpKind::Compare(CompareKind::Equals),
                 TypedExpr::var(k.clone()),
-            ))),
+            )))
+            .into(),
         );
         let ty = Type::pi(k.clone(), Type::Base(BaseType::Int), refined);
         assert_eq!(ty.to_string(), "((k: Int) ⇒ {Int | __elem == k})");
@@ -2520,10 +3023,11 @@ mod tests {
 
         // Stored, though, it is the index: the spelling is metadata that
         // identity ignores, so the refinement is α-canonical.
-        let Type::Refinement(_, r) = &**codomain else {
+        let Type::Refinement(_, refinements) = &**codomain else {
             panic!("expected the refinement");
         };
-        let TypedExprNode::BinOp { right, .. } = &r.predicate.node else {
+        let refinement = refinements.sole().expect("one refinement");
+        let TypedExprNode::BinOp { right, .. } = &refinement.predicate.node else {
             panic!("expected the dependent refinement");
         };
         let TypedExprNode::Var(reference) = &right.node else {
@@ -2544,7 +3048,7 @@ mod tests {
     fn an_unnamed_crossing_still_counts_when_rendering() {
         let refined = Type::Refinement(
             Box::new(Type::Base(BaseType::Int)),
-            Refinement::born(Rc::new(TypedExpr::var(crate::ccl::Name::pi_bound_bare(1)))),
+            Refinement::born(Rc::new(TypedExpr::var(crate::ccl::Name::pi_bound_bare(1)))).into(),
         );
         // (k: Int) ⇒ (Int ⇒ {Int | #1}) — one unnamed crossing in between.
         let ty = Type::Fun {
diff --git a/src/ccl/uniquify.rs b/src/ccl/uniquify.rs
index 18136a483..3ced31ecd 100644
--- a/src/ccl/uniquify.rs
+++ b/src/ccl/uniquify.rs
@@ -93,14 +93,16 @@ fn distinct_predicate_terms(expr: &Expr) -> Vec<Vec<crate::ccl::provenance::Node
         e.walk_children(|c| ids_of(c, out));
     }
     fn from_ty(t: &Type, acc: &mut HashMap<usize, Vec<NodeId>>, seen: &mut HashSet<usize>) {
-        if let Type::Refinement(_, r) = t {
-            let key = std::rc::Rc::as_ptr(&r.predicate) as usize;
-            if seen.insert(key) {
-                let mut v = Vec::new();
-                ids_of(&r.predicate, &mut v);
-                v.sort_unstable();
-                acc.insert(key, v);
-                from_expr(&r.predicate, acc, seen);
+        if let Type::Refinement(_, rs) = t {
+            for r in rs.iter() {
+                let key = std::rc::Rc::as_ptr(&r.predicate) as usize;
+                if seen.insert(key) {
+                    let mut v = Vec::new();
+                    ids_of(&r.predicate, &mut v);
+                    v.sort_unstable();
+                    acc.insert(key, v);
+                    from_expr(&r.predicate, acc, seen);
+                }
             }
         }
         t.walk_children(|c| from_ty(c, acc, seen));
@@ -350,13 +352,15 @@ impl Uniquifier {
     /// (see module docs), with every occurrence re-pointed at the rebuilt `Rc`
     /// via `memo`.
     fn ty(&mut self, t: &mut Type) {
-        if let Type::Refinement(_, r) = t {
+        if let Type::Refinement(_, refinements) = t {
             // A handle clone, so `self` stays freely borrowable for the rebuild —
             // which re-enters this same memo through `self.expr` → `self.ty`.
             let memo = self.memo.clone();
-            memo.rebuild(r, &(), |pred| {
-                self.expr(pred);
-                true
+            refinements.rewrite_each(|_, r| {
+                memo.rebuild(r, &(), |pred| {
+                    self.expr(pred);
+                    true
+                });
             });
         }
         t.walk_children_mut(|c| self.ty(c));
@@ -435,7 +439,7 @@ fn collect_node_ids(expr: &Expr) -> Vec<crate::ccl::provenance::NodeId> {
     use crate::ccl::provenance::NodeId;
 
     fn from_ty(t: &Type, out: &mut Vec<NodeId>) {
-        if let Type::Refinement(_, r) = t {
+        for r in t.refinements() {
             from_expr(&r.predicate, out);
         }
         t.walk_children(|c| from_ty(c, out));
@@ -517,7 +521,7 @@ mod tests {
     /// inside other refinements' predicate expressions.
     fn collect_refinements(e: &Expr, out: &mut Vec<Refinement>) {
         fn from_ty(t: &Type, out: &mut Vec<Refinement>) {
-            if let Type::Refinement(_, r) = t {
+            for r in t.refinements() {
                 out.push(r.clone());
                 collect_refinements(&r.predicate, out);
             }
diff --git a/src/interpreter/operator_conversion.rs b/src/interpreter/operator_conversion.rs
index 2c09be744..dc165b726 100644
--- a/src/interpreter/operator_conversion.rs
+++ b/src/interpreter/operator_conversion.rs
@@ -66,7 +66,7 @@ use std::{cell::RefCell, collections::HashMap, rc::Rc};
 /// conversion as the `input` argument.  Iteration is never inserted implicitly here — every
 /// iteration site is explicitly marked by a chain-head `Apply(predicate, Builtin::Iterate)`
 /// emitted by [`crate::ccl::planning`]'s `insert_iterate_markers` pass (plus zero or more
-/// `Apply(p, Builtin::Restrict)` mid-chain filters per refinement layer).  This module compiles
+/// `Apply(p, Builtin::Restrict)` mid-chain filters, one per refinement).  This module compiles
 /// `Iterate` to an `IterateExtent` tile (plus a `Restrict` filter when the predicate is
 /// non-trivial) and `Restrict` to a `Restrict` tile over the upstream input.  Arms that
 /// previously fell back to an implicit iteration when `input=None` now error out — a planner bug,
diff --git a/tests/compilation_pipeline/joins_aggregates_groupby.rs b/tests/compilation_pipeline/joins_aggregates_groupby.rs
index 1ad71eacf..1ed56f22a 100644
--- a/tests/compilation_pipeline/joins_aggregates_groupby.rs
+++ b/tests/compilation_pipeline/joins_aggregates_groupby.rs
@@ -303,7 +303,7 @@ fn test_groupby(#[case] code: &str, #[case] expected: Tile) {
 )]
 #[case(
     "[x for x in [y for y in [1,2,3] if y < 3] if x < 2]",
-    "iterate ▷ (([1, 2, 3] ≫ (id, 3 ▷ const) ▷ zip ≫ lt) ▷ restrict) ▷ ((cast([1, 2, 3]) ≫ (id, 2 ▷ const) ▷ zip ≫ lt) ▷ restrict) ≫ cast(cast([1, 2, 3])):({{[0, 2] | __elem ▷ ([1, 2, 3] ≫ (id, 3 ▷ const) ▷ zip ≫ lt)} | __elem ▷ (cast([1, 2, 3]) ≫ (id, 2 ▷ const) ▷ zip ≫ lt)} ⤇ Int)",
+    "iterate ▷ (([1, 2, 3] ≫ (id, 3 ▷ const) ▷ zip ≫ lt) ▷ restrict) ▷ ((cast([1, 2, 3]) ≫ (id, 2 ▷ const) ▷ zip ≫ lt) ▷ restrict) ≫ cast(cast([1, 2, 3])):({[0, 2] | __elem ▷ ([1, 2, 3] ≫ (id, 3 ▷ const) ▷ zip ≫ lt), __elem ▷ (cast([1, 2, 3]) ≫ (id, 2 ▷ const) ▷ zip ≫ lt)} ⤇ Int)",
     make_int_list(&[1])
 )]
 #[case(
diff --git a/tests/predicate_sharing.rs b/tests/predicate_sharing.rs
index d01347f1e..6baa7eaba 100644
--- a/tests/predicate_sharing.rs
+++ b/tests/predicate_sharing.rs
@@ -156,8 +156,8 @@ fn filtered_join_nesting_stays_shared() {
 
 /// `{Int | true}` over a fresh predicate `Rc`.
 fn refined_int() -> Type {
-    Type::Refinement(
-        Box::new(Type::Base(BaseType::Int)),
+    Type::refined_one(
+        Type::Base(BaseType::Int),
         Refinement::born(Rc::new(Expr::lit(Lit::Bool(true)))),
     )
 }
diff --git a/tests/predicate_sharing_review.rs b/tests/predicate_sharing_review.rs
index 7b2b78170..5f3498bf2 100644
--- a/tests/predicate_sharing_review.rs
+++ b/tests/predicate_sharing_review.rs
@@ -25,12 +25,12 @@ fn gt(l: TypedExpr, r: TypedExpr) -> TypedExpr {
 }
 /// `{_ | pred}`, a second occurrence of an existing predicate term.
 fn refined(pred: &Rc<TypedExpr>) -> Type {
-    Type::Refinement(Box::new(Type::Hole), Refinement::sharing(pred))
+    Type::refined_one(Type::Hole, Refinement::sharing(pred))
 }
 /// The predicate term of a `{_ | p}`.
 fn predicate_of(ty: &Type) -> &Rc<TypedExpr> {
-    let Type::Refinement(_, r) = ty else {
-        panic!("expected a refinement, got {ty}");
+    let [r] = ty.refinements() else {
+        panic!("expected exactly one refinement, got {ty}");
     };
     &r.predicate
 }
diff --git a/tests/programs/refinement/mod.rs b/tests/programs/refinement/mod.rs
index 612832293..7f4b6b9cb 100644
--- a/tests/programs/refinement/mod.rs
+++ b/tests/programs/refinement/mod.rs
@@ -4,6 +4,8 @@ use super::common::expect_compile_error;
 fn refinement() {
     expect_compile_error(
         include_str!("nested_refinement.cambra"),
-        "expected {{Int | __elem != 1} | __elem != 0}",
+        // The two written refinement levels are one refinement set, so the diagnostic
+        // names both refinements at one base rather than a nesting.
+        "expected {Int | __elem != 0, __elem != 1}",
     );
 }
diff --git a/tests/type_check.rs b/tests/type_check.rs
index 231dc4511..662ef4844 100644
--- a/tests/type_check.rs
+++ b/tests/type_check.rs
@@ -1670,8 +1670,8 @@ groups(0)
     let Type::Fun { domain: dom, .. } = &ty else {
         panic!("expected a partition function type, got {ty}");
     };
-    let Type::Refinement(_, r) = &**dom else {
-        panic!("expected a refined partition domain, got {ty}");
+    let [r] = dom.refinements() else {
+        panic!("expected a singly-refined partition domain, got {ty}");
     };
     let pred = cambra::ccl::symbolic::symbolic(&r.predicate);
     assert!(
@@ -1710,8 +1710,8 @@ apply0(groups)
     let Type::Fun { domain: dom, .. } = &ty else {
         panic!("expected a partition function type, got {ty}");
     };
-    let Type::Refinement(_, r) = &**dom else {
-        panic!("expected a refined partition domain, got {ty}");
+    let [r] = dom.refinements() else {
+        panic!("expected a singly-refined partition domain, got {ty}");
     };
     let pred = cambra::ccl::symbolic::symbolic(&r.predicate);
     assert!(
@@ -1744,8 +1744,8 @@ fn test_groupby_partition_stores_an_index_and_renders_the_binder() {
     let Type::Fun { domain: dom, .. } = &**codomain else {
         panic!("expected the partition function inside the key function, got {ty}");
     };
-    let Type::Refinement(_, r) = &**dom else {
-        panic!("expected a refined partition domain, got {ty}");
+    let [r] = dom.refinements() else {
+        panic!("expected a singly-refined partition domain, got {ty}");
     };
     // Stored: the reference is a bound index, not a free name. Read off the
     // term, because the *rendering* deliberately spells it as the binder.