diff --git a/src/ccl/design/type-inference.md b/src/ccl/design/type-inference.md index 21558ad9..97861364 100644 --- a/src/ccl/design/type-inference.md +++ b/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, diff --git a/src/ccl/infer/solver/compact.rs b/src/ccl/infer/solver/compact.rs index 80bdaefe..beea0e07 100644 --- a/src/ccl/infer/solver/compact.rs +++ b/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() { diff --git a/src/ccl/infer/solver/mod.rs b/src/ccl/infer/solver/mod.rs index 5a11a6f1..9220a9de 100644 --- a/src/ccl/infer/solver/mod.rs +++ b/src/ccl/infer/solver/mod.rs @@ -135,6 +135,18 @@ pub(crate) mod test_helpers { use crate::ccl::{FieldKey, Refinement, Type}; + /// `__elem == ` — the dependent-refinement predicate shape, aimed at a + /// specific Pi binder. Shared because a dependent codomain is the shape every + /// α-identity test needs, across `compact` and `spec_key`. + pub(crate) fn dep_pred(name: &str) -> Rc { + use crate::ccl::{BinOpKind, CompareKind, Name, TypedExpr}; + Rc::new(TypedExpr::binop( + TypedExpr::var(Name::elem()), + BinOpKind::Compare(CompareKind::Equals), + TypedExpr::var(Name::raw(name)), + )) + } + /// Build a `Type` from `FieldKey`-keyed fields: all-`Name` → `Record`, /// otherwise a dense `Tuple` (the only product shapes `ccl::Type` has). /// Sparse-`Index` inputs have no `Type` form — tests that need them diff --git a/src/ccl/infer/solver/spec_key.rs b/src/ccl/infer/solver/spec_key.rs index b0de6417..94bb7eb2 100644 --- a/src/ccl/infer/solver/spec_key.rs +++ b/src/ccl/infer/solver/spec_key.rs @@ -336,12 +336,12 @@ pub fn spec_key(ty: &Type) -> SpecKey { // One walk-wide `ctx` for both reads: its memo is keyed by polarity, so the // two reads share it without contaminating each other. SpecKey { - positive: key_go(ty, true, &Subst::id(), &mut ctx), - negative: key_go(ty, false, &Subst::id(), &mut ctx), + positive: key_go(ty, true, &Subst::id(), &mut ctx, 0), + negative: key_go(ty, false, &Subst::id(), &mut ctx, 0), } } -fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView { +fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx, pi_depth: u8) -> KeyView { match ty { // `BoundedHole` is a *pre-inference* annotation marker: `normalize_annotation` // erases it into a bounded variable before any constraint is emitted, so @@ -373,7 +373,7 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView // clone will actually carry — that is use-specific information, and two // uses discharging different arguments *should* key apart. Type::Refinement(inner, r) => { - let mut k = key_go(inner, pol, subst_acc, ctx); + let mut k = key_go(inner, pol, subst_acc, ctx, pi_depth); let r = subst_acc.force_refinement(r); if !k.refinements.contains(&r) { k.refinements.push(r); @@ -388,15 +388,15 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView } => { // The domain is contravariant — the flip that makes the dual read // follow an argument's *lower* bounds. - let dom = key_go(domain, !pol, subst_acc, ctx); - // A Pi binder shadows the accumulated substitution inside the - // codomain, as in `compact_go`. The binder *name* itself is not part - // of the key — see `SpecKey::fun`. - let cod_acc = match name { - Some(b) => subst_acc.shadow(b), - None => subst_acc.clone(), - }; - let cod = key_go(codomain, pol, &cod_acc, ctx); + let dom = key_go(domain, !pol, subst_acc, ctx, pi_depth); + // Canonical Pi binders (`Subst::canonical_pi_binder`), so a keyed + // predicate referencing the binder does so α-insensitively: two uses + // whose instantiation types differ only in source binder names key + // together. The canonical *name* is discarded — it is not part of + // the key (see `SpecKey::fun`); what matters is that the + // *references* were rewritten. + let cod_scope = subst_acc.canonical_pi_binder(name, pi_depth); + let cod = key_go(codomain, pol, &cod_scope.subst, ctx, cod_scope.depth); // Resolved through `KindMerge::of`, not off the `FunKind` itself: an // inferred kind is a variable whose identity is fresh per instantiation, // so keying on it would split every use; its *bounds* are the answer, and @@ -410,7 +410,7 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView rec: ts .iter() .enumerate() - .map(|(i, t)| (FieldKey::Index(i), key_go(t, pol, subst_acc, ctx))) + .map(|(i, t)| (FieldKey::Index(i), key_go(t, pol, subst_acc, ctx, pi_depth))) .collect(), ..Default::default() }, @@ -420,7 +420,7 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView .map(|(n, t)| { ( FieldKey::Name(SmolStr::from(n.as_str())), - key_go(t, pol, subst_acc, ctx), + key_go(t, pol, subst_acc, ctx, pi_depth), ) }) .collect(), @@ -429,7 +429,7 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView Type::Variant(tags) => KeyView { var: tags .iter() - .map(|(k, t)| (k.clone(), key_go(t, pol, subst_acc, ctx))) + .map(|(k, t)| (k.clone(), key_go(t, pol, subst_acc, ctx, pi_depth))) .collect(), ..Default::default() }, @@ -440,8 +440,8 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView domain, kind, } => { - let value = key_go(value, pol, subst_acc, ctx); - let domain = key_go(domain, pol, subst_acc, ctx); + let value = key_go(value, pol, subst_acc, ctx, pi_depth); + let domain = key_go(domain, pol, subst_acc, ctx, pi_depth); KeyView { history: BTreeMap::from([(*kind, (Box::new(value), Box::new(domain)))]), ..Default::default() @@ -477,7 +477,7 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView // does: a bound reached transitively arrives with every edge's // substitution composed. let inner_acc = Subst::then(&b.render_subst(), subst_acc); - acc.union(key_go(&b.ty, pol, &inner_acc, ctx)); + acc.union(key_go(&b.ty, pol, &inner_acc, ctx, pi_depth)); } ctx.visiting.remove(&memo_key); if memoizable && ctx.truncations == truncations_before { @@ -502,6 +502,78 @@ mod tests { use crate::ccl::infer_var::Bound; use crate::ccl::{BaseType, Lit, TypedExpr}; + /// **Finding, repaired: α-variant dependent types key together.** Before + /// canonical Pi binders (`key_go` renaming references to `Name::pi(depth)` + /// as it walks), the binder name — deliberately excluded from the key — + /// leaked back in through the *predicates* that reference it, so + /// `(𝑥: 𝐷) ⤇ {Int | __elem == 𝑥}` at one call site and its `𝑦`-twin at + /// another keyed apart and split a specialization that should be shared. + #[test] + fn spec_key_shares_alpha_variant_dependent_types() { + use super::spec_key; + use crate::ccl::infer::solver::test_helpers::dep_pred; + 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 fx = dep_fun("x"); + let fy = dep_fun("y"); + + // The relation reconciles the α-variants both ways… + let mut c = ConstrainCache::new(); + assert!(constrain_subtype(&fx, &fy, &mut c).is_ok()); + let mut c = ConstrainCache::new(); + assert!(constrain_subtype(&fy, &fx, &mut c).is_ok()); + // …and the specialization key now agrees. + assert_eq!( + spec_key(&fx), + spec_key(&fy), + "α-variant dependent instantiation types must share a specialization" + ); + } + + /// The key's canonical rename must stay **injective** over enclosing binders. + /// The key does not carry the binder name (see [`SpecKey::fun`]), so what + /// records which binder a predicate referenced is the rewritten reference + /// itself — and two keys that should differ collapse together if the rename + /// gives the inner and outer binders one name. A collapse here is an + /// *under*-split: two uses share a specialization whose interior was + /// resolved against the other's argument, which is the silent failure + /// `Subst::canonical_pi_binder` warns about. + #[test] + fn spec_key_keeps_distinct_binders_distinct() { + use super::spec_key; + use crate::ccl::infer::solver::test_helpers::dep_pred; + use crate::ccl::{FunKind, Name, Refinement}; + + 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!( + spec_key(&nested("y")), + spec_key(&nested("x")), + "keying must not conflate the inner and outer Pi binders" + ); + } + fn int() -> Type { Type::Base(BaseType::Int) } @@ -733,12 +805,14 @@ mod tests { true, &Subst::id(), &mut fresh_ctx(), + 0, ); merged.union(key_go( &Type::data_fun(int(), int()), true, &Subst::id(), &mut fresh_ctx(), + 0, )); assert_eq!( merged.fun.len(), @@ -771,12 +845,14 @@ mod tests { true, &Subst::id(), &mut fresh_ctx(), + 0, ); merged.union(key_go( &history(HistoryKind::Append), true, &Subst::id(), &mut fresh_ctx(), + 0, )); assert_eq!( merged.history.len(), diff --git a/src/ccl/lambda_elim.rs b/src/ccl/lambda_elim.rs index 6f796526..c83a37e2 100644 --- a/src/ccl/lambda_elim.rs +++ b/src/ccl/lambda_elim.rs @@ -1259,13 +1259,16 @@ fn elim_lambdas_impl(ctx: &mut ElimContext, expr: Expr) -> Result Result &'static str { match self { ReservedName::Elem => "__elem", + ReservedName::Pi(depth) => PI_SPELLINGS[depth as usize], } } } @@ -171,6 +189,11 @@ impl Name { Name::Reserved(ReservedName::Elem) } + /// The canonical Pi binder at `depth` (see [`ReservedName::Pi`]). + pub fn pi(depth: u8) -> Self { + Name::Reserved(ReservedName::Pi(depth)) + } + /// Mint a compiler-introduced binder of `kind` with a globally fresh /// `uid`. The named wrappers below are the call-site vocabulary. fn synthetic(kind: SyntheticKind) -> Self { diff --git a/src/ccl/subst.rs b/src/ccl/subst.rs index e023580f..c2fe4238 100644 --- a/src/ccl/subst.rs +++ b/src/ccl/subst.rs @@ -154,6 +154,32 @@ impl Mapping { #[derive(Clone, Debug, Default, PartialEq)] pub struct Subst(BTreeMap); +/// Everything a `Fun`'s codomain must be walked under, produced by one call to +/// [`Subst::canonical_pi_binder`]. +/// +/// The three fields travel together so that a walk cannot take the canonical +/// binder and then derive the codomain's depth itself. Getting the name right +/// and the depth wrong is what this type exists to prevent: entering a codomain +/// at the arrow's own depth names every enclosing binder `__pi0`, which +/// conflates the predicates that reference them while staying internally +/// consistent — and idempotent, so comparing a type against its own canonical +/// form does not detect it. What each walk owes the others, and the tests that +/// pin it, are in `src/ccl/design/type-inference.md`, "Canonicalizing a Pi +/// binder needs a position, so it happens at flattening". +#[derive(Debug, Clone)] +pub struct PiCodomain { + /// The canonical binder to record on the rebuilt arrow; `None` for a + /// non-dependent one. + pub binder: Option, + /// The substitution the codomain's predicate references resolve through — + /// this morphism with the binder's rename applied on top. + pub subst: Subst, + /// The codomain's own depth. Every arrow nests a binder's scope whether or + /// not it names one, so this is always one deeper than the arrow's; a + /// domain keeps the arrow's depth and is therefore walked without it. + pub depth: u8, +} + impl Subst { /// The identity substitution — a perfect no-op. `apply_*` on it returns the /// input structurally unchanged. @@ -317,6 +343,54 @@ impl Subst { Subst(m) } + /// The **canonical Pi binder** rule, in one place. + /// + /// A function type's binder at codomain-depth `depth` is the reserved + /// [`Name::pi`] name for that depth, and the rename rides the accumulated + /// substitution so that every reference to the old binder inside the + /// codomain — a dependent refinement predicate, say — is rewritten as that + /// codomain is walked. Returns the canonical binder and the substitution to + /// walk the codomain under; the caller recurses at `depth + 1` (a domain + /// keeps `depth`, since only codomain arrows nest a binder's scope). + /// + /// The depth makes the binder a *position*, and flattening is the first + /// point in the pipeline where a Pi reference has one: while a dependent + /// refinement rides a bound edge, the variable holding it need not sit under + /// the binder its predicate references, so there is no index to write. That + /// is why the rewrite cannot move earlier, and why the alternatives that + /// look like they remove it do not — see `src/ccl/design/type-inference.md`, + /// "Canonicalizing a Pi binder needs a position, so it happens at flattening". + /// + /// One shared name per position is what makes α-variant types flatten to + /// identical shapes, so they merge, their refinement copies dedup rather + /// than accumulating a dangling twin, and every identity built on the + /// flattened form is α-insensitive. + /// + /// **Three walks apply it and must agree exactly**, which is why the rule + /// lives here rather than being spelled out in each: `compact_go` (the + /// flattened bound graph), `spec_key::key_go` (the specialization key), and + /// [`Type::alpha_normalized`](crate::ccl::Type::alpha_normalized) (the pure + /// function the recorded-vs-recomputed walls compare through). A divergence + /// between the first two is *silent* and yields a shared clone whose + /// interior was resolved against a different use's argument. + pub fn canonical_pi_binder(&self, name: &Option, depth: u8) -> PiCodomain { + match name { + Some(b) => { + let canon = Name::pi(depth); + PiCodomain { + binder: Some(canon.clone()), + subst: self.extended_rename(b.clone(), canon), + depth: depth + 1, + } + } + None => PiCodomain { + binder: None, + subst: self.clone(), + depth: depth + 1, + }, + } + } + /// Extend this substitution with a fresh binder correspondence `k ↦ x` /// (the Pi-vs-Pi binder alignment derived in the codomain edge). `k` is a /// newly-scoped binder, so this is an insert, not a composition. diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index 4cad77a2..945e6afd 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -1088,6 +1088,12 @@ impl Type { /// the binder's presence — rebuilt combinator arrows (`fun_ty_or_hole`, /// [`Type::fun`]) are constructed with `name: None`. If those sites ever /// preserve binders on rebuilt arrows, this helper can retire. + /// + /// Blindness to binder *presence* is not blindness to binder *identity*. + /// Where the two sides can carry different binder names for the same + /// position — solver output is canonicalized to [`crate::ccl::Name::pi`] + /// while an independently-rebuilt type keeps the term's own names — + /// compose with [`Type::alpha_normalized`] first. pub fn without_pi_names(&self) -> Type { match self { Type::Fun { @@ -1136,6 +1142,70 @@ impl Type { } } + /// The **α-normal form**: every Pi binder renamed to the reserved + /// depth-indexed name ([`crate::ccl::Name::pi`]) and every predicate + /// reference rewritten through the rename — the same scheme the solver + /// applies as it flattens types (`compact.rs`), exposed as a pure + /// function so comparisons between solver output (already canonical) and + /// independently-rebuilt types (source-named binders) can meet on one + /// form. Two α-equivalent types have equal α-normal forms. + pub fn alpha_normalized(&self) -> Type { + use crate::ccl::subst::Subst; + fn go(t: &Type, depth: u8, subst: &Subst) -> Type { + match t { + Type::Fun { + name, + kind, + domain, + codomain, + } => { + let dom = go(domain, depth, subst); + let cod_scope = subst.canonical_pi_binder(name, depth); + let cod = go(codomain, cod_scope.depth, &cod_scope.subst); + Type::Fun { + name: cod_scope.binder, + kind: kind.clone(), + domain: Box::new(dom), + codomain: Box::new(cod), + } + } + Type::Refinement(base, r) => { + Type::Refinement(Box::new(go(base, depth, subst)), subst.force_refinement(r)) + } + Type::Tuple(ts) => Type::Tuple(ts.iter().map(|t| go(t, depth, subst)).collect()), + Type::Record(fs) => Type::Record( + fs.iter() + .map(|(n, t)| (n.clone(), go(t, depth, subst))) + .collect(), + ), + Type::Variant(tags) => Type::Variant( + tags.iter() + .map(|(k, t)| (k.clone(), go(t, depth, subst))) + .collect(), + ), + Type::History { + value, + domain, + kind, + } => Type::History { + value: Box::new(go(value, depth, subst)), + domain: Box::new(go(domain, depth, subst)), + kind: *kind, + }, + Type::BoundedHole(t) => Type::BoundedHole(Box::new(go(t, depth, subst))), + Type::Base(_) + | Type::UIntRange(_) + | Type::DataSource(_) + | Type::ChanDom(..) + | Type::Txn + | Type::Infer(_) + | Type::SharedHole(_) + | Type::Hole => t.clone(), + } + } + go(self, 0, &Subst::id()) + } + /// Create a fresh [`Type::Infer`] variable for use in tests. /// /// Use this only when constructing expressions in tests that will not be