Implied bounds, second take - #82

scalexm · 2018-02-05T21:38:00Z

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

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

nikomatsakis · 2018-02-05T21:54:12Z

    "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 · 2018-02-06T00:49:37Z

+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 · 2018-02-06T00:50:18Z

        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 · 2018-02-06T01:05:06Z

 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 · 2018-02-06T01:07:24Z

            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 · 2018-02-06T01:10:52Z

+        //
+        //    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 · 2018-02-06T01:11:14Z

+            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 · 2018-02-06T01:12:10Z

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


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

nikomatsakis · 2018-02-06T01:12:35Z

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


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

nikomatsakis · 2018-02-06T01:14:38Z

+
+            // 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 · 2018-02-06T14:11:10Z

@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 · 2018-02-08T09:38:02Z

@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.

…tionEq`

scalexm mentioned this pull request Feb 5, 2018

Add implied bounds #56

Closed

nikomatsakis reviewed Feb 6, 2018

View reviewed changes

scalexm added 5 commits February 6, 2018 16:30

Add implied bounds and WF requirements

a4ddd09

Add tests

9d4f4cb

Add WF requirements for projection types

a640bea

Add documentation

902d344

Add more comments

acd499f

scalexm force-pushed the implied-bounds-ok branch from 05f2322 to acd499f Compare February 6, 2018 19:31

scalexm and others added 4 commits February 6, 2018 21:44

Elaborate implied bounds in if goals

4bac247

fix comment

432c2ec

fix test; we now create some FromEnv goals first I guess

4506e42

WIP add test I expect to pass

91eda35

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

249bd61

…tionEq`

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

scalexm mentioned this pull request Feb 8, 2018

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

Closed

scalexm mentioned this pull request Jun 12, 2018

🔬 Tracking issue for RFC 2089: Extended Implied bounds rust-lang/rust#44491

Open

3 tasks

Conversation

scalexm commented Feb 5, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nikomatsakis left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

scalexm Feb 6, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nikomatsakis commented Feb 6, 2018 • edited by scalexm Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nikomatsakis commented Feb 8, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

scalexm commented Feb 5, 2018 •

edited

Loading

scalexm Feb 6, 2018 •

edited

Loading

nikomatsakis commented Feb 6, 2018 •

edited by scalexm

Loading

nikomatsakis commented Feb 8, 2018 •

edited

Loading