diff --git a/src/ccl/ccl_utils.rs b/src/ccl/ccl_utils.rs index c99a49af..cc812e46 100644 --- a/src/ccl/ccl_utils.rs +++ b/src/ccl/ccl_utils.rs @@ -699,6 +699,7 @@ pub(crate) fn strip_refinements(ty: &Type) -> Type { Type::Base(_) | Type::UIntRange(_) | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) | Type::DataSource(_) | Type::ChanDom(..) diff --git a/src/ccl/infer/api.rs b/src/ccl/infer/api.rs index fccfdd85..47e7793d 100644 --- a/src/ccl/infer/api.rs +++ b/src/ccl/infer/api.rs @@ -830,7 +830,10 @@ fn collect_type_errors( seen_refinements: &mut HashSet, ) { match ty { - Type::Hole => errors.push(InferError::UnresolvedHole { + // A `SharedHole` is a `Hole` with an identity, and just as transient: + // `normalize_annotation` resolves both. A survivor means the annotation + // never reached normalization, which is the same compiler bug either way. + Type::Hole | Type::SharedHole(_) => errors.push(InferError::UnresolvedHole { at: context_sym.to_string(), }), Type::Infer(var) => { diff --git a/src/ccl/infer/context.rs b/src/ccl/infer/context.rs index c9254eef..ceda023f 100644 --- a/src/ccl/infer/context.rs +++ b/src/ccl/infer/context.rs @@ -2,6 +2,7 @@ // InferCtx (Step 7c) // --------------------------------------------------------------------------- +use std::cell::RefCell; use std::collections::HashMap; use crate::ccl::ccl_utils::TermMemo; @@ -112,6 +113,20 @@ pub(super) struct InferCtx { /// which is what lets `LocatedInferError` require a node instead of carrying /// an `Option` that every consumer must then interpret. current_node_id: NodeId, + /// The variable each [`Type::SharedHole`] id normalizes to, so every + /// occurrence of one id resolves to the *same* variable — which is the whole + /// content of the marker (see [`Type::SharedHole`]). + /// + /// A `RefCell` because [`normalize_annotation`](Self::normalize_annotation) + /// takes `&self` and is called from a dozen places; threading `&mut` through + /// all of them to memoize one map would be churn for no gain. + /// + /// **First occurrence fixes the level.** Ids are minted per lowered construct + /// and every occurrence of one id sits in the same expression, so the level is + /// the same at each — but nothing here enforces that, and a future desugaring + /// that shared an id across a `let` RHS boundary would silently take the first + /// level it saw. + shared_holes: RefCell>, } impl InferCtx { @@ -127,6 +142,7 @@ impl InferCtx { pred_memo: Default::default(), lit_singletons: HashMap::new(), current_node_id: root, + shared_holes: RefCell::new(HashMap::new()), } } @@ -151,6 +167,17 @@ impl InferCtx { match ty { // A `Hole` annotation means "infer this" → fresh variable. Type::Hole => fresh_var(self.level), + // A `SharedHole` means "infer this, and it is the same one as that": + // the *first* occurrence of an id mints the variable and every later + // one reuses it. That identity is the entire mechanism — it is how a + // desugaring relates two positions whose common type only inference + // will learn (see [`Type::SharedHole`]). + Type::SharedHole(id) => self + .shared_holes + .borrow_mut() + .entry(*id) + .or_insert_with(|| fresh_var(self.level)) + .clone(), // Refinements ride the lattice: keep the wrapper, normalize the // inner (so a `Refinement(Hole, r)` source annotation becomes // `Refinement(?fresh, r)` rather than losing the refinement). diff --git a/src/ccl/infer/emit.rs b/src/ccl/infer/emit.rs index ef3bd66f..71ce52c7 100644 --- a/src/ccl/infer/emit.rs +++ b/src/ccl/infer/emit.rs @@ -343,6 +343,7 @@ fn emit_annotation_predicates(ty: &mut Type, ctx: &mut InferCtx) -> Result<(), L | Type::ChanDom(..) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => Ok(()), } } diff --git a/src/ccl/infer/solve.rs b/src/ccl/infer/solve.rs index 9089f1ee..7e363f2e 100644 --- a/src/ccl/infer/solve.rs +++ b/src/ccl/infer/solve.rs @@ -1207,6 +1207,7 @@ fn coalesce_type_predicates(ty: &mut Type, level: Level, ctx: &mut CoalesceCtx) | Type::ChanDom(..) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => {} } } diff --git a/src/ccl/infer/solver/compact.rs b/src/ccl/infer/solver/compact.rs index 07afd2fb..246db66b 100644 --- a/src/ccl/infer/solver/compact.rs +++ b/src/ccl/infer/solver/compact.rs @@ -615,7 +615,7 @@ fn compact_go( } // A bare `Hole` shouldn't reach the solver (emission turns it into a // fresh var), but treat it as no contribution for exhaustiveness. - Type::Hole => CompactType::empty(), + Type::Hole | Type::SharedHole(_) => CompactType::empty(), Type::Fun { name, kind, diff --git a/src/ccl/infer/solver/constrain.rs b/src/ccl/infer/solver/constrain.rs index db78f615..1494de1e 100644 --- a/src/ccl/infer/solver/constrain.rs +++ b/src/ccl/infer/solver/constrain.rs @@ -950,7 +950,8 @@ pub fn extrude(ty: &Type, pol: bool, target_level: Level, cache: &mut ExtrudeCac | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn - | Type::Hole => ty.clone(), + | Type::Hole + | Type::SharedHole(_) => ty.clone(), Type::Fun { name, kind, diff --git a/src/ccl/infer/solver/mod.rs b/src/ccl/infer/solver/mod.rs index 89a0c1d5..21824f0b 100644 --- a/src/ccl/infer/solver/mod.rs +++ b/src/ccl/infer/solver/mod.rs @@ -91,7 +91,12 @@ pub fn type_level(ty: &Type) -> Level { // instantiation), which reads it directly and is exempted from the // `type_level` short-circuit. Type::ChanDom(..) => 0, - Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) | Type::Txn | Type::Hole => 0, + Type::Base(_) + | Type::UIntRange(_) + | Type::DataSource(_) + | Type::Txn + | Type::Hole + | Type::SharedHole(_) => 0, } } diff --git a/src/ccl/infer/solver/scheme.rs b/src/ccl/infer/solver/scheme.rs index 1e489d92..e8fbc1fe 100644 --- a/src/ccl/infer/solver/scheme.rs +++ b/src/ccl/infer/solver/scheme.rs @@ -227,9 +227,12 @@ pub fn freshen_above( return ty.clone(); } match ty { - Type::Base(_) | Type::UIntRange(_) | Type::DataSource(_) | Type::Txn | Type::Hole => { - ty.clone() - } + Type::Base(_) + | Type::UIntRange(_) + | Type::DataSource(_) + | Type::Txn + | Type::Hole + | Type::SharedHole(_) => ty.clone(), // A channel domain minted inside the generalized definition // (level > lim) is *quantified* exactly like a variable — each // instantiation is its own channel. But a rigid name cannot be diff --git a/src/ccl/infer/solver/spec_key.rs b/src/ccl/infer/solver/spec_key.rs index ea5823f8..4d988541 100644 --- a/src/ccl/infer/solver/spec_key.rs +++ b/src/ccl/infer/solver/spec_key.rs @@ -358,7 +358,7 @@ fn key_go(ty: &Type, pol: bool, subst_acc: &Subst, ctx: &mut KeyCtx) -> KeyView // no `Hole` reaches a use's instantiation type in the first place. The // arm is for exhaustiveness, and "no information here" is the honest // reading if one ever did. - Type::Hole => KeyView::default(), + Type::Hole | Type::SharedHole(_) => KeyView::default(), // A refinement rides the position it refines. The accumulated substitution // is forced on it exactly as `compact_go` does, so a suspended // dependent-application discharge lands in the key as the predicate the diff --git a/src/ccl/lower/exprs.rs b/src/ccl/lower/exprs.rs index 5b2445f7..e8a1d479 100644 --- a/src/ccl/lower/exprs.rs +++ b/src/ccl/lower/exprs.rs @@ -71,6 +71,19 @@ pub(super) fn lower_call( let collection = lower_expr(&args[0], ctx)?; let key_fn = lower_expr(&args[1], ctx)?; + // A partition function's **domain is the type of its keys**, and nothing + // in the lowered shape says so. One `SharedHole` states it, on the key + // application and on the domain of the group-by's own `data_fun` + // annotation — the two positions the claim is about. (`__gb_k` is an + // artifact of this desugaring, so the binder stays a plain `Hole` and + // takes its type from the annotation like any other parameter.) + // + // On the annotation's domain the edge is also **directional for free**: + // `bind_annotation` records `inferred <: ann` and a function type is + // contravariant in its domain, so this reduces to `key_ty <: ⟨the + // parameter⟩` — produced keys flow *into* the domain, rather than the two + // being forced equal. + let key_ty = ctx.fresh_shared_hole(); // `bare_pred` (and the `collection` clone inside it) lives in the // cast target's refinement predicate — a type slot outside the // `walk_children` domain — so its nodes are deliberately untagged. @@ -78,7 +91,8 @@ pub(super) fn lower_call( Expr::apply( Expr::apply(Expr::var(Name::elem()), collection.clone()), key_fn, - ), + ) + .with_user_annotation(key_ty.clone()), BinOpKind::Compare(CompareKind::Equals), Expr::var("__gb_k"), ); @@ -99,7 +113,7 @@ pub(super) fn lower_call( // concrete-kind stamp — see `emit_node`), so its kind is data-by- // construction rather than guessed from its (scalar key) domain. Ok(Expr::lambda("__gb_k", Type::Hole, cast) - .with_user_annotation(Type::data_fun(Type::Hole, Type::Hole))) + .with_user_annotation(Type::data_fun(key_ty, Type::Hole))) } "sum" | "max" => { if args.len() != 1 { diff --git a/src/ccl/lower/mod.rs b/src/ccl/lower/mod.rs index 0c23ee27..a1d045ee 100644 --- a/src/ccl/lower/mod.rs +++ b/src/ccl/lower/mod.rs @@ -81,7 +81,7 @@ use std::{ use crate::{ ccl::{ - Branch, Expr, Lit, TypedExprNode, + Branch, Expr, Lit, Type, TypedExprNode, lineage::{Nature, RewriteLabel}, }, chl_parser::ast::{Expr as ChlExpr, RecordField, Span, Spanned, Stmt as ChlStmt}, @@ -327,9 +327,23 @@ pub struct LoweringContext { /// enclosing or sibling scope. Within a block, the *last* definition of a name /// wins (see [`pre_register_mut_param_fns`]). pub(super) mut_param_fns: HashSet, + + /// Counter behind [`fresh_shared_hole`](Self::fresh_shared_hole). + next_shared_hole: u32, } impl LoweringContext { + /// A fresh [`Type::SharedHole`] id, unique within this lowering. + /// + /// Use one id per *relation* a desugaring wants to state, and stamp it on + /// every position that relation covers: inference normalizes equal ids to one + /// variable, so two positions carrying the same id are held to the same type. + /// Ids are meaningless outside the tree they were minted for. + pub(super) fn fresh_shared_hole(&mut self) -> Type { + let id = self.next_shared_hole; + self.next_shared_hole += 1; + Type::SharedHole(id) + } /// Register a data source so that `name()` lowers to `Source(name)`. pub fn register_source( &mut self, diff --git a/src/ccl/subst.rs b/src/ccl/subst.rs index 4e53df09..f2def1de 100644 --- a/src/ccl/subst.rs +++ b/src/ccl/subst.rs @@ -761,6 +761,7 @@ impl Subst { | Type::DataSource(_) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => {} // a nominal channel domain names its defer @@ -979,6 +980,7 @@ impl Subst { | Type::DataSource(_) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => ty.clone(), // rename the named defer binder, mirroring the @@ -1089,7 +1091,8 @@ pub fn type_contains_infer(ty: &Type) -> bool { | Type::DataSource(_) | Type::ChanDom(..) | Type::Txn - | Type::Hole => false, + | Type::Hole + | Type::SharedHole(_) => false, Type::Infer(_) => true, Type::Fun { domain, codomain, .. @@ -1137,6 +1140,7 @@ fn collect_type_fv( | Type::ChanDom(..) | Type::Txn | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) => {} Type::Fun { name, diff --git a/src/ccl/ty.rs b/src/ccl/ty.rs index 15d5f16c..20a290b1 100644 --- a/src/ccl/ty.rs +++ b/src/ccl/ty.rs @@ -555,6 +555,20 @@ pub enum Type { /// `UnresolvedHole` (treat as a compiler bug, not a user-facing error). /// Created exclusively by [`TypedExpr::new`] and [`crate::ccl::TypedBinding::new_unannotated`]. Hole, + /// A [`Hole`](Type::Hole) with an **identity**: every occurrence carrying the + /// same id normalizes to the *same* inference variable. + /// + /// This is how lowering states a relation between two type positions it cannot + /// name. A plain `Hole` says "infer this", and each occurrence gets its own + /// fresh variable; `SharedHole(id)` says "infer this, and it is the same one as + /// that" — the weakest thing that lets a desugaring connect two positions whose + /// common type only inference will learn. + /// + /// **Transient, like `Hole`**: `normalize_annotation` resolves it, and a + /// survivor is a compiler bug (`UnresolvedHole`). Ids are minted per + /// [`LoweringContext`](crate::ccl::lower::LoweringContext) and are meaningless + /// outside the tree they were minted for. + SharedHole(u32), /// Unresolved type variable, identified by a unique [`crate::ccl::InferVarId`]. /// /// Created during inference by the inference pass @@ -774,6 +788,9 @@ impl fmt::Display for Type { None => write!(f, "{{{t} | {}}}", symbolic::symbolic(&r.predicate)), }, Type::Hole => write!(f, "_"), + // A hole with an identity renders as one: `_#0` and `_#1` are distinct + // requests, two `_#0`s are the same one. + Type::SharedHole(id) => write!(f, "_#{id}"), Type::Infer(var) => write!(f, "?{}", var.uid), Type::DataSource(name) => write!(f, "source({name})"), Type::ChanDom(name, _) => write!(f, "chan({name})"), @@ -989,6 +1006,7 @@ impl Type { Type::Base(_) | Type::UIntRange(_) | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) | Type::DataSource(_) | Type::ChanDom(..) @@ -1023,6 +1041,7 @@ impl Type { Type::Base(_) | Type::UIntRange(_) | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) | Type::DataSource(_) | Type::ChanDom(..) @@ -1064,6 +1083,7 @@ impl Type { Type::Base(_) | Type::UIntRange(_) | Type::Hole + | Type::SharedHole(_) | Type::Infer(_) | Type::DataSource(_) | Type::ChanDom(..) diff --git a/tests/type_check.rs b/tests/type_check.rs index 9943c2d4..1c450ff0 100644 --- a/tests/type_check.rs +++ b/tests/type_check.rs @@ -23,6 +23,7 @@ use cambra::ccl::{ }; use cambra::chl_parser::{self, ast as chl_ast}; use cambra::interpreter::{BaseType, Extent, TestDataSource}; +use indoc::indoc; use rstest::rstest; // --------------------------------------------------------------------------- @@ -585,6 +586,105 @@ fn test_collection_union_heterogeneous_rejected() { // GroupBy + aggregate tests // --------------------------------------------------------------------------- +// A group-by's key type is its key function's codomain, and the lowering says so +// **directly** rather than leaving it to be recovered through the partition +// predicate's `==`. +// +// `__gb_k`'s only occurrence in the lowered shape is as an operand of that +// comparison, so without a stated relation its type can only arrive backwards +// along the operand requirement that relates a comparison's two sides — making a +// group-by's key inference depend on an operator's internals. One +// `Type::SharedHole` states it, carried by the key application and by the domain of +// the group-by's own `data_fun` annotation; these cases pin that the key resolves +// to the key function's result type and not to the collection's element type. +// +// The relation is **not** visible in `test_lower_groupby`'s snapshots, because +// `symbolic` does not render annotations. These are the tests that cover it. +#[rstest] +#[case("groupby([1, 2, 3], \\x -> x)", int())] +#[case("groupby([(a=1, b=\"w\"), (a=2, b=\"e\")], \\r -> r.b)", string())] +fn test_groupby_key_type_comes_from_the_key_function(#[case] code: &str, #[case] key_ty: Type) { + let ty = infer_program(code); + let Type::Fun { domain, .. } = &ty else { + panic!("a group-by is a function from key to partition, got {ty}"); + }; + assert_eq!(**domain, key_ty, "wrong key type for {code}"); +} + +/// The key type of the group-by in `code`'s result, which is expected to be a +/// tuple of two group-bys — one per instantiation / occurrence under test. +fn groupby_key_types(code: &str) -> (Type, Type) { + let ty = infer_program(code); + let Type::Tuple(parts) = &ty else { + panic!("expected a pair of group-bys, got {ty}"); + }; + let key_of = |t: &Type| match t { + Type::Fun { domain, .. } => (**domain).clone(), + other => panic!("a group-by is a function from key to partition, got {other}"), + }; + (key_of(&parts[0]), key_of(&parts[1])) +} + +// A `SharedHole` id states an identity, and that identity is scoped to the one +// lowered construct that minted it. Sharing is the whole point of the marker, so +// over-sharing is its characteristic failure — and it has two shapes, one per +// case here. Both collapse the two key types into a single variable, so both +// surface the same way: not as a wrong key type but as an `Int | String` +// collision that rejects the program outright. +// +// - **Across instantiations of one construct.** A `def` is lowered once, so +// its body carries one id however many times it is called. What keeps the +// instantiations apart is not the marker but ordinary generalization: +// `normalize_annotation` resolves the id to an inference variable minted at +// the current level, and from then on freshening treats it like any other +// quantified variable. The `def` here is the case that would notice if it +// did not — e.g. if the variable were minted at level 0 and so never +// generalized (the level caveat on `InferCtx::shared_holes`). +// - **Across distinct constructs.** The id → variable memo lives on the +// inference context, so every group-by in a program shares one table; ids +// minted per construct must stay distinct within a lowering. +#[rstest] +#[case::polymorphic_def(indoc! {r#" + def by_key(c, f): + groupby(c, f) + ints = by_key([1, 2, 3], \x -> x) + strs = by_key([(a=1, b="w"), (a=2, b="e")], \r -> r.b) + (ints, strs) +"#})] +#[case::two_occurrences(indoc! {r#" + ints = groupby([1, 2, 3], \x -> x) + strs = groupby([(a=1, b="w"), (a=2, b="e")], \r -> r.b) + (ints, strs) +"#})] +fn test_groupby_key_relation_is_per_occurrence(#[case] code: &str) { + assert_eq!(groupby_key_types(code), (int(), string()), "for {code}"); +} + +// The tests above pin what a group-by's key type *resolves to*; this one pins +// that the key type is still **enforced** at a lookup. Stating the relation on +// the `data_fun` annotation makes the edge directional (`key_ty <: ⟨domain⟩` — +// contravariance), and a directional edge is exactly the kind that can go slack +// without any test noticing: every case above would still pass if a lookup at an +// unrelated key type were silently accepted. +// +// Asserted on the rendered message rather than the error *variant*: which check +// catches this is a property of how `==` is typed, not of the key relation, so +// pinning the variant would make the test fail on any change to that — it says +// only that the two types met and were refused. +#[test] +fn test_groupby_lookup_at_wrong_key_type_rejected() { + let errs = infer_program_err(indoc! {r#" + groups = groupby([(a=1, b="w"), (a=2, b="e")], \r -> r.b) + groups(1) + "#}); + assert!( + errs.iter() + .map(|e| format!("{e:?}")) + .any(|msg| msg.contains("Int") && msg.contains("String")), + "expected the Int key to be rejected against the String key type, got {errs:?}" + ); +} + #[test] fn test_groupby_aggregate() { // groups = groupby([1, 2, 3], \x -> x)