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

src/ccl/design/type-inference.md

@@ -912,6 +912,40 @@ The expected binder is **always globally fresh** (proposal §5.2 verbatim; the 
 
 The pipeline passes downstream of inference treat function types structurally and compare modulo the Pi binder (`Type::without_pi_names`). **Refinement-predicate compilation is deferred out of lambda-elim** (proposal §6.3): predicates ride through inference and lambda-elim in their bare pointful form (a bare boolean over the implicit `REFINEMENT_BINDER`), and **planning** compiles them. Order matters: the group-by / hash-join recognizers run *first*, on the bare form — compiling first would destroy the pointful shapes they match (see the pointful-join-recognizers plan) — and `planning::compile_refinement_predicates` then runs the lambda-elim → simplify sub-pipeline on each remaining predicate (keyed by predicate `Rc` identity) before the generic `iterate`/`restrict` lowering consumes it. This is what lets a refined collection — including a group-by over a *filtered* source (`[sum(x) for x in groupby([y+10 for y in xs if y<6], key)]`) — compile to a runtime `Restrict`/`Filter` rather than reaching op-conversion as an un-compiled predicate. Single-key dependent lookups (`sum(groupby(xs, key)(k))`) and the nested filtered-source group-by both run end-to-end with correct values.
 
+### Canonicalizing a Pi binder needs a position, so it happens at flattening
+
+`compact_go` and `spec_key::key_go` rewrite every arrow's binder to `Name::pi(depth)` as they flatten a type, and no earlier stage does; `Subst::canonical_pi_binder` owns the rule. The depth counts enclosing codomain arrows, so the canonical binder is a *position*, and flattening is the first point in the pipeline where a Pi reference has one.
+
+Before flattening it has none. A dependent refinement is recorded on an inference variable as an ordinary bound, and the variable holding it need not sit under the binder the predicate references. Lowering a group-by produces the shape `lower/exprs.rs`'s tests pin:
+
+```
+λ __gb_k → cast(({_ | __elem ▷ xs ▷ key_fn == __gb_k} ⤇ _), λ __gb_i → __gb_i ▷ xs)
+```
+
+`emit_lambda` types the outer lambda as `(__gb_k: 𝐾) ⇒ …`, and the refinement mentioning `__gb_k` reaches the solver as a bound on the cast's own variable — a position with no enclosing arrow at all. What relates that bound to its binder is the suspended discharge riding the edge, not containment. The two-sided storage above is what makes that work when `fn_ty` is still a variable at the apply site and its concrete Pi arrives later (the opaque/higher-order case, O3).
+
+So the scheme has to satisfy two facts at once. α-variant dependent types must compare equal, or `SpecKey` splits uses that should share a specialization and merged bounds keep a dangling twin — the behaviours `spec_key_shares_alpha_variant_dependent_types` and `alpha_variant_bound_merge_is_canonical` pin. And a reference is unpositioned for as long as it lives on an edge. Flattening is where those meet: it walks the graph and emits a type whose Pi references sit under their binders (`coalesce_compact_go` keeps a binder exactly when the codomain references it), and `check_scope_valid` then holds every coalesced node's type to its lexical scope.
+
+`ReservedName::Pi` holds a `u8`, so what lands in the flattened form is an index; `__pi0` is its `Display`. Naming a reference while it is unpositioned and indexing it once it is not is the locally-nameless discipline, with the abstraction step at the only place that can host it.
+
+#### Alternatives, and what each one breaks on
+
+Each of these removes the rewrite, and each is recorded because it does not work.
+
+- **Mint canonical binders at emission**, so nothing renormalizes. The index counts enclosing *codomain* arrows, making it a property of a binder's position in a finished type rather than of the binder. `emit_lambda` types an inner lambda before knowing what will wrap it, and placing a type in a codomain shifts every Pi binder inside it: `\s -> groupby([1,2,3,4], \x -> x // 2)` infers with the group-by's binder at `__pi1`, where the same term standing alone puts it at `__pi0`.
+
+- **Count from the inside out** — from the reference to its binder rather than from the root — so the encoding survives wrapping and emission can mint it. Wrapping is not the obstruction; the unpositioned edge is. A reference on a bound whose binder is not an ancestor has no number to carry under either direction of counting, and that is the common case rather than a corner: it is what every group-by produces.
+
+- **Give `Type` an α-invariant `PartialEq`/`Hash`** and leave the names alone. The comparison needing α-insensitivity is a `RefinementSet` dedup — `RefinementSet::insert` in `compact_go`'s refinement arm, and `merge_refinements` where two bounds meet — and the binder sits on the enclosing `CompactFun`, one frame above the values being compared. `Eq` and `Hash` take no context parameter, and `ConstrainCache` keys a `HashMap` on `(Type, Type)`, so `Hash` must be a function of the value alone.
+
+- **Rename at merge rather than at flattening**: have `CompactFun::merge` rewrite the incoming side's references onto the incumbent's binder. This one works, and moves the rewrite somewhere worse — once per merge in a fold over a variable's bounds instead of once per flatten — while the surviving binder is the first arrival's again, which is the arrival-order dependence the canonical form exists to remove.
+
+The invariant: a Pi reference is a `Name` while it rides an edge and an index once flattened. What the three walks that flatten owe each other differs, and neither obligation follows from sharing the rule.
+
+`compact_go` and `Type::alpha_normalized` must assign the *same* index, because `lambda_elim` compares a solver-produced type — canonical already, through the first — against an independently rebuilt one by normalizing both through the second (`compacting_is_a_fixpoint_of_alpha_normalization`).
+
+`spec_key::key_go` owes only **injectivity** over enclosing binders. A key is compared with other keys and carries no binder name (`SpecKey::fun`), so a consistent relabelling is invisible there; conflating two binders under one index is not, because it makes two uses share a specialization whose interior was resolved against the other's argument. Injectivity is what each walk is tested for — `canonical_binders_keep_distinct_binders_distinct` and `spec_key_keeps_distinct_binders_distinct` — and it is the property `Subst::canonical_pi_binder` cannot establish by itself: a walk that entered a codomain at the arrow's own depth would name every binder `__pi0`, which is internally consistent and idempotent, so comparing a type against its own canonical form does not detect it.
+
 ## 4.6 Data vs compute functions
 
 > **Status: implemented, minus Σ.** The `FunKind` marker, kind inference,

src/ccl/infer/solver/compact.rs

@@ -508,7 +508,7 @@ pub fn compact_type(ty: &Type) -> CompactGraph {
         recursive: HashMap::new(),
         rec_vars: BTreeMap::new(),
     };
-    let term = compact_go(ty, true, &Subst::id(), None, &mut st);
+    let term = compact_go(ty, true, &Subst::id(), None, &mut st, 0);
     CompactGraph {
         term,
         rec_vars: st.rec_vars,
@@ -572,8 +572,10 @@ struct CompactState {
 /// (`src/ccl/infer/solver/spec_key.rs`) traverses `Type` in lockstep with this
 /// function: the same polarity flip on a `Fun` domain, the same no-flip on
 /// `History` children, the same `then(edge_subst, subst_acc)` composition at a
-/// bound edge, the same binder shadowing for a Pi codomain, the same
-/// `(uid, pol)` cycle guard. That agreement *is* the soundness argument for a
+/// bound edge, the same `(uid, pol)` cycle guard. (The Pi-binder
+/// canonicalization they also share is not duplicated — both call
+/// [`Subst::canonical_pi_binder`], which owns that rule.) That agreement *is*
+/// the soundness argument for a
 /// specialization key: a bound the key cannot see is one the clone's own
 /// resolution cannot see either, because the clone resolves through this walk
 /// over the same edges from the same side. Nothing enforces it, so a new `Type`
@@ -587,6 +589,7 @@ fn compact_go(
     subst_acc: &Subst,
     parents: Option<&ParentPath<'_>>,
     st: &mut CompactState,
+    pi_depth: u8,
 ) -> CompactType {
     match ty {
         // Not a type — an annotation-position obligation, erased by
@@ -613,7 +616,7 @@ fn compact_go(
         // The predicate is an immutable term, so a non-vacuous force builds a
         // fresh predicate from the (freshened) bound's content directly.
         Type::Refinement(inner, r) => {
-            let mut ct = compact_go(inner, pol, subst_acc, parents, st);
+            let mut ct = compact_go(inner, pol, subst_acc, parents, st, pi_depth);
             let r = subst_acc.force_refinement(r);
             if !ct.refinements.contains(&r) {
                 ct.refinements.push(r);
@@ -633,17 +636,16 @@ fn compact_go(
             // per child mirrors Scala's `Set.empty` argument — cycles
             // span only one variable's bound chain, not across
             // function boundaries.
-            let dom = compact_go(d, !pol, subst_acc, None, st);
-            // A Pi binder shadows the accumulated substitution inside the
-            // codomain (it binds the name locally), so restrict it there.
-            let cod_acc = match name {
-                Some(b) => subst_acc.shadow(b),
-                None => subst_acc.clone(),
-            };
-            let cod = compact_go(c, pol, &cod_acc, None, st);
+            let dom = compact_go(d, !pol, subst_acc, None, st, pi_depth);
+            // Canonical Pi binders (`Subst::canonical_pi_binder`, which states
+            // the rule and why the three walks applying it must agree). The
+            // rename also shadows any outer mapping of the source binder, which
+            // is what the previous `shadow(b)` was for.
+            let cod_scope = subst_acc.canonical_pi_binder(name, pi_depth);
+            let cod = compact_go(c, pol, &cod_scope.subst, None, st, cod_scope.depth);
             CompactType {
                 fun: Some(CompactFun {
-                    name: name.clone(),
+                    name: cod_scope.binder,
                     kind: KindMerge::of(kind),
                     domains: vec![dom],
                     codomain: Box::new(cod),
@@ -656,7 +658,10 @@ fn compact_go(
         Type::Tuple(ts) => {
             let mut compacted = BTreeMap::new();
             for (i, v) in ts.iter().enumerate() {
-                compacted.insert(FieldKey::Index(i), compact_go(v, pol, subst_acc, None, st));
+                compacted.insert(
+                    FieldKey::Index(i),
+                    compact_go(v, pol, subst_acc, None, st, pi_depth),
+                );
             }
             CompactType {
                 rec: Some(compacted),
@@ -668,7 +673,7 @@ fn compact_go(
             for (n, v) in fs {
                 compacted.insert(
                     FieldKey::Name(SmolStr::from(n.as_str())),
-                    compact_go(v, pol, subst_acc, None, st),
+                    compact_go(v, pol, subst_acc, None, st, pi_depth),
                 );
             }
             CompactType {
@@ -683,7 +688,7 @@ fn compact_go(
             // payload depth is unaffected.
             let mut compacted = BTreeMap::new();
             for (k, v) in tags {
-                compacted.insert(k.clone(), compact_go(v, pol, subst_acc, None, st));
+                compacted.insert(k.clone(), compact_go(v, pol, subst_acc, None, st, pi_depth));
             }
             CompactType {
                 var: Some(compacted),
@@ -700,8 +705,8 @@ fn compact_go(
             domain,
             kind,
         } => {
-            let value = compact_go(value, pol, subst_acc, None, st);
-            let domain = compact_go(domain, pol, subst_acc, None, st);
+            let value = compact_go(value, pol, subst_acc, None, st, pi_depth);
+            let domain = compact_go(domain, pol, subst_acc, None, st, pi_depth);
             CompactType {
                 history_slot: Some((Box::new(value), Box::new(domain), *kind)),
                 ..Default::default()
@@ -798,7 +803,7 @@ fn compact_go(
                 // arrives with every edge's morphism composed (design §3.6).
                 // Identity edges leave `subst_acc` unchanged (the common case).
                 let inner_acc = Subst::then(&b.render_subst(), subst_acc);
-                let bc = compact_go(&b.ty, pol, &inner_acc, Some(&new_parents), st);
+                let bc = compact_go(&b.ty, pol, &inner_acc, Some(&new_parents), st, pi_depth);
                 bound = Some(match bound {
                     None => bc,
                     Some(acc) => CompactType::merge(pol, acc, bc),
@@ -820,7 +825,7 @@ fn compact_go(
             if no_concrete {
                 for b in opposite_bounds.iter() {
                     let inner_acc = Subst::then(&b.render_subst(), subst_acc);
-                    let bc = compact_go(&b.ty, !pol, &inner_acc, Some(&new_parents), st);
+                    let bc = compact_go(&b.ty, !pol, &inner_acc, Some(&new_parents), st, pi_depth);
                     bound = Some(match bound {
                         None => bc,
                         Some(acc) => CompactType::merge(!pol, acc, bc),
@@ -849,6 +854,142 @@ fn compact_go(
 mod tests {
     use super::*;
 
+    /// **Finding, repaired: merging α-variant dependent bounds is canonical.**
+    /// Before canonical Pi binders, the merged fun shape kept the *first
+    /// arrival's* binder while the refinement sets unioned both α-copies of one
+    /// constraint, coalescing to the order-dependent — and dangling —
+    /// `(𝑥: 𝐷) ⤇ {{Int | __elem == 𝑥} | __elem == 𝑦}`. With `compact_go`
+    /// renaming binders and references to `Name::pi(depth)` as bounds flatten,
+    /// α-variants compact identically: the copies dedup, the binder is
+    /// arrival-independent, and nothing dangles.
+    #[test]
+    fn alpha_variant_bound_merge_is_canonical() {
+        use crate::ccl::infer::solver::test_helpers::dep_pred;
+        use crate::ccl::infer::solver::{
+            ConstrainCache, coalesce_compact, compact_type, constrain_subtype, fresh_var,
+            simplify_type,
+        };
+        use crate::ccl::{FunKind, Name, Refinement};
+
+        let dep_fun = |binder: &str| Type::Fun {
+            name: Some(Name::raw(binder)),
+            kind: FunKind::Data,
+            domain: Box::new(Type::UIntRange(3)),
+            codomain: Box::new(Type::Refinement(
+                Box::new(Type::Base(BaseType::Int)),
+                Refinement::born(dep_pred(binder)),
+            )),
+        };
+        let coalesce_with_order = |first: &Type, second: &Type| {
+            let v = fresh_var(0);
+            constrain_subtype(&v, first, &mut ConstrainCache::new()).unwrap();
+            constrain_subtype(&v, second, &mut ConstrainCache::new()).unwrap();
+            coalesce_compact(&simplify_type(compact_type(&v))).unwrap()
+        };
+        let (fx, fy) = (dep_fun("x"), dep_fun("y"));
+        let a = coalesce_with_order(&fx, &fy);
+        let b = coalesce_with_order(&fy, &fx);
+        assert_eq!(
+            a, b,
+            "α-variant bound merge must be arrival-order-independent"
+        );
+        // The α-copies collapsed: one binder, one predicate, nothing dangling.
+        let Type::Fun { name, codomain, .. } = &a else {
+            panic!("expected a function, got {a}");
+        };
+        assert_eq!(*name, Some(Name::pi(0)));
+        let Type::Refinement(base, _) = &**codomain else {
+            panic!("expected exactly one refinement layer, got {codomain}");
+        };
+        assert!(
+            !matches!(&**base, Type::Refinement(..)),
+            "the two α-copies of one constraint must dedup to one layer, got {codomain}"
+        );
+    }
+
+    /// The canonical rename must keep distinct enclosing binders distinct: a
+    /// predicate referencing the *inner* binder denotes a different type from one
+    /// referencing the *outer*, and the two must not flatten alike.
+    ///
+    /// This is the defect a shared rule cannot rule out on its own. A walk that
+    /// entered the codomain at the arrow's own depth would name both binders
+    /// `__pi0`, conflate the two predicates, and still be internally consistent —
+    /// idempotent, even, so comparing a type against its own canonical form would
+    /// not notice. Injectivity is what has to be asserted.
+    #[test]
+    fn canonical_binders_keep_distinct_binders_distinct() {
+        use crate::ccl::infer::solver::compact_type;
+        use crate::ccl::infer::solver::test_helpers::dep_pred;
+        use crate::ccl::{FunKind, Name, Refinement};
+
+        // `(x: [0,3]) ⤇ ((y: [0,4]) ⤇ {Int | __elem == 𝑏})`, for 𝑏 the inner
+        // binder in one case and the outer in the other.
+        let nested = |referenced: &str| Type::Fun {
+            name: Some(Name::raw("x")),
+            kind: FunKind::Data,
+            domain: Box::new(Type::UIntRange(3)),
+            codomain: Box::new(Type::Fun {
+                name: Some(Name::raw("y")),
+                kind: FunKind::Data,
+                domain: Box::new(Type::UIntRange(4)),
+                codomain: Box::new(Type::Refinement(
+                    Box::new(Type::Base(BaseType::Int)),
+                    Refinement::born(dep_pred(referenced)),
+                )),
+            }),
+        };
+        assert_ne!(
+            compact_type(&nested("y")).term,
+            compact_type(&nested("x")).term,
+            "canonicalization must not conflate the inner and outer Pi binders"
+        );
+    }
+
+    /// `compact_go` and [`Type::alpha_normalized`] must agree on the assignment,
+    /// because `lambda_elim` compares a solver-produced type (canonical already,
+    /// through this walk) against an independently rebuilt one by normalizing
+    /// both. Flattening the normal form is therefore a fixpoint.
+    #[test]
+    fn compacting_is_a_fixpoint_of_alpha_normalization() {
+        use crate::ccl::infer::solver::compact_type;
+        use crate::ccl::infer::solver::test_helpers::dep_pred;
+        use crate::ccl::{FunKind, Name, Refinement};
+
+        let dep = |binder: &str, base: Type| {
+            Type::Refinement(Box::new(base), Refinement::born(dep_pred(binder)))
+        };
+        let fun = |binder: Option<&str>, domain: Type, codomain: Type| Type::Fun {
+            name: binder.map(Name::raw),
+            kind: FunKind::Data,
+            domain: Box::new(domain),
+            codomain: Box::new(codomain),
+        };
+        // A binder sits in a *domain* (which keeps the arrow's own depth) and an
+        // unnamed arrow nests a scope, so every clause of the rule is exercised.
+        let ty = fun(
+            Some("x"),
+            fun(
+                Some("a"),
+                Type::UIntRange(3),
+                dep("a", Type::Base(BaseType::Int)),
+            ),
+            fun(
+                None,
+                Type::UIntRange(4),
+                fun(
+                    Some("y"),
+                    Type::UIntRange(5),
+                    dep("y", dep("x", Type::Base(BaseType::Int))),
+                ),
+            ),
+        );
+        assert_eq!(
+            compact_type(&ty).term,
+            compact_type(&ty.alpha_normalized()).term,
+            "compact_go must assign the same canonical binders as `alpha_normalized`"
+        );
+    }
+
     /// Compact merge at positive polarity unions tags.
     #[test]
     fn compact_merge_variants_positive_unions() {