Disjointness based on associated types.

[withoutboats]

Rendered

[withoutboats]

cc @sgrif you may have had use cases for this in Deisel?

cc @ticki if you want, "proofs that two type variables are disjoint" seems like a good opportunity for writing up some formal judgments

[sgrif]

Yeah, I've definitely needed this in Diesel. I don't recall the specific place that I'm working around it, but it was likely of the form

impl<T> Something for T where T: Expression<SqlType=VarChar> {
    // ...
}

impl<T> Something for T where T: Expression<SqlType=Text> {
    // ...
}

Honestly, I had figured that this was a bug and not an explicit decision.

[comex]

Perhaps add a rule that instantiations of generic types with disjoint parameters are disjoint. i.e.

impl<T: Trait1<Item=X>> Trait2 for Foo<T> { ... }
impl<T: Trait1<Item=Y>> Trait2 for Foo<T> { ... }

or even

impl<T: Trait1<Item=X>, U: Trait2<Item=Foo<T>>> Trait3 for U { ... }
impl<T: Trait1<Item=Y>, U: Trait2<Item=Foo<T>>> Trait3 for U { ... }

[withoutboats]

Yeah. We don't have good, consistent language about this, but when I wrote "two type variables" I meant any type variables (really I meant any type, whether an abstract variable or a concrete type, since the first rule only applies to concrete types), whether they be the receiver of the trait or not (I realize the summary is less broad than this, oops).

This is exactly what I had in mind when I said this rule was recursive.

[sgrif]

Is there any case where T is disjoint but Foo<T> is not disjoint today? If not it seems redundant to re-specify it here.

[withoutboats]

@comex was talking about the transitivity of the disjunction rule, but perhaps we should note that if T is disjoint with U and X is a type constructor of the kind type -> type, X<T> is disjoint with X<U>. No reason this couldn't be a roundup to establish and document some of the basic disjunction rules.

EDIT: Actually, this may impact how that rule is implemented. Currently I think all disjunction is based on inequality of concrete types (e.g. we can just see that Foo<Bar<Baz<i32>> is not Foo<Bar<Baz<bool>>), but now that rule also needs to take into account type variables that are bound exclusively.

[withoutboats]

Honestly, I had figured that this was a bug and not an explicit decision.

I think the best word for this is 'omission' - the current rules are correct so its not really a bug, but no one ever decided this rule shouldn't be added as well. This kind of disjointness just hasn't been evaluated for inclusion yet.

[seanmonstar]

Perhaps the motivation section should be updated to not be in first person, per #61?

[durka]

What about an impl where you don't specify the associated type at all, but use it in the implementation?

trait Tr { type A; }

impl<T: Iterator> Tr for T {
    type A = T::Item;
}

[withoutboats]

@durka What type do you think T might be disjoint with?

[durka]

None, I guess.

[withoutboats]

I agree, none of the disjointness rules seem to make T there disjoint with any other types (except for local reasoning shenanigans)

[cristicbz]

There are a bunch of issues about this, including one I filed early last year: rust-lang/rust#23341, rust-lang/rust#20400, rust-lang/rust#30191

(thought it would be useful to link to them)

[withoutboats]

Looking at each of those:

• rust-lang/rust#20400 - This is exactly what this RFC should resolve.
• rust-lang/rust#23341 - this is a bit tricky. Technically, after this RFC, this should compile, but I believe that this acceptance should be treated as a bug and - once Rust has explicit mutual exclusion - you should be required to add that impl !Bar for u8 { }
• rust-lang/rust#30191- this looks like the examples are invoking all kinds of weirdness, but like the previous example I don't think we should rely on implicit negative bounds ever, to avoid backcompat traps (and this is also why its important to provide explicit negative bounds)

See also #1148 & #1658

[james-darkfox]

Any progress on this issue?

[burdges]

I've run into this with a toy branch where I wanted to replace some macros that ran over numeric types with type constraints. I believe the type constraint based version made more sense, but it failed and I never thought deeply enough to say anything. If this happens, then great. If this is not a good idea, then maybe comment could be added to the documentation?

[eddyb]

@Mark-Simulacrum hit this in rust-lang/rust#37270 where they needed two impls for different iterator element types, but had to proxy to a trait dispatched on <Self as Iterator>::Item instead.

[withoutboats]

@rfcbot fcp merge

[rfcbot]

Team member @withoutboats has proposed to merge this. The next step is review by the rest of the tagged teams:

• @aturon
• @eddyb
• @nikomatsakis
• @nrc
• @pnkfelix
• @withoutboats

Concerns:

• negative reasoning (#1672 (comment))
• underspecified (#1672 (comment))

Once these reviewers reach consensus, this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[nikomatsakis]

Hmm. I would like to see something like this proposal go forward, but I'm a bit wary here.

@rfcbot concern negative reasoning

This seems to be strongly connected to negative reasoning. Basically the argument here is that we can prove that two where clauses are mutually incompatible, which isn't how our coherence check works now. I do think it makes sense to go in this direction, but I want to approach it with a somewhat more formal approach.

Along those lines, I've been working on converting our trait system into a lambda-prolog-based logic in this repository. I'm not all that far along yet, but I hope that it can give us a basis for reasoning better about negative reasoning and its impact.

That said, I think that these changes likely fit fairly well with our trait system logic (modulo my "underspecified" concern below). Basically I think what we should be shooting for is something that relies only on minimal logic. Essentially, in prolog terms, somewhere we can define an "inconsistent" predicate. I think we would translate this RFC as follows:

inconsistent :- 
    <P[0] as Trait<P[1]...P[n]>>::Item = X,
    <P[0] as Trait<P[1]...P[n]>>::Item = Y,
    not_equal X Y. // note that this is a predicate we have to define =)

@rfcbot concern underspecified

Today we only have X = Y constraints in our system. This would introduce X != Y -- even if only limited to cherence -- and the RFC doesn't specify very clearly what this means. It gives some simple examples (u32 and i32 are unequal) but (for example) what about &'a u32 and &'b u32, or T and U?

Presumably the answer is that all variables would be considered potentially equal, and the only way to prove two types are disjoint is if they are unified with distinct nominal types (i.e., u32 vs i32, or Rc vs Arc), right?

In any case, more examples are certainly needed. But I do think we'll be able to specify this nicely.

[withoutboats]

About under-specification:

The reference case is interesting because it introduces subtyping, presumable &'a u32 != &'b u32 iff 'a has no overlap with 'b? I don't think there's a time when coherence has enough info to prove that and we can leave these as considered overlapping at least for now.

T != U not only if they are unified with distinct types but also if they are bound by disjoint traits (for example because those traits have incompatible associated types); that is, the rule this is aimed at introducing should apply recursively.

I wrote this RFC very quickly (as I write every RFC I actually publish 😉) and it could definitely use revision to be more formal.

[nikomatsakis]

@rfcbot concern underspecified

Today we only have X = Y constraints in our system. This would introduce X != Y -- even if only limited to cherence -- and the RFC doesn't specify very clearly what this means. It gives some simple examples (u32 and i32 are unequal) but (for example) what about &'a u32 and &'b u32, or T and U?

Presumably the answer is that all variables would be considered potentially equal, and the only way to prove two types are disjoint is if they are unified with distinct nominal types (i.e., u32 vs i32, or Rc vs Arc), right?

In any case, more examples are certainly needed. But I do think we'll be able to specify this nicely.

[nikomatsakis]

@withoutboats I'd be happy to work with you on it

[withoutboats]

I've realized this can express mutually exclusive traits and that it therefore carries all of the baggage associated with that feature.

// Two disjoint types
struct Left;
struct Right;

trait Exclusive {
    type Distinguisher;
}

// Foo and Bar are mutually exclusive because their associated types are
// disjoint.
trait Foo: Exclusive<Distinguisher = Left> { }
trait Bar: Exclusive<Distinguisher = Right> { }

trait Baz { }

// These impls are recognized as non-overlapping because the type parameters
// implement two exclusive forms of the same trait
impl<T: Foo> Baz for T { }
impl<T: Bar> Baz for T { }

If this RFC were accepted, it would resolve the most pressing use for general explicit mutual exclusion in my code, because the traits I want to make exclusive already have a supertrait parameterized by a dummy type that ought to be an associated type, but for lack of this feature.

[burdges]

Just ran into this again when trying to be generic over built in numeric types. I could work around the first times I ran into this if all the core numeric types functionality, like leading_zeros(), MAX, etc. lived in traits, but this time I was trying to do something more akin to specialization, so even that won't help.

[burdges]

Appears there are some situations where you can circumvent needing this using a parameterized helper trait to make the associated type behave exactly like a type parameter.

trait Helper<N> { ... }
impl<F> Helper<u16> for F where ... { ... }
impl<F> Helper<u32> for F where ... { ... }
impl<F> Helper<u64> for F where ... { ... }

trait Stuff {
    type N;
}

impl<T,NN> Stuff for T where T: Helper<NN> {
    type N = NN;
}

I'd expect logic to tends towards landing in Helper though, which gets ugly.

[nrc]

ping @nikomatsakis @withoutboats any progress here?

[nikomatsakis]

Nope, @withoutboats and I haven't really talked. I remain concerned in the same way as before. =) I have been hoping to catch up with @withoutboats online and chat about this at some point though.

[aturon]

@withoutboats can you cancel the FCP request until you've had a chance to revise?

[withoutboats]

@rfcbot fcp cancel

[rfcbot]

@withoutboats proposal cancelled.

[withoutboats]

@rfcbot fcp postpone

I'm proposing we postpone this and #1658 for a later date, when chalk is up and running, and we can put forward a unified proposal for how to expand the negative reasoning performed by our coherence system.

I still want something like this RFC someday, but keeping this RFC open is not tracking progress toward that goal at all, and I think these two RFCs will want to be majorly revised into a single proposal.

[rfcbot]

Team member @withoutboats has proposed to postpone this. The next step is review by the rest of the tagged teams:

• @aturon
• @eddyb
• @nikomatsakis
• @nrc
• @pnkfelix
• @withoutboats

No concerns currently listed.

Once these reviewers reach consensus, this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[rfcbot]

The final comment period is now complete.

[withoutboats]

Closing as postponed.