Challenges and Solutions for Extending Coinduction: Normalizes-to Goals

proven 1) without relying on 2) for the used impl of `Trait`. ```rust trait Trait: SuperTrait {} impl<T: Trait> Trait for T {} // Keeping the current setup for coinduction // would allow this compile. Uff :< fn sup<T: SuperTrait>() {} fn requires_trait<T: Trait>() { sup::<T>() } fn generic<T>() { requires_trait::<T>() } ``` This is not really fundamental to coinduction but rather an existing property which is made unsound because of it. ##### Possible solutions The easiest way to solve this would be to completely remove 2) and always elaborate `T: Trait` to `T: Trait` and `T: SuperTrait` outside of the trait solver. This would allow us to also remove 1), but as we still have to prove ordinary `where`-bounds on traits, that's just additional work. While one could imagine ways to disable cyclic uses of 2) when checking 1), at least the ideas of myself - @lcnr - are all far to complex to be reasonable. #### `normalizes_to` goals and progress A `normalizes_to` goal represents the requirement that `<T as Trait>::Assoc` normalizes to some `U`. This is achieved by defacto first normalizing `<T as Trait>::Assoc` and then equating the resulting type with `U`. It should be a mapping as each projection should normalize to exactly one type. By simply allowing infinite proof trees, we would get the following behavior: ```rust trait Trait { type Assoc; } impl Trait for () { type Assoc = <() as Trait>::Assoc; } ``` If we now compute `normalizes_to(<() as Trait>::Assoc, Vec<u32>)`, we would resolve the impl and get the associated type `<() as Trait>::Assoc`. We then equate that with the expected type, causing us to check `normalizes_to(<() as Trait>::Assoc, Vec<u32>)` again. This just goes on forever, resulting in an infinite proof tree. This means that `<() as Trait>::Assoc` would be equal to any other type which is unsound. ##### How to solve this **WARNING: THIS IS SUBTLE AND MIGHT BE WRONG** Unlike trait goals, `normalizes_to` has to be *productive*[^1]. A `normalizes_to` goal is productive once the projection normalizes to a rigid type constructor, so `<() as Trait>::Assoc` normalizing to `Vec<<() as Trait>::Assoc>` would be productive. A `normalizes_to` goal has two kinds of nested goals. Nested requirements needed to actually normalize the projection, and the equality between the normalized projection and the expected type. Only the equality has to be productive. A branch in the proof tree is productive if it is either finite, or contains at least one `normalizes_to` where the alias is resolved to a rigid type constructor. Alternatively, we could simply always treat the equate branch of `normalizes_to` as inductive. Any cycles should result in infinite types, which aren't supported anyways and would only result in overflow when deeply normalizing for codegen. experimentation and examples: <https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view> Another attempt at a summary. - in projection eq, we must make progress with constraining the rhs - a cycle is only ok if while equating we have a rigid ty on the lhs after norm at least once - cycles outside of the recursive `eq` call of `normalizes_to` are always fine

This section addresses issues related to `normalizes_to` goals in the context of coinduction. It explains that allowing infinite proof trees with `normalizes_to` goals can lead to unsoundness because projections should normalize to a single type. It provides a code example to demonstrate how this can result in infinite loops and incorrect type equality. It suggests that `normalizes_to` goals need to be 'productive,' meaning the projection should normalize to a rigid type constructor. The section also explores alternative solutions, such as treating the equate branch of `normalizes_to` as inductive and ensuring that cycles result in infinite types.