Coinduction for Free: The Three-Value Lattice That Makes rustc's Trait Solver Terminate

TL;DR: Trait solving can loop: impl Trait for T where proving T: Trait requires proving T: Trait. rustc’s next-generation solver handles this with coinduction — assume success, then iterate until the answer stops changing. The interesting part is the small lattice that classifies a cycle, and the fact that the cycle’s kind is recomputed from scratch on every stack push instead of being cached.

The cycle

The classic cycle in trait solving:

rust
trait Foo {}
impl<T: Foo> Foo for T {}   // needs `T: Foo` to prove `T: Foo`

When the solver is asked “does T: Foo hold?”, it picks the impl, which requires T: Foo — the same question. A naive solver detects the cycle and gives up (“overflow”). A coinductive solver assumes the answer is “yes”, finishes the current derivation, and then checks whether the assumption holds.

The lattice

rust
// compiler/rustc_type_ir/src/search_graph/mod.rs:115-158

/// In the initial iteration of a cycle, we do not yet have a provisional
/// result. In the case we return an initial provisional result depending
/// on the kind of cycle.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum PathKind {
    /// A path consisting of only inductive/unproductive steps. Their initial
    /// provisional result is `Err(NoSolution)`. We currently treat them as
    /// `PathKind::Unknown` during coherence until we're fully confident in
    /// our approach.
    Inductive,
    /// A path which is not be coinductive right now but we may want
    /// to change of them to be so in the future. We return an ambiguous
    /// result in this case to prevent people from relying on this.
    Unknown,
    /// A path with at least one coinductive step. Such cycles hold.
    Coinductive,
    /// A path which is treated as ambiguous. Once a path has this path kind
    /// any other segment does not change its kind.
    ///
    /// This is currently only used when fuzzing to support negative reasoning.
    /// For more details, see #143054.
    ForcedAmbiguity,
}

impl PathKind {
    /// Returns the path kind when merging `self` with `rest`.
    ///
    /// Given an inductive path `self` and a coinductive path `rest`,
    /// the path `self -> rest` would be coinductive.
    ///
    /// This operation represents an ordering and would be equivalent
    /// to `max(self, rest)`.
    fn extend(self, rest: PathKind) -> PathKind {
        match (self, rest) {
            (PathKind::ForcedAmbiguity, _) | (_, PathKind::ForcedAmbiguity) => {
                PathKind::ForcedAmbiguity
            }
            (PathKind::Coinductive, _) | (_, PathKind::Coinductive) => PathKind::Coinductive,
            (PathKind::Unknown, _) | (_, PathKind::Unknown) => PathKind::Unknown,
            (PathKind::Inductive, PathKind::Inductive) => PathKind::Inductive,
        }
    }
}

Four values, not three — the fourth, ForcedAmbiguity, exists only so the fuzzer can inject negative reasoning. The key property is that extend is a join on the lattice Inductive < Unknown < Coinductive < ForcedAmbiguity, and it behaves like max: a single coinductive step makes the whole path coinductive.

Note that Unknown is deliberately not the bottom. Inductive ∪ Unknown = Unknown, not Inductive. The Unknown value exists because the solver does not yet trust its own inductive-cycle detection, so it refuses to commit:

rust
// compiler/rustc_next_trait_solver/src/solve/search_graph.rs:45-90

fn initial_provisional_result(
    cx: I,
    kind: PathKind,
    input: I::CanonicalInput,
) -> (QueryResult<I>, AccessedOpaques<I>) {
    match kind {
        PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
        PathKind::Unknown | PathKind::ForcedAmbiguity => {
            response_no_constraints(cx, input, Certainty::overflow(false))
        }
        // Even though we know some cycles to be unproductive, we still treat them
        // as unknown for now. This is both as we are not 100% confident in the
        // implementation yet and any incorrect errors would be unsound there.
        //
        // The affected cases are also fairly artificial and not necessarily desirable
        // so keeping this as ambiguity is fine for now.
        //
        // See `tests/ui/traits/next-solver/cycles/unproductive-in-coherence.rs` and
        // `tests/ui/traits/next-solver/overflow/recursive-self-normalization-simple.rs`
        // for examples where this would matter.
        //
        // FIXME(-Znext-solver=coinductive): Long term, we probably do want to
        // return `NoSolution` here. This should happen separately from the
        // stabilization of the new solver.
        PathKind::Inductive => unreachable!(),
    }
}

So a coinductive cycle starts with “yes”, and an unknown cycle starts with “ambiguous, probably overflow”. The PathKind::Inductive arm is unreachable!() because rustc never constructs one yet — the FIXME says what would change.

Why the kind is recomputed rather than cached

The cycle’s kind is not stored on the stack frame; it is folded over the stack segment between the head and the current entry, every time a goal is pushed. The consequence is that the kind of a cycle is always correct with respect to the current path, even when the same head is reached by different routes.

That matters because a head can be reached both inductively and coinductively. In that case, the cycle is coinductive (a single coinductive step suffices) and the solver may shortcut to “yes” — but only if all the usages of that head agree.

The fixpoint, with three escape hatches

rust
// compiler/rustc_type_ir/src/search_graph/mod.rs:1370-1445

let mut encountered_overflow = false;
let mut i = 0;
loop {
    let result = D::compute_goal(self, cx, input, inspect);
    let stack_entry = self.stack.pop();
    encountered_overflow |= stack_entry.encountered_overflow;
    debug_assert_eq!(stack_entry.input, input);

    // If the current goal is not a cycle head, we are done.
    //
    // There are no provisional cache entries which depend on this goal.
    let Some(usages) = stack_entry.usages else {
        return EvaluationResult::finalize(stack_entry, encountered_overflow, result);
    };

    // If it is a cycle head, we have to keep trying to prove it until
    // we reach a fixpoint. We need to do so for all cycle heads,
    // not only for the root.
    //
    // See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
    // for an example.
    //
    // Check whether we reached a fixpoint, either because the final result
    // is equal to the provisional result of the previous iteration, or because
    // this was only the head of either coinductive or inductive cycles, and the
    // final result is equal to the initial response for that case.
    if let Ok(fixpoint) = self.reached_fixpoint(&stack_entry, usages, result) {
        self.rebase_provisional_cache_entries(
            &stack_entry,
            RebaseReason::ReachedFixpoint(fixpoint),
        );
        return EvaluationResult::finalize(stack_entry, encountered_overflow, result);
    } else if usages.is_empty() {
        self.rebase_provisional_cache_entries(&stack_entry, RebaseReason::NoCycleUsages);
        return EvaluationResult::finalize(stack_entry, encountered_overflow, result);
    }

    // If computing this goal results in ambiguity with no constraints,
    // we do not rerun it. It's incredibly difficult to get a different
    // response in the next iteration in this case. These changes would
    // likely either be caused by incompleteness or can change the maybe
    // cause from ambiguity to overflow. Returning ambiguity always
    // preserves soundness and completeness even if the goal could
    // otherwise succeed or fail.
    //
    // This prevents exponential blowup affecting multiple major crates.
    // As we only get to this branch if we haven't yet reached a fixpoint,
    // we also taint all provisional cache entries which depend on the
    // current goal.
    if let Some(kind) = D::is_ambiguous_result(result) {
        self.rebase_provisional_cache_entries(&stack_entry, RebaseReason::Ambiguity(kind));
        return EvaluationResult::finalize(stack_entry, encountered_overflow, result);
    };

    // If we've reached the fixpoint step limit, we bail with overflow and taint all
    // provisional cache entries which depend on the current goal.
    i += 1;
    if i >= D::FIXPOINT_STEP_LIMIT {
        debug!("canonical cycle overflow");
        let result = D::fixpoint_overflow_result(cx, input);
        self.rebase_provisional_cache_entries(
            &stack_entry,
            RebaseReason::Ambiguity(D::FIXPOINT_OVERFLOW_AMBIGUITY_KIND),
        );
        return EvaluationResult::finalize(stack_entry, encountered_overflow, result);
    }

Four exits:

Not a cycle head → done.
Fixpoint reached → done. The check is that the new result equals the previous provisional result, or (on the first iteration) equals the initial provisional result and all usages had the same path kind.
No usages → the head was referenced but its value did not matter.
Ambiguity without constraints → stop, keep the ambiguity. This is the anti-blowup rule, and the comment is unusually honest about it: “This prevents exponential blowup affecting multiple major crates.”
Step limit (8) → overflow.

Without rule 4, a cycle that keeps producing “ambiguous but constraint-free” answers would be re-run eight times, each time re-running the whole subtree — a multiplicative blowup of up to 8^k.

The lattice again, this time as a bitmask

The same lattice shows up in the cache-validity machinery, where “which kinds of paths reach this goal” is a set, and sets of path kinds are stored as bitflags:

rust
// compiler/rustc_type_ir/src/search_graph/mod.rs:428-476

impl PathsToNested {
    /// The implementation of this function is kind of ugly. We check whether
    /// there currently exist 'weaker' paths in the set, if so we upgrade these
    /// paths to at least `path`.
    #[must_use]
    fn extend_with(mut self, path: PathKind) -> Self {
        match path {
            PathKind::Inductive => {
                if self.intersects(PathsToNested::EMPTY) {
                    self.remove(PathsToNested::EMPTY);
                    self.insert(PathsToNested::INDUCTIVE);
                }
            }
            ...

A set of path kinds as a 5-bit mask, with the join implemented as “upgrade weaker paths to at least this one”. That turns “is this cache entry still applicable?” into an O(1) bitmask test instead of an enumeration of paths.

Where it lives

compiler/rustc_type_ir/src/search_graph/mod.rs — PathKind, extend, the fixpoint loop, PathsToNested.
compiler/rustc_next_trait_solver/src/solve/search_graph.rs — initial_provisional_result, the Delegate policy.
compiler/rustc_next_trait_solver/src/solve/mod.rs — FIXPOINT_STEP_LIMIT.

Takeaway

Coinduction is usually taught as “assume true, then check”. The part that makes it implementable is the classification of the cycle into kinds and the discipline of recomputing that classification compositionally, rather than caching it. Once the kind is a value in a small lattice with a max join, everything else — the initial assumption, the shortcut condition, the cache-validity check — falls out of the algebra.