- 
                Notifications
    You must be signed in to change notification settings 
- Fork 183
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