Confusion arround how obligations are checked by type system

help
1

I am a little confused about how obligations (as defined in the compiler dev book) are handled by the type checker.

In my naive understanding, when we include a where clause, we are adding obligations. The type checker will then attempt to make sure that these obligations can be fulfilled.

Further, when writing a impl block, we can write blocks that are made non-overlapping via where clauses. For instance, this compiles just fine in the playground (also on nightly).

trait MarkerTraitA{}
trait MarkerTraitB{}

trait Takes <T>{
    fn take(&self, val : T);
}

struct Message<T>(T);


struct Wrapper<T>{
    val: T
}


impl<T> Takes<T> for Wrapper<T> where 
Message<T> : MarkerTraitA {
    fn take(&self, val : T){
        return;
    }
}

impl<T> Takes<T> for Wrapper<T> where 
Message<T> : MarkerTraitB {

    fn take(&self, val : T){
        return;
    }
}


fn main(){
    return;
}

Though, I am a little confused that this compiles correctly, as I have specified bounds that should not be able to be satisfied given that we are bounding with a local type and trait (and therefore, by the orphan rule, we have the complete set of implementations, no upstream or downstream create can ever add more).

With one added line, we can make this not compile:

trait MarkerTraitA{}
trait MarkerTraitB{}

trait Takes <T>{
    fn take(&self, val : T);
}

struct Message<T>(T);

impl<T> MarkerTraitA for Message<T>{} // this is the added line here

struct Wrapper<T>{
    val: T
}



impl<T> Takes<T> for Wrapper<T> where 
Message<T> : MarkerTraitA {
    fn take(&self, val : T){
        return;
    }
}

impl<T> Takes<T> for Wrapper<T> where 
Message<T> : MarkerTraitB {

    fn take(&self, val : T){
        return;
    }
}


fn main(){
    return;
}

This throws the error:

error[E0283]: type annotations needed: cannot satisfy `Wrapper<T>: Takes<T>`
  --> src/main.rs:25:22
   |
25 | impl<T> Takes<T> for Wrapper<T> where 
   |                      ^^^^^^^^^^
   |
note: multiple `impl`s satisfying `Wrapper<T>: Takes<T>` found
  --> src/main.rs:18:1
   |
18 | / impl<T> Takes<T> for Wrapper<T> where 
19 | | Message<T> : MarkerTraitA {
   | |_________________________^
...
25 | / impl<T> Takes<T> for Wrapper<T> where 
26 | | Message<T> : MarkerTraitB {
   | |_________________________^

The use of E0283 is rather confusing to me, as this error seems to be a type inference error, whereas I would expect the "true" error to be that there does not exists an implementation that satisfies the bounds, but maybe I am barking up the wrong tree with this idea that where clause bounds have to be able to be satisfied. Looks like RFC2056 allows for "trivial where clause bounds", but I can't seem to track down why in the first case this compiles but it stumbles on the second.

Thanks for reading, and I apologize in advance if I am missing something rather obvious here.

2

I believe that is incorrect. You have found an edge case where because there are no impls of either of the MarkerTraits, you can have two impl<T> Takes<T> for Wrapper<T>, each with a never-satisfied where bound so that they effectively do not exist, but I believe in the general case where any impls exist, you will always get an error if you have two impl<T> Takes<T> for Wrapper<T> regardless of their bounds.

The kind of trivial bounds that are not supported and which that RFC proposes supporting are ones which are not generic, i.e. where SomeConcreteType: MarkerTraitA. This is mostly relevant only to macro-generated code which can’t know up front whether the trait will be implemented. Your case is not affected because your bound contains a generic parameter, the T in where Message<T>: MarkerTraitA.

1 Like
3

There are no orphan rule violations, since Takes<_> is a local trait (and Wrapper<_> is a local type).

However, the overlap check can still fail. In the compiling code, it does not fail, because the trait solver can employ negative reasoning. Negative reasoning won't make assumptions about potential implementations that could exist elsewhere under the orphan rules, but it can assume you won't locally add some conflicting implementation.

Negative reasoning can take into account where clauses, for example this compiles.

impl<T> Takes<T> for Wrapper<T> where Message<T> : MarkerTraitA {}
impl<T> Takes<T> for Wrapper<T> where Message<T> : MarkerTraitB {}

impl<T> MarkerTraitA for T where T: Clone {}
// Works because `Message<_>` is not `Clone` and you control that
impl MarkerTraitA for Message<()> {}
impl MarkerTraitB for Message<String> {}

fn test<T>(_: Wrapper<T>) where Wrapper<T>: Takes<T> {}

fn main(){
    test(Wrapper(()));
    test(Wrapper(String::new()));
}

The question remains, why doesn't in compile when you add a blanket implementation for Message<T>: MarkerTraitA? I'm not :100: sure but I think it's just some shortcoming of the current trait solver. It compiles if you add a bound (besides Sized). And it compiles with the next solver enabled globally (but I can't guarantee that won't change).

3 Likes
4

I spent some time stepping through this part of the compiler. Not sure if it was particularly helpful, but it was a good way to kill some free time.

From what I can gather, for each of these implementation blocks:

impl<T> Takes<T> for Wrapper<T> where 
Message<T> : MarkerTraitA {
    fn take(&self, val : T){
        return;
    }
}

impl<T> Takes<T> for Wrapper<T> where 
Message<T> : MarkerTraitB {

    fn take(&self, val : T){
        return;
    }
}

it appears to me that the compiler creates the "goal" Wrapper<T> as Takes<T> with the the added context information that we can assume that there exists an implementation that will satisfy the where clause (it actually looks like this is manually inserted from the where clause into the candidate list via the function assemble_candidates_from_caller_bounds inside candidate_assembly.rs ).

So for the first implementation block, we are trying to prove the goal Wrapper<T> as Takes<T> and we are free to assume Message<T> as MarkerTraitA.

From what I can tell, the compiler then checks both implementations as possibly satisfying this goal. The first implementation (which generated this goal to begin with), has the nested obligation Message<T> as MarkerTraitA which, again, the compiler seems to take as an assumption. The second implementation has the nested obligation Message<T> as MarkerTraitB, which comes up empty when the compiler attempts to generate a candidate list (which makes sense, there is no impl blocks for it). Therefore, the we only get one implementation that satisfies this goal given the assumptions and so we don't have to do any further checking.

For the second, we are trying to prove Wrapper<T> as Takes<T> and we are free to assume Message<T> as MarkerTraitB. Running the same logic as for the first block, we get that again there is only one implementation that satisfies this goal given the assumptions.

Since both block's goals were satisfied uniquely, this compiles correctly.

Now for the second case, the one that fails to compile:

trait MarkerTraitA{}
trait MarkerTraitB{}

trait Takes <T>{
    fn take(&self, val : T);
}

struct Message<T>(T);

impl<T> MarkerTraitA for Message<T>{} // this is the added line here

struct Wrapper<T>{
    val: T
}


// I'm calling this "impl one"
impl<T> Takes<T> for Wrapper<T> where 
Message<T> : MarkerTraitA {
    fn take(&self, val : T){
        return;
    }
}

// I'm calling this "impl two"
impl<T> Takes<T> for Wrapper<T> where 
Message<T> : MarkerTraitB {

    fn take(&self, val : T){
        return;
    }
}


fn main(){
    return;
}

The first implementation block follows its logic without issue, closely mirroring the logic in the case that does compile. The problem is when we check the goal from the second implementation block.

Here the compiler appears to again make the goal Wrapper<T> as Takes<T> and manually assumes that Message<T> as MarkerTraitB holds. Again, it appears that both implementations are checked with this assumption. The first generates the nested obligation Message<T> as MarkerTraitA. The problem now is that this nested obligation is actually satisfied. Therefore, we end up with both implementations being valid candidates that satisfy this goal. The compiler then appears to attempt to winnow to narrow and check for overlap, but it appears (and I have not dug into this too much) that this winnow check fails to select a correct implementation and instead reports these two implementations as being overlapping (which also seems to mean there is some weird non-commutativity going on here, impl one was determined to be uniquely satisfied by itself, but impl two seems to struggle and thinks it has overlap with impl one).

Anyways, thanks for the response and examples, I think figuring out the peculiarities of why the existing trait system does what it does here is for more learned rustaceans than myself so I am happy with just leaving it at "it's a limitation that (as of now) does not exist in the new solver".

5

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.