Closed
Description
Currently we treat cycles (i.e. seeing the same clause twice) as Ambiguous
. However, this is not desirable as in the presence of tautologies like (u8: Foo) :- (u8: Foo)
(which may appear while elaborating clauses à la #12), Chalk will answer Ambiguous
to the query u8: Foo
when u8
does not implement Foo
, whereas we would prefer an error.
We can't treat cycles as errors or else the following query:
trait Foo { }
struct S<T> { }
struct i32 { }
impl<T> Foo for S<T> where T: Foo { }
impl Foo for i32 { }
exists<T> { T: Foo }
would return Unique; substitution [?0 := i32]
whereas it should be ambiguous because there is an infinite family of solutions.
A possible strategy for handling cycles would be to use tabling in order to feed back the cycles and possibly produce new answers until we reach a fixed point, in which case we know that we have all the answers.
Metadata
Metadata
Assignees
Labels
No labels