TAIT overview

Old solver

Inferring opaques in the old solver is mainly the responsibility of two parts of the type system:

Relations - Eq, Sub, TypeRelating (NLL) handle cases when opaques are equated with other types.
replace_opaque_types_with_inference_vars, which manually folds a type, replacing any in-scope opaques with inference variables, which is itself used in to places:
- Checking a function body, replacing the TAITs and RPITs that show up in the signature with infer vars eagerly. This is necessary to handle fallback correctly.
- In projection predicates. This is necessary to not break backwards-compatibility with nested RPITs that don't meet bounds.
  - real world example in linkerd
  - A minimal test using no nightly features

Old solver (more notes):

Replace with infer vars for RPITs and TAITs in function signatures — main place both are constrained
For other cases, such as local variables and structs with TAIT return type, the eq and sub relations eagerly, depending on DefineOpaqueTypes
- Bubble is too inaccurate so we need to not define types eagerly in some cases to avoid spurious errors.
Borrowck does not replace opaques eagerly with infer vars, and handles opaques in the relation
Opaques in queries act subtly different due to DefiningAnchor::Bubble
Projections are weird, can coincidentally replace opaques with infer vars outside of queries due to hack (link issue)

`DefineOpaqueTypes`

Since Eq and similar relations all succeed when comparing an opaque type against any type satisfying its bound, we sometimes run into issues (similar to how comparing against inference vars always succeeds).

Contrary to its outdated documentation, it is not used just

to prevent predicate matching from matching anything against opaque types.

But most usage sites (2/3rd) are now rejecting opaque types from being equal to any type fulfilling its bounds and registering said type as a hidden type.

It is a feature grown out of necessity of how we do type checking and how opaque types in the old solver work.

type Foo = impl Debug;

fn test() {
    // case 1:
    let x: Foo = 22_i32; // Coercion from i32 to Foo?
}

type Foo = impl Debug;

 fn test() {
    // case 2:
    let a: Option<_> = None;
    let x: Foo = a.unwrap(); // Coercion from ?X to Foo?
}

Bubbles!!

Image Not Showing Possible Reasons

The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported

Learn More →

DefiningAnchor::Bubble –

collect all the possible impact cases, re-apply at the call site, which is a bit risky
- in case we drop those annotations on the floor
can define if things hold "modulo opaques"
can also impact the flow of trait resolution in "potentially unexpected" ways

one challenging case:

opaque1 = opaque2, which is the hidden type of the other?
- in bubble environment, we cannot know
- we currently create a predicate and bubble that out

Background

Don't want to go into much detail about how the type_of query actually delegates out to the typeck queries to find out where an opaque is defined. This doesn't change between the old solver, and is pretty well detailed in the dev guide.

New solver:

Alias-relate predicate is responsible for all opaque eq ty, opaques are only constrained in obligations
Returns constrained opaques in query response

type Foo = impl Sized;

fn main() {
    let x: Foo = 22;
    println!("{x}"); // does this compile or not? Yes in new solver, no in old solver.

    let x: impl Debug = 22; // Does this just require Debug or is it like RPIT?
    println!("{x}");
}

fn tyeq<T>(_: T, _: T) {}
fn main() {
    type Foo = impl Sized;
    let x: Foo = 42u32;
    let y: impl Sized = 42u32;
    tyeq(x, 0u32); // ?
    tyeq(y, 0u32); // ?
}

Self::Something = impl

impl X {
    type Something = impl Whatever;
    
    fn foo() {
        let x: Self::Something = ...;
    }
}

Michael's point:

Given a type lambda application Lambda<...Ti...>, it should be valid to change to ?X = Ti and Lambda<...?x...>.
- Specific example: T::Foo normalization

errs: Recursive calls act as real opaques, not replaced w/ infer vars

fn foo() -> impl Debug {
    if something {
        foo()
    } else {
        22
    }
}

fn foo() -> impl Debug {
    let x: u32 = foo();
    loop {}
}

errs (old solver):

fn eq<T>(a: T, _: T) -> T { a }

fn foo() -> impl Sized {
    let x = eq(foo(), 1u32);
    println!("{x}"); // error :(
    loop {}
}

(Workaround is:)

fn eq<T>(a: T, _: T) -> T { a }
fn foo() -> impl Sized {
    let x = eq(foo(), 1u32);
    println!("{}", x as u32); // OK
    loop {}
}

Happens in super_combine for all relations (eq and sub don’t have the opaque handling code special to them)
Opaques can end up being revealed locally later on
Pre-populate borrowck
- no fulfillment context

Problems with new solver:

Opaques can only be defined once modulo regions
opaque use in the defining scope

type TAIT = impl Display;

fn use(x: TAIT) {
    // this side-steps autoderef
    Display::fmt(&x, ...);

    // in old solver: this works
    // in new solver: errors with ambiguity
    x.fmt(...)
}

fn define() -> TAIT {
    1
}

// Compiles today
// Fails in new solver
fn rpit_example(n: u32) -> impl std::fmt::Display {
    if n > 0 {
        rpit_example(n - 1).to_string()
    } else {
        format!("Hello, Ferris")
    }
}

fn main() { }

project goals in non-defining use in defining scope: https://rust.godbolt.org/z/e5sbrrjP8

trait TAIT = impl Iterator<Item = u32>;

fn impls_iter<T: Iterator<Item = U>, U>(_: T) {}

fn non_defining_use(x: TAIT) {
    impls_iter(x)
}

TC: Is there an old-solver/new-solver difference for?: https://rust.godbolt.org/z/1cTh8r5Mh

#![feature(type_alias_impl_trait)]

type Foo = impl Sized;
fn foo() -> Foo {}
fn bar() -> impl Sized { foo() }
//^~ error: opaque type's hidden type cannot be another opaque type from the same scope

// Question is:
// - do we choose to constrain `Foo` to the RPIT of `bar` (error) or vice versa (ok)

How do we align new and old solver behavior

Pass in a specific defining anchor instead of bubble
- this will impact caching
- something something wf

Expected outcomes

Some more confidence about the future of TAIT and its interaction with the new trait solver.
?

Key questions for discussion

Notes from the meetup itself

Niko: unsound examples of opaque types?

https://github.com/rust-lang/rust/issues?q=is%3Aopen+label%3AI-unsound+label%3AA-impl-trait

NM: What do we have to do to stabilize TAIT before the new trait solver is stabilized?

CE: I feel like, with a couple of exceptions, the new solver accepts more code than the old solver.

// Ok only in old solver, fundamental limitation in new solver
type Tait<'x> = impl Sized;
fn foo<'a, 'b>(x: &'a (), y: &'b ()) -> (Tait<'a>, Tait<'b>) {
    (x, y)
}

// Ok in new and old solver
type Tait<T> = impl Sized;
fn foo<X, Y>(x: X, y: Y) -> (Tait<X>, Tait<Y>) {
    (x, y)
}

// hacky workaround
fn foo<'a, 'b, T, U>(x: T, y: U) -> (Tait<T>, Tait<U>)
where
    T: Into<&'a ()>,
    U: Into<&'b ()>,
{
    (x, y)
}

TC: What if it's non-defining?

#![feature(type_alias_impl_trait)]

// OK in old solver, overflow in new solver.
type Tait<'x> = impl Sized;
fn define<'x>(x: &'x u8) -> Tait<'x> { x }
fn non_defining<'a, 'b>(x: &'a u8, y: &'b u8) -> (Tait<'a>, Tait<'b>) {
    (define(x), define(y))
//  ^~ error[E0275]: overflow evaluating the requirement `Tait<'_> <: Tait<'a>`
}

https://rust.godbolt.org/z/TnsjeP4xP
Projection goals non-defining use in defining scope





















// passes with old impl, ambiguous with the new one.
#![feature(type_alias_impl_trait)]
trait Trait {
    type Assoc;
}
impl<T: Copy> Trait for T {
    type Assoc = T;
}
fn needs_trait<T: Trait<Assoc = T>>() {}

type Tait = impl Copy;

fn define() -> Tait {}

fn check() {
    needs_trait::<Tait>();
    //[new]~^ ERROR type annotations needed
    //[new]~| NOTE cannot satisfy `<Tait as Trait>::Assoc == Tait`
}

fn main() {}

oli made a bad PR
Image Not Showing Possible Reasons
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
Learn More →
- https://github.com/rust-lang/rust/pull/113169

Things to do

remove Bubble and always pass in the actual anchor, test perf on old solver
opaque_types_defined_by query should return not just a list of opaques in the signature, but also a list of opaques that are in scope (and thus are in their defining scope)
- need to walk up the module tree and check all direct module members for type aliases that define TAITs (not walk into children of anything).
get rid of check_opaque_type_well_formed or check_opaque_meets_bounds
error if the same opaque type is constrained twice (with different lifetimes) in the same body (to be forward compat with the new solver)
error on RPITs that are only constrained in dead code (to fix https://github.com/rust-lang/rust/issues/112417)
make opaque_types_defined_by reject functions that mention the same TAIT twice with different lifetime params
Error if projection in signature normalizes to include a TAIT.
- opaque_types_defined_by may have cycle errors if we do that (says errs, oli thinks he already implemented that and go no cycles)
go through uses of DefineOpaqueTypes::No and either document or change them
- E-easy: flip it to Yes, see what tests fail, document the site by mentioning the test. If no tests fail, change them and leave a comment that there's no test excersising it.
-Zunleash-the-tait-inside-of-you to turn off any errors that are not needed for soundness (e.g. only needed for semver)

Min-TAIT discussion

Date: 2023-10-11

Technical constraints…

Cannot define TAITs twice modulo regions (New)
Image Not Showing Possible Reasons
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
Learn More →
but
Image Not Showing Possible Reasons
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
Learn More →
- This constraint will remain
- Can make the old solver act more like this
- can we create good diagnostics here
- also affects RPIT
  - need additional book-keeping in new solver to be able to improve the region error: open an issue for this, not blocking anything
- Should make it an error when we have a defining function with two taits modulo regions
TAITs act weirdly when aliases are in its defining usage's generic arguments (New)
Image Not Showing Possible Reasons
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
Learn More →
- We can fix this in the new trait solver
- improve diagnostics plz
underspecified where we define TAITs and where we treat them as rigid (New, Old)
TAITs being defined to other TAIT
Image Not Showing Possible Reasons
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
Learn More →
- One defining scope, one not-defining scope (Old)
  - should define, possible by always providing the defining scope
  - achievable if we don't use bubble 🫧🫧🫧
- Both defining scope (New, old)
  - should always either hard error or be ambig
auto trait leakage (New, old)
Image Not Showing Possible Reasons
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
Learn More →
- Cycle errors (revealing auto traits)
- non-defining use in defining scope in new solver? doesn't work once there is an auto trait bound
Projection goals for non-defining use in defining scope (New)
Image Not Showing Possible Reasons
- The image file may be corrupted
- The server hosting the image is unavailable
- The image path is incorrect
- The image format is not supported
Learn More →
defining scope changes will be breaking (new, old)
- (e.g.) No projection normalization in signature restriction
- could make everything defining and error if it's not allowed
  - forces us to handle non-defining uses in defining scopes

// Emit an eager error here?
type Tait<'x> = impl Sized;
fn define<'a, 'b>(x: &'a u8, y: &'b u8) -> (Tait<'a>, Tait<'b>) {
    (x, y)
}

// OK in old solver, overflow in new solver.
type Tait<'x> = impl Sized;
fn define<'x>(x: &'x u8) -> Tait<'x> { x }
fn non_defining<'a, 'b>(x: &'a u8, y: &'b u8) -> (Tait<'a>, Tait<'b>) {
    (define(x), define(y))
//  ^~ error[E0275]: overflow evaluating the requirement `Tait<'_> <: Tait<'a>`
}


// OK in old solver and new solver.
mod m {
  pub type Tait<'x> = impl Sized;
  pub fn define<'x>(x: &'x u8) -> Tait<'x> { x }
}
use m::*;
fn non_defining<'a, 'b>(x: &'a u8, y: &'b u8) -> (Tait<'a>, Tait<'b>) {
    (define(x), define(y))
}

// https://rust.godbolt.org/z/7M89PhWxW
struct Inv<'a>(Cell<&'a ()>);
type Tait2<'x> = impl Sized;
fn non_defining_2<'a>(x: Inv<'a>) -> Tait2<'a> {
    let q = ();
    let p = &q;
    if false {
        let _: i32 = non_defining_2(Inv(Cell::new(p)));
    }
    1i32
}

…and how to avoid them

List of core issues:

non-defining use in defining scope is not allowed
- we check it during type_of or whatever

ideas:

Only define TAIT once
- Maybe once modulo regions, maybe once per body, once at all
Treat only taits in signature as defining scope

Conceptually, we want TAIT to act as much like RPIT as possible.
- oli: having TAIT in arguments is not much more complicated
- errs: let statements too?
- lcnr: If the tait is somewhere in signature, theoretically it doesn't matter if you're able to name the TAIT in the function. It does matter if you can name the TAIT, people are gonna do weird stuff with it.
- errs: If you define it once, then you can name it any time you want.
- lcnr: It would prevent non-defining usages in defining scope, though.

// The minimum desirable?
mod tait {
    type Tait = impl Sized;
    struct Foo(Tait);
    fn must_define() -> Foo { Foo(()) }
}

oli: Annoying rustc changes:

Newtype replacement pattern:

#![feature(type_alias_impl_trait)]
fn is_send<T: Send>(_t: &T) {}

pub use self::hidden::Opaque;
struct Concrete;

mod hidden {
    use super::Concrete;
    pub type Opaque = impl Sized;
    pub(super) fn into_opaque(x: Concrete) -> Opaque { x }
    pub(super) fn from_opaque(x: Opaque) -> Concrete { x as Concrete }
}

pub fn init() -> Opaque {
    hidden::into_opaque(Concrete)
}

pub fn frob(x: Opaque) -> Opaque {
    is_send(&x); // No cycle errors.
    let x: Concrete = hidden::from_opaque(x);
    hidden::into_opaque(x)
}

Proposal

Image Not Showing Possible Reasons
The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported
Learn More →

(preferred)

Forever:
- A function must have the TAIT (or a type that contains it) in the signature.
  - or some defines syntax in the future
For now (we never expect to relax):
- TAITs can only be defined once modulo regions.
For now (can be relaxed later):
- A function that mentions the TAIT (or a type that contains it) in the signature, it must define it.
  - Because of lazy norm and how the new trait solver is more complete, this is an area of difference between the old and new solver. It would be easy to break things here. And the old trait solver is underspecified here. (Oli: It is fixable in the old solver.) So we're saving space here.
- Only one function in the defining scope can mention the TAIT (or a type that contains it) in the signature.
  - Can create a dedicated diagnostic for this case, avoiding all cycle errors and other hard to diagnose issues for users.
  - This is the most arbitrary. We have the machinery to allow this. But it prevents people from writing functions that are passthrough. It allows us to write earlier and better diagnostics. But this is an artificial restriction we could lift easily. We could put this behind a separate feature gate.
- Error if projection in signature normalizes to include a TAIT.
  - Saves space for making opaque_types_defined_by query smarter.
Properties:
- All cycle errors are real cycle errors in the new solver.
- Changes that allow more items to define the TAIT to the signature rule would be breaking changes.

future work

non-defining uses in the defining scope, "pass through pattern"
defining uses outside of the defining scope: defines syntax
- attribute can be used to mark multiple (all defining!) functions as defining, and then the error goes away
multiple functions can define the same TAIT
change signature check to normalize projections
- normalizing to opaque types has to be a hard error before then, otherwise people use this as a design pattern

oli: if defines attr acts like an XOR then it's simple.

lcnr: XOR behavior is bad for IDEs

type Alias = impl Iterator<Item = u32>;
fn wrapper() -> Alias {
    define(0)
}
fn define(x: u32) -> Alias {
    [x].into_iter()
}

Defines in the WC outside of the defining scope:

mod taits {
    pub type Foo<T> = impl Future<Output = T>;
}
use taits::*;

fn make_foo<T>() -> Foo<T>
where
    defines(Foo<T>)
{ todo!() }

https://docs.rs/tokio-util/latest/tokio_util/sync/struct.ReusableBoxFuture.html

Proposal

Image Not Showing Possible Reasons
The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported
Learn More →

modules with a tait can only have a single function
strictly more restrictive than proposal 0

Proposal

Image Not Showing Possible Reasons
The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported
Learn More →

Image Not Showing Possible Reasons
The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported
Learn More →

attributes ftw has to match fn to tait?
- annoying to implement :<
- unclear how exactly it should work, requires a bunch of design work
probably gonna be blocked by T-lang

Proposal

Image Not Showing Possible Reasons
The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported
Learn More →

oli: Only allow one usage of a TAIT in the entire crate

errs: no

design constraints

future compatibility
clearly communicate constraints, e.g. lints/clear errors

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`	在筆記中貼入程式碼
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.

TAIT overview

Old solver

DefineOpaqueTypes

Bubbles!!

Background

How do we align new and old solver behavior

Expected outcomes

Key questions for discussion

Notes from the meetup itself

Things to do

Min-TAIT discussion

Technical constraints…

…and how to avoid them

Proposal Image Not Showing Possible Reasons The image file may be corruptedThe server hosting the image is unavailableThe image path is incorrectThe image format is not supported Learn More → (preferred)

future work

Proposal Image Not Showing Possible Reasons The image file may be corruptedThe server hosting the image is unavailableThe image path is incorrectThe image format is not supported Learn More →

Proposal Image Not Showing Possible Reasons The image file may be corruptedThe server hosting the image is unavailableThe image path is incorrectThe image format is not supported Learn More →

design constraints

`DefineOpaqueTypes`

Proposal

Image Not Showing Possible Reasons
The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported
Learn More →

(preferred)

Proposal

Image Not Showing Possible Reasons
The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported
Learn More →

Proposal

Image Not Showing Possible Reasons
The image file may be corrupted
The server hosting the image is unavailable
The image path is incorrect
The image format is not supported
Learn More →