New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implied bounds, second take #82

Merged
merged 10 commits into from Feb 8, 2018

Conversation

Projects
None yet
2 participants
@scalexm
Copy link
Collaborator

scalexm commented 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.

@scalexm scalexm referenced this pull request Feb 5, 2018

Closed

Add implied bounds #56

@nikomatsakis
Copy link
Member

nikomatsakis left a comment

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

@@ -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)),

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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

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

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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

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

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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

This comment has been minimized.

@scalexm

scalexm Feb 6, 2018

Author Collaborator

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.

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

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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

This comment has been minimized.

@scalexm

scalexm Feb 6, 2018

Author Collaborator

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.

@@ -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(),

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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").

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

(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.)

This comment has been minimized.

@scalexm

scalexm Feb 6, 2018

Author Collaborator

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.

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

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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

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

This comment has been minimized.

@nikomatsakis

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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

type Value;
}

impl Bar for i32 {

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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

type Value;
}

impl<K> Foo for Set<K> {

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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


// 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(..) => (),

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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.

This comment has been minimized.

@scalexm

scalexm Feb 6, 2018

Author Collaborator

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

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

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

This comment has been minimized.

@nikomatsakis

nikomatsakis Feb 6, 2018

Member

Can we put a more explicit comment then? =)

@nikomatsakis

This comment has been minimized.

Copy link
Member

nikomatsakis commented 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.

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

@nikomatsakis

This comment has been minimized.

Copy link
Member

nikomatsakis commented 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:

// `T: Foo<U = Bar>` -- projection equality
<s:Ty> ":" <t:Id> "<" <a:(<Comma<Parameter>> ",")?> <name:Id> <a2:Angle<Parameter>>
"=" <ty:Ty> ">" =>
{
let mut args = vec![Parameter::Ty(s)];
if let Some(a) = a { args.extend(a); }
let trait_ref = TraitRef { trait_name: t, args: args };
let projection = ProjectionTy { trait_ref, name, args: a2 };
WhereClause::ProjectionEq { projection, ty }
},

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.

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

1 check passed

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

@scalexm scalexm referenced this pull request Jun 12, 2018

Open

🔬 Tracking issue for RFC 2089: Implied bounds #44491

0 of 3 tasks complete
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment