Skip to content

Commit 6863ff1

Browse files
committed
Add missing last element of a coinductive cycle
1 parent 82ed96b commit 6863ff1

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

src/solve/solver.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,12 @@ impl Solver {
136136
// if all the components of the cycle also have coinductive semantics, we accept
137137
// the cycle `(?0: AutoTrait) :- ... :- (?0: AutoTrait)` as an infinite proof for
138138
// `?0: AutoTrait` and we do not perform any substitution.
139-
if self.stack.iter().skip(index).all(|s| s.goal.is_coinductive(&*self.program)) {
139+
if self.stack.iter()
140+
.skip(index)
141+
.map(|s| &s.goal)
142+
.chain(Some(&goal))
143+
.all(|g| g.is_coinductive(&*self.program))
144+
{
140145
let value = ConstrainedSubst {
141146
subst: Substitution::empty(),
142147
constraints: vec![],

0 commit comments

Comments
 (0)