# new cycle semantics

## relevant docs

- https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w
- https://hackmd.io/nwRk504pQQ2qUPr87HXkWQ

ideal layout (also for dev-guide)
- what are cycles, when do they occur (examples)
- sometimes cycles should be productive and "hold"
- must not always be the case
- underlying model
- specifically: two exception
- asdj,hsedfedf

When checking trait bounds, we frequently have cyclic dependencies. There are multiple places where these are allowed implicitly:

enum List<T> {
    Nil,
    Cons(T, Option<Box<List<T>>),
}

impl<T: Clone> Clone for List<T> {
    fn clone(&self) -> List<T> {
        mach self {
            List::Nil => List::Nil,
            List::Cons(value, cons) => {
                // `cons.clone()` requires `List<T>: Clone`
                // and is used as part of the "proof object" for
                // `List<T>: Clone`.
                List::Cons(value.clone(), cons.clone()),
            }
        }
    }
}

## what

The underlying idea:

- to prove a goal, we build a proof tree
- this proof tree is a potentially infinite directed, acyclic graph
- all finite branches hold
- infinite branches hold only as long as they have an infinite amount of productive steps
- a productive step is "recursing into an impl", i.e. proving the where-clauses of impls

Why is this meassure of productivity appropriate:
- when we state that some trait bound - e.g. `List<T>: Clone` - holds, we promise that we're able to resolve all its associated items.
- if these associated items rely on other associated items, these can also be provided at every step of the (potentially infinite) chain
- if you're unable to get an impl to resolve an associated item at some point, shit's broken

### Non-productive cycles

While these rules will result in most cycles being productive, there will still be some cycles we have to treat as unproductive.

#### Normalization

trait Trait {
    type Assoc;
}
impl<T> Trait for T {
    type Assoc = <T as Trait>::Assoc;
}

- `normalizes_to(<T as Trait>::Assoc, u32)`
- `<T as Trait>::Assoc eq u32`
- `normalizes_to(<T as Trait>::Assoc, u32)` unproductive cycle ERROR

TODO: we could weaken the requirement to consider normalizes-to steps which normalize the associated type to a rigid type to be productive. However, these cycles would require infinitely sized types which we do not want to exist.

We do still want cycles involving normalization to be productive:

trait Trait {
type Assoc;
}

impl Trait for i32 {
type Assoc = <u32 as Trait>::Assoc;
}

impl Trait for u32
where
i32: Trait<Assoc = ()>,
{
type Assoc = ();
}

- `normalizes_to(<i32 as Trait>::Assoc, ())`
  - `equate(Alias<u32>, ())`
    - `normalizes_to(<u32 as Trait>::Assoc, ())`
      - `equate((), ())` ok
      - `i32: Trait` ok
      -  `normalizes_to(<i32 as Trait>::Assoc, ())` cycle

The cycle steps through a where-clause, allowing this to be 

#### Proving implications

- prove `T: Trait` via `for<T: Trait> T: Trait` in env
    - requires `T: Trait` unproductive cycle ERROR

This is necessary as we could otherwise prove all trait bounds. `for<T: Trait> T: Trait` does hold
- instantiate binder: prove `!T: Trait` with `!T: Trait` in env
    - trivial

Note that while proving an implication may not rely on an impl, it is impossible to use an implication in the empty environment without proving its antecedent in the empty environment, at which point it can only be discarded via an impl.

### Implied assumptions

This approach is unsound wrt to implied assumptions. we currently have these in two cases.

#### super trait elaboration for where-bounds

trait Magic: Copy {}
// Given that one is able to assume `T: Copy` from a
// `T: Magic` where-bound, both the impl and `fn copy_from_magic`
// compile successfully.
impl<T: Magic> Magic for T {}
fn copy_from_magic<T: Magic>(x: T) -> (T, T) {
(x, x)
}

fn main() {
// This means that we need to error here!
copy_from_magic::<String>();
}

- `String: Magic`
    - impl
        - where-bound `String: Magic`: cycle, should be OK

To error when using `copy_from_magic`, we need to check `String: Copy` at this point. To do so, we prove all super-trait constraints of `Magic` whenever we use an impl.

If we prove `T: Magic` using a where-bound we need to prove `T: Magic` when using the item. To use an item with a `T: Magic` bound in an empty environment, we need to discard this bound via an impl at some point.

#### alias bounds

trait Trait {
type Assoc: Copy
where
Self: Trait;
}

impl<T> Trait for T {
// Proving `T: Copy` while being able to assume `T: Trait`
// and therefore `<T as Trait>::Assoc: Copy` can be made to
// fail, but feels highly dangerous.
type Assoc = T
where
Self: Trait;
}

fn copy_via_alias_bound<T: Trait>(x: T::Assoc) {
drop(x);
drop(x);
}

fn copy_via_alias_bound_hidden<T: Trait>() {
let x: Option<T::Assoc> = None;
drop(x);
drop(x);
}

fn main() {
let x = String::new();
copy_via_alias_bound::<String>(x);
}

To handle this case, we also prove all item bounds when applying an impl. This requires us to prove implications when handling GATs. Similar to the general case of implications, while we could prove the antecedent using the environment, at some point this assumption will need to be proven in the empty environment, which will only be able to use an impl. Using item bounds should require proving that the trait is implemented?

For the above example, `fn main` proves `String: Trait`, which should not hold:
- `String: Trait` via impl
  - `String: Trait => <String as Trait>::Assoc: Copy` non-productive step
    - assume `String: Trait`, prove `<String as Trait>::Assoc: Copy`
      - proving `<String as Trait>::Assoc: Copy` via normalization fails
      - proving via alias-bound requires proving `String: Trait`
        - ??? how does this actually fail?

Do we have to prove the where-bounds of the aliases itself non-productively? we can't, it's GATs.


TODO: How to handle opaque types.


## changes from the status quo

On stable, cycles are only treated as productive - which we currently call coinductive - if all involved goals are `T: Sized`, `T: AutoTrait`, or `WellFormed(T)`. All such cycles will be productive with the proposed approach.

As auto traits and `Sized` have no super traits or associated items, its only nested goals are the where-clauses of the impl. `WellFormed` goals cannot cycle without indirection through some other goal. As all cycles need to therefore include auto traits or `Sized` goals, and the only way these can directly depend on other auto trait or `Sized` goals is via where-clauses, all such cycles will continue to be productive.

### concerns and breakage

- we will need to prove trait where-clauses when normalizing: https://github.com/rust-lang/trait-system-refactor-initiative/issues/80

- projection bounds in super traits may cause non-productive cycles when checking them? needs testing

### "coinduction"?

question mark