Remove the remaining uses of `old_orphan_rules`

[arielb1]

UPDATED ISSUE:

The original issue that was reported by @arielb1 has largely been resolved. However, there remain some traits that were added before the new rules were completed, and which do not conform. Those traits are currently distinguished with old_orphan_check markers. The remaining work is to fix these traits:

• BorrowFrom
• BorrowFromMut
• IntoCow
• ToOwned
• PartialEq

- @nikomatsakis

ORIGINAL ISSUE:

The current version of orphan checking does not prevent me from break coherence if impls from different crates are non-orphan because of different type parameters of the same type, for example:

base.rs:

pub trait Base { fn work(&self); }

foo.rs:

extern crate base;
pub struct Foo;

impl<T> base::Base for (Foo, T) {
  fn work(&self) { println!("foo!"); }
}

bar.rs:

extern crate base;
pub struct Bar;

impl<T> base::Base for (T, Bar) {
  fn work(&self) { println!("bar!"); }
}

foobar.rs:

extern crate foo;
extern crate bar;
extern crate base;
use base::Base;

fn main() { (foo::Foo, bar::Bar).work(); }

Which of course ICE-s with a trans ambiguity.

[arielb1]

cc @nikomatsakis

[nikomatsakis]

@arielb1 that is definitely a hole! Nominating. Interesting, have to think a bit about what the best way is to patch the rules for this case.

[arielb1]

By the way, the ambiguity can also occur between the receiver and one of the trait's type parameters:

base.rs:

pub trait Base<T> { /* ... */}

foo.rs:

extern crate base;
pub struct Foo;
impl<T> base::Base<Foo> for T {}

bar.rs:

extern crate base;
pub struct Bar;
impl base::Base<T> for Bar {}

With <Bar as base::Base<Foo>> being ambigious.

[nikomatsakis]

Some relevant comments from @arielb1 on IRC: https://botbot.me/mozilla/rust-internals/2014-12-03/?msg=26759795&page=7

[nikomatsakis]

I thought this through. I am mildly uncomfortable with @arielb1's proposed rules in that I do not expect the ordering of type parameters to be significant (which is not to say that those rules would not solve the problem). @aturon and I worked through some examples and we felt like these rules captured our intution reasonably well:

Local(Trait<T2...Tn> for T1) =
    Trait is local || (
       exists i. Local(Ti) &&
       forall i. Ti is not a type parameter
    )
Local(Type<T1...Tn>) =
    Type is local || (
       exists i. Local(Ti) &&
       forall i. Ti is not a type parameter
    )

This can be summarized as "type parameters can only appear as parameters of a local type/trait". This seems to cover the various cases I can think of. I have not tried to prove it sound but I believe it is. Of course I thought that before. :) Once I've had some more coffee, I might take a crack at that, seems like it should be a simple inductive exercise.

[arielb1]

@nikomatsakis

The version you wrote is broken:

// Crate a:
struct A;
impl<T> Base for Pair<Option<T>, Option<A>> {}
// Crate b:
struct B;
impl<T> Base for Pair<Option<B>, Option<T>> {}

Which follows the rules, as Option<T> isn't a type parameter (it just contains one).

A working variant is my second version of the rule: let ≺ be the partial order on nodes in a trait-ref generated by Trait ≺ Self ≺ Tᵢ in the trait-ref 〈Trait〈Tᵢ〉 for Self〉, Type ≺ Tᵢ in a type Type〈Tᵢ〉, then for every type parameter node Q in the trait-ref there exists a local node L such that L ≺ Q.

[nikomatsakis]

@arielb1 that does not follow the rules because of their recursion nature. Note that the Pair type is not local, and neither is Option, and hence the rules recurse in and ultimately reject both impls because of their use of a type parameter.

[nikomatsakis]

(Not to say the rules are perfect, as I said, I have to go back through the list of examples I had and make sure they accept/reject correctly, I'm a bit nervous about the exists vs forall)

[nikomatsakis]

(Or maybe that's the point, perhaps you are correct and I haven't quite formulated the rules the way I wanted them)

[arielb1]

By the way, the partial-order rules in sequent form:

Rule C0:
a crate
T type
T has-no-free-parameters
---------------------------------
a ⊢ T complete

Rule C1:
a crate
T type
a ⊢ T local
---------------------------------
a ⊢ T complete

Rule T0:
a crate
Q unsubstituted-type
Q defined-in a
∀i. Pᵢ type
---------------------------------
a ⊢ Q〈Pᵢ〉 local

Rule T1:
a crate
Q unsubstituted-type
∀i. Pᵢ type
∀i. a ⊢ Pᵢ complete
∃i. a ⊢ Pᵢ local
---------------------------------
a ⊢ Q〈Pᵢ〉 local


Rule R0:
a crate
Tr unsubstituted-trait
∀i. Pᵢ type
S type
Tr defined-in a
---------------------------------
〈Tr〈Pᵢ〉 for S〉 local

Rule R1:
a crate
Tr unsubstituted-trait
∀i. Pᵢ type
S type
a ⊢ S local
---------------------------------
〈Tr〈Pᵢ〉 for S〉 local

Rule R2:
a crate
Tr unsubstituted-trait
∀i. Pᵢ type
S type
a ⊢ S complete
∀i. a ⊢ Pᵢ complete
∃i. a ⊢ Pᵢ local
---------------------------------
〈Tr〈Pᵢ〉 for S〉 local

[nikomatsakis]

I created btw a repository for experimenting with rules and their effects on various scenarios:

https://github.com/nikomatsakis/orphan

[brson]

1.0 P-backcompat-lang

[nikomatsakis]

The repository now contains an encoding of the rules that I think more accurately captures what I was going for, and has the side benefit of being (afaik) sound. An impl of some trait Trait for some type Type (multidispatch can be considered as a tuple) is legal if:

• Trait is defined in the current crate OR (Type is local AND Type is covered)

A type Type is local if:

• It contains at least one nominal type defined in the current crate

A type Type is covered if:

• All type parameters appear underneath a local type constructor

If you find that textual definition confusing, see the code.

In any case, I think this is a subset of @arielb1's definition (as expected). The reason is that @arielb1's requirement was that, when iterating Trait<Self,T1,...Tn> in pre-order, a local type always appeared before any type-parameter. In these rules, the type parameter must appear underneath a local type, so by definition it appears after the local type in pre-order.

@arielb1 let me know what you think!

[nikomatsakis]

@arielb1 points out that this rule prohibits impl<T> Iterator<T> for Vec<T>, which seems reasonable and mildly useful. ;) He also opened a PR on the orphan repo implementing his order-dependent suggestion. I am coming to the idea that this is the only way to preserve the expressiveness we want.

Note in particular that if we permit

Crate 1: impl<T> Iterator<T> for Foo<T>
Crate 2: impl<A,B> Iterator<Bar<A>> for B

then there is a potential coherence conflict for Iterator<Bar<Foo<T>> for Foo<T>.

However, it may be that we can avoid ordering dependency by permitting "uncovered" type parameters as long as they are covered somewhere. I have to try and prove this.

[nikomatsakis]

An argument in favor of the "must be covered somewhere" is that I think you can always reduce it to an ordered set (pre-order) by reordering the parameters in a given trait/type.

[nikomatsakis]

Never mind, that is truly for one impl. Still, I think the rule is sound, though I haven't written up a full proof (of course, I thought the original was sound too). The intuition is that you will ultimately require a cyclic type to violate it.

[nikomatsakis]

@arielb1 writes a proposed proof of the "all type parameters must be covered" rule in IRC here: https://botbot.me/mozilla/rust-internals/2014-12-12/?msg=27397345&page=5

I haven't read it deeply enough to comment yet.

[arielb1]

Prettier Proof:
Definitions:

Substitution - written as Ty[{Tₖ←Sₖ|k}], substitutes the
parameters Tₖ with the arguments Sₖ. For example,
Option⟨T⟩[T←Vec⟨uint⟩] = Option⟨Vec⟨uint⟩⟩
DefId - same as in rustc
TyDefId - DefId of a type (struct/enum/etc.)
TrDefId - DefId of a trait
Type - same as in rust
Complete Type - a type without free type parameters
TraitRef - ⟨TrDefId⟨T₁, .., Tₖ⟩ for Type⟩

an impl is treated as
∀S₁∀S₂...∀Sₖ BOUNDS→impl(⟨Trait⟨...⟩ for Self⟩[{Tᵢ←Sᵢ|i}]

defid-of(Type) = def-id of the root (e.g.
defid-of(Option(Pair(Foo,Bar⟩⟩) = Option

Type/TraitRef contains-defid DefId : lexical containment

Type/TraitRef contains-type Type : structural containment

Q contains-type Ty is true when there exists a P that
contains-param T, and Q=P[T←Ty].

These 3 overloaded relations will be labeled as
T⪯Q. Of course, T≺Q when T⪯Q and T≠Q.

Lemmas I'm using:

Substitution:
S0: ⪯ is a partial order.
S1: ⪯ respects substitution: if Tᵢ is a parameter, S⪯T and Ty⪯Tᵢ,
then S⪯Ty[Tᵢ←T]
S2: defid-of is preserved by substitution:
if Ty is not a type parameter, then
defid-of(Ty[{Tᵢ←Sᵢ}]) = defid-of(Ty)
S3: If defid-of(Ty)⋠Q, and Ty⪯Q[{Tᵢ←Sᵢ|i}], then
∃Tᵢ. Tᵢ⪯Q ∧ Ty⪯Sᵢ

Combinatorics:
C0: The only finite directed acyclic graph with no vertex
of non-zero indegree is the empty graph.
C1: A subgraph of a directed acyclic graph is also directed and
acyclic
C2: The graph of a partial order is directed and acyclic

Main Theorem:
Let R₁=⟨TrB⟨...⟩ for ...⟩, R₂=⟨TrA⟨...⟩ for ...⟩ be TraitRefs,
U₁...Uₖ, V₁...Vₗ be types, such that
R₁[{Tᵢ←Uᵢ|i}] = R₂[{Tᵢ←Vᵢ|i}].

And, for all i, if Tᵢ⪯R₁, then there exists a
Ty that is not a type parameter, such that Tᵢ⪱Ty⪯R₁ and
defid-of(Ty)⋠R₂, and vice-versa (if Tᵢ⪯R₂, then there exists a
non-type-parameter Ty, such that Tᵢ⪱Ty⪯R₂ and defid-of(Ty)⋠R₁)

Then for no i and j, Tᵢ⪯Rⱼ (neither trait-ref contains
type parameters).

Proof:

Let i be such that Tᵢ⪯R₁. There exists a Ty such
that Tᵢ≺Ty⪯R₁ and defid-of(Ty)⋠R₂.
By the definition of substitition, Tᵢ[{Tᵢ←Uᵢ|i}] = Uᵢ, so
Uᵢ≺Ty[{Tᵢ←Uᵢ|i}]. Ty is not a type parameter, so
defid-of(Ty[{Tᵢ←Uᵢ|i}])⋠R₂. By S3,
there exists a j such that Tⱼ⪯R₁ and Uᵢ≺Ty[{Tᵢ←Uᵢ|i}]⪯Vⱼ,
and we get that ∀i.Tᵢ⪯R₁→∃j.Tⱼ⪯R₂∧Uᵢ≺Vⱼ. By swapping R₁ and R₂, this argument also proves ∀i.Tᵢ⪯R₂→∃j.Tⱼ⪯R₁∧Vᵢ≺Uⱼ.

Let G be the graph of the partial order ≺ restricted to
{Vⱼ|Tⱼ⪯R₁} ∪ {Uⱼ|Tⱼ⪯R₂}. This graph is directed, acyclic, and
finite, and every vertex of it has a non-zero indegree (by
the previous paragraph), so it is empty.

Q.E.D.

[nikomatsakis]

I implemented this check. Interestingly, like so many things I have in progress, it seems to be somewhat blocked on associated types, in that the Hash impls are not legal otherwise:

impl<S, T:Hasher<S>> Hash<S> for Type<T> { ... }

S here is uncovered. (You could rewrite this pattern so that Type takes S as a parameter as well.)

For now I plan to land the new check with a (deprecated) feature-gate that disables it, so that old code can continue to work until everything else is in place.

[nikomatsakis]

This is the actual example where I encountered a problem:

impl<S: hash::Writer, Sized? T: Hash<S>> Hash<S> for Box<T>

[nikomatsakis]

Another interesting example that fails (from libgraphviz):

impl<'a, T: PartialEq, Sized? V: AsSlice<T>> Equiv<V> for MaybeOwnedVector<'a, T>

This seems to be a pattern that is just inexpressible?

(That is, relating a local type to any type that implements some trait).

[arielb1]

These do work with the "privileged self" variant of the order-based rules. Maybe we can find a mix of the covering-based and ordering-based rules that supports this?

[nikomatsakis]

I updated the issue to better highlight what remains to be done, and made a checklist of traits that are still using old_orphan_check for one reason or another.

[aturon]

Nominating to move to P-backcompat-libs.

This will largely go away with the stabilization of std::borrow (which is currently blocked) but there are a couple other instances lurking.

[pnkfelix]

P-backcompat-libs, 1.0 beta.