When does backwards trait inference happen?

help
1

As you might expect, the following code fails with a type annotations needed error (playground)

trait X {}

impl X for [u8; 10] {}

pub fn test<T>() where T: X {}

fn main () {
    test();
}

My intuition for the reason is that trait resolution would need to do backwards inference to figure out what instance to pick for the unification variable for T, and it doesn't do that (either for computational reasons, because the # of instances could blow up, or because it might be fragile? not sure).

However, here is a slightly more complex set-up that does work (in some cases) (playground):

trait X {}

// FAILS; ambiguous instance
//impl X for [u8; 10] {}

impl X for [u8; 11] {}

trait Gen<T> {}

// FAILS
//impl<T, S> Gen<T> for S {}

// FAILS
//impl<T, const M: usize> Gen<T> for [u8; M] {}

// WORKS
impl<const N: usize, T> Gen<[u8; N]> for T {}

// WORKS
//impl<const N: usize, const M: usize> Gen<[u8; N]> for [u8; M] {}

fn test<T, Y>(_y: Y)
where
    T: X,
    Y: Gen<T>,
{
}

fn main() {
    let x = [0; 10];
    test(x);
}

The trick seems to be that through the Gen<T> bound on test, we can partially instantiate T, and once it is partially instantiated, the compiler will go look for an instance that satisfies bound X and unifies with the partially-instantiated variable for T. This works as long as only one instance matches the partially-instantiated bound [u8; ?N] : X.

Hence my question; is the behavior of the trait resolver in cases such as these documented somewhere? I tried to have a look at the rust compiler devs book (Trait solving - Rust Compiler Development Guide), but didn't see any mention of this specifically. I was (pleasantly) surprised that this worked.

2

There are a couple of mentions on that page of 'if there is only one entry in the set, then we are done'. That's the relevant behavior, I believe. I usually call this the "only one impl" rule.

It's also a problematic behavior; it makes it a breaking change to add some possible trait implementations. Therefore, I recommend not writing code that relies on it.

2 Likes
3

You're right that this page mentions the ambiguity error in case multiple instances are available. I agree that this makes for fragile code and should be avoided.

What it does not seem to mention is why my first toy example fails, whereas the second one succeeds. There seems to be another, implicit rule at work that makes the "only one impl" rule fire (i.e. make candidate generation happen) only when the proof obligation has been partially instantiated.

2 Likes