review

Author: lcnr

src/solve/coinduction.md

@@ -57,9 +57,26 @@ As we cannot check for infinite trees, we instead search for patterns for which
 they would result in an infinite proof tree. The currently pattern we detect are (canonical)
 cycles. If `T: Send` relies on `T: Send` then it's pretty clear that this will just go on forever.
 
-With cycles we have to be careful with caching. Due to canonicalization of regions and inference
-variables we also have to rerun queries until the provisional result returned when hitting the cycle
-is equal to the final result.
+With cycles we have to be careful with caching. Because of canonicalization of regions and
+inference variables encountering a cycle doesn't mean that we would get an infinite proof tree.
+Looking at the following example:
+```rust
+trait Foo {}
+struct Wrapper<T>(T);
+
+impl<T> Foo for Wrapper<Wrapper<T>>
+where
+    Wrapper<T>: Foo
+{} 
+```
+Proving `Wrapper<?0>: Foo` uses the impl `impl<T> Foo for Wrapper<Wrapper<T>>` which constrains
+`?0` to `Vec<?1>` and then requires `Wrapper<?1>: Foo`. Due to canonicalization this would be
+detected as a cycle.
+
+The idea to solve is to return a *provisional result* whenever we detect a cycle and repeatedly
+retry goals until the *provisional result* is equal to the final result of that goal. We
+start out by using `Yes` with no constraints as the result and then update it to the result of
+the previous iteration whenever we have to rerun.
 
 TODO: elaborate here. We use the same approach as chalk for coinductive cycles.
 Note that the treatment for inductive cycles currently differs by simply returning `Overflow`.

src/solve/trait-solving.md

@@ -51,7 +51,8 @@ Also add issues where each of these rules have been broken in the past
 ### 1. The trait solver has to be *sound*
 
 This means that we must never return *success* for goals for which no `impl` exists. That would
-simply be unsound by assuming a trait is implemented even though it is not.
+simply be unsound by assuming a trait is implemented even though it is not. When using predicates
+from the `where`-bounds, the `impl` whill be proved by the user of the item.
 
 ### 2. If type checker solves generic goal concrete instantiations of that goal have the same result