Give CompactType's refinement slot the None sentinel its shape slots carry

[dpmills]

CompactType::merge could not tell "no refinement contribution here" from "a value that guarantees nothing": both were the empty RefinementSet, and an empty set is absorbing under the positive intersect, so a bare variable's contribution erased refinements a sibling bound established. Three places worked around that — merge's imposes_nothing guard, the bound fold keeping the variable out until the end, and the opposite-polarity fallback's refinement union. refinements becomes Option<RefinementSet>, the sentinel rec, var, and fun already carry, with None as the merge identity; a hole and a bare variable are the only contributions that are not values and keep it, and CompactType::value builds the rest.

dissolve_read_feeds' reconstructed channel now imposes nothing rather than an empty refinement set — it re-expresses content already at the position rather than arriving as a second bound — so a refined feed read keeps its refinements. Nothing else changes behavior: the suite passes forward, under DEEP_TYPECHECK=1, and under CAMBRA_REFINEMENT_ORDER=reverse.

Asserting it

CompactType::refinements documents that None is the merge identity and belongs to exactly the two contributions that are not values — a hole and a bare variable — while Some(empty) is a value guaranteeing nothing. Nothing in the type system says so: every value-shaped arm has to be built from CompactType::value, across a dozen construction sites, and a position that carried content with the slot absent would absorb a sibling bound's refinements instead of intersecting with none of its own, so Int joined with {Int | p} would keep p.

refinement_slot_present is that post-condition, checked on compact_type_with's output and on every recursive-variable bound it recorded. Variable contributions are not content: a bare variable's whole content is its identity, so vars is the one populated field the slot may accompany as None.

Three tests keep the checker from being vacuous — it accepts the hole and the bare variable, and rejects content with the slot absent both at the root and below it. The whole suite passes with the assert live, so the invariant holds on every program the corpus compiles.

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