Type functions: state a relationship between type variables other than subtyping

src/ccl/ccl_utils.rs

@@ -560,9 +560,17 @@ pub(crate) fn strip_refinements(ty: &Type) -> Type {
             domain: Box::new(strip_refinements(domain)),
             kind: *kind,
         },
+        // Strip *inside* the arguments — a structural rewrite, not a reduction.
+        // Every operator's reduction already drops value-level claims, so this is
+        // belt-and-braces rather than the mechanism.
+        Type::App { fun, args } => Type::App {
+            fun: fun.clone(),
+            args: args.iter().map(strip_refinements).collect(),
+        },
         Type::Base(_)
         | Type::UIntRange(_)
         | Type::Hole
+        | Type::SharedHole(_)
         | Type::Infer(_)
         | Type::DataSource(_)
         | Type::ChanDom(..)

src/ccl/infer/api.rs

@@ -122,7 +122,7 @@ impl Drop for InferArena {
         // Take back every variable minted during the run and sever its bound
         // edges, so the (otherwise cyclic) refcounts can all reach zero.
         for var in crate::ccl::arena_exit() {
-            let mut bounds = var.bounds.borrow_mut();
+            let mut bounds = var.bounds_mut();
             bounds.lower.clear();
             bounds.upper.clear();
         }
@@ -337,6 +337,52 @@ pub enum InferError {
         /// Display label for the message (see the type docs — not the location).
         at: String,
     },
+    /// A type function's operands have no base in common — `1 + "a"`.
+    ///
+    /// Distinct from [`InferError::IncompatibleBounds`], and the distinction is the
+    /// reason this is its own variant rather than that one reused. There, a
+    /// *variable* collected two bounds that cannot meet, and the rejection is about
+    /// what inference declines to invent (an untagged sum). Here each operand is
+    /// perfectly well typed and nothing was inferred badly — the operator simply has
+    /// no rule relating an `Int` to a `String`, which is a statement about the
+    /// operator.
+    NoCommonBase {
+        /// The type function, as it is spelled in a type (`Add`, `Greater`).
+        fun: String,
+        /// The operand bases, rendered, in argument order.
+        bases: Vec<String>,
+        /// Display label for the message (see the type docs — not the location).
+        at: String,
+    },
+    /// The operands agree on a base the operation is not defined for — `"a" * "b"`.
+    ///
+    /// The dual of [`NoCommonBase`](InferError::NoCommonBase): there the operands
+    /// disagree, here they agree and the *operator* is what has nothing to say.
+    UndefinedForBase {
+        /// The type function, as it is spelled in a type (`Mul`, `Sub`).
+        fun: String,
+        /// The offending base, rendered.
+        base: String,
+        /// Display label for the message (see the type docs — not the location).
+        at: String,
+    },
+    /// A [`Type::App`] survived inference without reducing — the strict wall's
+    /// guard on a transient type, like the [`Type::History`](crate::ccl::Type) and
+    /// [`Type::ChanDom`](crate::ccl::Type) checks beside it rather than a diagnosis
+    /// a program earns.
+    ///
+    /// Materialization always either reduces an operator or poisons the position it
+    /// sits at (`compact_go`'s `Compute` arm), and every stamped type is
+    /// materialized, so nothing should reach here. An operator whose arguments the
+    /// program never determined does *not*: it reduces to the unresolved position
+    /// itself and is reported as [`InferError::UnresolvedInfer`], which is the
+    /// honest description — the arguments are undetermined, not the rule.
+    UnreducedApp {
+        /// Display string of the unreduced type-function application.
+        ty: String,
+        /// Display label for the message (see the type docs — not the location).
+        at: String,
+    },
     /// A partial tuple or partial record was not resolved to a concrete type.
     UnresolvedPartial {
         /// Display string of the partial type.
@@ -572,6 +618,23 @@ impl std::fmt::Debug for InferError {
             InferError::UnresolvedInfer { id, at } => {
                 write!(f, "Unresolved inference variable {id} in expression: {at}")
             }
+            InferError::NoCommonBase { fun, bases, at } => {
+                write!(
+                    f,
+                    "Operands of {fun} have no base in common: {} in expression: {at}",
+                    bases.join(" vs ")
+                )
+            }
+            InferError::UndefinedForBase { fun, base, at } => {
+                write!(f, "{fun} is not defined on {base} in expression: {at}")
+            }
+            InferError::UnreducedApp { ty, at } => {
+                write!(
+                    f,
+                    "Type function {ty} never reduced in expression: {at} \
+                     (a compiler bug — materialization reduces or rejects)"
+                )
+            }
             InferError::UnresolvedPartial { kind, at } => {
                 write!(f, "Unresolved partial {kind} in expression: {at}")
             }
@@ -832,7 +895,17 @@ 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(),
+        }),
+        // A type function that never reduced. Reported like an unresolved
+        // variable — it is the same failure (the program did not determine
+        // enough), one level up: the arguments are missing rather than the type.
+        Type::App { .. } => errors.push(InferError::UnreducedApp {
+            ty: ty.to_string(),
             at: context_sym.to_string(),
         }),
         Type::Infer(var) => {
@@ -2983,6 +3056,33 @@ mod tests {
         );
     }
 
+    /// Corrupting an operator's result type is caught by `typecheck`, for both
+    /// operators whose result is a [`Type::App`].
+    ///
+    /// The wall sees through the operator only because Check *resolves* a
+    /// rule-derived variable before reconciling it: the rule hands back a fresh
+    /// variable whose lower bound is `Add(α, β)` / `Less(α, β)`, and an unreduced
+    /// operator is opaque to `constrain_subtype`, so without the resolve the
+    /// bound-closure walk stops there and the corruption goes unnoticed.
+    #[test]
+    fn test_typecheck_operator_wrong_result_type() {
+        for (op, corrupted) in [
+            (BinOpKind::Arithmetic(ArithmeticKind::Add), BaseType::String),
+            (BinOpKind::Compare(CompareKind::Less), BaseType::Int),
+        ] {
+            let mut ctx = TypeInferenceContext::new();
+            let mut expr = Expr::binop(Expr::lit(Lit::Int(1)), op, Expr::lit(Lit::Int(2)));
+            infer(&mut expr, &mut ctx).unwrap();
+            expr.ty = Type::Base(corrupted.clone());
+            let errs = typecheck(&expr).expect_err("a wrong result type must be caught for {op:?}");
+            assert!(
+                errs.iter()
+                    .any(|e| matches!(e, InferError::TypeMismatch { .. })),
+                "expected a TypeMismatch for {op:?}, got {errs:?}"
+            );
+        }
+    }
+
     /// Corrupting a `Compare` result type away from `Bool` is caught by `typecheck`.
     #[test]
     fn test_typecheck_compare_wrong_result_type() {

src/ccl/infer/check.rs

@@ -16,6 +16,7 @@ use super::emit::{
     emit_variant_ctor,
 };
 use super::schemes::OperatorSchemes;
+use super::solve::resolve_var_type;
 use super::typing::{Typing, peel_refinements_outer};
 use super::{lit_base, map_constrain_err};
 
@@ -425,6 +426,23 @@ fn check_node_rule(expr: &mut Expr, ctx: &mut CheckCtx) -> Result<Type, LocatedI
     // case — eliminators that destructure return the function's own codomain,
     // constructors rebuild the same product), the subtype check is reflexive
     // and trivially holds, so skip the (deeper, allocating) `constrain_subtype`.
+    // A rule that applies an operator scheme hands back a fresh variable whose only
+    // content is the scheme's result, so comparing it directly to the recorded type
+    // records an upper bound and discovers a disagreement only if the bound-closure
+    // reaches one — and a `Type::App` on the variable's lower bounds stops that
+    // walk, since an unreduced application is opaque to the solver. Resolving first is
+    // what makes the operator reduce, which is the whole reason its result *is* an
+    // operator (see `OperatorSchemes`, "An operand requirement must be reachable
+    // from the result type"). Without this the wall cannot see a wrong `1 + 2 :
+    // String` or `1 < 2 : Int` at all.
+    //
+    // Narrow on purpose: only a rule-derived type that is still a bare variable is
+    // resolved. Every other rule rebuilds a ground type from its children, where
+    // resolution is the identity and the comparison already has everything.
+    let ty = match &ty {
+        Type::Infer(_) => resolve_var_type(&ty).unwrap_or(ty),
+        _ => ty,
+    };
     if ty != expr.ty {
         // Refinements included: this is the plain strict relation, like every other
         // check here. A rule that rebuilds a node's type from its children rebuilds