Add CannotProve solution
#45
Conversation
src/solve/fulfill.rs
Outdated
| /// Record that a goal has been processed that can neither be proved nor | ||
| /// refuted, and thus the overall solution cannot be `Unique` | ||
| ambiguous: bool, | ||
| cannot_prove: bool, |
There was a problem hiding this comment.
Nit: comment would be good
There was a problem hiding this comment.
Right, I'm changing that.
src/solve/fulfill.rs
Outdated
| } | ||
| }; | ||
|
|
||
| if ambiguous { | ||
| debug!("ambiguous result: {:?}", obligation); | ||
| obligations.push(obligation); | ||
| } | ||
|
|
||
| // If one of the obligations cannot be proven, then the whole goal | ||
| // cannot be proven either. |
There was a problem hiding this comment.
To make sure I understand: We don't stop immediately here because if we were to encounter a hard error somewhere else, that would "override" this cannot prove result, right?
There was a problem hiding this comment.
Yeah exactly. I'm adding a bit of documentation here too. Notice that for the same reason, in the case where the unification set cannot_prove = true, we don't return CannotProve early here:
https://github.com/scalexm/chalk/blob/cannot-prove/src/solve/solver.rs#L214
| @@ -346,7 +346,12 @@ impl<'s> Fulfill<'s> { | |||
| /// the outcome of type inference by updating the replacements it provides. | |||
| pub fn solve(mut self, subst: Substitution) -> Result<Solution> { | |||
| let outcome = self.fulfill()?; | |||
| if outcome.is_complete() && !self.ambiguous { | |||
|
|
|||
| if self.cannot_prove { | |||
There was a problem hiding this comment.
Instead of having a cannot_prove field, can we use a local variable in fulfill() and extend the Outcome enum? In that case, I think we would replace these two ifs with something like:
match outcome {
Outcome::CannotProve => return Ok(Solution::CannotProve),
Outcome::Complete => {
// No obligations remain, so we have definitively solved our goals,
...
return ...; // as before
}
Outcome::Incomplete => { /* fallthrough to figure out some good suggestions */ }
}There was a problem hiding this comment.
Ah, I see that in this case unify would have to return Outcome (or UnifyOutcome). This way is ok too. It feels a bit less direct to me somehow, but maybe some comments would suffice to clear it up.
There was a problem hiding this comment.
Yes and moreover unify is called outside of Fulfill (see previous comment) so unify would still have to change an internal state somehow, so I thought that a flag was lighter.
Added a
CannotProvesolution in order to deal with #44. In particular, unifying a for all variable with something else automatically leads toCannotProve(or error).CannotProvesolutions have the lowest priority when combining multiple solutions.Examples 1 and 2 in this issue are now all treated as
CannotProve. Example 3 is not shown in this PR since this specific issue arises only when elaborating clauses à la #12, but this PR will indeed resolve this ambiguity in the future.