Implied bounds, second take #82

scalexm · Feb 5, 2018

This is a full implementation of implied bounds as well as enforcing WF requirements on impls and type declarations.

The rules for WF requirements on traits are detailed in #12 (and in the code). The rules for types are much more simple (no need for co-recursion but we still have two predicates, WellFormed and FromEnv).

I was not greatly inspired for the tests, so one can feel free to add some more.

Fixes #11 and incidentally some form of bug related to #70. And eventually #12 will be resolved too.

nikomatsakis · Feb 6, 2018

nikomatsakis reviewed Feb 6, 2018

View changes

First round of comments. Will read in more depth tomorrow, especially the accumulator stuff. This is nice! 💯

nikomatsakis · Feb 6, 2018

chalk-parse/src/parser.lalrpop

@@ -29,17 +29,12 @@ pub Goal: Box<Goal> = {
 Goal1: Box<Goal> = {
    "forall" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::ForAll(p, g)),
    "exists" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::Exists(p, g)),
-    <i:IfKeyword> "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, i)),
+    "if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),


I am happy to see if_raw gone, I have to say. That always felt "yucky".

nikomatsakis · Feb 6, 2018

src/solve/test/mod.rs

+fn parse_and_lower_program(text: &str, solver_choice: SolverChoice, skip_coherence: bool)
+    -> Result<ir::Program>
+{
+    if skip_coherence {


It seems like this parameter is just always false? Can we just plain remove this?

nikomatsakis · Feb 6, 2018

src/solve/test/bench.rs

@@ -108,6 +109,7 @@ fn cycley_recursive_cached(b: &mut Bencher) {
        CYCLEY_GOAL,
        b,
        "Unique",
+        true


well I guess it's true here, but not (I take it) for the reasons stated? (why is it true here?)

The recursive solver fails to answer uniquely goals of the form <Bar as Foo>::Assoc: SomeTrait (or WellFormed(<Bar as Foo>::Assoc: SomeTrait)). So this is a temporary hack (de-activing checking WF requirements) so that the benchmark tests pass, but I should add a FIXME or something because this is really not ought to stay.

nikomatsakis · Feb 6, 2018

src/ir/mod.rs

@@ -747,13 +790,19 @@ impl<T> UCanonical<T> {
 }

 impl UCanonical<InEnvironment<Goal>> {
-    /// A goal has coinductive semantics if it is of the form `T: AutoTrait`.
+    /// A goal has coinductive semantics if it is of the form `T: AutoTrait`, or if it is of the
+    /// form `WellFormed(T: Trait)` where `Trait` is any trait. The latter is needed for dealing


I am mildly surprised that we don't want to just make all WellFormed goals coinductive. But I guess it's only needed for traits...

Well types only have where clauses of the form T: Trait, there are no WF(Type) where clauses so you never have the kinds of cycles encountered with traits.

nikomatsakis · Feb 6, 2018

src/lower/mod.rs

@@ -445,6 +447,10 @@ impl LowerWhereClause<ir::DomainGoal> for WhereClause {
            WhereClause::TraitRefWellFormed { ref trait_ref } => {
                ir::WellFormed::TraitRef(trait_ref.lower(env)?).cast()
            }
+            WhereClause::TyFromEnv { ref ty } => ir::FromEnv::Ty(ty.lower(env)?).cast(),


I am torn on the question of what this should mean:

if (T: Trait) { .. }

I am thinking maybe we should make that equivalent to if (FromEnv(T: Trait)) { .. } and then have an explicit form if (Implemented(T: Trait)) { .. }. Basically T: Trait would parse to an AST form whose expansion depends on whether it appears in a "clause" (in which case it is FromEnv) or a Goal (in which case it is "Implemented").

(That said, I'm not really sure when we would want to say if (Implemented(T: Trait)) { ... }.. but maybe it's useful when crafting unit tests or something.)

Yeah not really sure either, but I think converting to FromEnv(T: Trait) in clauses is a good thing, and the explicit goal Implemented would replace the former if_raw statement in a much nicer way.

nikomatsakis · Feb 6, 2018

src/lower/mod.rs

+        //
+        //    forall<T> {
+        //        Normalize(<T as Foo>::Assoc -> U) :- FromEnv(T: Foo<Assoc = U>)
+        //    }


As an aside, and not for this PR, I wonder if we can use macros to make this code less tedious to write.

nikomatsakis · Feb 6, 2018

src/lower/test.rs

+            impl<T> A for T where T: B {}
+        } error_msg {
+            "trait impl for \"B\" does not meet well-formedness requirements"
+        }


(maybe we should add a test where this succeeds?)

nikomatsakis · Feb 6, 2018

src/lower/test.rs

+                type Value;
+            }
+
+            impl Bar for i32 {


Maybe add a comment here: this fails because i32: Foo does not hold

nikomatsakis · Feb 6, 2018

src/lower/test.rs

+                type Value;
+            }
+
+            impl<K> Foo for Set<K> {


Here, Wf(Set<K>) implies K: Hash and hence OnlyEq<K> is WF

nikomatsakis · Feb 6, 2018

src/lower/wf.rs

+
+            // Type parameters and higher-kinded types do not carry any input types (so we can sort
+            // of assume they are always WF).
+            Ty::Var(..) | Ty::ForAll(..) => (),


Hmm, Ty::ForAll corresponds to for<'a> fn(&'a u32) or some such. I don't know that we can assume they are always WF. I think this accumulator probably doesn't want to accumulate into a vector, but rather to invoke a callback, because in the case of for<'a> we may want to create subuniverses? I have to read this code a bit more carefully I guess.

Actually we discussed that and for some reason we decided that higher-kinded types are always WF. This is similar to the fact that if we have this kind of function:

fn foo<T>(arg: HashSet<NotHash<T>>) { ... }

we would not issue any error until the function is called. For lifetime parametric function types, again an error would be issued only if a function of this type is ever called. We discussed that in our dropbox paper (see 2017.07.25).

Oh, right, I forgot about that. Basically we were assuming that for all types introduce their own implied bounds, right? Makes sense.

Can we put a more explicit comment then? =)

nikomatsakis · Feb 6, 2018

@scalexm ok so the changes to make then are:

add an explicit Implemented(T: Trait) in the AST
change T: Trait to lower to FromEnv in a clause
add a few comments:
- some in the tests
- but most importantly on the treatment of ForAll

Do you think you'll have time for that? Do you want me to do it? We should probably make more tests but I'm not inclined to block on that.

nikomatsakis · Feb 8, 2018

@scalexm

I read over the changes more thoroughly. Everything looks great. I looked briefly at the on-demand test was failing; for some reason it is now creating FromEnv tables (which fail to get proven). This is not unexpected, since you changed the program clauses. Seems fine.

However, I did notice one thing. It seems like you are treating T: Iterator<Item = U> as a "normalize" rule, but in fact it parsed as a "projection equality" rule:

https://github.com/rust-lang-nursery/chalk/blob/4defa33befbffd9239c5c293f3e56ec4e8fd810e/chalk-parse/src/parser.lalrpop#L201-L210

The intention is that "projection eq" is the "normal" rule, with Normalize being something that only comes from impls (i.e., trans could use it to find the "true" type).

Anyway, I pushed a final commit with a test that fails as a result -- but I think is expected to pass.

scalexm referenced this pull request Feb 5, 2018
Closed
Add implied bounds #56

scalexm added some commits Jan 25, 2018

Add implied bounds and WF requirements

a4ddd09

Add tests

9d4f4cb

Add WF requirements for projection types

a640bea

Add documentation

902d344

Add more comments

Loading status checks…

acd499f

scalexm force-pushed the scalexm:implied-bounds-ok branch from 05f2322 to acd499f Feb 6, 2018

Change `WellFormed/FromEnv::Normalize` to `WellFormed/FromEnv::Projec…
…tionEq`

Loading status checks…

249bd61

nikomatsakis merged commit 4f007d9 into rust-lang:master Feb 8, 2018
1 check passed

1 check passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details

scalexm referenced this pull request Feb 8, 2018
Closed
StreamingIterator code panics with "zipping things of mixed type" #70

scalexm referenced this pull request Jun 12, 2018
Open
🔬 Tracking issue for RFC 2089: Implied bounds #44491
0 of 3 tasks complete

rust-lang/chalk

Implied bounds, second take #82

Implied bounds, second take #82

scalexm commented Feb 5, 2018 •

edited

scalexm referenced this pull request Feb 5, 2018

Add implied bounds #56

nikomatsakis reviewed Feb 6, 2018

View changes

nikomatsakis left a comment

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

nikomatsakis commented Feb 6, 2018 •

edited by scalexm

scalexm added some commits Jan 25, 2018

scalexm force-pushed the scalexm:implied-bounds-ok branch from `05f2322` to `acd499f` Feb 6, 2018

scalexm and others added some commits Feb 6, 2018

This comment has been minimized.

nikomatsakis commented Feb 8, 2018 •

edited

nikomatsakis merged commit `4f007d9` into rust-lang:master Feb 8, 2018
1 check passed

1 check passed

scalexm referenced this pull request Feb 8, 2018

StreamingIterator code panics with "zipping things of mixed type" #70

scalexm referenced this pull request Jun 12, 2018

🔬 Tracking issue for RFC 2089: Implied bounds #44491

rust-lang/chalk

Join GitHub today

Implied bounds, second take #82

Conversation

scalexm commented Feb 5, 2018 • edited

scalexm referenced this pull request Feb 5, 2018

nikomatsakis reviewed Feb 6, 2018 View changes

nikomatsakis left a comment

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

scalexm Feb 6, 2018 • edited

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

nikomatsakis commented Feb 6, 2018 • edited by scalexm

scalexm added some commits Jan 25, 2018

scalexm force-pushed the scalexm:implied-bounds-ok branch from 05f2322 to acd499f Feb 6, 2018

scalexm and others added some commits Feb 6, 2018

This comment has been minimized.

nikomatsakis commented Feb 8, 2018 • edited

Hide details View details nikomatsakis merged commit 4f007d9 into rust-lang:master Feb 8, 2018 1 check passed

1 check passed

scalexm referenced this pull request Feb 8, 2018

scalexm referenced this pull request Jun 12, 2018

scalexm commented Feb 5, 2018 •

edited

nikomatsakis reviewed Feb 6, 2018

View changes

scalexm Feb 6, 2018 •

edited

nikomatsakis commented Feb 6, 2018 •

edited by scalexm

scalexm force-pushed the scalexm:implied-bounds-ok branch from `05f2322` to `acd499f` Feb 6, 2018

nikomatsakis commented Feb 8, 2018 •

edited

nikomatsakis merged commit `4f007d9` into rust-lang:master Feb 8, 2018
1 check passed