add basic support for dyn Trait and impl Trait

[nikomatsakis]

Status: @KiChjang is working on the first steps.

---

The goal here is to extend chalk with basic support for dyn Trait and (opaque) impl Trait types. This involves a few steps:

• extend chalk-parser to support dyn and impl syntax, along with the ast
• extending chalk-ir to be able to represent such types
• extending chalk-solve so that when we have to prove something like dyn Foo: Foo, we judge that to be true (similarly impl Foo: Foo) -- blocked on Port DomainGoal matching from rustc #216
• adding tests for cases like
  • unifying dyn Foo with a struct type (error)
  • unifying impl Foo with a struct type (error)
  • checking that dyn Foo: Foo (without any impl)
  • checking that dyn Foo: Bar does not hold
  • checking that impl Foo: Foo (without any impl)
  • checking that impl Foo: Bar does not hold
    • hmm, we're going to have to figure out "auto trait leakage"

This is judged to be a "medium" complex project, suitable for a dedicated beginner. After this work is done, the next step is #203.

[nikomatsakis]

Mentoring instructions for extending chalk-parser

We want to extend the grammar and AST to have dyn and impl types. Those types would basically consist of vectors of these types I think:

chalk/chalk-parse/src/ast.rs

Lines 81 to 86 in 6fd1808

	#[derive(Clone, PartialEq, Eq, Debug)]
	/// An inline bound, e.g. `: Foo<K>` in `impl<K, T: Foo<K>> SomeType<T>`.
	pub enum InlineBound {
	TraitBound(TraitBound),
	ProjectionEqBound(ProjectionEqBound),
	}

[nikomatsakis]

Mentoring instructions for extending chalk-ir

Extending chalk-ir should be relatively straightforward, though there are some interesting raised by it. I think we want to extend the Ty type:

chalk/chalk-ir/src/lib.rs

Line 217 in 6fd1808

pub enum Ty {

to include two new variants, Dyn and Opaque. These probably look like:

enum Ty {
    ...
    Dyn(Vec<QuantifiedWhereClause>), // dyn Trait
    Opaque(Vec<QuantifiedWhereClause>), // impl Trait
}

These are the counterpart to the existing ForAll type:

chalk/chalk-ir/src/lib.rs

Line 244 in 6fd1808

ForAll(Box<QuantifiedTy>),

we then have to adjust the lowering code to lower the AST to them, which would be done "sort of vaguely" like the existing code for ForAll.

Note that these types introduce a level of binder -- this is so that you can represent the (unknown) Self type with a debruijn variable. i.e., something like dyn Foo<Bar> would wind up represented as

Dyn(^0: Foo<Bar>`)

where ^0 represents "debruijn variable with depth 0.

[nikomatsakis]

cc @scalexm -- I forget, how much of this did you do in #200 ?

[nikomatsakis]

(Also, the mentoring instructions here are fairly sketchy, consider it as future work)

[KiChjang]

Has anyone started working on this? If not, I'd like to try and take a stab at this.

[KiChjang]

I've opened #226 to further discuss the issues regarding the implementation on the chalk solver.

[nikomatsakis]

OK, @KiChjang, so what's missing from your PR is that we need to extend the "clause" lowering code. The basic rule that we want to create is that whenever the "self-type" is dyn Foo or impl Foo, we can add a rule that dyn Foo: Foo and impl Foo: Foo.

This would be done in the "clauses" code -- which is the code that takes a goal we are trying to prove and produces the "program clauses" that could be used to do so. Most of this work is done in this function right now:

chalk/chalk-solve/src/clauses.rs

Lines 131 to 140 in df09cc6

	/// Returns a set of program clauses that could possibly match
	/// `goal`. This can be any superset of the correct set, but the
	/// more precise you can make it, the more efficient solving will
	/// be.
	fn program_clauses_that_could_match(
	db: &dyn RustIrDatabase,
	environment: &Arc<Environment>,
	goal: &DomainGoal,
	clauses: &mut Vec<ProgramClause>,
	) {

and in particular I think the first thing we want to do is to extend this case, where we are trying to prove case like Implemented(P0: SomeTrait<P1..Pn>).

chalk/chalk-solve/src/clauses.rs

Line 142 in df09cc6

DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => {

What I think we want to do is to add a new case, right around this "FIXME" line at the end.

In particular, we want to look at the self type and check whether it is a "dyn" or "impl" trait type. If you rebase this PR on master, you'll find a convenient helper on the TraitRef type caller self_type_parameter that you can use for this. The idea would be basically be to match the self-type and -- if it is a dyn or impl type -- then we know we are solving a goal like dyn <Predicates>: ....

These <Predicates> are actually a lambda like exists<Self> { Predicates }. So what we want to do is to replace the Self with the dyn Type -- so that if we had a type like dyn Iterator, we would get predicates like dyn Iterator: Iterator. We can then just push these into the clauses vector.

This isn't as targeted as it could be. For example, if we're being asked for program clauses to solve Implemented(dyn Foo: Bar), we will wind up returning a program clause Implemented(dyn Foo: Foo), which isn't really relevant. But that's ok, it'll get screened out later, and we can tweak how that works later.

[nikomatsakis]

The next step here is #275

[nikomatsakis]

So I think this is basically done. There are some caveats worth keeping in mind. For example, chalk assumes presently that the binders in a dyn/impl Trait are sorted into a canonical ordering. In any case, I'm going to close this, thanks @KiChjang ❤️