coinduction semantics in the recursive solver

[nikomatsakis]

The recursive solver introduced by @flodiebold in #351 isn't handling coinduction correctly. A number of the tests have "FIXME" results. (See comment.)

This issue has been assigned to @zaharidichev via this comment.

[zaharidichev]

@rustbot claim

[nikomatsakis]

So I described in high-level terms the way I think we should implement this. It builds on the way that the recursive solver handles cycles now.

How inductive solver works

The basic structure for handling cycles in the recursive solver is "iterate until we reach a fixed point". For inductive cycles, I think the mental model is that we are "discovering more and more answers". Therefore we have a kind of lattice that works like this (values begin at the first entry and move towards the final one):

• Error (zero answers)
• Some unique answer with a substitution; I'll write this as Unique(T) but the idea is really that there is Unique(S) where S is some substitution like [V0 = T0, ..., Vn = Tn] where V0..Vn are the input variables from the goal
• Ambiguous (multiple answers, or answers that may or may not be true because of floundering)

We start out with the result of error (i.e., no answers) and then we try to solve the goal via all the "routes" available to us (i.e., applying each possible program clause). Each clause might have back an answer in the form above. If for example we have two clauses, and we get back Error from one and Unique(Vec<u32>) from the other, then the answer would be Unique(Vec<u32>). Similarly, if any clause gives back Ambiguous, then the result is always ambiguous.

If multiple clauses give back answers, though, things can be a bit more complicated. If the answers are "incompatible", then the result is just ambiguous: so if our two clauses gave back u32 and i32, then we can't find a single unique answer that encompasses both of them (but which doesn't also encompass other things). That is, we couldn't summarize as ?T, because that would be overly general.

There are also cases where neither is more general than the other. For example, consider two answers like (?T, u32) and (u32, ?U). Both are instantiations of the other, but neither is strictly more general. We have to return ambiguous for this, because (?T, ?U) would admit too many answers, and (u32, u32) would be too narrow.

But sometimes you have cases where there are two answers, but one of them is an "instantiation" of the other. The easiest to see is that one answer might be Unique(u32) but the other would be Unique(?T) -- i.e,. in one case we proved that it's true for any ?T. In that case, u32 is clearly just some instance of that. We can therefore pick Unique(?T) as the solution.

Change the starting value for coinductive goals

So to make this work for coinductive goals like (say) Foo<?T>: Send, you basically just change the starting value. The intuition is that we start out assuming that the goal is provable, and we are looking for evidence that it is not.

The actual process remains unchanged otherwise: we start with a different starting value, but then we look for solutions from the various clauses and combine them in the same way, in order to find the most general solution. Then we check whether we've reached a fixed point and, if not, we iterate again. (If we ever reach an ambiguous result, we can stop immediately, and indeed we must do so for various obscure reasons.)

Mixed inductive/co-inductive cycles

One weird case to be careful of are mixed inductive/co-inductive cycles. I think the correct handling there is that if we see a cycle that terminates on a co-inductive goal, but there are inductive goals on the stack, then this is always an error, regardless of what the saved value is.

This means for example that if you have something like

impl<X: Debug> Send for Foo<X> { }
impl<X> Debug for Foo<X> where Foo<X>: Send { }

then we would get an error. This is because we get a stack like

• Foo<X>: Send requires
• Foo<X>: Debug requires
• Foo<X>: Send which is a mixed cycle, so we return error (which propagates back up).

I would like to write a better argument for what's going on here, but for now I'll leave it at this.

(Question: should we always fail on a 'mixed stack' regardless of which is the 'head goal'?)

Edits in the code that are needed

I think we need to do two things.

First, we need to remove this logic:

chalk/chalk-solve/src/recursive.rs

Lines 152 to 159 in 1781c43

	let (current_answer, current_prio) = combine::with_priorities_for_goal(
	self.program.interner(),
	&canonical_goal.canonical.value.goal,
	old_answer.clone(),
	old_prio,
	current_answer,
	current_prio,
	);

That logic combines the "old saved answer" with the "new answer we found from the clauses". But this isn't really what we want to do. We actually just want to save the new answer if it's different and then iterate, we don't need to combine with the result from a previous iteration. On a quick test locally, I found that removing this logic had no ill-effects.

Second, we need to change the starting value for a given goal depending on whether it is coinductive or not. That starting value is set automatically when the search graph node is created here:

chalk/chalk-solve/src/recursive.rs

Line 245 in 1781c43

let dfn = self.context.search_graph.insert(&goal, depth);

Third, we would I think want to change the combine method for combining solutions. It doesn't currently take into account the idea of one solution being "more specific" than another. This will cause it to yield ambiguity more often. I'm not sure if this will effect any test cases today, but we could probably make some tests that should work but yield ambiguity.

[nikomatsakis]

I started exploring this in https://github.com/nikomatsakis/chalk-ndm/tree/recursive-coinductive -- just the first step I mentioned above. Could be a fine starting point for someone else.

[zaharidichev]

Perfect. I will pick it up then ! Thanks a lot for the help!