Canonicalize each arrow's Pi binder as the solver flattens types

[dpmills]

A dependent function type's binder name leaks into two identities that are meant to be blind to it. spec_key excludes the binder from the key, but a dependent refinement predicate references it, so (𝑥: 𝐷) ⤇ {Int | __elem == 𝑥} and its 𝑦-twin key apart and split a specialization two uses should share. Merging α-variant bounds keeps the first arrival's binder while unioning both copies of one predicate, coalescing to an arrival-order-dependent type whose second predicate references a binder that is no longer there. Both flattening walks now rename each arrow's binder, and every codomain reference to it, to the reserved __pi{depth} name, so α-equivalence coincides with structural equality on the flattened form.

Subst::canonical_pi_binder owns the rule; its doc comment names the three walks that apply it and what a silent divergence between them costs. Type::alpha_normalized is that scheme as a pure function, which lambda_elim's debug assertions compose with without_pi_names to compare canonical solver output against a type rebuilt from the term's own binders.

A regression test in compact.rs and one in spec_key.rs state the repaired findings.

Why the rewrite sits at the flattening layer rather than at emission or in a comparison, and what the four alternatives break on, is recorded in type-inference.md; canonical_pi_binder cites it.

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

[dpmills]

Superseded by the scoped-inference-variables branch (dmills/scoped-infer-vars): the flatten-time canonicalization is replaced by the locally-nameless coordinate — indices assigned once at abstraction instead of canonical names assigned across three walks with an unchecked birth-to-flatten window. This PR's regression tests carried over as that design's acceptance tests (see type-inference.md, "Scoped inference variables: stored fragments close against a telescope"). #77 and up are restacked onto the new branch.