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

[dpmills]

A polymorphic operator's requirement cannot be stated as a signature. The only relation a signature can put between two operands is that they share a variable, which also forces every other lattice dimension to agree — so one operand's refinement became a requirement on the other, and a refinement both operands carried survived onto a value the operator computed rather than selected. Arithmetic, comparison and negation now state a trait instead: unrelated inference variables per operand, plus an obligation recorded beside the graph. Because an operator's result is an ordinary variable rather than a marker standing for a computation, information still flows backwards through it — so a function typechecks without its call sites, and (1 + 2) and True is an ordinary bound conflict. The refinement strip in apply_binary_scheme goes away rather than being fixed: a syntactic peel does nothing for an operand still holding a Type::Infer.

src/ccl/infer/solver/traits.rs opens with the vocabulary; type-inference.md carries the design. One term to fix here, because it reads two ways: an obligation is a single claim with two halves, and neither alone is "the obligation" — the operands are types some implementation accepts, and each associated position is what that implementation associates.

Traits associate types; they are not functions

A trait names associated types (Rust's term) rather than having an output, and a type is associated only when it depends on the types satisfying the trait. Three shapes result — unary with an Output (Negatable), binary with one (Addable), binary with none (Equatable/Orderable) — each exercised by ordinary programs (each_trait_shape_types_a_real_program).

What an obligation determines

A candidate set shrinks as base types arrive, and an associated type is deposited once every survivor agrees on it — onto associated positions only, since the obligation is their sole source of information while an operand always has the program's own left <: A edge. How much is determined is therefore a property of the table, and shrinks as it grows including for an associated type: \x -> x + 1 has result Int only because Int in the second position leaves one row, and Addable(Float, Int) ⇝ Float would open the result just as the parameter already is. Hence agreement, not uniqueness, as the deposit condition.

Each variant's doc states its shape — how many types it is over, and what it associates — and Trait::arity/assocs read that shape off the table so the prose cannot drift from the rows (every_trait_has_a_consistent_shape).

Delivery

One invariant carries the mechanism — a concrete type reaching an operand variable must reach the obligation watching it — and the bound closure does not provide it. A variable's lower bounds are written in four places, delivery is wired into each, and all four are load-bearing: deleting one fails exactly its own case in a_concrete_operand_reaches_its_obligation. The design doc argues it; verify_narrowing_is_complete checks it on every program rather than trusting it.

Consequences

test_lambda_unapplied asserts an open parameter with the codomain per case; test_collect_multi_conflict and test_unary_neg_wrong_type see NoTraitImpl naming the trait instead of a mismatch against a hardcoded domain. a_register_that_reads_itself_still_gets_a_type ports #51's recurrence cases, which pin something stronger here: narrowing consumes bounds as they are recorded rather than resolved types, so an obligation never enters the recurrence — the base it needs sits on the register's seed.

max's comparability tripwire flips, closing type-checker-traits-comparability. Comparable(γ) on its codomain is the fourth shape — unary, associating nothing, since the scheme already returns an element of what it consumes.

[dpmills]

This change is part of the following stack:

• Freshening asks a different question than type_level, so it needs its own #71
  • SharedHole: let lowering state that two type positions are the same #72
    • Traits: state what an operator requires of its operands, not that they are the same #73 ◀
      • Restrict opposite-polarity fallback to only undetermined positions #87
      • Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
        • Annotations stop standing in for binder structure, and stop outliving inference #60
          • Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63
            • A mutable variable read is an explicit operation, not a subtyping rule #64
              • Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it #62
                • constrain_go asserts the uniquely-keyed invariant it rests on #74
                  • Update the value-Case fan-out's prose to the DisjointJoin it builds #75
                  • Canonicalize each arrow's Pi binder as the solver flattens types #76
                  • Hold a refined type's refinements in one unordered set instead of nested layers #77
                  • Derive a Cast's refinements from its term instead of overwriting the target #78
                  • Add a Lean model of the CCL type system and fuzz the solver against it #79
              • Split transactional commit stores by connected components of transaction blocks #91
                • Build the await_final terminal read as a completion-point sample, and give the as-of read its own term #92
                  • Feed both writers' decision bodies through tiles, retiring WriterBuffer #93
                  • Add an end-to-end walkthrough of mutability, from CHL source to operators #97

_{Change managed by git-spice.}

[sortalongo]

Review in progress. Stopped at ## Discharge is incremental for now