support "specialized" impls

[nikomatsakis]

This is a step towards full support for specialization (#9). This particular step sidesteps some of the trickier bits of specialization (in particular, it sidesteps the parts related to regions and soundness). The goal is this:

• If we know that impl A specializes impl B, adjust the logic to take that into account.

I'll try to post more detailed mentoring instructions, but here are some high-level notes:

Specialization does not effect whether or not a trait is implemented. Therefore, the "lowering" for an impl ought to be unaffected -- overlapping impls simply mean more than one way to prove the same set of types, and the solver ought to be able to handle that.

The "normalization rules", however, are effected. If you have an impl with a default item:

impl Iterator for Foo<T> {
  default type Item = u32;
}

then we cannot normalize <Foo<T> as Iterator>::Item to u32 unless we know that there is no "more specific" impl that applies.

Moreover, at least in rustc at the moment, we sometimes wish to assume that a more specialized impl could be added in the future. In rustc, we currently distinguish between "reveal mode", at which point we are allowed to normalize a default type, and "normal mode", when we are not.

[nikomatsakis]

The basic idea then is to add a few sorts of domain goals:

• RevealMode
• Overrides[Id](P0: Trait<P1..Pn>) -- where Id is the identity of an associated type value.

We never generate program clauses for RevealMode. Rather, those are inserted into the environment by rustc.

Overrides[Id] would be generated by specializing impls. i.e., imagine this:

impl Iterator for Foo<T> { // impl A
  default type Item = u32; // associated-type-value with id V0
}
impl Iterator for Foo<String> { // impl B
  type Item = char; // associated-type-value with id V1
}

Impl B specializes impl A, so when lowering V0 we would generate a rule like:

forall<T> {
  Normalize(<Foo<T> as Iterator>::Item -> u32) :-
    Reveal,
    not { Overrides[V0](Foo<T>: Iterator) }
}

Lowering V1 we would generate rules like:

Overrides[V0](Foo<String>: Iterator).

Normalize(<Foo<String> as Iterator>::Item -> u32).

Note that since V1 is not declared default, it doesn't add any "criteria" like Reveal etc to do its normalization. The first rule, Overrides[V1], would also disable the rule from impl A.

[nikomatsakis]

As @sunjay pointed out on Zulip, an obvious first step is:

Extend the parser to support default type Foo = Bar inside of an impl; that should be a flag on the associated type value.

[nikomatsakis]

Presently we have code to build a specialization forest:

chalk/chalk-solve/src/coherence.rs

Lines 77 to 78 in 3238c6d

	// Build the forest of specialization relationships.
	fn build_specialization_forest(&self) -> Fallible<Graph<ImplId, ()>> {

In order to figure out which impls specialize which other ones, I think for now we'd probably build on that, but we have to think about how to do it. This gets to a related topic, I realize, which is that I think we want chalk-solve to integrate more closely with salsa and have some query structure of its own. I'll think about that and try to leave a few notes, but that might be a good next step.

[nikomatsakis]

Given that we now have default type Foo = Bar parsing, I think the new steps are:

• Add a RevealMode and Overrides domain goal as described in this comment
• Modify the lowering for default type to include the Overrides clause

These are relatively simple steps but they don't do anything interesting yet. The next step is where things get more exciting. We would want to take the build_specialization_forest logic and -- when we see that impl A specializes impl B -- generate program clauses for that. I'll have to persue the code a bit to decide how that should best work.

[sunjay]

The next steps are described in this paper document.

Summary of next steps:

• Create a specialization_forest(trait_id) query with this code extracted
• Extend RustIrDatabase trait with a specialization_forest() method
  • it can invoke the query we just added
  • might want to change specialization forest to have the actual graph rather than just a map
• Extend the clause generation code to use that method and create Overrides clauses
  • We can iterate over all impls with lower priority than the one we are currently generating clauses for and generate overrides for them

Each of these steps leads to finishing off the unimplemented!() part of my PR #230.

[nikomatsakis]

A note to help me remember:

I was debating if this lowering could lead to a need to handle "negative cycles". In particular, it seems at first glance plausible that a clause like:

forall<T> {
  Normalize(<Foo<T> as Iterator>::Item -> u32) :-
    Reveal,
    not { Overrides[V0](Foo<T>: Iterator) }
}

might wind up recursively dependent on itself (i.e., part of proving Overrides[V0](Foo<T>: Iterator) would require proving Normalize(<Foo<T> as Iterator>::Item -> u32)). But I don't think this should be possible because we first to do a check where Reveal is not provable, and we know that everything can be proven..? But then again we don't have to prove Overrides[V0](Foo<T>: Iterator) in that formulation, I don't think, so maybe that's not correct. Worth trying to create an example here.

[nikomatsakis]

I suppose you could write something sort of self-contradictory like this:

impl Iterator for Foo<T> { // impl A
  default type Item = u32; // associated-type-value with id V0
}

impl Iterator for Foo<String>
where
    Foo<String>: Iterator<Item = u32>,
{ // impl B
  type Item = char; // associated-type-value with id V1
}

In this case, proving that

• Normalize(<Foo<String> as Iterator>::Item -> u32>
• would require proving that not { Overrides[V0](Foo<String>: Iterator) }
• which would require proving that Normalize(<Foo<String> as Iterator::Item -> u32)
• which would require proving that not { Overrides[V0](Foo<String>: Iterator) }
• which is a negative cycle

Ugh, I wonder if we're going to have to extend chalk-engine to handle such cycles correctly after all. Of course, this program ultimately I think wouldn't be expected to compile, and it's hard to imagine such things arising in practice. And maybe it's some kind of special case of negative cycles.

[Aaron1011]

What's the current status of this issue? It looks like some specialization-related methods have been added (build_specialization_forest, visit_specializations_of_trait).

[nikomatsakis]

With respect to my example, I realize now that this setup would probably fail in rustc because we require that there is a DAG between traits with respect to references from specializing impls.