clarify disjointedness rules

[nikomatsakis]

@glaebhoerl raised this question in the original RFC thread:

For the purposes of disjointness, Trait<Type1> and Trait<Type2> are considered to be unrelated traits, right?

To which I -- rather blithely -- replied "yes". And that is certainly the intention. But it raises an interesting question, in that it intersects with our compiler's ability to do negative reasoning. For example, consider this program, with two placeholders XXX and YYY:

trait Trait<A> {
    let mut x: i32;
    let mut y: i32;
}

fn foo<T>(foo: T)
    where T: Trait<i32> + Trait<u32>,
{
    let p = &mut foo.<Trait<XXX>::x>;
    let q = &mut foo.<Trait<YYY>::y>;
    use(p, q);
}

This program ought to be legal iff XXX "==" YYY and illegal otherwise (because it would be an illegal borrow). But what is this "==" operator?

Ordinarily, we prefer solutions where we know "a priori" whether two types must be unified -- that is, I'd rather not say "if the borrows p and q overlap, then we will enforce that XXX == YYY, but otherwise we don't". This is because, right now, borrowck consumes the output of typeck. I'd rather say that "typeck determines what XXX and YYY are, and borrowck examines that". And mostly I think this would work fine here, but it's something to keep in mind. This question becomes particularly acute around regions; for example, if XXX were &'a i32 and YYY were &'b i32, for some regions 'a and 'b, are those distinct types? Often we have a lot of flexibility in which regions we pick.

I think that, for borrowck, the answer would be that types which are equal "modulo" regions can be considered equal, and everything else unequal -- unequal is the conservative path. We could be even stricter around regions to start and require precise equality. But that shouldn't be needed because any two types that only different modulo the precise regions involved ought to map to the same underlying impls.

Anyway, this is also probably something that can be worked out in the course of implementation -- the problems don't seem too scary -- but it's good to keep in mind.