Reordering where clauses can change program behavior

[aturon]

Here's a contrived example:

use std::fmt::Debug;

trait Left<T> {}
trait Right<T> {}

trait Join<U> {
    fn test();
}

// With the reordering,
//   impl<T, U> Join<U> for T where T: Right<U>, T: Left<U>, U: Default + Debug {
// you'll get a different output
impl<T, U> Join<U> for T where T: Left<U>, T: Right<U>, U: Default + Debug {
    fn test() {
        println!("{:?}", U::default())
    }
}

impl<T, U: Default + Debug> Left<U> for T {}
impl<T, U: Default + Debug> Right<U> for T {}

fn try_it<T: Default + Debug>() where T: Left<bool>, T: Right<()> {
    <T as Join<_>>::test()
}

fn main() {
    try_it::<u8>() // the type here is irrelevant
}

In the order given, the output is false. If you swap the order as suggested in the comment, the output is ().

What's happening here is a combination of a few things. The Join impl creates obligations in order of its where clauses, and the solution to each obligation informs inference, which affects future obligations. At the same time, when it comes time to show T: Left<U>, for example, it can be proved either by virtue of the blanket impl or the where clause on try_it. We currently give preference to the where clause, which then drives inference.

The same mechanisms also lead to cases where:

1. Adding a valid where clause can cause code to stop compiling.
2. Adding a where clause can change program behavior.

These issues seem fairly fundamental to the where clause preference approach, which is something we likely cannot change backwards compatibly (and there were good reasons for it in the first place). So it's possible that we will just have to live with these consequences. But I wanted to file a bug for posterity.

[aturon]

cc @nikomatsakis @arielb1 @eddyb @withoutboats

[cramertj]

Is there some reason this isn't just considered a bug in inference? I'd have expected this to fail to infer _ in the call to <T as Join<_>>::test(), since there are multiple valid choices for _. It seems reasonable to make that change as long as a crater run doesn't turn up tons of nastiness. IIRC we've allowed breaking changes to inference in the past as a result of adding trait impls (see #40952 caused by #40028).

[aturon]

@cramertj It's not a bug per se -- it's the direct result of intentional behavior. In particular:

pub trait Foo<T> { fn foo(&self) -> T; }
impl<T> Foo<()> for T { fn foo(&self) { } }
impl Foo<bool> for bool { fn foo(&self) -> bool { *self } }

pub fn foo<T>(t: T) where T: Foo<bool> {
   println!("{:?}", <T as Foo<_>>::foo(&t));
}
fn main() { foo(false); }

This program prints false, because the where clause on foo trumps the blanket impl and guides inference. That trumping behavior is done deliberately, but it's the cause of most of these issues.

Now the obvious question is: why did we want that trumping behavior in the first place? I don't think it's clearly documented, unfortunately, but @nikomatsakis may be able to remember. (It was a decision made in the run-up to 1.0).

One easy way to tell would be to turn off the trumping behavior (very easy) and see what breaks when bootstrapping. I'm pretty confident it will fail to bootstrap and build std, but that might point us to the common place where this matters. And if it doesn't... then we should indeed crater it.

@cramertj, are you interested in trying such an experiment? I can mentor on the rustc side.

[cramertj]

@aturon Absolutely!

The trumping behavior makes sense to me when it's giving priority to a where clause over an external blanket impl, but I don't understand why the order of the where clauses should matter.

[withoutboats]

It seems like a 'correct implementation' of this trumping would find "two trumps" - ?U = bool and ?U = () and it should therefore be ambiguous, whereas in the example in aturon's second comment there is only one trump, ?U = bool.

[cramertj]

@withoutboats Exactly.

[aturon]

The trumping behavior works exactly as you say: it only applies when there's exactly one where clause.

The thing that makes this example cause problems, nevertheless, is that we have two distinct trait bounds for the Join impl, and that in general in type inference, solving one bound needs to provide inference information for the next bound to solve. In detail:

• There's a call to test, which means we need to show T: Join<?U> under the assumptions that T: Left<bool> and T: Right<()>.
• There's just one Join impl, so it's the one we must use. Now we need to show T: Left<?U> and T: Right<?U> under the assumptions that T: Left<bool> and T: Right<()>.
• We start by trying to show T: Left<?U>
  • The blanket impl of Left could apply (since we don't yet know what ?U is). However, we have a single where clause, T: Left<bool>, that we can apply to show T: Left<?U>.
  • Because of the trumping rule, this single applicable where clause means we pick ?U = bool
• Now we need to show T: Right<?U> where ?U = bool
  • Here, the where clause T: Right<()>, is not applicable to our goal; we discard it.
  • That leaves only the blanket impl, which we can indeed use.

The key is that we must separately prove T: Left<?U> and T: Right<?U> to prove Join, and from that perspective, only one of the where clauses at a time applies.

@cramertj The relevant piece of code is here. You could start just by changing true to false and seeing what happens :-)

[aturon]

Oh and here's the code that drives the overall "impl selection" process, which in turn drives inference. You can see, in particular, that it insists on winnowing down to a single "candidate" to yield back meaningful information. But part of that winnowing is removing all impls if there are applicable where clauses.

[arielb1]

Winnowing can't be the cause because it runs inside a probe - the order dependence occurs at the "outermost level" of trait selection:

use std::fmt::Debug;

trait Left<T> {}
trait Right<T> {}

impl<T, U: Default + Debug> Left<U> for T {}
impl<T, U: Default + Debug> Right<U> for T {}

// replacing the order of `T: Left<U>` & `T: Right<U>` changes result
fn movable<T, U>() where T: Left<U>, T: Right<U>, U: Default + Debug {
    println!("{:?}", U::default())
}

fn try_it<T: Default + Debug>() where T: Left<bool>, T: Right<()> {
    movable::<T, _>();
}

fn main() {
    try_it::<u8>() // the type here is irrelevant
}

[aturon]

@arielb1 See my explanation here. Winnowing is a crucial part of why this example works, but is not the direct source of order dependence. Fulfillment is.

[cramertj]

So I messed around with this a bit-- I tried disabling the candidate_should_be_dropped_in_favor_of logic entirely, then honing down to just removing preference for ParamCandidates, then disabling preference over ImplCandidates. All resulted in the same error:

error[E0283]: type annotations required: cannot resolve `Self: any::Any`
   --> src/libcore/any.rs:88:1
    |
88  | / pub trait Any: 'static {
89  | |     /// Gets the `TypeId` of `self`.
90  | |     ///
91  | |     /// # Examples
...   |
110 | |     fn get_type_id(&self) -> TypeId;
111 | | }
    | |_^
    |
    = note: required by `any::Any`

@nikomatsakis addressed why the trumping logic is necessary in this comment. Later in the same comment, it's pointed out that this trumping applies even in cases with leftover inference variables, which is what's happening in the issue here. Perhaps we could check if there are remaining inference variables before applying trumping behavior?

Overall, however, I'd prefer a solution that allowed us to keep the trumping behavior, but detect situations in which the the ordering of where clauses causes trumping of the same inference type to be flipped. In this case, trumping for proving T: Right<?U> in isolation results in a different value of U than when using trumping behavior for proving T: Left<?U>. If we could identify those situations, we could disable trumping only in the cases where it would result in ordering conflicts.

Can anyone (@nikomatsakis, @aturon) comment on the performance costs of such an approach? I suppose we could always try it and see.

[eddyb]

The method is needs_infer and it's O(1).

[cramertj]

@eddyb Sorry, I should have been more clear: I'm not concerned about the performance cost of disabling trumping when deciding inference variables-- I was concerned about the performance cost of disabling trumping for inference only when trumping order would be changed by where clause ordering. For this to work, I think we'd need to compute the result of applying trumping for each where clause independently, and then check to see if starting with different where clauses resulted in conflicting decisions for inference variables. If there is a conflict, we'd report an ambiguity.

[aturon]

@cramertj I'm not quite following the example error you're giving -- I'm having a hard time understanding where Self is coming up in the code being pointed at. Can you elaborate a bit?

I should mention, btw, that I don't think this order-sensitivity is likely to pose any real practical problems; the example is very contrived. I was guided to it by thinking carefully about things in Chalk and realizing that it was possible, even though we thought the trait system avoided it. So I personally wouldn't be inclined to try to test for order-sensitivity, regardless of performance.

But I would like to understand a bit better how widely trumping ends up mattering in practice.