Improve coinduction handling in recursive solver #457
Conversation
Signed-off-by: Zahari Dichev <[email protected]>
typo |
|
@flodiebold do you think you could take a look at this? |
|
It seems fine code-wise, but I don't really know a lot about coinduction or how it works, so probably it would be better if @nikomatsakis can take a look as well. |
zaharidichev
changed the title
There was a problem hiding this comment.
Thanks for doing this! It was really helpful to read. I'm going to take a bit of time and do a review of how the recursive solver works, and in particular to sketch out how I think caching should be working, taking into account the desire to do (a) salsa-style caching and (b) parallel solving and also now (c) getting coinduction correct. I think it might yield a slightly different variation on this approach, but I'm not sure yet.
| @@ -16,10 +16,37 @@ use rustc_hash::FxHashMap; | |||
|
|
|||
| type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>; | |||
|
|
|||
| #[derive(Clone, Debug, PartialEq, Eq)] | |||
There was a problem hiding this comment.
We should add a comment to this struct clarifying its role
| #[derive(Clone, Debug, PartialEq, Eq)] | ||
| pub struct Answer<I: Interner> { | ||
| pub solution: Solution<I>, | ||
| pub delayed_goals: Vec<UCanonicalGoal<I>>, |
There was a problem hiding this comment.
...and we should comment this field especially
| } | ||
| } | ||
|
|
||
| pub fn needs_refinement(&self) -> bool { |
There was a problem hiding this comment.
We should comment this =)
| !self.delayed_goals.is_empty() | ||
| } | ||
|
|
||
| pub fn combine(self, other: Answer<I>, interner: &I) -> Self { |
There was a problem hiding this comment.
Similarly an example would be great here
| @@ -105,7 +132,35 @@ impl<'me, I: Interner> Solver<'me, I> { | |||
| debug!("solve_root_goal(canonical_goal={:?})", canonical_goal); | |||
| assert!(self.context.stack.is_empty()); | |||
| let minimums = &mut Minimums::new(); | |||
| self.solve_goal(canonical_goal.clone(), minimums) | |||
| self.solve_goal(canonical_goal.clone(), minimums).map(|a| { | |||
| assert!(a.delayed_goals.is_empty()); // at this point there should be no delayed goals | |||
There was a problem hiding this comment.
Is this true? In some of the more extreme examples I found that you had to have delayed goals that required iteration even at the root level I think, but maybe that is hapenning in the solve_goal routine...
| }) | ||
| } | ||
|
|
||
| fn refine_answer( |
There was a problem hiding this comment.
Comment: when is this invoked in the process of solving, and what is an example input/output?
There was a problem hiding this comment.
What is goal and what is answer?
| return value.clone(); | ||
| return value.clone().and_then(|a| { | ||
| if a.needs_refinement() { | ||
| self.refine_answer(goal.clone(), a, minimums) |
There was a problem hiding this comment.
It seems like the main role of this routine is to remove "trivial" self-cycles, right? How can those come about here -- i.e., if we are retrieving a value from the cache, would it ever have trivial self-cycles?
| self.apply_solution(free_vars, universes, constrained_subst); | ||
| progress = true; | ||
| } | ||
| } | ||
|
|
||
| solution.is_ambig() | ||
| delayed_goals.extend(answer.delayed_goals); |
There was a problem hiding this comment.
plausibly we might filter out delayed goals here in this step
| binders: goal.clone().canonical.binders, | ||
| }), | ||
| vec![goal], | ||
| )); |
There was a problem hiding this comment.
So I was to think a bit about this -- in particular, I think the recursive solver can handle this case differently than the SLG solver. Unlike the SLG solver, it's ok for intermediate queries in the recursive solver to not get cached (and/or get cached at the end, along with everything else). I have to review how we handle caching and minimums, but I suspect that we want to work towards a setup where the cache itself never has delayed goals, they are always ephemeral things that exist on the stack during solving.
|
@nikomatsakis Thanks a bunch for the feedback. I will address the comments and revise my logic here. If you happen to arrive at any more insights, feel free to share :) |
|
@nikomatsakis I think I am a bit stuck on that. I understand the overall intended approach but have a few questions:
For some reason all of this makes my head hurt at times :) |
|
Closing this. I think we want to go with the alternative approach @nikomatsakis described. |
This change is an attempt to handle coinduction semantics better when solving with the recursive solver. The main idea is that we introduce the concept of solutions with delayed goals that can be refined later. The main concepts behind the approach are borrowed from: https://rust-lang.github.io/chalk/book/engine/logic/coinduction.html Would love to know if I missed something obvious.
Fix: #399
Signed-off-by: Zahari Dichev [email protected]