SharedHole: let lowering state that two type positions are the same

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(..)

src/ccl/infer/api.rs

@@ -830,7 +830,10 @@ fn collect_type_errors(
     seen_refinements: &mut HashSet<crate::ccl::PredicateId>,
 ) {
     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) => {

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<HashMap<u32, Type>>,
 }
 
 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).

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(()),
     }
 }

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(_) => {}
     }
 }

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,

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,

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,
     }
 }
 

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

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

src/ccl/lower/exprs.rs

@@ -71,14 +71,28 @@ 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.
             let bare_pred = Expr::binop(
                 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 {

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<String>,
+
+    /// 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,

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,

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(..)