Monomorphization: key specializations on instantiation identity, not a resolved type

src/ccl/ccl_utils.rs

@@ -298,7 +298,7 @@ pub fn is_trivially_true_predicate(expr: &Expr) -> bool {
 /// `D ⇒ D` with no refinement wrapper: the refinement would carry no
 /// information, and skipping it keeps program dumps and golden tests
 /// free of `{D | true ▷ const}` noise.  The refinement gets a freshly
-/// built predicate term — safe because witnesses match by structural
+/// built predicate term — safe because refinements match by structural
 /// predicate equality, while walkers key DAG dedup on the [`PredicateId`].
 ///
 /// Op-conversion compiles `Apply(p, Iterate)` to an `IterateExtent` tile
@@ -476,7 +476,7 @@ fn restamp_spine_result(node: &mut Expr, new_result: Type) {
 /// `Fun(Refinement(_, _), _)` — a refinement on a function domain.  Inference
 /// no longer *requires* this (any `target` with `value_ty <: target` is a
 /// well-typed upcast), but it is the only shape lowering produces today and
-/// the one [`crate::ccl::lambda_elim`]'s groupby reconstruction reads a witness
+/// the one [`crate::ccl::lambda_elim`]'s groupby reconstruction reads a refinement
 /// off of, so this asserts the lowering contract: a non-conforming target is
 /// a construction-time bug, not a user error, so it panics rather than
 /// emitting a cast `lambda_elim` would mishandle.  See [`TypedExprNode::Cast`]
@@ -491,14 +491,14 @@ pub fn make_cast(value: Expr, target_ty: Type) -> Expr {
     Expr::cast(value, target_ty)
 }
 
-/// Read the domain refinement off a cast target type — the refinement witness a
+/// Read the domain refinement off a cast target type — the refinement a
 /// [`make_cast`] target carries on its `Fun(Refinement(_, r), _)` shape.
 ///
 /// [`crate::ccl::lambda_elim`]'s cast-wrapped-lambda arm calls this on a
 /// [`TypedExprNode::Cast`]'s `target` to reattach the refinement to the
 /// reconstructed `groupby` lambda.  (Inference does not need it: it types the
 /// cast as the upcast `value_ty <: target` and lets the solver carry the
-/// witness.) The returned `Refinement` shares the predicate's `Rc<Expr>` with
+/// refinement.) The returned `Refinement` shares the predicate's `Rc<Expr>` with
 /// `target`.
 pub fn cast_target_refinement(target: &Type) -> Option<Refinement> {
     let Type::Fun { domain, .. } = target else {

src/ccl/channelize.rs

@@ -1838,14 +1838,14 @@ fn collection_union_type(feeds: &[Expr]) -> Type {
                 match &cod {
                     None => cod = Some((**codomain).clone()),
                     // The channel's element type is the **join** of its
-                    // contributions, so a witness only survives if every one of them
+                    // contributions, so a refinement only survives if every one of them
                     // establishes it: `c << 1` and `c << 2` contribute
                     // `{Int | __elem == 1}` and `{Int | __elem == 2}` and the channel
                     // is a plain `Int`. This is the register law (`emit`'s `MutWrite`
                     // rule) for the append-kind history: a channel is not one value
                     // but the sequence its contributions produce.
                     Some(c) if c != &**codomain => {
-                        cod = Some(join_witnesses(c, codomain));
+                        cod = Some(join_refinements(c, codomain));
                     }
                     // Every `<<` contribution to one channel is constrained into
                     // the channel's shared `value` var at inference, so the
@@ -1880,16 +1880,16 @@ fn collection_union_type(feeds: &[Expr]) -> Type {
 }
 
 /// The join of two types that agree modulo refinements: their shared skeleton
-/// carrying only the witnesses **both** sides establish.
+/// carrying only the refinements **both** sides establish.
 ///
-/// Witnesses are compared structurally, as everywhere else (`Refinement`'s
+/// Refinements are compared structurally, as everywhere else (`Refinement`'s
 /// `PartialEq`), and the skeletons must already agree — the caller's
 /// `debug_assert` states that invariant.
-fn join_witnesses(a: &Type, b: &Type) -> Type {
+fn join_refinements(a: &Type, b: &Type) -> Type {
     let mut layers: Vec<Refinement> = Vec::new();
     let mut cur = a;
     while let Type::Refinement(inner, r) = cur {
-        if type_carries_witness(b, r) {
+        if type_carries_refinement(b, r) {
             layers.push(r.clone());
         }
         cur = inner;
@@ -1901,11 +1901,11 @@ fn join_witnesses(a: &Type, b: &Type) -> Type {
         .fold(cur.clone(), |acc, r| Type::Refinement(Box::new(acc), r))
 }
 
-/// Whether `ty`'s own refinement layers include `witness`.
-fn type_carries_witness(ty: &Type, witness: &Refinement) -> bool {
+/// Whether `ty`'s own refinement layers include `refinement`.
+fn type_carries_refinement(ty: &Type, refinement: &Refinement) -> bool {
     let mut cur = ty;
     while let Type::Refinement(inner, r) = cur {
-        if r == witness {
+        if r == refinement {
             return true;
         }
         cur = inner;

src/ccl/context.rs

@@ -1008,7 +1008,7 @@ pub fn compile_program(
     // graph an adjacency that doesn't chain would otherwise hide. Planning
     // surfaces each iterated / join-satisfying extent on its producer's
     // codomain (`refine_codomain` / `set_codomain`) and the strict checker
-    // matches the fresh refinement witnesses it mints by structural predicate
+    // matches the fresh refinements it mints by structural predicate
     // equality, so the staging shapes now validate without re-blinding the
     // check or peeling cast refinements.
     typecheck(&join_planned).expect("type error after join planning");

src/ccl/design/ir.md

@@ -95,7 +95,7 @@ Lambdas do not survive to the dataflow graph: [lambda elimination](optimization.
 
 Lowering ([`ccl_utils::make_cast`]) emits it for list-comprehension filters, for-loop `if`-guards, and `groupby`. The only `target` shape lowering produces today is `Fun(Refinement(_, 𝑝), _)`: a function type whose domain carries the predicate `𝑝`, so the cast attaches a refinement to a collection function's domain. `target` is the lowering-time *specification* (its domain/codomain are typically `Type::Hole`, carrying only the refinement); the resolved cast type lands on `expr.ty` after inference — the same `user_annotation`-vs-`ty` split used elsewhere.
 
-`Cast` is an **upcast**: its whole typing rule is the single subtype obligation `value_ty <: target`. For the domain refinement lowering emits, that holds by contravariance — `(𝐷 ⇒ 𝑉) <: ({𝐷 | 𝑝} ⇒ 𝑉)` because `{𝐷 | 𝑝} <: 𝐷` — so viewing an unrefined-domain collection function at a refined-domain type is sound. A *covariant* refinement (casting `Int` to `{Int | 𝑝}`) correctly *fails* the check — acquiring a value-level refinement is a runtime/SMT-checked narrowing, not an upcast. How the solver discharges the refinement obligation — flowing the demanded witness onto the target-domain variable and stacking it so chained casts compose — is covered in [type-inference.md](type-inference.md#45-dependent-refinements-via-pi-types).
+`Cast` is an **upcast**: its whole typing rule is the single subtype obligation `value_ty <: target`. For the domain refinement lowering emits, that holds by contravariance — `(𝐷 ⇒ 𝑉) <: ({𝐷 | 𝑝} ⇒ 𝑉)` because `{𝐷 | 𝑝} <: 𝐷` — so viewing an unrefined-domain collection function at a refined-domain type is sound. A *covariant* refinement (casting `Int` to `{Int | 𝑝}`) correctly *fails* the check — acquiring a value-level refinement is a runtime/SMT-checked narrowing, not an upcast. How the solver discharges the refinement obligation — flowing the demanded refinement onto the target-domain variable and stacking it so chained casts compose — is covered in [type-inference.md](type-inference.md#45-dependent-refinements-via-pi-types).
 
 `lambda_elim`, planning, and operator conversion carry the domain refinement through to a runtime `Restrict`: a `Cast` around a group-by lambda becomes a **Pi-const** form whose refinement planning's pointful group-by recognizer reads off the predicate, while a `Cast` wrapping point-free filter/guard code survives lambda elimination unchanged and is consumed as a domain refinement at planning — see [optimization.md](optimization.md). The current `Cast` only honours domain-refinement targets; the direction for a general `𝑈 ⇒ 𝑇` cast is in [type-inference.md](type-inference.md#6-future-work).