---
# System prepended metadata

title: Shallow Subtyping Ahoy

---

# Shallow Subtyping Ahoy

## Current goals

### Active

* Remove universe logic from NLL
    - current step is:
        - https://github.com/rust-lang/rust/pull/97641/
    - next step is:
        - move the projection logic into fulfill path so that we only produce
            - type parameters
            - regions
        - then we can remove a lot of the "outlives" code
    - next step is:
        - handle type parameters and regions in fulfill by searching parameter bounds etc
        - we can remove the "outlives" code entirely
        - and NLL no longer has to think about higher-ranked stuff
            - can remove universes from NLL* niko to think about how new subtyping algorithm coallesces of lifetime edges and model in a-mir-formality

### Deferred and upcoming

* extend param-env with new facts as we enter closure, thread param-env through as we add things to fulfillment context so that it affects outlives obligations in a natural way
* `coerce-unsized` refactoring (oh dear god)
* `fudge_inference_if_ok`
    * do some experiments on it and document them!
        * replace with `commit_if_ok`
        * remove trait solving
        * ... 
    * ignoring for now
* remove trait solving from diagnostics code  and use evaluation instead

## 2023-02-20

https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view#cycle-outside-of-eq-OK

```
WC = Atom
   | WC => WC
   | WC and WC
   | forall X. WC
  
Atom = Trait({Ty})
     | Ty = Ty
     | Ty : Ty
     
Goal = WC
     | All({Goal})
     | Any({Goal})
     | WC => Goal // <--
     | not Goal.
     | coherence-mode Goal
     | exists X. Goal
     | forall X. Goal
     
Prog = (Trait, Impl)
Impl = 
```

```rust!
trait Eq: PartialEq {}

// Eq(X) => PartialEq(X) -- nonproductive 

impl<T: ?Sized> Iterator for T {
    type Item = T::X;
}

// (T::X = U) => Iterator::Item = U -- nonproductive

fn foo<T>() 
where
    T: Trait,  // <-- 
	T: Trait => T: Trait,
{
	
}

fn main() {
    foo::<u32>();
    // (u32: Trait => u32: Trait)
}
```

* Alias bound candidates:

```rust
trait Trait {
    type Assoc;
}

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

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

- `normalizes_to(Alias<i32>, ())`
    - `equate(Alias<u32>, ())` unproductive
        - `normalizes_to(Alias<u32>, ())`
            - `equate((), ())` OK
            - `is_implemented(i32: Trait)` OK
            - `normalizes_to(Alias<i32>, ())` cycle, OK


model above

```
// from impl Trait for i32

Trait(i32).
(Trait(i32), Trait::Assoc(u32) = U) => (Trait::Assoc(i32) = U). [nonproductive]

Trait(u32).
(Trait(u32), Trait(i32), Trait::Assoc(i32) = ()) => (Trait::Assoc(u32) = ()). [productive]
```

- try to prove `Trait::Assoc(i32) = ()` [nonproductive]
    - prove `Trait(i32), Trait::Assoc(u32) = U` 
        - prove `Trait(i32)`
            - done.
        - prove `Trait::Assoc(u32) = ()` [productive]
            - prove `Trait(u32), Trait(i32), Trait::Assoc(i32) = ()`
                - prove `Trait(u32)`. done.
                - prove `Trait(i32)`. done.
                - prove `Trait::Assoc(i32) = ()` [ignore the cycle]
                  - prove `Trait(i32), Trait::Assoc(u32) = U` 
                    - prove `Trait(i32)` done.
                    - prove `Trait::Assoc(u32) = ()` [productive cycle, stop]
    - prove `Trait::Assoc(u32) = ()` [via some nonproductive rule] ...

---

Induction

by definition:

```
P             in TruePropositions
Q             in TruePropositions
----------    then
R             in TruePropositions
```

TruePropositions is a subset of Z, where Z is "propositions that are sound"

we must prove this :

```
              if
P             in Z
Q             in Z
----------    then
R             in Z
```

if we can prove that, we know that TruePropositions <= Z because it is the smallest pre-fixed-point that fits the rules

---

Coinduction

you get to assume the conclusion

but you must prove the premises

not a valid coinductive rule:

```
X <: Y
Y <: Z
--------- [transitive]
X <: Z
```

* you give me an arbitrary X, Y, and Z
    * we know that X <= Z
        * we must prove that
            * X <: Y
            * Y <: Z
        * we can't do that, we don't know anything about Y


contrast with induction:

* you give me an arbitrary X, Y, and Z
    * we assume X <: Y and Y <: Z
        * must prove that X <: Z
            * e.g., we could proceed by cases, looking at each case of X / Z or whatever


---

Sized = Def A

Def B

```
-------
*mut T is Sized

T: Sized
U: Sized
-------
(T, U) is Sized
```

if we show that Def B is a subset of Def A

and we know that any subset of Def A is "correct by definition"

then we know that Def B is corret

"the set of all `=` which look like `A(...) = R<R<R<...>>>`"

and can we show that `R<...>` is correct

## 2023-02-13

- TAIT
	- oli PR: https://github.com/rust-lang/rust/pull/107891

## 2023-01-23

- new solver outline and many candidates ready, testable with `-Ztrait-solver=next`
    - global cache is missing, have to talk to cjgillot about whether order of dependencies (which depends on the root node of cycle) matters
    - region obligations / canonicalization is current target
- canonicalization
    - compress universes for AA and EE patterns (but not AEA or EAE)
    - evaluate caching for params and improve what we get
- specialization
    - you can model it without `neg` except during reveal
    - but I wonder if you can use a lattice value and then talk about the "maximum"
    - completeness -- do we have an issue where we inconsistently decide whether the same specialized impl applies twice?


## 2022-12-19

### oli: higher-kinded function pointers

Bunch of weirdness here around pattern matching. Modes:

* partial-eq
* if there is no partial-eq impl, we currently error out, but some edge cases where you can match on it by destructuring it completely into its inner pieces
* if you take apart constants, might not always be able to do, ideally we'd not have that logic, but either be able to take it apart entirely *or* call `PartialEq`

Tried moving it to valtree, but it breaks for things that lack a `PartialEq` impl

https://github.com/rust-lang/rust/pull/99531

```rust
trait FnPointer { }

impl FnPointer for "any fn(..)" { }
```


```rust
const C: DummyType = DummyType::V1;

fn foo(d: DummyType) {
    match d {
        // Error b/c type of constant does not have StrucuralEq trait,
        // but sometimes we accept `&&C`  or something because backwards
        // compatibility.
        C => (),
        _ => panic!(),
    }
}

fn foo2(d: &&DummyType) {
    // Currently we would panic, but with valtree, we would not;
    // but right now values must be StructuralEq, so valtree would fail.
    match d {
        &&C => (),
        _ => panic!(),
    }
}

enum DummyType {
    V1,
    V2,
}

impl PartialEq for DummyType {
    fn eq(&self, other: &Self) -> bool {
        false
    }
}

impl Eq for DummyType {
}
```

```rust
fn foo(x: u32, y: u32) {
    assert_eq!(x, y);
    prove (bar(x) == bar(y));
}

fn bar(x: u32)
{}
```

### niko: functional logic programming deep dive

good survey paper

https://www.informatik.uni-kiel.de/~mh/papers/GanzingerFestschrift.pdf

* given a function `foo` 
    * returns a value along with constraints
* function definitions are "equational", i.e., more like inductive rules
    * as in logic programming

```
foo(X, 0) = 0
foo(22, _) = 23
```

in other words:

* In Haskell, `foo(22, 0)` is 0
* In e.g. Curry, `foo(22, 0)` is `0` and `23`
---

* three concepts
    * functions (like `foo` above), defined with equations
    * data constructors (like rigid types, in mir-formality terminology)
    * primitives, integers, whatever
* limitatiojns
    * no talk of coinducive reasoning or what that might even mean
    * just prolog-y, first order horn claus, meaning:
        * no forall
        * no implication
        * no etc

### niko: poking on a-mir-formality very slowly

### lcnr

* finished solver PR
    * think we should merge it as is
    * but some parts which I don't like
* worried about perf of normalizes-to
    * it includes output, GAT arguments
    * this is going to cause fewer cache hits
* 

## 2022-12-12

lcnr

* structure of new solver is doing very well
    * notes https://hackmd.io/
    * wip branch https://github.com/lcnr/rust/tree/evaluate-new
        * https://github.com/lcnr/rust/blob/5bc1b429e941da979356a62443ca5c1e7ab40210/compiler/rustc_trait_selection/src/solve/trait_goals.rs

### coherence leak-check

```rust
impl MyTrait for T
where 
   for<'b> T: OtherTrait<'b>
{
    
}

struct Foo { }

impl MyTrait for Foo { }

impl OtherTrait<'static> for Foo { }

trait MyTrait { }

trait OtherTrait<'l> { }

fn main() { }
```

https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=b19eb566e3686da2d689f9989c21a607

examples that don't compile today but which would require us to process nested region obligations, even in reveal-all mode:

```rust
impl<T> MyTrait for T
where 
   for<'b> T: OtherTrait<'b>
{
    
}

struct Foo { }

impl MyTrait for Foo { }

impl<'l> OtherTrait<'l> for Foo 
where 'l: 'static
{ }

trait MyTrait { }

trait OtherTrait<'l> { }

fn main() { }
```

```rust
impl<T> MyTrait for T
where 
   for<'b> T: OtherTrait<'b>
{
    
}

struct Foo { }

impl MyTrait for Foo { }

impl<'l> OtherTrait<'l> for Foo 
where Foo: ThirdTrait<'l>
{ }

impl ThirdTrait<'static> for Foo 
{ }

trait MyTrait { }

trait OtherTrait<'l> { }

trait ThirdTrait<'l> { }

fn main() { }
```


```rust
impl<T> MyTrait for T
where 
   for<'b> T: OtherTrait<'b>
{
    
}

struct Foo { }

impl MyTrait for Foo { }

impl<'l> OtherTrait<&'l ()> for Foo 
where Foo: ThirdTrait<&'l ()>
{ }

impl ThirdTrait<&'static ()> for Foo 
{ }

trait MyTrait { }

trait OtherTrait<T> { }

trait ThirdTrait<T> { }

fn main() { }
```

### query results

```
Foo(?T) :-
    
```

with the result that `?T = Vec<?U>`

`forall<?U> ?T = Vec<?U>`

```
query:
    ?0 in U0
    !1
    ?2 in U1

result:
    ?2 = ?0 = Vec<?3> where ?3 is fresh
```

### or region constraints

niko's desire: we instead just pick the best?

```rust
#[marker]
trait Marker {}

impl<'a> Marker for (&'a (), &'static ()) {}
impl<'a> Marker for (&'static (), &'a ()) {}
```

or

```rust
trait NotMarker { }

fn foo()
where
    (&'a (), &'static ()): NotMarker,
    (&'static (), &'a ()): NotMarker,
{}
```


## 2022-11-07

* https://github.com/rust-lang/rust/pull/103488
    * TAIT in impl block signatures
    * good, needs test :sparkles: 
    * also merge all the "register a specific obligation" functions
        * just allow registering obligations
* remove recursion limit
    * just check type "size" (complexity)
        * note: clippy may want to reuse
        * cache in type flags?
        * nice: no more dependency on trait solver internal "stack depth"
* lazy normalization
    * `equate(t1, t2)`
    * `normalizes_to(alias -> ty)`
    * `deep_normalize(t1 -> t2)`

```rust
trait Iterator { type Item; }

// equate(<T as Iterator>::Item, <T as Iterator>::Item).
// forall<U> { equate(<T as Iterator>::Item, U) :- normalizes_to(<T as Iterator>::Item -> U) }
// forall<Self, U, V> {
//   deep_normalize(<Self as Iterator>::Item -> V) :-
//     normalizes_to(<Self as Iterator>::Item -> U),
//     deep_normalize(U, V)
// }

impl<T> Iterator for Vec<T> {
    type Item = T;
}

// forall<T> { normalizes_to(<Vec<T> as Iterator>::Item -> T) }

struct Vec<T> { }

// forall<T, U> { deep_normalize(Vec<T> -> Vec<U>) :- deep_normalize(T -> U) }
```

why normalizes-to can't be simply coinductive

```rust
trait Foo { type FooItem; }
trait Bar { type BarItem; }

impl Foo for () {
    type FooItem = <() as Bar>::BarItem;
}

impl Bar for () {
    type BarItem = <() as Foo>::FooItem;
}

// normalizes_to(<() as Bar>::BarItem, T) 
// holds if normalizes_to(<() as Foo>::FooItem, T)
// holds if normalizes_to(<() as Bar>::BarItem, T) :check:
```

implied bounds:

```rust
trait FromResidual<R> {}
trait Try: FromResidual<<Self as Try>::Residual> {
    type Residual;
}

struct Ready<T>(T);
impl<T> Try for Ready<T> {
    type Residual = Ready<()>;
}
impl<T> FromResidual<<Ready<T> as Try>::Residual> for Ready<T> {}
```
- `wf(<Ready<T> as Try>::Residual)` requires
-  `Ready<T>: Try`, which requires because of the super trait
-  `Ready<T>: FromResidual<Ready<T> as Try>::Residual>`, which has an impl which requires **because of implied bounds**
-  `wf(<Ready<T> as Try>::Residual)` :tada: **cycle**


```rust
trait FromResidual<R> {}
trait Try: FromResidual<<Self as Try>::Residual> {
    type Residual;
}

impl<T> Try for Ready<T>
{
    type Residual = Ready<()>;
}
impl<T> FromResidual<<Ready<T> as Try>::Residual> for Ready<T> 
where
    Ready<T>: Try<Residual = Ready<()>>,
{}
```

- `wf(<Ready<T> as Try>::Residual)` requires
-  `Ready<T>: Try`, which requires because of the super trait
-  `Ready<T>: FromResidual<Ready<T> as Try>::Residual>`, which has an impl which requires **because of implied bounds**
-  `normalizes_to(<Ready<T> as Try>::Residual -> Ready<()>)`, which has an impl (`Try`) which requires **because of implied bounds**
-  `wf(Ready<T>)` :heavy_check_mark: 
-  



## 2022-10-31

### lcnr

* explicit implied bounds:
    * wf for placeholders: https://github.com/rust-lang/rust/pull/103565
        * problem is now the impl has a `WF(A)`
        * so when we try to prove `for<'a> Foo<&'a T>` we need to prove `for<'a> WF(&'a T)`
            * this requires `T: 'a` and hence you get `for<'a> T: 'a`
                * which requires `'static`
        * this bothers niko because it means that proving `WF(&'a T)` requires proving `T: 'a` 
            * but proving `for<'a> WF(&'a T)`... does not?
        * lcnr also doesn't love it
    * end of hackmd, cycle: https://hackmd.io/_F7hq8ldSr-PuqudZ1A-nA
```rust
trait FromResidual<R> {}
trait Try: FromResidual<<Self as Try>::Residual> {
    type Residual;
}

struct Ready<T>(T);
impl<T> Try for Ready<T> {
    type Residual = Ready<()>;
}
impl<T> FromResidual<<Ready<T> as Try>::Residual> for Ready<T> {}
```

### coinduction

```rust
// is_implemented(T: Magic) :- has_impl(T: Magic), is_implemented(T: Copy)
trait Magic: Copy { }

// this impl is accepted by a-mir-formality
impl<T: Magic> Magic for T { }
// proves that we have a valid impl of Magic if these conditions hold
// (including `is_implemented(T: Magic)`)

// effectively equivalent to:
impl<T: Copy> Magic for T { }

fn and_for_my_next_trick<T: Magic>(t: T) -> (T, T) {
    (t, t)
}

fn main1() {
    let s: String = "foo".into();
    
    // but this call is an error:
    // has to prove `is_implemented(String: Magic)`
    // which requires proving `is_implemented(String: Copy)` this fails
    let (s1, s2) = and_for_my_next_trick(s);
}


fn main2() {
    let s: u32 = 22;
    
    // this call is ok
    let (s1, s2) = and_for_my_next_trick(s);
}
```

do want to support perfect derive though, which is inherently cyclic, that's the whole point?

```rust
struct List<T> {
    value: T,
    next: Link<List<T>>,
}

impl<T> Ord for List<T>
where
    T: Ord,
    Link<List<T>>: Ord,
{}

impl<T> Ord for Link<List<T>>
where
    T: Ord,
    List<T>: Ord,
{}

trait Ord: PartialOrd { }
```

lcnr poins out that in the typical perfect derive, you don't need the cycle to show that the supertraitsof the trait itself hold

but in this example, assuming `T: Ord => T: PartialOrd` would be nice...


```rust
struct List<T> {
    value: T,
    next: Link<List<T>>,
}

impl<T> Ord for List<T>
where
    T: Ord,
    Link<List<T>>: Ord,
{}

impl<T> Ord for Link<List<T>>
where
    T: Ord + PartialOrd,
    List<T>: Ord,
{}

trait Ord: PartialOrd { }
```

### scalexm's setup

push the iteration "out"

given 

```rust
struct Foo<T: Ord> { }
```

```rust
wf(Foo<T>) :- wf1(Foo<T>), wf(T). // wf is coinductive

wf1(Foo<T>) :- T: Ord. // wf1 is inductive
```

write-ups from before...

https://rust-lang.github.io/chalk/book/clauses/wf.html

## 2022-10-24

- lcnr check-in
    - was blocked on reveal-all in const evaluation
        - but lcnr thinks this is ok ( niko would like to discuss :) )
        - https://hackmd.io/yzMnKd9ZQRCclXBl9hWS3A
    - implied bounds: https://hackmd.io/_F7hq8ldSr-PuqudZ1A-nA
    - non-fatal overflow: https://hackmd.io/As4PNCebR_GablOyRvPC0Q
    - "could have done shallow subtyping a few months ago with a slightly changed approach"
- nikomatsakis
    - been working on a-mir-formality.rs in the riir branch
        - realized need `not-provable` goals to integrate `T: !Trait` more correctly
            - also needed for specialization
        - working towards a deep dive to read through the ideal design
- oli
    - TAIT has a remaining coherence issue (implementing traits for opaque types)
        - lcnr has a proposed solution 
        - diagnostics and incompleteness issues remain
        - next step is to talk to t-lang about it
    - effects!! and ~const
- talking with diagnostic people:
    - The fulfill nested obligation stuff sometimes makes sense: https://github.com/weiznich/rust-foundation-community-grant/blob/883de46cbea5873bcc4af60e47f872efaa77a2b7/test_cases/tests/diesel/queryable_order_mismatch.stderr

- tait: https://github.com/rust-lang/rust/issues/99840
```rust
#![feature(type_alias_impl_trait)]
type Alias = impl Sized;

fn constrain() -> Alias {
    1i32
}

trait HideIt {
    type Assoc;
}

impl HideIt for () {
    type Assoc = Alias;
}

pub trait Yay {}

impl Yay for <() as HideIt>::Assoc {}
impl Yay for i32 {} // this doesn't error
```

[Playground](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=d6a35d225a80a861d8b7b3904ec96f17)

@lcnr fix: relating opaque types in coherence should always result in ambiguity.

relating projections also has to be ambiguous https://github.com/rust-lang/rust/issues/102048

opaque ty late in `Equate`: https://github.com/rust-lang/rust/blob/1481fd964bac3c750c7e1b21206fdaa60346c456/compiler/rustc_infer/src/infer/equate.rs#L95-L112


```rust
type Foo = impl Debug;
pub trait Yay { }
impl Yay for Foo { }

fn foo() {
    is_yay::<u32>();   // ?? 
    is_debug::<u32>(); // OK
    is_yay::<Foo>();   // OK
    is_debug::<Foo>(); // ?? fails now to select
}

fn is_yay<T: Yay>() { }
fn is_debug<T: Debug>() { }
```


```rust
type Foo = impl Debug;

pub trait Yay { }
impl Yay for u32 { }

fn foo() {
    is_yay::<Foo>(); // ?? fails now to select
}

fn is_yay<T: Yay>() { }
```


Problem unsound impl for opaque type:

```rust
#![feature(type_alias_impl_trait)]

trait Foo {}
impl Foo for () {}
type Bar = impl Foo;
fn _defining_use() -> Bar {}

trait Trait<T, In> {
    type Out;
    fn convert(i: In) -> Self::Out;
}

impl<In, Out> Trait<Bar, In> for Out {
    type Out = Out;
    fn convert(_i: In) -> Self::Out {
        unreachable!();
    }
}

impl<In, Out> Trait<(), In> for Out {
    type Out = In;
    fn convert(i: In) -> Self::Out {
        i
    }
}

fn transmute<In, Out>(i: In) -> Out {
    <Out as Trait<Bar, In>>::convert(i)
}

fn main() {
    let d;
    {
        let x = "Hello World".to_string();
        d = transmute::<&String, &String>(&x);
    }
    println!("{}", d);
}
```

## 2022-10-06

- general catch up
    - https://github.com/rust-lang/rust/pull/102635
    - https://github.com/rust-lang/rust/pull/102713
- is it better to have "ideal view" discussions 1:1 or with a group?
    - expected audience: michael, lcnr, jack, nikomatsakis
    - https://chalk-it-up.netlify.app/
- "ideal" query solver design, but also ambiguity + lifetimes
    - lcnr idea doc: https://hackmd.io/yqurQvKsT-uAifHzzkm0OQ


### chalk overview

* `is_implemented(P0: Trait<P1..Pn>)`
* `normalizes_to(<P0 as Trait<P1..Pn>::Type<Pn..Pm>, T)`
* ...other stuff...

* Query:
    * canonical binders
    * plus environment
    * plus a goal (see above)

### normalizes-to

* Defined by each impl

```rust
impl<T> Iterator for MyIter<T> {
    type Item = T;
    
    fn next() -> { }
}
```

```
forall<T> {
    normalizes_to(<MyIter<T> as Iterator>::Item, T) :-
        is_implemented(T: Sized).
}
```

```
forall<T> {
    normalizes_to(<MyIter<T> as Iterator>::{next}, fn-def(next)) :-
        is_implemented(T: Sized).
}
```

```
forall<T> {
    normalizes_to(<MyIter<T> as Iterator>::{next}, fn-def(next)) :-
        reveal,
        is_implemented(T: Sized),
        not is_specialized(<MyIter<T> as Iterator>::{next}). // "extend the logic" to include not, encode specialization in the lowering
}
```

"defeasible"

### lifetimes

* universal lifetimes
* existential lifetimes
* end result of trait solving:
    * for each existential lifetime, have outlives edges to/from other existential lifetimes + universals
    * fail if this creates a connection between universal lifetimes that isn't in the environment

```rust
fn foo<'a, 'b>(x: &'a u32) -> &'b u32 { 
    x // fail to prove subtyping (eventually)
}
```

have to prove `for<'a, 'b> { &'a u32 <: &'b u32 }`, can't do it because `'a: 'b` isn't provable

```rust
trait Foo<'a, 'b> { }

impl<'a, 'b> Foo<'a, 'b> for ()
where
    'a: 'b,
{ }

impl<'a, 'b> Foo<'a, 'b> for i32
{ }
```
`?x: Foo<'a, 'b> where !'a: 'b`

```rust
fn test<'a, 'b>() {
    bar::<'a, 'b, _>(); // would get inferred to i32, perhaps surprisingly
}

fn bar<'a, 'b, T: Foo<'a, 'b>>() {}
```

if we canonicalize all lifetimes to existential variables: you get back ambiguity

* the environment + the trait system know how to deal with universals
* but when we canonicalize, we convert all lifetimes in the goal to fresh existentials
    * if this succeeds, must be true "no matter what"
* the borrow checker:
    * has an env E that DOES have the universals in it
    * it performs queries and applies the result to this environment
        * this could yield an error
    * if there is no error:
        * we are left with a graph of existential lifetimes in the root universe and outlives relationships between them and the universal placeholders

```rust
fn test<'a, 'b>() {
    bar::<'a, 'b, ()>();
    // query is:
    // 
    //     (): Foo<?a, ?b>
    // 
    // result is:
    // 
    //     OK(?a: ?b)
    //
    // we apply this to our input and get !a: !b, which is an error.
    // 
    // we report error to user.
}

fn bar<'a, 'b, T: Foo<'a, 'b>>() {}
```

```rust
trait Foo<'a, 'b> { }

impl<'a, 'b> Foo<'a, 'b> for ()
where
    'a: 'b,
{ }

impl<'a, 'b> Foo<'a, 'b> for i32
{ }

fn test<'a, 'b>() {
    bar::<_>(); // inferred to i32 ?
    baz::<_>(); // ambiguous ?
}

fn bar<T>()
where
    for<'a, 'b> T: Foo<'a, 'b>,
{}

fn baz<T>()
where
    for<'a, 'b> if ('a: 'b) { T: Foo<'a, 'b> },
{}
```

```rust
trait Foo<'a, 'b> { }

impl<'a, 'b> Foo<'a, 'b> for ()
where
    'a: 'b,
{ }


trait Bar<'a>
where
    Self: Foo<'a, 'a>
{}

impl<'a, T: Foo<'a, 'a>> Bar<'a> for T {} 
```
- `Foo<'a, 'a>` to ambig
- `Bar<'a>` to ok

??? sus

### chalk solver 

https://rust-lang.github.io/chalk/book/recursive.html

* stack of
    * canonicalized query
        * creates an inference context with the contents of that query
        * simplifies this to various candidates, any of must be true
        * for each candidate, a list of subgoals, all of whihc must be true
            * if the canonicalized subgoal is on the stack, does some smart stuff to deal with cycles
                * tag the things on the stack as "in progress", use an interim value
        * once we've got an answer:
            * if we were tagged as veing part of a cycle, we repeat, using this answer as the interim value
            * if we get the same result twice, we're done (fixed point)
            * then we can cache all things that were participating in the cycle at once

### things niko wants to talk about next time :)

* coherence
* diagnostics

## 2022-09-28

* Implied bounds -- what is the right way?
    * https://github.com/rust-lang/rust/issues/102360 
        * fix by always erasing regions, don't specialcase static in evaluate, rewrite evaluate :3
        * consider removing dyn trait backcompat hack
    * always kept `'static` in https://github.com/rust-lang/rust/pull/102205
    * downgrade to `ModuloRegions` https://github.com/rust-lang/rust/blob/d9297d22ad9edc2b56f0dd8734c1187a0c88be69/compiler/rustc_trait_selection/src/traits/select/mod.rs#L1026-L1036

`for<'hr> fn(&'hr &'a (), FoutlivesS<'a, 'hr>)`

`for<'hr> if ('a: 'hr) fn(&'hr &'a (), FoutlivesS<'a, 'hr>)`

This has to be converted to a canonical predicate:

* Version 1: `for<'hr> if (?0: 'hr) fn(&'hr &?0 (), FoutlivesS<?0, 'hr>)`
    * `(&?0 u32, &?0 u32): Trait<?0, ?1>` is true if
        * `(&?0 u32, &?1 u32): OtherTrait<?0>`
    * `(&?1 u32, &?0 u32): Trait<?0, ?1>` is true if
        * `(&?1 u32, &?0 u32): OtherTrait<?0>`
* Version 2: `for<'hr> if (?0: 'hr) fn(&'hr &?0 (), FoutlivesS<?1, 'hr>)`
    * probably equivalent to the one below when it comes to caching
* Version 3: `for<'hr> if (erased: 'hr) fn(&'hr &erased (), FoutlivesS<erased, 'hr>)`

region variables in the root universe get erased for ctfe and codegen

can't consider root universe region stuff for evaluate/fulfill

root universe rn not only `ROOT` because we dont decrease universe counter

implied bounds are exclusively region relations in root universe.

- GOAL: higher ranked region obligations only in fulfill
- Q: Do implied bounds impact higher ranked region obligations?
    - no, well maybe, yes?

Question is:

```
fn foo<'a, 'b>() -> &'a u32 
{
    if you have to prove ?0: 'a...
        ...you find that `'static: 'a` is the only bound...
        ...and so you wind up with an relation `?0: 'static` in the solution, which gets passed to borrow check
    but if you have to prove 'a: ?0...
        ...you find no bounds on `'a` and you just get back false
}
```

concern:

* if the type check knows that `'a: 'b`
* 

## 2022-09-21

### oli

Effect system hacking continues.

For the change to lifetime capture (TAIT), just do the PR and nominate it? Last soundness bug should get merged tomorrow.

### lcnr

https://github.com/rust-lang/rust/pull/101478

```rust
// cycle example that uses size-of
mod ayy {
    pub type Foo = impl Sized;
    fn foo() -> Foo {}
}
fn foo2(x: &u32) -> &impl Debug {
    let y = [0; 1 + size_of::<ayy::Foo>()];
    ...
}

// "trivial" cycle example
fn foo2(x: &u32) -> &impl Debug {
    let y = [0; 1 + 2];
    ...
}

// ill-formed environment example
#![feature(trivial_bounds)]
#![feature(type_alias_impl_trait)]
trait Trait {
    const ASSOC: usize;
}

use constraining_context::Foo;
mod constraining_context {
    pub type Foo = impl Sized;
    fn constrain() -> Foo {}
}

fn yikes()
where
    Foo: Trait,
{
    let _ = [0u8; <Foo as Trait>::ASSOC];
}


//
use constraining_context::Foo;
trait Trait {
    type Foo;
}

struct SomeType<T: Trait> { value: <T as Trait>::Foo }

fn yikes()
where
    Foo: Trait,
{
    // Here:
    // * Layout code would encounter assoc-ty projection
    // * Can fail to normalize, yields Too Generic
    [0; size_of::<SomeType<Foo>>()]
}


//
use constraining_context::Foo;
trait Trait {
    type Foo;
}

struct SomeType<T: Trait> { value: T }

fn yikes()
where
    Foo: Trait,
{
    // Here:
    // * Layout code would encounter opaque type
    // * Could try to reveal it
    //     * But: result may not be WF
    //     * Either: we check that and fail (meh)
    //     * or we substitute within the param env "hmm"
    [0; size_of::<SomeType<Foo>>()]
}
```
possible solution:

* normalize in layout with reveal
    * but don't use reveal-everywhere
* only normalize just this opaque type both in param env and as value

```rust
fn reveal_one(opaque_type: DefId, foldable: impl TyFoldable) {
    // we can apply this to (ParamEnv, Ty)
    // when we encounter a Opaque type in layout
    // and we preserve WF'dness
}
```

*but*

we leak info about how the opaque type uses its parameters.

```rust
// size_of(Foo<X>) is valid for any X
type Foo<T>: Bound = u32;

// size_of(Foo<X>) is only valid for concrete X,
// since we are evaluating before monomorphization
type Foo<T>: Bound = T;
```
eval with generic params is already linted against, e.g.
```rust
const fn foo<T>() -> usize {
    // We might instead branch on `std::mem::size_of::<*mut T>() < 8` here,
    // which would cause this function to fail on 32 bit systems.
    if false {
        std::mem::size_of::<T>()
    } else {
        8
    }
}

fn test<T>() {
    let _ = [0; foo::<T>()];
    //~^ WARN cannot use constants which depend on generic parameters in types
    //~| WARN this was previously accepted by the compiler but is being phased out
}
```

```rust
let x: [u8; size_of(usize)] = [0; size_of(*const T)];
```

but pre-existing in some sense:

```rust
// Compiles with lint
use std::mem::size_of;
fn test<T>() {
    let _: [u8; size_of::<usize>()] = [0; size_of::<Foo<T>>()];
}

struct Foo<T> {
    x: *const T
}
```
```rust
const fn foo() -> impl const Iterator<Item = usize> {
    (0..100)
}

fn main() {
    let x: [u8; 4950] = [0; foo().sum::<usize>()];
}
```

## 2022-09-07

### lcnr

- one level deeper :3 https://github.com/rust-lang/rust/pull/101478
    - removing reveal::all pre-trans
    - we use it during elaborate-drop
        - which happens before mir-for-ctfe query
    - notes about errors:
        - better to keep this PR clean
            - add some notes explaining common situations where this arises
            - maybe a `--explain` entry
        - as followup, could...
            - thread a `Ty<'tcx>` through 
- wip on moving things into param-env
    - no current blockers

### big picture

* [ ] goal: moving HRTB logic out of borrow check and into trait checker (this creates the interface that polonius wants)
    * [ ] step 1: have fulfillment context simplify outlives obligations into `a: 'b` and `T: 'a` results [draft PR](https://github.com/rust-lang/rust/pull/97641/)
        * [ ] need implied bounds during fulfillment
            * [ ] need to pass implied bounds into borrowck trait solving queries
                * [x] extract implied bounds into a query
                * [ ] move implied bounds into parameter environment
                    * [ ] cycles due to Reveal::All (#101478)
    * [ ] step 2: handle type parameters and regions in fulfill by searching parameter bounds etc
* [ ] goal: generalize inference to simple-sub algorithm
* [ ] goal: lazy normalization of associated types and other aliases
* [ ] goal: richer set of types (implication types, existential types, and forall's that are independent from `fn` and `dyn`)

### RPIT refactor

```rust
trait SomeTrait<'a>: Debug { }

fn foo<'a, T>(t: T) -> impl Debug
where
    T: SomeTrait<'a>
{
    t
}

type Foo<T>: Debug // OpaqueTy
where
    T: SomeTrait<'static>; // uh oh
```

```rust
trait SomeTrait<'a>: OtherTrait { }
trait OtherTrait {
    type Assoc;
}

fn foo<'a, T>(t: T) -> impl PartialEq<T::Assoc>
where
    T: SomeTrait<'a>
{
    t
}
```

what it would be nice to produce:

```rust
type Foo<T>: Debug // OpaqueTy
where
    exist<'a> T: SomeTrait<'a>;
```

can we support this in some way that is "sufficient" for opaque types, if not totally general?


```rust
trait SomeTrait2<'a, 'b> { }

type Foo<T>: Debug // OpaqueTy
where
    exist<'a> T: SomeTrait2<'a, 'a>;
```

* you could imagine an `Exists` predicate and a `&&` predicate
    * proving this predicate is easy:
        * create inference variables
    * having it in your environment is harder:
        * create placeholders and we don't do that dynamically very well right now, though we do it from time to time (e.g., for HRTB)
        * would have to be able to extend ParamEnv with new predicates, which we cannot currently do, but which would be a big unblocker
            * are there places we cache results without the ParamEnv? that would be a problem
            * dig into implications as the next step -- what and where exactly do we want these?

```rust
trait SomeTrait2<'a, 'b> { }

type Foo<T, exists 'a>: Debug // OpaqueTy
where
    T: SomeTrait2<'a, 'a>;
```

```rust=
fn foo<'a, T>(t: T) -> impl PartialEq<T::Assoc>
where
    T: SomeTrait<'a>,
    T: SomeOtherTrait<'a>
{
    type Foo<..> = 
    t
}
```

```rust
trait Foo<'a, T>
where
    T: Trait<'a>
{}

fn something<'a, T, U>() -> impl Sized
where
    U: Foo<'a, T>,
    T: Trait<'a>, // <-- required  for `U: Foo` to be WF
```

also

```rust
impl<'a, T: Foo<'a> + Bar<'a>> Bop for T {}
fn something<'a, T>(t: T) -> impl Bop
where
    U: Foo<'a>,
    U: Bar<'a>,
{
    t
}
```

```rust=
fn foo<'a, 'b, T>() where if ('a: 'b) { T: Trait<'a> } {
    
} 
```
`'a: 'b => 'a: 'b`


```rust
fn foo<'a, 'b>(
    obj: with(cx: &mut Context) => Dyn<Debug>
    
)
where
    ('a: 'b) => Something
{
    
}

fn bar() {
    foo(); // prove `?a: ?b => Something`
}

fn foo<'a, 'b, T>
where
    T: Trait<'a> + Trait<'b>
{
    /* 
    prove T: Trait<?c> ? 
    
    should ?c be 'a or 'b
    
    marker traits has this problem
    */
}
```

## 2022-08-17

Still working on moving things into trait solving. 

Hitting a lot of unexpected road blocks.

[Updates here]()

## 2022-07-06

### TAIT soundness update
* Have 3 PRs in-flight, each blocked on a 4th one, which is waiting on FCP to complete
* After that, we should be good on soundness/completion
* https://rust-lang.github.io/impl-trait-initiative/explainer.html ?
* If you use a TAIT in a trait definition...
    * https://github.com/rust-lang/rust/issues/57961

```rust
#![feature(type_alias_impl_trait)]

mod foo {
    pub type X = impl Sized;

    pub trait Foo {
        type Bar: Iterator<Item = X>;
    }
    
}

impl foo::Foo for () {
    type Bar = std::vec::IntoIter<u32>;
}

fn incoherent() {
    let f: X = 22_i32;
}

fn main() {}
```

niko's take:

* We can make #5

```rust
#![feature(type_alias_impl_trait)]

type X = impl Sized;

trait Foo {
    type Bar: Iterator<Item = X>;
    
    fn into_bar(self) -> Self::Bar;
}

impl Foo for () {
    type Bar = std::vec::IntoIter<X>;
    
    fn into_bar(self) -> Self::Bar {
        vec![22, 44].into_iter()
    }
}

fn incoherent() {
    let f: X = 22_i32;
}

fn main() {}
```

[playground](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=9e0087d42f4b22b4f0ac6b59577d5378)

### Type outlives

* Implied bounds PRs have landed :tada: 
* Link! :link: 
    * https://hackmd.io/vAj2CA8aS9mDL_xJlkVH7Q?both#Implied-bounds-can-be-accessed-early-what-now
* Status of https://github.com/rust-lang/rust/pull/97641/ ?


```rust
struct BiVar<T, U>
where T: Foo<Item = U> { }

for<'a, 'b> fn() -> BiVar<(), &'a &'b u32>
<:
for<'a, 'b> fn() -> BiVar<(), &'a &'b u32>

for<'a, 'b> fn() -> BiVar<(), &'a &'b u32>
<:
for<'a, 'b> fn() -> BiVar<(), _>
```

* when we generalize BiVar, we introduce a `?T` for which we have to prove WF
* we make `?T` a subtype (or equated, or something) with `&'a &'b u32`
    * where `'a` and `'b` are higher-ranked placeholders
* this will eventually fail to compile because `'b: 'a` cannot be proven

### established 

* primary goal: 
    * remove higher-ranked stuff from borrow check
* secondary goal:
    * improve the trait code to handle higher-ranked things in a uniform way, accommodating implied bounds, etc
* `leak_check` is used...
    * in the selection context, to weed out candidates (e.g. `impl<T> Trait for fn(T)` vs `impl<T> Trait for fn(&T)`)
* danger:
    * if trait checker is looking at implied bounds to make decisions
        * and they are not part of the param env
        * could mess up our caching schemes
    * however
        * if the only thing that looks at them is FulfillmentContext, when solving an outlives obligation, should be ok *for now*
* 

## 2022-06-29

- random doc https://hackmd.io/vAj2CA8aS9mDL_xJlkVH7Q
- goal for now:
    - design for implied bounds
    - new unsoundness? [#98543](https://github.com/rust-lang/rust/issues/98543)
    - problem is:
        - when we check the Where Clauses for WF, we take the implied bounds into account
        - this means that we assume `&'a &'b ()` is WF
        - if you remove the argument:
            - https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=f4d1ac7cb7db5201bfda54e669c7edbf
            - you get an error
- implied bounds: `foo<'a, 'b>(x: &'a &'b ()) {}`
    - `foo(&&())` -- some kind of proving here to ensure that implied bounds are met
    - `(foo as fn(_))(&&())`
        - check or warn when upcasting?
        - real fix needs implication types
- https://github.com/rust-lang/rust/pull/97890
- `for<'a, 'b> fn(&'a &'b ()) <: fn(&'long &'short)` 


```rust
struct Foo<'a, 'b>
//where 'b: 'a
{
    x: &'a u32,
    y: &'b u32
}


Foo<'long, 'long>
<:
Foo<'long, 'short>

// Add where clause

struct Foo<'a, 'b>
where 'b: 'a
{
    x: &'a u32,
    y: &'b u32
}


Foo<'long, 'long>
<:
Foo<'long, 'short> // <-- where did this come from?
```


Niko's feeling is that all predicates should be able to assume their *inputs* are wf, so...

* `IsSubtype(A, B)` // the rules for this should be able to assume A and B are well-formed

just like

* `A: SomeTrait<B>` // can assume that A, B are well-formed

```
NormalizesTo(AliasTy, Ty)
                      -- role of this is an output role, which is interestingly different
                      
NormalizesTo succeeds, then Ty is well-formed
```

```rust
trait Foo {
    type Item: Foo;
}

struct RequiresOrd<T: Ord>();

impl Foo for u32 {
    type Item = RequiresOrd(f32); // <-- Error here
}

impl Foo for i32 {
    type Item = <u32 as Foo>::Item;
}

fn do_stuff<T: Foo>() {
    // I get to assume T is WF....
    let x = T::Item; // this must be WF
}
```

```
is_impl(T: Ord) :-
    has_impl(T: Ord), // (a) if the user wrote `impl Foo for T`, and the where-clauses on the impl are met, this will be true    
    has_impl(T: Eq), // (b) trait where clauses must hold
    well_formed(type T). // (c) input types must be WF
```

```rust
trait Ord: Eq
where
    WF(Self),
{
    
}

impl<T> Ord for T
where
    T: Ord
{
    // The impl has to prove that the where-cluases on the trait hold
    // -- but they are also being proven by the person using the impl (who is proving `is_impl`)
    // -- this is because the impl actually can't do it, if you have coinduction + other stuff
    
}
```

Niko's conclusion:

* impls don't get to assume that trait things are true
    * they only get to assume their where clauses
    * but we add 

```mermaid
flowchart LR
    UserSyntax --> HIR
    HIR --> LogicalPredicates
```

```mermaid
flowchart LR
    UserSyntax --> HIR1
    HIR1 --> HIR2
    HIR2 --> LogicalPredicates
    HIR1["has only the where clauses the user wrote"]
    HIR2["has add'l where clauses that are implied, e.g., by types being WF"]
```

## 2022-06-14

- [#97641](https://github.com/rust-lang/rust/pull/97641/)
    - don't have two `compute_components` impls
        - it's bad
    - current state
        - break down complex types into type parameters, projections
    - next step is:
        - move the projection logic into fulfill path so that we only produce
            - type parameters
            - regions
        - then we can remove a lot of the "outlives" code
    - next step is:
        - handle type parametrs and regions in fulfill by searching parameter bounds etc
        - we can remove the "outlives" code entirely
        - and NLL no longer has to think about higher-ranked stuff
            - can remove universes from NLL
            - 

- soundness bug: [#98095](https://github.com/rust-lang/rust/issues/98095)
    - placeholders aren't handled correctly

## 2022-06-29

- random thoughts https://hackmd.io/vAj2CA8aS9mDL_xJlkVH7Q

## 2022-06-01

### oli/formality

Poked at formality...

* Casts in MIR are unimplemented
* Trying to document evaluation order of assignments
    * Operand order?
        * All left-to-right
    * Tricky cases
        * moves from raw pointers
        * derefs, indices
* WF regression, wanted to use it to to better understand how this stuff works

### lcnr: ???

### Niko: roadmap around implications

* extending implications isn't hard but
* if we're going to extend param-env with new outlives relations like `T: 'a`
    * need to modify the outlives code (see lcnr's PR below) to derive facts from the param-env and not straight from fn decl
* caching questions:
    * if we are adding new facts into the 

rough plan:

* extend param-env with new facts as we enter closure, thread param-env through as we add things to fulfillment context so that it affects outlives obligations in a natural way
    * challenges:
        * less cache hits
        * param-env may contain inference variables? -- no different than today probably, but maybe
        * there's probably code in the type checker that assumes it can leak param-envs all over the place and hence will wind up using the old one


```rust
trait PartialEq<T> 
{ }

impl<A, B, C> PartialEq<B> for A
where A: PartialEq<C>
//                 ^ if we did allow this, the trait solver would be picking C out of thin air
{
    
}


// but could still have goal `T: PartialEq<?X>`
//
// if there are no "unbound" inference variables like `?X`...can probably remove placeholders we don't reference
//
// we might be able to look at the final result and make the same conclusion


// we could someday support this, which formality does
impl<A, B> PartialEq<B> for A
where exists<C> { A: PartialEq<C> }
{
    
}

```

### TAITs

* adding in WF checks is kind of a pain, causes some regressions

problem:

* function that has more bounds than the type itself; we need to check WF of final type without those bounds
* but this is causing some regressions

```rust
// edition:2018
// check-pass
// revisions: stock sugg

trait Trait<Input> {
    type Output;
}

#[cfg(not(sugg))]
async fn walk<F>(filter: F)
where
    for<'a> F: Trait<&'a u32> + 'a,
    for<'a> <F as Trait<&'a u32>>::Output: 'a,
{
}

#[cfg(sugg)]
async fn walk<F: 'static>(filter: F) // <-- the 'static shouldn't be needed
where
    for<'a> F: Trait<&'a u32> + 'a,
    for<'a> <F as Trait<&'a u32>>::Output: 'a,
{
}

fn main() {}
```

this code doesn't compile either

```rust
fn foo<F>(f: F) 
where
    for<'a> F: 'a,
{
    foo(f);
}

fn main() { }
```


## 2022-05-18

### split of clauses/goals

### lcnr's PR

looking at https://github.com/lcnr/rust/pull/7/

how to relate types and lifetimes

* `!T: !a`
    * i.e., two placeholders
    * entireley handled by the trait code
* `!T: ?a`
    * i.e., an inference variable
    * the simple-sub approach

simple-sub:

* add a `-outlived-by-` edge to `?a`
    * `?a -outlived-by- !T`
* later on, if there is `?a: !b`
    * that would add a `?a -outlives- !b` edge
    * when you add this 2nd edge, you also find every thing `?a` is `-outlived-by-` and relate that to `!b`
        * `!T -outlives- !b` --> added as a new obliation, back into the trait solver

example:

```rust
&'a for<'b> fn(&'b ())
```

[`for<'b> fn(&'b ()): 'a` example](https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=4df8772c96b7b4f3c0d84bd512274628)

```
fn(&u8) : !a
```


```rust
for<T> T: 'a
```

### refactorings

* `coerce-unsized` refactoring (oh dear god)
* `fudge_inference_if_ok`
    * do some experiments on it and document them!
        * replace with `commit_if_ok`
        * remove trait solving
        * ... 
    * ignoring for now
* remove trait solving from diagnostics code  and use evaluation instead
* 

## 2022-05-11

### Part 1: trait solver handles higher-ranked stuff

Imagine you have this goal:

```
exists<'b> { for<'a> ('a: 'b) }
```

What trait solver would try to do...

```
exists<'c> all(('a : 'c), ('c : 'b))
                ^^^^^^^ must come from environment
```

```
exists<'a> { for<'b> ('a: 'b) }
```

in rustc today:

* the leak-check does this kind of rules
* this is equivalently doing this more often

### implications for coherence

wasm-bindgen pattern, simplified

```rust
trait SomeTrait { }
impl SomeTrait for for<'a> fn(&'a u8) { }
impl<'b> SomeTrait for fn(&'b u8) { }
```

* `for<'a> fn(&'a u8) == fn(&?b u8)`
    * `for<'a> fn(&'a u8) <= fn(&?b u8)`
        * `fn(?a) <= fn(?b)`
            * `exists<'a> { exists<'b> ('b: 'a) }`
            * `?b -outlives- ?a` :heavy_check_mark: (two inference vars always generate bounds and successfully compare)
                * add this to the environment, of course
    * `fn(&?b u8) <= for<'a> fn(&'a u8)`
        * new universe, add the placeholder !a into it
        * `fn(?b) <= fn(!a)`
            * `exists<'b> { forall<'a> ('b: 'a) }`
            * `!a <= ?b`
            * `!a -outlives- ?b`
                * look for lower bounds on `!a` in the environment; we find none (because we don't have empty)
                * `any()` --> error :x:


* in mir formality all outlives constraints are handled by the trait solver,
    * except for inference variables on all sides
    * trait solver breaks down more complex outlives bounds
* if we wanted to make rustc closer to this model:
    * we would extend fulfillment context so that when it has a outlives(P1, P2) obligation
        * it tries to process it per the rules in mir-formality
        * note that mir-formality sometimes uses Any goals (which rustc does not have)
    * we would still have outlives constraints getting generated and ultimately fed to borrow checker but they would be simpler, borrow checker would not need to know about universes
    * we would remove leak check in favor of the fulfillment context code above, which would sometimes lead to ordinary trait solving errors


Today:

* inference context
    * `RegionConstraintStorage` is updated with new constraints
        * add in `A <= B` constraints, which could be between any two regions in any universes
        * add in `R in (R1...Rn)` member constraints
        * add verifys
* fulfillment context
    * gets `RegionOutlives`
        * invokes `region_outlives_predicate` helper
            * which directly adds a `r1 -outlives- r2`
    * gets `TypeOutlives`
        * registers region obligation, which is a type-outlives relation `T: r`
* when relating types, and maybe at other times, we directly call `make_subregion` to create `r1 -outlives- r2` relations
* `process_registered_region_obligations`
    * part of regionck / borrowck, once type inference is done
    * extracts registered region obligations, invokes `type_must_outlive` to break them down into simpler constructs


Tomorrow:


* inference context
    * `RegionConstraintStorage` only stores constraints between regions of equal universe (or something like that)
* `region outlives requirements` are also handled by fufillment context in the case where placeholders are being related to other variables
    * help break down some of these cases
* `type_must_outlives` should be part of trait solving
    * produce new predicates for all components
    * type could be inference var:
        * just stay ambigous, mark blocked on the var and wait
    * later step: split goals and predicates
    * later step: add `any` predicates
        * annoying with projections, actually: no best way :trolldance:
            * let the trait solver pick something it likes :grin: 
* benefits:
    * simplified borrow checker and unblocked polonius
    * resolved the leak-check "question"
        * we know when/how the leak-checks, it is done by resolving type-must-outlives
    * opens the door to infering which closure parameters are higher-ranked

Immediate next steps that are unblocked:

* Begin refactoring `type_must_outlives` into trait solving (@lcnr)
* Refactor predicates into goals/clauses and support nested predicates (@oli-obk)
* Add implication goals ?? 
    * might be better to wait until the previous thing is done, might even have to

## Before 2022-05-11

* implementor: lcnr, oli-obk
* End state:
    * Refactor subtyping algorithm such that subtyping between higher-ranked types and associated types is handled by generating obligations that are fed to the fulfillment context.
* Milestones along the way:
    * Move region solving to trait solving
    * Refactor predicates into goals/clauses and support nested predicates
        * add the goals for All, Exists, Any 
    * Add implication goals
        * create an extended parameter context
        * question mark: the FreeRegionRelation code needs to be driven by the paramenv, look at how hard that is
    * Move leak check into fulfillment context
        * when you have a `'a: 'b` where they are not in same universe, rewrite with bounds from environment
    * Process higher-ranked subtyping via fulfillment context:
        * Refactor into goals/clauses and where-clauses and not just predicates
        * Add `Exists` and `All(P1, P2)` predicates
        * Convert to forall-exists
        * Remove the leak check while we're at it (yay!) (maybe!)
    * Fix #25860 by...
        * Add Implies predicate to solver
        * Desugar `fn() <: fn()` to include "plus implied bounds are entailed"
    * Process associated type subtyping:
        * Add `Any(P1, P2)` predicates
        * When relating an associated type we generate goals instead
    * Fix all the weird edge cases that lcnr was referring to and remove normalization from all over the compiler, remove norm under binders
    * Go get a :beer: and celebrate a job well done
* Side effects
    * Pave the way to close #25860
    * Fix lazy norm, simplify other stuff
    * Maybe it helps const?! I don't know.
* next step:
    * oli-obk, lcnr, and nikomatsakis to do an intro hackathon session
