permit context to control subgoal selection order

[nikomatsakis]

The on-demand solver, when faced with an X-clause, currently always selects the "last" literal in the list. This is pretty silly. It would be smarter to look for literals that are closer to being solved, and maybe make some heuristics that look at the traits involved.

I think it might be useful to have a rough idea of the "inputs" and "outputs" from given domain goals (many prologs have modal annotations of this kind, I've not looked deeply at how they work). So for example given this set of pending goals:

NormalizeTo(<T as Bar>::Item -> ?U)
?U: Foo

It would be better to start with the normalization, since otherwise we would wind up enumerating all type variables that implement Foo.

In fact, targeting this scenario is the primary rule we need, I think, given Rust's limitations around constrained type parameters on impls. (Rustc has some similar logic already, actually.)

[nikomatsakis]

This is where we select the next goal to pursue:

https://github.com/rust-lang-nursery/chalk/blob/fa1837ed99260f01f1ad5f1978cc88644f06c9ed/chalk-slg/src/logic.rs#L369-L376

Right now, the SLG solver doesn't really know anything about the content of the domain goals, so we'd probably want to add some sort of callback to let it sort. The simplest thing would be to assign each domain goal a priority -- that would let us put normalizations first -- or perhaps better yet have a way for it to yield up "inputs" and "outputs", so we can build up a kind of DAG.

[leoyvens]

I imagine that if we had a dependency graph for goals, we could have rustc error messages only report the minimal set of obligation failures that need to be fixed for the code to compile.

[nikomatsakis]

We discussed this some on Zulip. The rough design we are thinking of is as follows:

• Extend the InferenceTable trait, or else add a new SelectionOps trait
• It should contain a method fn subgoal_index(&mut self, &ExClause<I>) -> usize that selects the subgoal to process from a given ex-clause

A call to this method would replace this line where we currently just always pick the "last" subgoal:

https://github.com/rust-lang-nursery/chalk/blob/0e30fab937f32294cda00e3e6b2e0811fcbdceba/chalk-engine/src/logic.rs#L487-L494

[KiChjang]

With #193 merged, we have extended InferenceTable to contain a method named next_subgoal_index, but still haven't figured the specifics of which goal to prioritize/deprioritize.

[jackh726]

Status:

This function is now here:

chalk/chalk-engine/src/slg.rs

Line 26 in a3a3e1e

pub(crate) fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize {

We still don't have better logic of strand prioritization though