-
Notifications
You must be signed in to change notification settings - Fork 184
Closed
Labels
current-sprintBeing worked on in the current sprintBeing worked on in the current sprint
Description
We should experiment with returning to a "recursive style" solver in chalk. As described in this gist, recursive solving does offer some potential advantages:
- if we extend the setup, it may resolve the ambiguous associated type problem (ironic since we previously removed the recursive solver in part because we couldn't make it handle associated types well)
- less overall work, at the cost of completeness
- cleaner handling for multiple threads doing queries at once without locking (the cache is separated from the main solver stack)
- smoother integration into systems like chalk
Work items:
- Initial PR
- Coinduction semantics coinduction semantics in the recursive solver #399
- Invoke
program_clauses_for_goal
on the canonicalized form vs instantiating the goal first (comment)
This issue has been assigned to @flodiebold via this comment.
Metadata
Metadata
Assignees
Labels
current-sprintBeing worked on in the current sprintBeing worked on in the current sprint