# lazy norm funtime

https://github.com/rust-lang/trait-system-refactor-initiative/issues/61

trait Tr<'a> {
    type Assoc;
}

fn outlives<'o, T: 'o>() {}

fn foo<'a, 'b, T: Tr<'a, Assoc = ()>>() {
    outlives::<'b, T::Assoc>();
    // fail to prove `<T as Tr<'a>>::Assoc: 'b` which is `(): 'b`
}

- https://github.com/rust-lang/trait-system-refactor-initiative/issues/63

trait Mirror {
    type Assoc;
}
impl<T> Mirror for T {
    type Assoc = T;
}

fn is_static<T: 'static>() {}

fn test<T>() where <T as Mirror>::Assoc: 'static {
    is_static::<T>();
    // fail to prove `T: 'static` even though there is a
    // `<T as Mirror>::Assoc: 'static` where-bound
    // (which normalizes to `T: 'static`). 
}

- https://github.com/rust-lang/trait-system-refactor-initiative/issues/59

trait StaticTy {
    type Item<'a>: 'static;
}

impl StaticTy for () {
    type Item<'a> = &'a ();
    // WF checking the impl proves `<() as StaticTy>::Item<'a>: 'static`
    // which uses an item bounds to prove that the item bound holds
}

fn foo<T: StaticTy>() { }

fn main() {
    foo::<()>();
    // Have to prove `(): StaticTy`
    //
    // which requires using the impl
    //
    // which requires proving the impl is well-formed, i.e., trait requires are met, and this proof is done inductively (it cannot assume `(): StaticTy` holds), which would lead us to prove this...
    // 
    // * `for<'a> <() as StaticTy>::Item<'a>: 'static`
    // 
    // Three ways to prove that an alias `A` outlives a lifetime `'x`
    // 
    // * all inputs outlive `'x`
    //     * prove `(): 'static` (true) and prove `for<'a> 'a: static` (false)
    // * the trait definition specifies `A` must outlive `'x` **and the trait is implemented**
    //     * prove `(): StaticTy` (inductive cycle)
    // * normalizing `A` to a type `T` and showing that `T` outlives `'x`
    //     * can normalize with impl to `&'a ()` but then must show that `for<'a> &'a (): 'static` (false)
    //     
    // Question: but is it ok to skip proving `(): StaticTy` (and hence that impl is WF) in that final step? If not, we would get trivial cycles all the time, which seems bad.
    //
    // Seems like we require that...
    // * Normalizing an assoc type does NOT require showing the trait is WF?
    // * Or do we do "1-step normalizing"
    // 
    // https://github.com/rust-lang/a-mir-formality/blob/13b4ad847d609142f92948656e32d5790d0bc28a/crates/formality-prove/src/prove/prove_wc.rs#L51-L62
    //
    // line 58: when proving the where-clauses on the impl hold, it can use the coinductive assumptions
    //
    // line 59: when proving the trait where-clauses hold (i.e., impl is well-formed), it does not
    //
    // (should extend a-mir-formality with this precise case)
}

longterm:

Using an impl requires proving all where bounds and item bounds of the trait inductive (everything which can be used as an alias bound, has to be proven)

- wf check - hopefully - also has to prove `WF(<() as StaticTy>::Item<'a>: 'static)`
- `WF(<() as StaticTy>::Item<'a>)`
- ... I would like us to prove `&'a (): 'static`. but why