# Chalk recursive solver

The recursive solver, as its name suggests, is a logic solver that works "recursively". In particular, its basic structure is a function like:

``````fn(Goal) -> Solution
``````

where the Goal is some canonical goal and the Solution is a result like:

• Provable(S): meaning the goal is provable and it is provably exactly (and only) for the substitution S. S is a set of values for the inference variables that appear in the goal. So if we had a goal like `Vec<?X>: Foo`, and we returned `Provable(?X = u32)`, it would mean that only `Vec<u32>: Foo` and not any other sort of vector (e.g., `Vec<u64>: Foo` does not hold).
• Ambiguous(S): meaning that we can't prove whether or not the goal is true. This can sometimes come with a substitution S, which offers suggested values for the inference variables that might make it provable.
• Error: the goal cannot be proven.

## Recursion: pros and cons

The recursive solver is so-called because, in the process of solving one goal, it will "recurse" to solve another. Consider an example like this:

``````trait A { }
impl<T: A> A for Vec<T> { }
impl A for u32 { }
impl A for i32 { }
``````

which results in program clauses like:

``````forall<T> { Implemented(Vec<T>: A) :- Implemented(T: A) }
Implemented(u32: A)
Implemented(i32: A)
``````

First, suppose that we have a goal like `Implemented(Vec<u64>: A)`. This would proceed like so:

• `Solve(Implemented(Vec<u64>: A))`
• `Solve(Implemented(u64: A))`
• returns `Error`
• returns `Error`

In other words, the recursive solver would start by applying the first rule, which would cause us recursively try to solve `Implemented(u64: A)`. This would yield an Error result, because there are no applicable rules, and that error would propagate back up, causing the entire attempt at proving things to fail.

Next, consider `Implemented(Vec<u32>: A)`. This would proceed like so:

• `Solve(Implemented(Vec<u32>: A))`
• `Solve(Implemented(u32: A))`
• returns `Provable` with no substitution (no variables)
• returns `Provable`

Finally, consider `Implemented(Vec<?X>: A)`. This is more interesting because it has a variable:

• `Solve(Implemented(Vec<?X>: A))`
• `Solve(Implemented(?X: A))`
• finds two viable solutions, returns `Ambiguous`
• returns `Ambiguous`

## Recursion and completeness

One side-effect of the recursive solver's structure is that it cannot solve find solutions in some cases where a traditional Prolog solver would be successful. Consider this example:

``````
#![allow(unused)]
fn main() {
trait A { }
trait B { }

impl<T: A + B> A for Vec<T> { }

impl A for u32 { }
impl B for u32 { }

impl A for i32 { }
impl B for i8 { }
}
``````

In the recursive solver, with a goal of `Implemented(Vec<?X>: A)`, we recursively try to prove `Implemented(?X: A)` and `Implemented(?X: B)`, which are both ambiguous, and we get stuck there.

The SLG solver in contrast starts by exploring `?X = u32` and finds that it works, and then later tries to explore `?X = i32` and finds that it fails (because `i32: B` is not true).