Auto traits #54

scalexm · 2017-07-11T17:55:07Z

Implement auto traits and negative impls.

For an auto trait AutoTrait, we generate a default impl for each type MyType where MyType: (!)AutoTrait does not unify with an existing positive or negative impl. A default impl will basically retrieve the field types FieldType1<...>, ..., FieldTypeN<...> within MyType and generate the impl:

impl<...> AutoTrait for MyType where FieldType1<...>: AutoTrait, ..., FieldTypeN<...>: AutoTrait

Negative impls do not generate any rule during lowering and are just here to deactivate default implementations (although they can be implemented for any trait, not just auto traits). Negative impls can overlap arbitrarily. Positive and negative impls for a same trait cannot overlap. Negative impls cannot define associated type values.
Goals of the form T: AutoTrait have coinductive semantics. If we encounter a cycle whose all components have coinductive semantics, we accept the cycle as an infinite proof and return Ok without performing any substitution.
The syntax for auto traits is #[auto] trait Send { }

nikomatsakis · 2017-07-12T23:20:52Z

chalk-parse/src/parser.lalrpop

@@ -47,12 +47,17 @@ StructDefn: StructDefn = {
    }
 };

+AutoKeyword: () = "#" "[" "auto" "]";


if you wanted to make auto usable as an identifier, you could do this:

Id: Identifier = { <l:@L> <s:RawIdent> <r:@R> => Identifier { str: intern(s), span: Span::new(l, r), } }; RawIdent: &'input str = { "auto", r"([A-Za-z]|_)([A-Za-z0-9]|_)*", };

Yeah I see, but actually I think #[auto] is fine now :)

scalexm · 2017-07-12T23:35:18Z

src/solve/solver.rs

+            // if all the components of the cycle also have coinductive semantics, we accept
+            // the cycle `(?0: AutoTrait) :- ... :- (?0: AutoTrait)` as an infinite proof for
+            // `?0: AutoTrait` and we do not perform any substitution.
+            if self.stack.iter().skip(index).all(|s| s.goal.is_coinductive(&*self.program)) {


Actually I missed chain(Some(goal.clone())) here, adding that...

nikomatsakis

Looks great! Left a few minor comments.

nikomatsakis · 2017-07-12T23:22:19Z

src/ir/mod.rs

@@ -84,8 +87,11 @@ impl Environment {
    pub fn add_clauses<I>(&self, clauses: I) -> Arc<Environment>
        where I: IntoIterator<Item = DomainGoal>
    {
+        use std::collections::HashSet;


not that I mind, but why not move this to the top of the module?

I'm perfectly ok with moving it to the top. I don't know why but some times I prefer local imports if they're used only at one little place. Not every time though haha.

nikomatsakis · 2017-07-12T23:55:47Z

src/lower/default.rs

+        }
+    }
+
+    fn provide_impl_for(&self, trait_ref: TraitRef, struct_datum: &StructDatum) -> bool {


Nit: let's call this impl_provided_for -- this name makes it sound to me like the fn is going to synthesize an impl

Right, actually I was reading this like "self provide_impl_for struct ?", but I agree this can be confusing.

nikomatsakis · 2017-07-13T00:01:50Z

src/solve/test.rs

+
+        goal {
+            forall<T> {
+                Vec<T>: Send


So this through me for a bit, but I guess it's true because struct Vec<T> { } has no fields

Indeed, but actually this test is not great, I'm going to change that.

scalexm · 2017-07-13T00:29:39Z

src/solve/test.rs

+        // In fact, as soon as there is a field which is referencing `T` with an indirection like `Foo<Bar<T>>`,
+        // we need to add the `WellFormed(T)` because the `if (T: Send)` elaborates `WellFormed(T: Send)` but not
+        // `WellFormed(T)`. This is not an issue, but is maybe a bit inconsistent.
+        goal {


@nikomatsakis so actually I added a comment here, which I think is interesting, and which is why I wanted the WF(T) reverse rules at first.

nikomatsakis · 2017-07-13T00:41:39Z

src/solve/solver.rs

+            if self.stack.iter()
+                         .skip(index)
+                         .map(|s| &s.goal)
+                         .chain(Some(&goal))


Heh. =) Funny oversight. Maybe add a test for this? Maybe not worth it.

Actually I realised that from a correctness point of view, that's the same thing because we already know that there is a cycle starting at index index, so the very first element of our iterator is also our current goal already. Anyway, let's keep it that way :)

scalexm · 2017-07-13T10:07:18Z

Actually the comment I've added on my last commit made me think of something which is not great. Given:

#[auto] trait Send { }
trait Clone { }

struct Clonable<T> where T: Clone { }

struct S<T> where T: Clone {
    data: Clonable<T>
}

// default impl generated:
// impl<T> Send for S<T> where Clonable<T>: Send, WF(Clonable<T>: Send)
//
// WF(Clonable<T>: Send) :- WF(Clonable<T>)
// WF(Clonable<T>) :- WF(T), T: Clone, WF(T: Clone)
// WF(T: Clone) :- WF(T)

we only have:

forall<T> {
    if (WellFormed(T), T: Send, T: Clone) {
        S<T>: Send
    }
}

With implied bounds, it's a bit better:

forall<T> {
    if (WellFormed(T), WellFormed(S<T>), T: Send) {
        S<T>: Send
    }
}

Basically it exposes WF checks for fields.

I don't know if this is a problem, but it feels awkward. I think we shouldn't expand the WF bounds on default implementations? This seems fine because expanding WF bounds on impls is only there to ensure that in things like:

trait SuperTrait { }
trait Trait : SuperTrait { }

impl<T> Foo for MyStruct<T> where T: Trait { }

we correctly check that T implements both Trait and SuperTrait to conclude that MyStruct<T>: Foo. There are no such bounds on default implementations.

As was discussed previously in PR #49, we shouldn't expose WF checks for fields (especially for proving things like S<T>: Send).

nikomatsakis · 2017-07-15T18:31:38Z

@scalexm remind me, are we waiting for any further changes here?

nikomatsakis · 2017-07-15T18:32:24Z

I guess we decided to tweak (or maybe tweak) how we approach the WF rules, right... I remember now =)

scalexm · 2017-07-15T18:43:13Z

@nikomatsakis Removing the WF(FieldType: Send) bounds on default implementations is fine for the moment (I did not push my commit yet, I'll do that within a few hours).

I'll open a second PR later for tweaking WF rules + implied bounds (I think what we discussed on Gitter works pretty well).

scalexm added 10 commits June 29, 2017 10:39

First try for negative impls and auto traits

d0ab9ac

Add documentation and tests

7796360

Add coherence rules

779ae25

Merge branch 'master' into cologic

12baae7

Fix tests and wf for negative bounds

2216603

Change strategy for coinductive semantics

3c66e1d

Add documentation

70f70f5

Disable negative trait bounds

a555776

Change syntax for auto traits

7f34963

Add newline at end of solve/test.rs

d76c379

nikomatsakis reviewed Jul 12, 2017

View reviewed changes

Merge branch 'master' into cologic

82ed96b

scalexm commented Jul 12, 2017

View reviewed changes

Add missing last element of a coinductive cycle

6863ff1

nikomatsakis approved these changes Jul 13, 2017

View reviewed changes

Change a test and some other minor things

4844044

scalexm commented Jul 13, 2017

View reviewed changes

nikomatsakis reviewed Jul 13, 2017

View reviewed changes

Do not expand where clauses for default impls

72e6553

nikomatsakis merged commit 7eb0f08 into rust-lang:master Jul 17, 2017

scalexm deleted the cologic branch July 17, 2017 11:53

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Auto traits #54

Auto traits #54

scalexm commented Jul 11, 2017

nikomatsakis Jul 12, 2017

scalexm Jul 12, 2017

scalexm Jul 12, 2017

nikomatsakis left a comment

nikomatsakis Jul 12, 2017

scalexm Jul 13, 2017

nikomatsakis Jul 12, 2017

scalexm Jul 13, 2017 •

edited

Loading

nikomatsakis Jul 13, 2017

scalexm Jul 13, 2017

scalexm Jul 13, 2017 •

edited

Loading

nikomatsakis Jul 13, 2017

scalexm Jul 13, 2017

scalexm commented Jul 13, 2017

nikomatsakis commented Jul 15, 2017

nikomatsakis commented Jul 15, 2017

scalexm commented Jul 15, 2017

Auto traits #54

Auto traits #54

Conversation

scalexm commented Jul 11, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

scalexm Jul 13, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

scalexm Jul 13, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

scalexm commented Jul 13, 2017

nikomatsakis commented Jul 15, 2017

nikomatsakis commented Jul 15, 2017

scalexm commented Jul 15, 2017

scalexm Jul 13, 2017 •

edited

Loading

scalexm Jul 13, 2017 •

edited

Loading