Two-way vs. one-way unification when resolving traits

language design
1

I'm trying to understand how trait resolving in the code below works:

enum Wrap<T> {
    W,
    WithVal(T),
}

struct Alt;

trait Two<B> {}

impl<T> Two<T> for Wrap<T> {}

fn f<P, Q>(p: P, q: Q) where P: Two<Q> {}

fn main() {
    f(Wrap::W, Alt);
}

This code generates these goals: (I'm using type<arg1, arg2, ...> syntax here instead of Rust-style arg1: type<arg2, ...>)

  • Two<Wrap<?t>, Alt> (where ?t is unconstrained unification variable)

And we have these impls:

  • Two<Wrap<T>, T>

When matching the impl heads, we instantiate this as Two<Wrap<?q>, ?q>. Now this matches the goal if we unify ?q ~ Alt, but this will also unify ?q ~ Alt, which will unify the unification variable in the goal as ?t ~ Alt. So the goal type also changes if we accept this matching.

Rust does this and this program type checks, but I've always thought unification when matching an impl is done one-way, updating the instantiated impl head's type variables but not never the goal's. I think one reason for this is because if you update the goal's type variables and you have a bunch of goals to solve, you may have to revert unifications done to try another (more general) impl. With a number of goals that share unification variables this may lead to backtrcking from a fair amount of work during trait resolving to try another impl, and for each impl choice you may have a number of alternative impls for the rest of the goals too.. not great from type-checking performance point of view.

My current best guess of how this works in Rust is: if you have just one candidate for a goal, you do two-way unification. Otherwise you do one-way. Is this correct?

(I asked an LLM, but for advanced niche topics like this they're often wrong, so I wanted to ask actual exprts here.)

2

Unification (relation in rustc parlance) takes variance as parameter. Unification as invariant will equate types (the variance can also change when deepening into types, like arguments of fn ptrs being contravariance). Trait solving unifies the trait ref of the impl with the trait ref at question invariably.

1 Like