Traits: state what an operator requires of its operands, not that they are the same

src/ccl/infer/api.rs

@@ -105,6 +105,11 @@ impl InferArena {
     /// [`crate::ccl::arena_enter`]).
     pub fn new() -> Self {
         crate::ccl::arena_enter();
+        // The trait-narrowing audit trail is per-run, exactly as the variable
+        // capture is: checking one run's obligations against another's graph would
+        // resolve variables that no longer have bounds.
+        #[cfg(debug_assertions)]
+        crate::ccl::infer::solver::traits::clear_watch_log();
         InferArena {
             _not_send_sync: std::marker::PhantomData,
         }
@@ -123,6 +128,10 @@ impl Drop for InferArena {
         // edges, so the (otherwise cyclic) refcounts can all reach zero.
         for var in crate::ccl::arena_exit() {
             var.bounds.borrow_mut().clear();
+            // A trait obligation holds its output `Type`, which holds a variable,
+            // which watches the obligation — a cycle of exactly the kind the bound
+            // lists make, and severed the same way.
+            var.watches.borrow_mut().clear();
         }
     }
 }
@@ -335,6 +344,29 @@ pub enum InferError {
         /// Display label for the message (see the type docs — not the location).
         at: String,
     },
+    /// An operator was used at operand types no instance of its trait
+    /// accepts — `1 > "a"`, `"a" - "b"`, or a polymorphic function applied at a type
+    /// its body's operators cannot handle.
+    ///
+    /// Distinct from [`InferError::TypeMismatch`] on purpose: the two operands did
+    /// not fail to *relate*, and neither is wrong on its own. What failed is the
+    /// operator's requirement about the pair, so the message names the trait and
+    /// what the position could have accepted rather than showing two types that
+    /// "don't match".
+    NoTraitInstance {
+        /// The trait with no instance left, e.g. `Addable`.
+        trait_: String,
+        /// The operand position (0-based) whose type ruled the last one out.
+        position: u8,
+        /// The base type found there. Boxed for the same reason
+        /// [`InferError::TypeMismatch`]'s types are — to keep `Result` small.
+        found: Box<Type>,
+        /// What that position could still have accepted, given what was already
+        /// known about the other operand.
+        accepted: Vec<Type>,
+        /// 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.
@@ -520,6 +552,25 @@ impl std::fmt::Debug for InferError {
                 }
                 Ok(())
             }
+            InferError::NoTraitInstance {
+                trait_,
+                position,
+                found,
+                accepted,
+                at,
+            } => {
+                let accepted = accepted
+                    .iter()
+                    .map(|t| t.to_string())
+                    .collect::<Vec<_>>()
+                    .join(" or ");
+                write!(
+                    f,
+                    "No {trait_} instance for {at}: operand {} is {found}, but \
+                     the only type accepted there is {accepted}",
+                    position + 1,
+                )
+            }
             InferError::MissingField { key, found, at } => match (key, found) {
                 // A tuple's positions are its width, so that is the fact to state: the
                 // projection asked for a position past the end.
@@ -1979,23 +2030,28 @@ mod tests {
     #[test]
     fn test_collect_multi_conflict() {
         // λ x → Apply(λ a:Int → a, Var(x)) + Apply(λ b:String → b, Var(x))
-        // `x` is the argument to both an Int-domain and a String-domain function.
-        // The sound one-way `arg <: domain` rule records `x <: Int` and
-        // `x <: String` — two upper bounds, with no eager cross-constraint — so
-        // the conflict surfaces structurally at coalesce when the bounds collide
-        // (`IncompatibleBounds`, an untagged-sum rejection) rather than as an
-        // eager `TypeMismatch` from the (retired) reverse `domain <: arg`. Both
-        // correctly reject the program.
+        // `x` is the argument to both an Int-domain and a String-domain function,
+        // whose results are then added.
+        //
+        // The rejection comes from the `+`, and names the actual problem: no
+        // `Addable` instance takes an `Int` and a `String`. It arrives during
+        // emission, as soon as both operand types are known — the operator states a
+        // requirement about the *pair*, so it need not wait for the two to collide on
+        // a shared variable at coalesce.
+        //
+        // The one-way `arg <: domain` rule that puts them there is what the
+        // `IncompatibleBounds` tests in `tests/type_check.rs` cover, joining two types
+        // without an operator in the way.
         let mut expr = double_apply_lambda(Type::Base(BaseType::Int), Type::Base(BaseType::String));
         let mut ctx = TypeInferenceContext::new();
         let errs = infer_bare(&mut expr, &mut ctx).expect_err("expected an Int/String conflict");
         assert!(
             errs.iter().any(|e| matches!(
                 e,
-                InferError::IncompatibleBounds { conflicting, .. }
-                    if conflicting.contains("Int") && conflicting.contains("String")
+                InferError::NoTraitInstance { trait_, found, .. }
+                    if trait_ == "Addable" && **found == Type::Base(BaseType::String)
             )),
-            "expected IncompatibleBounds Int/String, got {errs:?}"
+            "expected NoTraitInstance for Addable at a String operand, got {errs:?}"
         );
     }
 
@@ -2555,20 +2611,20 @@ mod tests {
     fn test_unary_neg_wrong_type() {
         let mut ctx = TypeInferenceContext::new();
         use crate::ccl::UnaryOpKind;
-        // -true → TypeMismatch(Bool, Int).
+        // `-true`: negation states `Negatable`, so the rejection names the trait and
+        // the type it will not accept rather than reporting a mismatch against a
+        // hardcoded `Int` domain.
         let mut expr = Expr::unary(UnaryOpKind::Neg, Expr::lit(Lit::Bool(true)));
-        let errs = infer_bare(&mut expr, &mut ctx)
-            .expect_err("expected TypeMismatch Bool/Int under inference");
+        let errs = infer_bare(&mut expr, &mut ctx).expect_err("Bool is not negatable");
         assert!(
             errs.iter().any(|e| matches!(
                 e,
-                InferError::TypeMismatch { type_a, type_b, .. }
-                    if matches!(
-                        (type_a.as_ref(), type_b.as_ref()),
-                        (Type::Base(BaseType::Bool), Type::Base(BaseType::Int))
-                    )
+                InferError::NoTraitInstance { trait_, position, found, .. }
+                    if trait_ == "Negatable"
+                        && *position == 0
+                        && **found == Type::Base(BaseType::Bool)
             )),
-            "expected TypeMismatch Bool/Int, got {errs:?}"
+            "expected NoTraitInstance for Negatable at a Bool operand, got {errs:?}"
         );
     }
 

src/ccl/infer/check.rs

@@ -18,6 +18,7 @@ use super::emit::{
 use super::schemes::OperatorSchemes;
 use super::typing::{Typing, peel_refinements_outer};
 use super::{lit_base, map_constrain_err};
+use crate::ccl::infer::solver::traits::{Assoc, Trait, offered_base};
 
 /// Post-inference structural type-check state.
 ///
@@ -113,6 +114,75 @@ impl Typing for CheckCtx {
         ann.clone()
     }
 
+    fn require_trait(
+        &mut self,
+        trait_: Trait,
+        operands: &[&Type],
+        assoc: Option<Assoc>,
+        at: &dyn Fn() -> String,
+    ) -> Result<Option<Type>, LocatedInferError> {
+        // No obligation is created here, for two independent reasons. Types are
+        // already concrete, so there is nothing to discharge incrementally; and Check
+        // runs outside any `InferArena`, so an obligation's variable⇄obligation cycle
+        // would never be broken.
+        //
+        // What this rule is *for* is supplying the node's type so the reconcile below
+        // has something to compare against — the common path, taken 3,812 times across
+        // the pipeline suite.
+        //
+        // The rejection branch is not a user-error backstop. Catching user type errors
+        // is entirely inference's job; Check exists to catch **compiler bugs that
+        // corrupt types**, which is why a Check error that is not `UnresolvedInfer`
+        // panics at the wall rather than being reported. So this firing means
+        // inference has a hole or a later pass rewrote the tree into something
+        // ill-typed — and it reuses `NoTraitInstance` for the same reason
+        // [`Typing::require_sub`] reuses `TypeMismatch` here: the error vocabulary
+        // describes the inconsistency, the wall supplies the interpretation. Measured
+        // across the suite: it never fires.
+        let bases: Option<Vec<&BaseType>> = operands.iter().map(|t| offered_base(t)).collect();
+        let Some(bases) = bases else {
+            // Pre-desugar residue (a `Feed` handle, an un-eliminated `Mut`, a
+            // still-`Infer` position under `Strictness::PreDesugar`) is not something
+            // this rule can judge — the strictness wall decides whether a residual
+            // type is tolerable at this point in the pipeline.
+            return Ok(assoc.map(|_| self.fresh()));
+        };
+        let matched = trait_
+            .instances()
+            .iter()
+            .find(|i| i.args.len() == bases.len() && i.args.iter().eq(bases.iter().copied()));
+        match matched {
+            Some(matched) => Ok(assoc.map(|name| {
+                matched
+                    .assoc_ty(name)
+                    .map(|b| Type::Base(b.clone()))
+                    .unwrap_or_else(|| fresh_var(self.level))
+            })),
+            None => {
+                // Blame the last position: with the earlier ones fixed, it is the one
+                // whose type ruled the instance out.
+                let position = bases.len().saturating_sub(1);
+                let prefix: Vec<BaseType> =
+                    bases[..position].iter().map(|b| (*b).clone()).collect();
+                let accepted: Vec<Type> = trait_
+                    .instances()
+                    .iter()
+                    .filter(|i| i.args.len() == bases.len() && i.args[..position] == prefix[..])
+                    .filter_map(|i| i.args.get(position).cloned().map(Type::Base))
+                    .collect();
+                let located = self.raise(InferError::NoTraitInstance {
+                    trait_: trait_.to_string(),
+                    position: position as u8,
+                    found: Box::new(Type::Base(bases[position].clone())),
+                    accepted,
+                    at: at(),
+                });
+                self.errors.push(located);
+                Ok(assoc.map(|_| fresh_var(self.level)))
+            }
+        }
+    }
+
     fn require_sub(
         &mut self,
         sub: &Type,
@@ -345,18 +415,18 @@ fn check_node_rule(expr: &mut Expr, ctx: &mut CheckCtx) -> Result<Type, LocatedI
         TypedExprNode::Apply { function, argument } => emit_apply(function, argument, ctx)?,
 
         TypedExprNode::BinOp { left, op, right } => {
-            let scheme = ctx.schemes.binop(*op).clone();
-            emit_binop(left, right, &scheme, ctx)?
+            let sig = ctx.schemes.binop(*op);
+            emit_binop(left, right, &sig, ctx)?
         }
 
         TypedExprNode::UnaryOp(op, inner) => {
-            let scheme = ctx.schemes.unary(*op).clone();
-            emit_unary(inner, &scheme, ctx)?
+            let sig = ctx.schemes.unary(*op);
+            emit_unary(inner, &sig, ctx)?
         }
 
         TypedExprNode::Aggregate { input, kind } => {
             let scheme = ctx.schemes.aggregate(*kind).clone();
-            emit_aggregate(input, &scheme, ctx)?
+            emit_aggregate(input, &scheme, *kind, ctx)?
         }
 
         // Check never generalizes (`is_generalizable` is `false`), so every

src/ccl/infer/context.rs

@@ -20,6 +20,7 @@ use super::emit::emit_node;
 use super::schemes::OperatorSchemes;
 use super::typing::Typing;
 use super::{coalesce_for_error, map_constrain_err};
+use crate::ccl::infer::solver::traits::{Assoc, Trait, TraitObligation};
 
 /// A lexical-scope entry: the binder's polymorphic scheme.
 ///
@@ -275,6 +276,41 @@ impl Typing for InferCtx {
         self.normalize_annotation(ann)
     }
 
+    fn require_trait(
+        &mut self,
+        trait_: Trait,
+        operands: &[&Type],
+        assoc: Option<Assoc>,
+        at: &dyn Fn() -> String,
+    ) -> Result<Option<Type>, LocatedInferError> {
+        debug_assert_eq!(
+            operands.len(),
+            trait_.arity(),
+            "{trait_} is over {} type(s); an operator wired to it must supply that many",
+            trait_.arity(),
+        );
+        let positions: Vec<Type> = operands.iter().map(|_| self.fresh()).collect();
+        // Only a requested association gets a variable for the obligation to settle;
+        // a pure requirement determines nothing and mints none.
+        let wanted = assoc.map(|name| (name, self.fresh()));
+        let obligation = TraitObligation::new(trait_, wanted.clone().into_iter().collect());
+        for (i, position) in positions.iter().enumerate() {
+            obligation.watch(position, i as u8);
+        }
+        // A trait whose instances already agree settles here, before any
+        // operand is known — the ordinary "all candidates agree" rule reaching its
+        // condition immediately, not a special case.
+        obligation
+            .try_deposit(&mut self.cache)
+            .map_err(|e| self.raise(map_constrain_err(e, &at())))?;
+        // Operands flow in as ordinary lower bounds, refinements and all. The
+        // narrowing hook peels them where the base actually arrives.
+        for (operand, position) in operands.iter().zip(&positions) {
+            self.require_sub(operand, position, at)?;
+        }
+        Ok(wanted.map(|(_, ty)| ty))
+    }
+
     fn require_sub(
         &mut self,
         sub: &Type,