# 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:
```rust
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
```rust
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
```rust
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:
```rust
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
```rust
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>`.
```rust
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
```rust
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>
```
```rust
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
```rust
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
```
```rust
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
```rust
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:
```rust
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
```rust
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
```rust
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.
```rust
#[marker]
trait Foo<'a, 'b> { }
impl<'a, 'b> Foo<'a, 'b> for () { }
impl<'a, 'b> Foo<'a, 'b> for ()
where
'a: 'b,
{ }
```
```rust
#[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
```rust
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:
```rust
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:
```rust
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
```rust
fn foo<'a, T>(t: &'a T) {
}
fn main() {
let f = foo;
f(None::<u32>);
f(None);
}
```
```rust
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);
}
```
```rust
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);
}
```
```rust
fn bar<'a>() -> &'a u32 { }
impl<'a> Fn<()> for bar
where
// where-clauses
{
type Output = &'a u32; // ERROR: 'a is not constrained
}
```
alternative translation:
```rust
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
Sign in with Wallet
Connect another wallet