Hold a refined type's refinements in one unordered set instead of nested layers

[dpmills]

A coalesced type's refinement layers stacked in constraint arrival order: two refined upper bounds meeting at one variable produced {{T | q} | p} or {{T | p} | q} by which arrived first. Subtyping never cared — the deficit machinery compares layers as a set — but Type's equality did, and equality is load-bearing wherever a type is an identity: the trivial-equality short-circuit, cache keys, the recorded-vs-recomputed walls. One Vec was serving three readings at once: a set to subtyping, a stack to planning, an identity to SpecKey.

Type::Refinement now carries a RefinementSet — unordered, deduplicated, set-semantic Eq/Hash — and Type::refined flattens, so {{T | p} | q} is unrepresentable and "which layer is outermost" cannot be asked. A canonical sort was tried twice and rejected: it pins the ambiguity instead of deleting it, and it denies planning the freedom to apply filters in whatever order it likes.

Three things the change makes explicit. Materializing refinements is a pipeline, so planning chooses an application order — which order is free, choosing differently in two places is not, and application_order is the one place it is chosen, keyed on rendered content rather than physical order. The recognizers were reading a chain positionally: groupby now finds the refinement shaped like its key equation and join tries each refinement as the join condition, both leaving the rest on the domain they pass downstream, where dropping them silently discarded a filter. An in-place predicate rewrite can make two refinements equal, and PartialEq reads cardinality, so RefinementSet::rewrite_each re-establishes the dedup instead of each of the eight rewrite sites arguing it.

CAMBRA_REFINEMENT_ORDER=reverse flips every set's physical order and CI runs the suite both ways. Set semantics makes that order meaningless by contract, and a consumer that lets it become observable compiles clean either way.

Review guide: ty.rs carries RefinementSet, the flattening constructors, application_order, and rewrite_each, and the rest follows from them mechanically. The behavioural sites are compact.rs's merge_refinements, the two planning walks over the application order, and the two recognizers. One test pins each of the three sections above: refinements_meeting_at_one_variable_do_not_depend_on_arrival_order, application_elem_types_follow_the_refinement_not_the_position, a_rewrite_that_collapses_two_refinements_leaves_a_set. The docs' "refinement layer" and "innermost first" are converted throughout.

[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.}