Freshening asks a different question than type_level, so it needs its own

src/ccl/infer/solver/scheme.rs

@@ -13,8 +13,6 @@ use crate::ccl::subst::Subst;
 use crate::ccl::ty::{FunKind, FunKindVar, FunKindVarId};
 use crate::ccl::{Bound, InferVar, InferVarId, Level, Refinement, Type, TypedExpr};
 
-use super::type_level;
-
 // ---------------------------------------------------------------------------
 // Polymorphic schemes
 // ---------------------------------------------------------------------------
@@ -165,21 +163,67 @@ fn freshen_kind_var(kv: &Rc<FunKindVar>, cache: &mut FreshenCache) -> Rc<FunKind
     f
 }
 
+/// The highest level of any inference variable **reachable** in `ty` — including
+/// the ones inside refinement predicates' own type slots.
+///
+/// This is deliberately *not* [`type_level`], and the difference is the whole
+/// point. The two answer different questions:
+///
+/// * [`type_level`] asks "does this participate in the lattice above `lim`?", for
+///   extrusion, bound-recording scope, and let-generalization. A refinement is
+///   lattice-blind, so it defers to its base and the predicate is correctly
+///   invisible; a `ChanDom` reports 0 so a rigid atom flows through bounds
+///   unchanged. Both are load-bearing there.
+/// * Freshening asks "does this contain a variable I must **copy**?" A predicate
+///   carries real type slots holding real quantified variables, so for *this*
+///   question they count.
+///
+/// Sharing one function between the two is what let an unfreshened predicate into
+/// a specialization clone: `type_level` reports the base's level for a nested
+/// refinement, so a type whose only above-`lim` content lives in a predicate
+/// short-circuits and is returned verbatim — still pointing at the definition's
+/// live inference variables, which `src/ccl/design/type-inference.md`
+/// ("3.1 Let-Polymorphism is Freshening (Instantiation)") states it must not.
+/// The symptom is a duplicate specialization: the clone reaches the same
+/// generalized `let` twice, once through freshened variables and once through
+/// the definition's own.
+fn freshen_level(ty: &Type) -> Level {
+    fn predicate_level(expr: &TypedExpr) -> Level {
+        let mut lvl = 0;
+        expr.walk_type_slots(|t| lvl = lvl.max(freshen_level(t)));
+        expr.walk_children(|c| lvl = lvl.max(predicate_level(c)));
+        lvl
+    }
+    // One walk, not `type_level` plus a second descent: `walk_children` already
+    // reaches every structural position, so the only thing to add is the
+    // predicate it documents itself as skipping. `ChanDom` needs no arm — it has
+    // no children and is not an `Infer`, so it contributes 0, which is the same
+    // answer `type_level` gives it and for the same reason.
+    let mut lvl = match ty {
+        Type::Infer(v) => v.level,
+        _ => 0,
+    };
+    if let Type::Refinement(_, r) = ty {
+        lvl = lvl.max(predicate_level(&r.predicate));
+    }
+    ty.walk_children(|c| lvl = lvl.max(freshen_level(c)));
+    lvl
+}
+
 pub fn freshen_above(
     lim: Level,
     ty: &Type,
     target: FreshenLevel,
     cache: &mut FreshenCache,
 ) -> Type {
-    // A `Refinement`'s `type_level` reflects only its base, but its predicate
-    // term carries its own type slots (which may hold quantified variables a
-    // low base hides). So never short-circuit a refinement on `type_level`;
-    // descend and freshen the predicate slots too (each leaf slot still
-    // short-circuits on its own level). A `ChanDom` is likewise exempt: it
-    // deliberately reports `type_level` 0 (its level must not trigger
-    // extrusion — see `type_level`), so its quantification is decided by the
-    // arm below from its *stored* introduction level.
-    if !matches!(ty, Type::Refinement(..) | Type::ChanDom(..)) && type_level(ty) <= lim {
+    // The short-circuit asks [`freshen_level`], not `type_level`: a refinement's
+    // predicate holds type slots whose quantified variables a low base hides, and
+    // freshening has to copy them (see [`freshen_level`] for why the two levels
+    // are different questions). A `ChanDom` is exempt outright: it deliberately
+    // reports level 0 (its level must not trigger extrusion — see `type_level`),
+    // so its quantification is decided by the arm below from its *stored*
+    // introduction level.
+    if !matches!(ty, Type::ChanDom(..)) && freshen_level(ty) <= lim {
         return ty.clone();
     }
     match ty {
@@ -544,6 +588,7 @@ fn freshen_subst_payloads(
 
 #[cfg(test)]
 mod tests {
+    use super::super::type_level;
     use super::*;
     use crate::ccl::ty::{FunKind, FunKindVar};
     use crate::ccl::{BaseType, InferVar};
@@ -589,6 +634,64 @@ mod tests {
         );
     }
 
+    /// A quantified variable reachable *only* through a refinement predicate must
+    /// still be freshened.
+    ///
+    /// The shape is the one a comprehension produces: a `Fun` whose every
+    /// structural position is ground (`[0,2] ⇒ Int`), carrying a refinement whose
+    /// base is also ground — so `type_level` reports 0 for the whole thing — while
+    /// the predicate holds a level-5 variable. Short-circuiting on `type_level`
+    /// returns the type verbatim and the clone keeps pointing at the definition's
+    /// live variable, which shows up downstream as a *duplicate* specialization:
+    /// the clone reaches one generalized `let` through both the freshened variable
+    /// and the original.
+    ///
+    /// Guarding a top-level `Refinement` is not enough — one level of nesting is
+    /// what the real shape has, and what this pins.
+    #[test]
+    fn a_variable_reachable_only_through_a_predicate_is_freshened() {
+        let quantified = InferVar::fresh(5);
+        // A predicate term whose *type slot* holds the quantified variable.
+        let predicate = Rc::new(
+            TypedExpr::lit(crate::ccl::Lit::Bool(true))
+                .with_ty(Type::Infer(Rc::clone(&quantified))),
+        );
+        let refined_domain = Type::Refinement(
+            Box::new(Type::UIntRange(3)), // ground base: hides the predicate's level
+            Refinement::sharing(&predicate),
+        );
+        let ty = Type::Fun {
+            name: None,
+            kind: FunKind::Compute,
+            domain: Box::new(refined_domain),
+            codomain: Box::new(Type::Base(BaseType::Int)),
+        };
+        assert_eq!(
+            type_level(&ty),
+            0,
+            "precondition: `type_level` cannot see the predicate's variable"
+        );
+
+        let mut cache = FreshenCache::new();
+        let fresh = freshen_above(0, &ty, FreshenLevel::At(1), &mut cache);
+
+        let Type::Fun { domain, .. } = &fresh else {
+            panic!("expected a function type");
+        };
+        let Type::Refinement(_, r) = &**domain else {
+            panic!("expected the refinement to survive freshening");
+        };
+        let Type::Infer(v) = &r.predicate.ty else {
+            panic!("expected the predicate's type slot to stay a variable");
+        };
+        assert_ne!(
+            v.uid, quantified.uid,
+            "a quantified variable reachable only through a predicate must be \
+             freshened — sharing it with the definition mints a duplicate \
+             specialization"
+        );
+    }
+
     #[test]
     fn freshening_mirrors_kind_var_links_onto_instantiation() {
         // Two `<:`-linked kind vars in one scheme must stay linked after