# 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 = 

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:

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

trait FnPointer { }

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

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 {
}

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

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:

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() { }

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() { }

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?

#[marker]
trait Marker {}

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

or

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)`

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

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:

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**

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

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

// 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?

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...

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

struct Foo<T: Ord> { }

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

#![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

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>() { }

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:

#![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

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

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

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`

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

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>>() {}

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> },
{}

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

// 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

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.

// 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.

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
}

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

but pre-existing in some sense:

// 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
}

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

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

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:

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?

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?

trait SomeTrait2<'a, 'b> { }

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

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

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

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
}

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

`'a: 'b => 'a: 'b`

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

#![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

#![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/ ?

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)`

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

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

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

flowchart LR
    UserSyntax --> HIR
    HIR --> LogicalPredicates

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

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

// 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

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:

&'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

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

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