Derive a Cast's refinements from its term instead of overwriting the target

[dpmills]

A rebuild pass resolves a cast's bases; it never decides its refinements. Four passes decided them, each by stamping a type derived from the surrounding term onto a cast slot, and each producing two copies of one refinement that render alike and refuse to dedup.

coalesce_node overwrote a Cast's target wholesale with the occurrence's coalesced view (expr.ty). Which refinements an occurrence's variable accumulates depends on the route bounds took through the graph, so two copies of one embedded cast — a comprehension source cloned into a filter predicate has its own variable per copy — coalesce carrying different refinement sets: one bare, one decorated with a sibling layer's filter. Refinement equality is deliberately cast-target-aware, so the copies refused to dedup, and which copy a position ended up holding depended on bound arrival order.

The overwrite becomes canonical_cast_ty: the coalesced view contributes its shape and bases; the refinements are determined by the term. A cast is an assertion — cast(value, {D | p} ⇒ V) asserts exactly p on top of whatever its value already established — so its target keeps its born refinements (fixed when lowering wrote the cast; inference resolves bases, never rewrites refinements), and the node's type is the value's own domain refinements joined with them (the walk is bottom-up, so the value's type is already canonical by induction). Target and type stay distinct: the post-inference check recomputes a cast's type as value-refinements ∪ target-refinements, and a target that also carried the value's refinements would double-book them — any divergence between the value's copy and the target's copy of one refinement surfaces as a duplicated refinement in the recomputation.

The other three sites, each the same rule applied later in the pipeline:

• simplify's collapse-a-chain-to-one-element rewrite stamped the chain's interface type wholesale onto a surviving Cast. The interface type is derived from neighbour types, which are route-dependent where inference left route-dependent types in eq-blind slots (a lambda param annotation inside a still-pointful predicate), so the stamp desynced the cast's recorded type from its term-determined refinements. The rewrite now restores the canonical type at construction.

• sync_cast_targets (at the tails of lambda_elim::run, planning::run, and inlining) copied that route-dependent expr.ty into the cast's target, promoting a benign, eq-invisible divergence into the one slot eq_refinement_predicate deliberately compares. The pass is retired; ccl_utils::canonicalize_cast_types replaces it — target = born refinements on the rebuilt view's bases, expr.ty = value-refinements ∪ born, and a chain headed by a cast follows its head's domain when the two differ only in refinements on one base (the post-pass check's reconcile is exact on domain refinements, so the recorded chain type must track its head). canonical_cast_ty moves to ccl_utils and is shared with coalesce.

• compile_refinement_predicates compiled a cast target's refinements against the target's bare base. A target holds only the cast's born refinements, so its sole refinement compiled with a bare __elem stamp — failing the checker's argument edge once the predicate function's domain carries the value's refinements. Target refinements are assertions on the cast's value, so they now compile against the value's domain, matching emit_cast, which types target predicates with __elem bound at the value's domain.

The desync is reachable and measured: 14 cast sites, in both physical refinement orders. Instrumenting canonical_cast_ty to report when the term-determined set differs from the view the old code installed wholesale counts 14 over the corpus, forward and reversed alike — a nested filter is enough ([a for a in [b for b in [1, 2, 3, 4] if b < 3] if a < 3], already in the suite). At each one the target had picked up the value's refinement in addition to its own born one: view {[0,3] | b < 3, cast(…) ▷ a < 3} against the term-determined {cast(…) ▷ a < 3}.

No inferred type changes, because the double-booking is currently absorbed rather than observed. The post-inference check recomputes a cast's type as value-refinements ∪ target-refinements, and the target's extra copy of the value's refinement is eq to the value's own, so the set deduplicates it — the representation change below this commit is what makes the defect latent, and under the old nested-layer representation the same 14 sites produced a duplicated layer.

The failure mode is the copies not being eq. Refinement equality is deliberately cast-target-aware, so two vintages of one refinement do not dedup, and then the recomputation disagrees with the recorded type while printing the same. Instrumenting RefinementSet::insert for a member that renders alike without being eq counts zero over the corpus in either order at this commit and below it, so that surface is currently unreached — a refinement's binding is its index rather than its spelling once the telescope coordinate is beneath the stack. The 14 sites are the reachable half, and removing the double-booking is what keeps the unreachable half unreachable.

a_cast_target_does_not_carry_its_value_s_refinements pins it: the nested filter above, compiled, with every cast asserted to carry no refinement its value already establishes. It fails on the parent commit, naming the doubled predicate.

Review guide: ccl_utils::canonical_cast_ty is the rule, and the four call sites are the change. predicates.rs also gains compile_refinements, extracting the per-refinement compile loop so a cast target and an ordinary refined domain share it.

[dpmills]

This change is part of the following stack:

• Scope inference variables with telescopes, and identify binder references by position #108
  • Hold a refined type's refinements in one unordered set instead of nested layers #77
    • Derive a Cast's refinements from its term instead of overwriting the target #78 ◀
      • Give CompactType's refinement slot the None sentinel its shape slots carry #115
        • Apply a function slot's domain rule once its kind is resolved, not at each merge #116
          • Give a function slot's domain alternatives an order-insensitive set #117
            • Reject a product with no fields instead of answering Unit #118
              • Model the type system in Lean, and check the solver's subtyping and bound merge against it #109

_{Change managed by git-spice.}