rust-lang / chalk

An implementation and definition of the Rust trait system using a PROLOG-like logic solver
https://rust-lang.github.io/chalk/book/
Other
1.85k stars 182 forks source link

Implement GATs #116

Closed scalexm closed 6 years ago

scalexm commented 6 years ago

Step 1

The grammar needs to be extended to support bounds and (quantified) where clauses on associated types like in:

trait Foo {
    type Item<'a, T>: Clone where Self: Sized;
}

The grammar is located parser.lalrpop, and the AST in ast.rs.

When this is done, this item: https://github.com/rust-lang-nursery/chalk/blob/eeb21829c1e847921261ad820b5b2ec35b649c76/chalk-parse/src/parser.lalrpop#L204-L207 won't be needed anymore because we will be using QuantifiedWhereClauses everywhere.

We would also remove where clauses on associated type values because they are useless: https://github.com/rust-lang-nursery/chalk/blob/eeb21829c1e847921261ad820b5b2ec35b649c76/chalk-parse/src/parser.lalrpop#L104-L111

Step 2

Currently, a where clause of the form where T: Foo<Item = U> translated to a single domain goal ProjectionEq(<T as Foo>::Item = U). We would need this clause to be translated to two distinct domain goals:

Currently, we cannot translate one AST where clause to multiple IR domain goals. This means that the following trait: https://github.com/rust-lang-nursery/chalk/blob/eeb21829c1e847921261ad820b5b2ec35b649c76/src/lower/mod.rs#L437-L439 should be changed into something like:

trait LowerWhereClause<T> {
    fn lower(&self, env: &Env) -> Result<Vec<T>>;
}

Step 3

Now we should be in a position where we can implement the various rules written in this comment (niko's comment just below can be ignored, it was basically merged into the main one). This includes:

Note: the organization of these two files will change after #114 is fixed, so the preceding text may become obsolete.

Step 4

At that point, the domain goal WellFormed(ProjectionEq) will be unused. See #115 for the next steps.

cc @rust-lang-nursery/wg-traits

scalexm commented 6 years ago

Follow-up (should be straightforward): support quantified bounds on GATs, both in the grammar and in the rules, e.g.

trait Foo {
    type Item<V>: forall<'a> Fn(&'a V);
}
scalexm commented 6 years ago

(Reopening because of the follow-up)