Disambiguating Overlapping Trait Implementations

I have the following traits, that the compiler thinks are overlapping:

impl<I> Sub<Ib<I>> for Ib<I> where I : BidirectionalIteratorImpl {...} 
impl<I> Sub<I::DistanceTypeImpl> for Ib<I> where I : BidirectionalIteratorImpl {...}

Now I know that I::DistanceTypeImpl will never be Ib<I> so these implementations do not overlap. How can I tell the compiler that they don't overlap?

This is necessary because the distance between two iterators is a scalar, but we can also subtract a scaler from an iterator (moving the iterator backwards).

Currently you cannot tell the compiler that they don't overlap. In general, there's no introduce a rule that two generic types don't overlap. If Rust had negative bounds, you could do something like this though:

trait Ibish { }
impl<I> Ibish for Ib<I> { }
trait BidirectionalIteratorImpl {
    type DistanceTypeImpl: !Ibish

As far as I know, there hasn't been any discussion of a mechanism to exclude specific types as invalid for an associated type.

I think subtraction is a fairly fundamental operation to be able to represent, so it would seem an important problem to solve. This kind of thing works well in C++, which seems to be able to use both specialisation and associated types without problems, something that seems to cause big problems for Rust's type system. C++ concepts will add a strict type system to templates, which again seems to have no problems with specialisation or associated types. I guess this all stems from the separate compilation thing, as C++ templates require whole program compilation.

What is the reason you cannot use associated types with specialisation?

I tried this on the nightly build:


trait BidirectionalIterator {
    type DistanceType: NotBidirectionalIterator;

trait NotBidirectionalIterator {}
impl NotBidirectionalIterator for .. {}
impl<I> !NotBidirectionalIterator for I where I : BidirectionalIterator {}

trait Test<I> {}
impl<I> Test<I> for I where I : BidirectionalIterator {}
//impl<I> Test<I::DistanceType> for I where I : BidirectionalIterator {}

fn main() {}

It seems even though we can deduce that the clauses cannot overlap, the compiler cannot. Either the compilers overlap detection needs improvement, or we need a way for the programmer to promise they don't overlap, with obviously the potential for the program to go wrong at runtime if it turns out the promise was made incorrectly. Something like #[disjoint(Test)] which would override the overlap testing.

I think the correct solution is neither of these but somewhere between them. The user should be able to declare that two sets of types are are disjoint, and it should be a compile time error if they are not. I think it is important that the user makes a declaration, because I think if it is implicit, users will unintentionally rely on disjointness they did not intend and have difficulty refactoring when they want these sets to no longer be disjoint.

I agree that declarable mutual exclusion is a desirable property for the coherence system, but it is not a feature yet. Trying to hack it in with OIBITs is a probably a bad idea. Complex operator overloading like what you are attempting here is one of the use cases that is blocked on this feature.

It would also be good to be able to do !Num so definitions don't overlap with the standard arithmetic ones, and avoid having to wrap types in structs just to get it to work, which makes the code a lot more complex than it should be.

I think I will use some appropriate unique named methods for now, and come back to the overloading later.

I have replaced the overloading of +/- with 'add' and 'dif' methods as it simplifies the code quite a bit because it no longer needs type wrappers. The other problem is that because the difference between two iterators has a different type from subtracting a 'distance' from an iterator I need a different function name for that, so I have 'dif' for calculating the distance between two iterators and 'sub' to subtract a distance from an iterator.

As +/- have associated types any overloading cannot use specialisation. It would be nice to have negative trait bounds and better overlap detection for trait implementations so that operators could be overloaded more easily to match their mathematical uses. Technically points and vectors have the same addition/subtraction behaviour, so Rust at the moment cannot implement addition and subtraction for domains where distance has a different type than location (which is the general case) but only a subset where distance and location have the same type.