# Types team meetup!?

## Agenda

* Nailing down initiatives, projects, features
* Who's doing what?
* How do they fit together?
* Example: GATs
* What problems are there currently, and what will it take to fix them?

### Day 1

Questions to answer
- Is this feature something we need to follow and slot into a roadmap?
- Does this have any surpising or complicated interactions with other features?

Feature planning

## nice to have but not worth talking about right now"

- Inherent associated types (https://github.com/rust-lang/rust/issues/8995)
- mostly astconv esque work, at least given today's architecture
- Better temporary lifetimes (https://github.com/rust-lang/rust/issues/15023)
- Ding Xiang Fei has been working on stuff in this area
- DST/custom coercions (https://github.com/rust-lang/rust/issues/18598)
- probably want an RFC before we stabilize anything else here
- Nonparametric dropck (https://github.com/rust-lang/rust/issues/28498)
- Fn traits (https://github.com/rust-lang/rust/issues/29625)
- would like to get this to work
- blocked on variadic generics, is there some subset?
- using the *tuple* interacts with unsized arguments
- could have an RFC for something like `impl Fn(&u32) for Blah`
- (but how does the return type work?)
- may_dangle (https://github.com/rust-lang/rust/issues/34761)
- Autoderef and autoref in operators (https://github.com/rust-lang/rust/issues/44762)
- Arbitrary self types (https://github.com/rust-lang/rust/issues/44874)
- Unsized rvalues (https://github.com/rust-lang/rust/issues/48055)
- Generalized two-phase borrows (https://github.com/rust-lang/rust/issues/49434)
- Impl trait in const and static items (https://github.com/rust-lang/rust/issues/63065)
- Impl trait (https://github.com/rust-lang/rust/issues/63066)
- Reservation impl (https://github.com/rust-lang/rust/issues/64631)
- Reserved from never impl (https://github.com/rust-lang/rust/issues/64715)
- we really should remove these, since never type stabilization stalled out anyhow
- Dyn upcasting (https://github.com/rust-lang/rust/issues/65991)
- Complex generic constants (https://github.com/rust-lang/rust/issues/76560)
- Associated const equality (https://github.com/rust-lang/rust/issues/92827)
- Impl trait in fn output (https://github.com/rust-lang/rust/issues/99697)
- Dyn star (https://github.com/rust-lang/rust/issues/102425)
- https://github.com/rust-lang/rust/issues/49682
- https://github.com/rust-lang/rust/issues/49206

## fixable soundness issues

- https://github.com/rust-lang/rust/issues/88901

## wtf is this

- https://github.com/rust-lang/rust/issues/85099
- https://github.com/rust-lang/rust/issues/84366
- https://github.com/rust-lang/rust/issues/68015

## closed

- Better where clauses (https://github.com/rust-lang/rust/issues/17657)
- Revised coercion rules (https://github.com/rust-lang/rust/issues/18469)
- DST coercions (https://github.com/rust-lang/rust/issues/27732)
- Associated type defaults (https://github.com/rust-lang/rust/issues/29661)
- blocked on .. nothing? groups? something?
- Constants in patterns (https://github.com/rust-lang/rust/issues/31434)

## no real work needed

- Auto traits (https://github.com/rust-lang/rust/issues/13231)
- no plan to stabilize ability for end-users to add auto traits (semver hazard)
- main thing is negative impls, but that's a separate bullet
- unsoundness that requires negative impls to be fixed properly?
- https://github.com/rust-lang/rust/issues/93367
- Unsized tuple coercion (https://github.com/rust-lang/rust/issues/42877)

## interesting interaction with solver

core solver discussion points

- removing the winnowing step
- and how we might approach backwards compatibility
- how to do leak check / region relationships, ensuring the erasure invariants
- elaboration : top down, bottom up, etc
- coinduction and overflow and normalization

core solver considerations

- Universe transition (https://github.com/rust-lang/rust/issues/56105)
- Re-remove leak check (https://github.com/rust-lang/rust/issues/59490)
- Trait aliases (https://github.com/rust-lang/rust/issues/41517)
- interacts with elaboration and expanded implies bounds, potentially
- Trait alias implementation (https://github.com/rust-lang/rust/issues/55628)
- Lazy normalization (https://github.com/rust-lang/rust/issues/60471)
- Overlapping impls of marker traits (https://github.com/rust-lang/rust/issues/29864)
- Trivial constraints in where clauses (https://github.com/rust-lang/rust/issues/48214)

interesting future-y discussions

- Refined trait impls (https://github.com/rust-lang/rust/issues/100706)
- Negative impls (https://github.com/rust-lang/rust/issues/68318)
- const generics / const eval
- Early vs late bound sadness

low priority

- Extended implied bounds (https://github.com/rust-lang/rust/issues/44491)
- Impl trait in type aliases (https://github.com/rust-lang/rust/issues/63063)
- (extended) GATs (https://github.com/rust-lang/rust/issues/95451
- object safety
- implied bounds
- type quantification
- Associated type bounds (https://github.com/rust-lang/rust/issues/52662)
- `Foo<T: Bar>` -- any reason not to stabilize this?
- implemented with impl trait (why?), leveraging some kind of weird hole
- maybe related to the way that we don't know `T::Item: Debug` in a case like this `fn foo<T: Bar<Item = U>, U>`?
- Existential generator madness
- "auto traits for generators"
- forall implied bounds
- `for<'a> &'a T: Foo` means:
- `for<'a> if(well-formed('a), well-formed(&'a T)) &'a T: Foo`
- which via elab implies `T: 'a`

super sci-fi

- Type equality constraints in where clauses (https://github.com/rust-lang/rust/issues/20041)

## maybe discuss this week

- Fundamental (https://github.com/rust-lang/rust/issues/29635)
- could separate types vs traits?
- dyn trait unsoundnesses
- https://github.com/rust-lang/rust/issues/50781
- https://github.com/rust-lang/rust/issues/44454
- https://github.com/rust-lang/rust/issues/57893

## if we're ridiculously successful

- Specialization (https://github.com/rust-lang/rust/issues/31844)
- `for<'a>` closures (https://github.com/rust-lang/rust/issues/97362)
- talk out the type inference that would make this unnecessary?
- Never type (https://github.com/rust-lang/rust/issues/35121)
- need simulacrum
- resolve_trait_on_defaulted_unit (https://github.com/rust-lang/rust/issues/39216)
- is this .... still a thing? should it be closed?
- Tweaks to object safety (https://github.com/rust-lang/rust/issues/43561)
- various parts
- not really about core trait solver, so prob don't deep dive this week
- https://github.com/rust-lang/rust/issues/50781
- Async closure (https://github.com/rust-lang/rust/issues/62290)
- interacts with gats? impl limitations? something??
- Const trait (https://github.com/rust-lang/rust/issues/67792)
- Static async fns in traits (https://github.com/rust-lang/rust/issues/91611)
- Coherence can be bypassed by an indirect impl for a trait object #57893 https://github.com/rust-lang/rust/issues/57893

### Coinduction notes

https://github.com/rust-lang/rust/issues/80807

### Day 1

* Key things to work backwards from
* Static AFIT
* Lazy norm -- motivated by bugs and cycles in various features
* Existential Generator Madness
* GAT implied bounds
* Perfect derive
* Basic restrictions on trait solver
* everything requires soundness
* codegen requires soundness in face of lifetime erasure
* explore the edge cases here
* coherence requires completeness
* Trait solver rewrite based on this and above

#### Static AFIT

Where it's at:

trait Foo {
    async fn bar(&mut self);
}

impl Foo for u32 {
    async fn bar(&mut self) {}
}

RPITIT (:frog: types)

works apart from lifetime limitations that you wouldn't have seen before

trait Foo {
    fn bar<'a>(&'a mut self) -> (Self::bar::rpitit)<Self, 'a>
        type rpitit<'a>: Future<Output = ()>;
}

impl Foo for u32 {
    fn bar<'a>(&'a mut self) -> (Self::bar::opaque)<'a>
    {
        type opaque<'a> = impl Future<Output = ()> + 'a
    }
}

async fn main() {
    let x = u32;
    x.bar().await;
}

normalizing rpitit for an impl invokes a query that computes values of rpitit for given method from given impl / trait substitution:

* get signature from trait, replace rpitit's with inference variables
* get signature from impl
* equate them, take values from the inference variables

buggy case https://github.com/rust-lang/rust/issues/103457

pub trait SpiDevice {
    async fn transaction<'a, F: 'a>(&'a mut self, f: F);
}

impl SpiDevice for () {
    async fn transaction<'a, F: 'a>(&'a mut self, f: F) {}
    // duplicates 'a and so we have the wrong 'a
}

fixed by [PR #103491](https://github.com/rust-lang/rust/issues/103491) but other relates problems don't get fixed yet; extended work in [PR #103499](https://github.com/rust-lang/rust/pull/103449).

We could ship by fixing above, which is more of a lowering concern, and thus this is independent from solver details we are focused on currently. But to cleanup and simplify, interacts with:

* eliminating early/late-bound
* how we manage refinement

Two other things that we don't need to discuss now

* lowering to make it more like an assoc type
* how does this show up in a-mir-formality

#### Lazy norm -- motivated by bugs and cycles in various features

What do we even mean by this?

* Don't eagerly normalize after substitution
* During relations, generate projection equality goals
* Basically what Boxy's PR does: https://github.com/rust-lang/rust/pull/96912
* Blocked on overflow
* Might be blocked on "inference in evaluate" (siblings in evaluate don't affect one another)
* Places where we have to explicitly normalize
* codegen
* layout
* various places might force "shallow" normalization:
* type checker calls to structurally resolve:
* field access
* method invocation
* trait checker / candidate assembly for certain traits:
* `Tuple` trait and other where built-in traits like `DiscriminantKind`, `Pointee`
* Auto traits
* Coercion
* Associated type in impl signatures?
* Falls out from relating (has worse performance for filtering impls)
* Is this related? https://github.com/rust-lang/rust/issues/87755
* Also this: https://github.com/rust-lang/rust/issues/80807

#### Existential Generator Madness

For example: https://github.com/rust-lang/rust/issues/104382

Today we have

* `Generator(exists<'a...> [Ty...])`

!0 fresh
(['a => !0] T): Send
------------------
(exists<'a> T): Send

but we should have

* `Generator(exists<'a...> if (WF(Ty)...) [Ty...])`

This solves the issue where we might need to normalize a type within a struct field, for example.

but this only solves some problems. Other problems:

* You could have send impls that have add'l lifetime requirements beyond WF; this is a problem for TAITs and other forms of auto-trait leakage as well
* But there might also be other constraints

#### Gat Implied Bounds

Example from the test https://github.com/rust-lang/rust/blob/master/src/test/ui/generic-associated-types/bugs/hrtb-implied-1.rs:

use std::fmt::Debug;

pub trait LendingIterator {
    type Item<'this>
    where
        Self: 'this;
}

pub struct WindowsMut<'x> {
    slice: &'x (),
}

impl<'y> LendingIterator for WindowsMut<'y> {
    type Item<'this> = &'this mut () where 'y: 'this;
}

fn print_items<I>(_iter: I)
where
    I: LendingIterator,
    for<'a> I::Item<'a>: Debug, // <- Currently requires I::Item<'static>
{
}

fn main() {
    let slice = &mut ();
    //~^ temporary value dropped while borrowed
    let windows = WindowsMut { slice };
    print_items::<WindowsMut<'_>>(windows);
}

#### Perfect derive

struct List<T> {
    value: T,
    next: Option<Box<List<T>>>,
}

trait Trait { }

impl<T> Trait for List<T>
where
    T: Trait,
    Option<Box<List<T>>>: Trait,
{}

Basically requires coinduction

Doing coinduction in a reasonable way requires a "unified eval/fulfill" where solving traits is more cleanly separated from the surrounding context

#### Basic restrictions on trait solver

* Solve(Goal) = Yes | No | Ambiguous
* Sound: Yes means "true"
* Complete: No means "false"
* Ambiguous is always ok to return
* Adding ambiguity in solver makes fewer things compile
* Removing ambiguity makes more things compile
* Everything requires soundness
* Coherence requires completeness
* because it must prove negative goals
* `not { coherence-mode(G) }`
* If type checker solves goal G and gets result X, at monomorphization time solving equivalent of G should also get result X
* have to figure out how to formulate this precisely, and take into account defaults/specialization
* tl;dr type-checker shouldn't conclude X when, at monomorphization time, X will be false
* `fn foo<T: Into<u32>>(x: T) { let i = x.into(); ... }`
* have to be thoughtful about existential goals here, e.g., this is why adding `exists<G>` as a where-clause is prob not a good idea
* Information about free regions should not affect results of trait solver ("at top level")
* because it will be used in the codegen, where we don't know the lifetimes
* Associated type normalization (in monomorphized state) yields at most one unique result
* What does "true" mean for a `is_implemented(T: Ord)` predicate:
* there is a combination of impls that matches `T`, and all where clauses are satisfied with other impls
* can form cycles, or could be a cycle of infinite length (think about this one...?)
* Two types being equal means trait solver returns same results for them
* thanks to !@$#!@$! TypeId, have to have canonical versions of types ("strongly normalizing")
* https://github.com/rust-lang/rust/issues/97156
* Monomorphization always succeeds (modulo size limits)
* trait solving in codegen never dive
* can still have non-normalizable projections (if there are forall types) but should never need to normalize them
* Interesting completeness cases:
* Normalization
* Relating lifetimes to one another

#### Scary unsoundnesses

https://github.com/rust-lang/rust/issues?page=1&q=is%3Aopen+is%3Aissue+label%3AI-unsound

* [Oli's overview from March](https://hackmd.io/OzhI-Ub1SpWVzPj0IwRdpw)

[orphan check incorrectly handles projections](https://github.com/rust-lang/rust/issues/99554)


### Day 2

Trait solver rewrite covering...

* How we get the capabilities we need for features
* Diagnostics
* Borrow checker / polonius interface

Deep dive into a couple issues

@lcnr's goals:
1) Remove fulfill
2) Evaluate be canonical

For evaluate to be canonical, need overflow to be non-fatal

#### canonicalize and coinduction

Want to canonicalize instead of freshening:
- cycles?

requires evaluate to return inference results

Coinductive cycle: `Vec<?a>: Send` requires `Vec<?b>: Send`
Canonicalize: both result in `Vec<^0>: Send`
The evaluation requires `?a` to be `Vec<?b>`.

trait Foo {}
struct Wrapper<T>(T);

impl<T> Foo for Wrapper<Wrapper<T>>
where
    Wrapper<T>: Foo
{} 

query: does `Wrapper<?0>: Foo` hold?
- candidate: `impl<T> Foo for Wrapper<Wrapper<T>>` -> `?0 -> Wrapper<?1>`
- nested: `Wrapper<?1>: Foo` COINDUCTIVE CYCLE OK
- query returns `OK`: `?0 = Wrapper<?1>`

lcnr solution: if it constrains infer vars: requires rerun with substitutions applied: `Wrapper<Wrapper<?1>>: Foo`

Chalk:

goal {
    exists<T> {
        Wrapper<T>: Foo
    }
} yields[SolverChoice::slg_default()] {
    expect![["Unique; for<?U0> { substitution [?0 := Wrapper<^0.0>] }"]]
}

Full test: https://github.com/rust-lang/chalk/pull/784

---

inductive

struct Vec<T> { }

impl<T> Foo for Vec<T>
where
    T: Foo + Copy,
{ }

impl<T> Foo for u32
{ }

// Question: ?T: Foo has one result Vec<u32>

struct Vec<T> { }

impl<T> Foo for Vec<T>
where
    T: Foo + Copy,
{ }

impl<T> Foo for u32
{ }

Strategy A (external iteration):

* push on stack
* when cycle occurs, consider ok
* commit final result to cache
* caller checks: if non-empty subst, re-execute with subst applied

Strategy B (internal iteration, a la chalk):

* push on stack with intermediate result
* when cycle occurs, use intermediate result
* execute until fixed point, then commit results to global cache

trait Foo<Y> { }

impl<A, B> Foo<A> for Vec<B>
where
    A: Foo<B>

// What Niko thought was being proposed, but which was broken
// 
// Canonical query
//   ?X: Foo<?Y>
//      ?X = Vec<?B>
//      ?Y = ?A
//      ?A: Foo<?B> -- canonically equal, ok result
//   Vec<?B>: Foo<?Y>
//      Vec<?B> = Vec<?B'>
//      ?Y = ?A'
//      ?A': Foo<?B'> -- canonically equal, ok result
//   done, successful

trait Trait<'a, 'b> {}

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

goal `(): Trait<'a, 'b>`
- requires `'b: 'a`
- requires `(): Trait<'static, 'a>` COINDUCTIVE CYCLE: OK

external iteration approach: DONE (can instead rerun until region obligations are saturated)

internal iteration approach: rerun with the `'b: 'a` requirement: results in an additional `'a: 'static` requirement. Then rerun deduplicates and is done.

(sidenote: erasing `'static` ok https://github.com/rust-lang/rust/pull/102472)

Question:

* interaction with region obligations

---

Formality canonical query:

https://github.com/nikomatsakis/a-mir-formality/blob/main/crates/formality-logic/src/env/query.rs

Basically:

* Renumber all free variables (placeholders, existential) in order of appearance
* Compress universes
* Return a map

Two knobs:

* How do you handle lifetimes?
* what should canonical form of `T: Trait<'a, 'a>` be?
* `T: Trait<^0, ^1>` // <-- erased identity
* `T: Trait<^0, ^0>`
* `erase(T: Trait<'a, 'a>) ==> T: Trait<?0, ?1>` for two fresh variables `?0, ?1`
* replaces every free lifetime with a fresh existential variable in the goal
* there is a "erase identity" step that type checker should do
* (how does that interact with universes?)
* (how does it work with recursive queries?)

wasm-bindgen pattern

trait T {
    fn x() {}
}

impl<A> T for fn(A) {}
impl<A> T for fn(&A) {} // cause #[warn(coherence_leak_check)] on nightly 2020-03-29

fn main() {
    <fn(&'static u8)>::x();
    <fn(&u8)>::x(); // requires the impl<A> T for fn(&A) to compile
}

related pattern:

trait T {
    fn x() {}
}

impl<'a, A> T for fn(&'a A) {}
impl<A> T     for for<'a> fn(&'a A) {} // cause #[warn(coherence_leak_check)] on nightly 2020-03-29

fn main() {
    <fn(&'static u8)>::x();
    <fn(&u8)>::x(); // requires the impl<A> T for fn(&A) to compile
}

`fn(&'static String)` and `for<'a> fn(&'a String)` are both `'static` and can be converted to `dyn Any`. Must not be able to downcast `fn(&'static String)` to `for<'a> fn(&'a String)`.

* Related pattern with self = `for<'a> fn(&'a u8)`
* erased version is equal to itself `for<'a> fn(&'a u8)`
* create two alternative paths, one for each impl
* path A: equate `fn(&?0 A)` with `for<'a> fn(&'a A)`
* in mir-formality
* `equate(fn(&?0 A), for<'a> fn(&'a A))` returns a goal
* `for<'a> equate(fn(&?0 A), fn(&'a A))`
* `equate(&?0 A), fn(&!1 A))`
* `?0 = !1`
* searches the environment for bounds on `!1`
* finds none
* errors
* we want this to fail at some point
* path B: equate `for<'a> fn(&'a A)` with `for<'a> fn(&'a A)`
* we want this to succeed
* done

trait Region<'a> { }

struct Foo { }
impl<'a> Region<'a> for Foo { }

struct Bar { }
impl Region<'static> for Bar { }

impl<T> Debug for T
where
    for<'a> T: Region<'a>,
{}

impl Debug for Bar { }

fn main() {
    // is_implemented(Foo: Debug)
    // is_implemented(Bar: Debug)
}

* Solving `Foo: Debug`
* subgoal `for<'a> Foo: Region<'a>`
* `Foo: Region<!1>`
* erase/canonicalize that to `Foo: Region<?0>` with ?0 in universe 1
* we get back a "true" result with (effectively) no constraints
* ok this works
* Solving `Bar: Debug`
* impl Debug for Bar is ok
* subgoal `for<'a> Bar: Region<'a>`
* `Bar: Region<!1>`
* erase/canonicalize that to `Bar: Region<?0>` with ?0 in universe 1
* we get back a "true" result with `?0 = 'static`
* unify `!1` and `'static'`, error
* ok, take Bar impl

trait Region1<'a, 'b> { }
trait Region2<'a, 'b> { }

impl<'a, 'b, T> Region1<'a, 'b> for T
where
    T: Region2<'a, 'b>
{}

struct Foo { }

struct Bar { }

impl<'a, 'b> Region2<'a, 'b> for T { }

impl<'a, 'b> Region2<'a, 'b> for T
where
    'b: 'a,
{ }

impl<T> Debug for T
where
    for<'a, 'b> T: Region1<'a, 'b>,
{}

fn main() {
    // is_implemented(Foo: Debug)
    // is_implemented(Bar: Debug)
}

* Now when we prove `Bar: Debug`...
* `subgoal(for<'a, 'b> Bar: Region1<'a, 'b>)`
* `Bar: Region2<'?a, '?b>` will result in `?a = ?b`
* errors out here

ambiguous candidates: need to drop one because of regions
- `impl<'a, 'b: 'a> Trait<'a, 'b> for Foo`
- `impl<'a: 'b, 'b> Trait<'a, 'b> for Foo`

goal: `for<'a, 'b> where { 'a: 'b } Foo: Trait<'a, 'b>`

"scary" situation:

* two impls, only way to distinguish is via a `'a: 'b` relation that we know not to hold because of universes
* if we erase universe information in recursive solving, we will encounter ambiguity here

argument:

* this case must fail coherence

proof 1:

* coherence instantiates all those lifetimes with fresh variables in some equal universe, so it could never distinguish them

proof 2:

* by contradiction:
* if we accepted those two impls, there could be other code which tries to solve `T: Trait<'a, 'b>` at codegen time and it could never tell the difference
* but you could imagine coherence accepting and having type check ensure we never reach codegen in a case where the regions would be erased (i.e., outside of higher-ranked thing)

scary situation:

* we have `Any` goal: 2 candidates one fails due to higher ranked region stuff
* when proving, don't know that one fails
* have to return region obligations

"solution":
* allow `OR` of region obligations from canonical queries

issue:
* polonius doesn't like it :(
* exponential combinations when combined with AND

but: higher ranked stuff in `OR` can be discarded by the solver at a later point, can merge stuff in root universe.

#[marker]
trait Foo<'a, 'b> { }

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

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

#[marker]
trait Foo<'a, 'b> { }

impl<'a, 'b, T: OtherTrait> Foo<'a, 'b> for T { }

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

Results of a query:

* Yes
* Binder:
* Substitution
* "External" constraints:
* Region constraints
* or
* Opaque type constraints
* ...other things?
* Maybe
* Definite guidance
* `Foo<?T>: Debug` and there's an impl `Foo<Vec<T>>: Debug`
* you get back: ambiguous, but `for<?U> { ?T = Vec<?U> }`
* Suggested guidance
* Due to overflow
* No

Chalk: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/solve.rs

When can you stop early:

* ANY:
* If you get YES with no external constraints, can always stop
* Otherwise, must continue, because a future "maybe" could be a YES with no external constraints
* YES || AMBIGUOUS = AMBIGUOUS, unless YES has no external constraints
* ALL:
* NO && AMBIGUOUS = NO, so if you get NO, can always stop
* Otherwise, must continue
* YES && AMBIGUOUS = AMBIGUOUS, duh

#### Overflow and timeout

Ways to prevent infinite work

* Size of goal
* Quantum exceeded

Both are non-fatal

One scheme:

* Non-DFS search + root goal quantum
* track total work for the root goal
* if it exceeds a given threshold, return and cache OVERFLOW for root node (but no internal nodes are cached)
* take a breadth-first strategy (or something like it)
* can combine with size-of-goal limit
* maybe delete work from completed things?
* Per-branch quantum, reduce the depth for subsequent branches on overflow
* if one branch goes too high, then reduce depth
* tricky interaction with caching etc
* weird but maybe worth trying

#### How do we get there

* Incremental steps vs bigger rewrite
* Steps lcnr has in mind
* Evaluate
* Overflow
* Canonicalize each step along incremental
* Freshen goals independently
* Returning "inference artifacts"
* i.e., adopting something like the "query result" above?
* Stop special-cased static in freshening ??
* Remove fulfillment
* have to handle diagnostics somehow
* Winnowing
* This can be seen as special treatment for the "ANY" goal

No firm conclusion on best order to land PRs etc

#### Diagnostics

We seem to want to have a... compute tree, and (in interim) use that to synthesize a fulfillment error?

This could be achieved by

* some kind of associated type and we parameterize the solver over it
* some kind of callback that we invoke with events as we are doing the solving

#### Chalk vs rustc

* chalk status
* ty::Param TyKind variant
* recursive solver has some open bugs that result in ambiguity
* SLG solver doesn't manage associated types
* const eval which is completely unintegrated

#### trait solver rewrite

#### Trait alias deep dive :)

RFC: https://github.com/rust-lang/rfcs/blob/master/text/1733-trait-alias.md

What are they?
- Traits with one builtin impl

trait Bar {}
trait Foo where Self: Bar {}

### Day 3

Spillover, if we have extra time...

* borrow checking?
* modeling trait aliases?
* type aliases?
* specialization?

#### What questions do we want to ask trait solver and where

* Goal =
* `is_implemented(T: ...)`
* `...`

#### Trait solver rewrite hacking

Chalk:
- https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/solve.rs#L12
- https://github.com/rust-lang/chalk/blob/master/chalk-ir/src/lib.rs#L3019

Entry function:

struct ParamEnv {
    hypotheses: Vec<Predicate>,
}

struct Query {
    env: ParamEnv,
    goal: Predicate,
}

type CanonicalQuery = Canonical<Query>;

type CanonicalResult = Canonical<Result>,

fn select(infcx, trait_obligation) -> Candidate {
    assemble_trait_candidates
    
    filter_candidates
}

fn evaluate_goal_query(
    tcx: TyCtxt,
    query: CanonicalQuery
) -> CanonicalResult {
    let cx = EvalCtxt::new(tcx);
    cx.evaluate_goal(query)
}


struct EvalCtxt {
    coherence_mode: CoherenceMode,
    stack: Vec<CanonicalQuery>,
    // Provisional results, need to be fed into query system after the query is finished
    cached_results: Map<CanonicalQuery, Result>
}

enum Result {
    Yes {
        substitutions: ...,
        // Opaques and regions
        external_constraints: ...,
    },
    Maybe {
        substititons: ...,
        cause: MaybeCause,
    },
    No,
}

enum MaybeCause {
    // These substitutions are *required* for us to prove it in this context, but not *sufficient*
    //
    // (After monomorphization, there could be other substitutions for which the goal would be true)
    Definite,
    
    // Our "educated guess" is that the user wants this substitution.
    Suggested,
    
    // Why have you done this to me
    Overflow,
}

struct EvalNode {
    result: CanonicalResult,
    minimum: Option<usize>,
    on_stack: Option<usize>, // if true, index in the vector where this appears on stack
}

V1:

enum CacheHit {
    Done(CanonicalResult),
    InProgress(..),
    Miss,
}

impl EvalCtxt {
    fn check_cache(query: CanonicalQuery) -> CacheHit {
        // checks global and local caches
        ..
    }
    
    fn evaluate_goal(
        self,
        query: CanonicalQuery,
    ) -> CanonicalResult 
    {
        match self.check_cache(query) {
            Done(result) => return result,
            InProgress(data) => {
                // Mark that we find this goal at this stack depth
                self.mark_stack(data);
                return if cycle_is_coinductive {
                    ...
                } else {
                    ...
                };
            }
            Miss => self.push_stack(query),
        }
        loop {
            let result = self.compute_goal(query);
            if no_cycle || final_solution == self.stack.top().solution {
                return final_solution;
            }
                    
            self.stack.top().solution = final_solution;   
        }
        // puts stuff into cache or what not
        self.finalize_evaluate(result)
    }
    
    fn compute_goal(self, query: CanonicalQuery) -> CanonicalResult {
        let (infcx, Query { env, goal }) = InferCtxt::new(query);
                
        if goal is too big {
            return overflow;
        }
        
        let result = match goal.kind() {
            Trait(tr) => self.compute_trait_goal(env, tr),
            Projection(proj) => self.compute_projection_goal(env, proj),
            Boring => ok,
        };
        
        canonicalize(result)
     }
     
     fn compute_trait_goal(self, env: Environment, goal: TraitGoal) -> Result {
        let mut results = vec![];

        // filters out No results
        self.assemble_and_evaluate_trait_candidates(&mut results);

        final_solution = self.deal_with_multiple_trait_candidates(results)
    }
         
    fn assemble_and_evaluate_trait_candidates(env, goal: TraitGoal, results: &mut Vec<CandidateAndCanonicalResult>) {
        if goal.self_type() is projection {
            // Treat ambiguity as ok here
            let result = self.evaluate_normalizes_candidate(goal);
            results.push(result);
            
            if result is yes {
                return;
            }
        }
        
        from_impls(&mut results);
        from_param_env(&mut results);
        from_...(&mut results);
    }
    
    fn evaluate_normalizes_candidate(goal: TraitGoal) -> CanonicalResult {
        // or we adjust subst or something
        let v = fresh_inference_var();
        match self.evaluate_goal(normalizes_to(goal.self_type(), v)) {
            Yes => self.evaluate_goal(goal.with_self_type(v)),
            r => r,
        }
    }
    
    fn compute_projection_goal(self, env: Environment, goal: ProjectionGoal) -> Result {
        // try normalize
        let candidate_with_results = vec![]
        assemble_and_evaluate_trait_candidates(env, goal.as_trait()).filter_map(|t| to_proj_candidate_and_unify(t));
        assemble_other_proj_candidates_and_unify(env, goal, &mut candidate_with_results);
        
        
        // whether we unify before resolving ambiguity or not is user visible.
        // 
        // example
        // 
        // impl Item for Vec<u32> {
        //     type Item = u32;
        // }
        // impl Item for Vec<i32> {
        //     type Item = i32;
        // }
        // 
        // if you have `<Vec<?T> as Item>::Item = u32`, can I infer that `?T = u32`?
        // In today's compiler no, but with this version, yes.
        // 
        // Maybe this impacts method resolution or other things, not obvious whether
        // this will cause breakage in practice.
        deal_with_multiple_projection_candidates(candidate_with_results)
    }
         
    fn evaluate_candidate(self, candidate: Candidate) -> CanonicalResult {
        probe {
            let goals = confirm_candidate(candidate);
            self.evaluate_all(goals)
        }
    }

    fn evaluate_all(self, goals: &[Goal]) -> CanonicalResult {
        blah
        
        // do the "overflow thing" -- if a goal overflows, check remaining goals for error
        // but in some mode that suppresses caching ...? or which only goes so deep recursively?
    }
}

### Early, late

fn foo<'a, T>(t: &'a T) {
    
}

fn main() {
    let f = foo;
    f(None::<u32>);
    f(None);
}

struct foo<T> {
    /* fn def */
}

impl<'a, T> Fn<(&'a T,)> for foo<T>
where
    // where-clauses
{
    
}

fn main() {
    let f: /* foo<_> */ = foo;
    f(&None::<u32>);
    f(&None);
}

struct foo<'a, T> {
    /* fn def */
}

impl<'a, T> Fn<(&'a T,)> for foo<'a, T>
where
    // where-clauses
{
    
}

fn main() {
    let f: /* for<'a, T> if (WC) foo<'a, T> */ = foo /* for<'a, T> foo<'a, T> */ as for<'a> if (WC[T/?T]) foo<'a, ?T>;
    f(&None);
    f(&None);
}

fn bar<'a>() -> &'a u32 { }

impl<'a> Fn<()> for bar
where
    // where-clauses
{
    type Output = &'a u32; // ERROR: 'a is not constrained
}

alternative translation:

fn bar<'a>() -> &'a u32 { }
struct bar<'a> { }

impl<'a> Fn<()> for bar<'a>
where
    // where-clauses
{
    type Output = &'a u32; // OK
}

#103448 -- we're in agreement on this general approach! Quite close to what was discussed above.

### syntactic vs semantic equality

hit some weird errors

would be a perf improvement

### Goals

Current focus:

* Building a platform that can scale to the new features we will need
* Sound, testable, documented type system
* Sustainable open-source team to maintain this

Next summer:

- A WIP new trait solver (testable)
- MIR Formality is testable against Rust test suite
- Features:
- TAIT
- RPITIT

EOY 2023: New foundations designed and in initial use

- New trait solver replaces evaluate, but not used everywhere
- Onboarding plan and documentation for new trait solver
- MIR Formality integrated into language design process

EOY 2024: New foundations shipped and shared

- New trait solver shared by rustc and rust-analyzer
- milestone: type-ir used by rustc/rust-analyzer
- Clean API for extensible trait errors / visualization
- at least available internally
- Shiny new features:
- Polonius
- GAT implied bounds
- impl trait every-dang-where
- Edition boundary things
- Trait changes e.g. opt-in dyn-ness
- Inference changes --
- make `Into` stop inferring?
- early-late interactions?

EOY 2027: :euro: Profit :euro:

- (Types) I-unsound issues resolved :tada:
- Most extensions are easy to do; large extensions are feasible
- MIR Formality passes 99.9% of Rust test suite

#### Const generics

It's hard.

https://github.com/rust-lang/rust/issues/98956