@@ -210,7 +210,15 @@ fn coinductive_unsound1() {
210210
211211 goal {
212212 forall<X > { X : C1orC2 }
213- } yields_all[ SolverChoice :: slg( 3 , None ) ] {
213+ } yields[ SolverChoice :: slg( 3 , None ) ] {
214+ "No possible solution"
215+ }
216+
217+ goal {
218+ forall<X > { X : C1orC2 }
219+ } yields[ SolverChoice :: recursive( ) ] {
220+ // FIXME -- recursive solver doesn't handle coinduction correctly
221+ "Unique; substitution [], lifetime constraints []"
214222 }
215223 }
216224}
@@ -251,7 +259,8 @@ fn coinductive_unsound2() {
251259
252260 goal {
253261 forall<X > { X : C1orC2 }
254- } yields_all[ SolverChoice :: slg( 3 , None ) ] {
262+ } yields {
263+ "No possible solution"
255264 }
256265 }
257266}
@@ -298,8 +307,8 @@ fn coinductive_multicycle1() {
298307
299308 goal {
300309 forall<X > { X : Any }
301- } yields_all [ SolverChoice :: slg ( 3 , None ) ] {
302- "substitution [], lifetime constraints []"
310+ } yields {
311+ "Unique; substitution [], lifetime constraints []"
303312 }
304313 }
305314}
@@ -338,8 +347,8 @@ fn coinductive_multicycle2() {
338347
339348 goal {
340349 forall<X > { X : Any }
341- } yields_all [ SolverChoice :: slg ( 3 , None ) ] {
342- "substitution [], lifetime constraints []"
350+ } yields {
351+ "Unique; substitution [], lifetime constraints []"
343352 }
344353 }
345354}
@@ -388,7 +397,8 @@ fn coinductive_multicycle3() {
388397
389398 goal {
390399 forall<X > { X : Any }
391- } yields_all[ SolverChoice :: slg( 3 , None ) ] {
400+ } yields {
401+ "No possible solution"
392402 }
393403 }
394404}
@@ -439,5 +449,12 @@ fn coinductive_multicycle4() {
439449 forall<X > { X : Any }
440450 } yields_all[ SolverChoice :: slg( 3 , None ) ] {
441451 }
452+
453+ goal {
454+ forall<X > { X : Any }
455+ } yields[ SolverChoice :: recursive( ) ] {
456+ // FIXME -- recursive solver doesn't have coinduction correctly
457+ "Unique; substitution [], lifetime constraints []"
458+ }
442459 }
443460}
0 commit comments