Freshening asks a different question than type_level, so it needs its own

[dpmills]

A specialization clone must share no live inference state with the definition it was cloned from. That invariant breaks when a quantified variable is reachable only through a refinement predicate: freshen_above short-circuits on type_level, which is predicate-blind (it reports a Refinement's base level), so a type whose only above-cutoff content sits in a nested predicate is returned verbatim — still pointing at the definition's own variables. The symptom is a duplicate specialization, the clone reaching one generalized let both through freshened variables and through the original's.

The fix is a second level function, not a change to type_level, whose predicate-blindness is load-bearing for its other callers (extrusion, bound-recording scope, should_generalize); freshen_level's doc comment states the two questions. No measured cost.

[dpmills]

This change is part of the following stack:

• Freshening asks a different question than type_level, so it needs its own #71 ◀
  • SharedHole: let lowering state that two type positions are the same #72
    • Traits: state what an operator requires of its operands, not that they are the same #73
      • Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
        • Annotations stop standing in for binder structure, and stop outliving inference #60
          • Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63
            • A mutable variable read is an explicit operation, not a subtyping rule #64
              • Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it #62
                • constrain_go asserts the uniquely-keyed invariant it rests on #74
                  • Update the value-Case fan-out's prose to the DisjointJoin it builds #75
                  • Canonicalize each arrow's Pi binder as the solver flattens types #76
                  • 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
                  • Add a Lean model of the CCL type system and fuzz the solver against it #79

_{Change managed by git-spice.}