[TC:]
The T-types meetup on 2023-10-11 included a discussion over the challenges that TAIT presents for the new trait solver and how to overcome those challenges. The result of the session was a consensus proposal for a minimal stabilization of TAIT that satisfies all T-types concerns. We'll describe that consensus proposal below.
In the last push to stabilize TAIT, we had introduced a signature restriction. This restriction requires that for functions and methods that constrain a hidden type, the opaque type must fall within a type that appears in the signature of the function or method. This was done, among other reasons, as it improves the performance of the compiler and other tools such as rust-analyzer.
In the implementation, it was later decided that, for now, projections would not be normalized ahead of performing this check. This was done to make the implementation simpler.
In the original proposal, this signature restriction was carefully specified such that it could be removed in a backward compatible way. That is, we were leaving the door open for T-lang to later decide to remove the signature restriction and allow any function within the defining scope to constrain the hidden type.
The main cost of leaving this door open is that, under the current implementation, we would emit cycle errors that would not be emitted if we were to close this door.
In the T-types proposal, we would close this door. The signature restriction would become a part of TAIT that could not be removed in a backward compatible way. This seems safe as, even aside from type system concerns, it's unlikely that T-lang would ever want to walk through this door for tooling and other reasons. The signature restriction does not limit expressiveness, and nearly all common uses of TAIT trivially pass the signature restriction.
There are two main cases where the signature restriction has to be explicitly considered. On is when defining static items from within a function. The other is when attempting to define an opaque type by passing a concrete type to a function that accepts the opaque type as an argument.
In both cases, there are two main solutions. One is to add where Opaqque: Any bounds on the function that wants to be defining. The other is to use the builder pattern.
As we'll describe below, combined with the other aspects of this proposal, the net result is that we would not emit any spurious cycle errors in the new solver. Any cycle error emitted would be a real cycle error, similar to the other ones that we emit in Rust today.
As mentioned, for implementation reasons, the signature restriction has been constrained such that projections are not normalized ahead of the check. We want to leave room to later make this check smarter and to allow some level of normalization to occur.
Consequently, under this proposal, we would reject code with an error if any projection within the signature of an item normalized to an opaque type for which the item is within the defining scope. E.g., this would be an error:
#![feature(type_alias_impl_trait)]
type Opaque = impl Sized;
trait Trait {
type Assoc;
}
struct Type;
impl Trait for Type {
type Assoc = Opaque;
}
fn define() -> Opaque {}
fn error(_: <Type as Trait>::Assoc) {}
// ~^ ERROR item signature contains opaque type through projection
We would plan to lift this restriction incrementally for any classes of projections that the signature restriction was later extended to allow.
Consider:
#![feature(type_alias_impl_trait)]
type Tait<'x> = impl Sized;
fn define<'a, 'b>(x: &'a (), y: &'b ()) -> (Tait<'a>, Tait<'b>) {
(x, y)
}
Conceptually, this function is constraining the hidden type for the opaque for<'x> Tait<'x> to &'x (). It constrains the hidden type twice, but that should be OK because each constraint is to the same type. The current trait solver accepts this code.
For the example above, the old trait solver works as follows:
In typeck, we observe that:
Tait<'a> := &'a ()
Tait<'b> := &'b ()
Then, in borrowck, we perform remapping and observe that:
Tait<'a> := &'a () ~~> Tait<'x> := &'x ()
Tait<'b> := &'b () ~~> Tait<'x> := &'x ()
Since these types are equal after remapping, borrowck is happy and this code is accepted.
The new solver does not. Furthermore, it's anticipated that the new solver will never accept this code for architectural reasons.
In the new trait solver, we canonicalize all lifetimes to unique existential lifetimes in the root universe. This is to make sure that we avoid any lifetime dependence when proving obligations. This is architecturally required for borrowck and codegen to be sane and to not have responses that change between those steps and HIR typeck. As a bonus, this approach is also better for caching.
For the example above, the new trait solver works as follows:
It observes that Tait<'a> must be equal to &'a ().
Since we haven't inferred anything yet for Tait<'a>, we register the definition Tait<'a> := &'a () in our opaque type storage.
We then notice that Tait<'b> must be equal to &'b (). Since we've already inferred that Tait<'a> := &'a (), we do two things:
First, we require that the opaque signatures Tait<'b> = Tait<'a>. This requires that 'b = 'a.
Next, we set the hidden types &'b () = &'a (). Note that this also requires 'b = 'a.
As in the old solver, this happens twice, once during typeck and once during borrowck. During typeck, we throw away the regions. However, during borrowck, we fail to prove that 'a = 'b, which results in the error. E.g.:
#![feature(type_alias_impl_trait)]
type Tait<'x> = impl Sized;
fn define<'a, 'b>(x: &'a (), y: &'b ()) -> (Tait<'a>, Tait<'b>) {
// ~^ ERROR lifetime may not live long enough
// ~| NOTE requires that `'a` must outlive `'b`
// ~| NOTE requires that `'b` must outlive `'a`
(x, y)
}
type Tait<'a> = impl Sized;
fn foo<'a: 'b, 'b: 'a>() -> Tait<'a> {
let x: Tait<'a> = [1, 2, 3];
{
let y = foo::<'b, 'a>(); // we know y is [i32; 3]
y.into_iter();
}
x
}
We propose a restriction such that, within a single item, multiple defining uses of an opaque type that only differ by lifetime arguments, you must be able to prove that the those lifetime arguments are equal.
The restriction is scoped within a single item because borrow checking happens at the level of single items and that is where we do opaque type inference.
This decision would not, strictly speaking, close a door on the language side to later allowing this. However, T-types is asking for T-lang to consider this door as closed in a practical sense given the design of the new trait solver.
This is the canonical example of what cannot be accepted by the new trait solver and that we will consequently disallow:
#![feature(type_alias_impl_trait)]
type Tait<'x> = impl Sized;
fn define<'a, 'b>(_: &'a (), _: &'b ()) -> (Tait<'a>, Tait<'b>) {
// ~^ ERROR lifetime may not live long enough
// ~| NOTE requires that `'a` must outlive `'b`
// ~| NOTE requires that `'b` must outlive `'a`
((), ())
}
Note that it doesn't matter whether or not the hidden type actually uses these regions.
If due to the bounds, we can prove that these regions are in fact equal, then we will allow the code. E.g.:
#![feature(type_alias_impl_trait)]
type Tait<'x> = impl Sized;
fn define<'a: 'b, 'b: 'a>(_: &'a (), _: &'b ()) -> (Tait<'a>, Tait<'b>) {
((), ())
}
Note that this restriction only applies to lifetime parameters. It's OK for defined opaque types to be equal modulo types. E.g, this is OK:
#![feature(type_alias_impl_trait)]
type Tait<X> = impl Sized;
fn define<A, B>(_: A, _: B) -> (Tait<A>, Tait<B>) {
((), ())
}
Note that, aside from the proposed temporary restriction that only one item may define an opaque type, it would be OK for two separate items to independently define an opaque type twice in a way that is equal modulo regions. E.g., this would be OK aside from the other restriction:
#![feature(type_alias_impl_trait)]
type Tait<'x> = impl Sized;
fn define_1<'x>(_: &'x ()) -> Tait<'x> {}
fn define_2<'x>(_: &'x ()) -> Tait<'x> {}
Note that it's OK for non-defining uses of the opaque type to use the opaque types in a way that is equal modulo regions. E.g., this is OK and works in both the new and the old solver:
#![feature(type_alias_impl_trait)]
use inner::*;
mod inner {
pub type Tait<'x> = impl Sized;
pub fn define<'x>(_: &'x ()) -> Tait<'x> {}
}
pub fn non_defining<'a, 'b>(
x: &'a (),
y: &'b (),
) -> (Tait<'a>, Tait<'b>) {
(define(x), define(y))
}
Even if non_defining were in the defining scope, this would be allowed under this rule because the opaque type is only defined once, though it would be currently disallowed because of the rule that requires items that mention opaque types in their signatures within the defining scope to define them. E.g., this would be allowed once the other restriction is lifted:
#![feature(type_alias_impl_trait)]
pub type Tait<'x> = impl Sized;
pub fn define<'x>(_: &'x ()) -> Tait<'x> {}
pub fn non_defining<'a, 'b>(
x: &'a (),
y: &'b (),
) -> (Tait<'a>, Tait<'b>) {
(define(x), define(y))
}
Note, however, that this currently results in an overflow on the new solver. We believe this will be fixed by #116369. In any case, this would be supported on a best-effort basis and may be subject to compiler limitations.
Currently a function that passes the signature restriction may or may not actually constrain the hidden type. Such a function may, e.g., simply pass through the opaque type without constraining its hidden type. E.g.:
#![feature(type_alias_impl_trait)]
type Tait = impl Sized;
fn define() -> Tait {}
fn passthrough(x: Tait) -> Tait {
x
}
There are many use-cases for this.
However, we propose that, for now, any function or method within the defining scope that passes the signature restriction must constrain the hidden type of any opaque type contained within a type that appears in the signature.
This restriction is helpful because, due to lazy normalization and the new trait solver being more complete, this is an area where there could be various subtle differences in what code might be accepted by the new and old trait solver. This is also an area where the old trait solver is underspecified, though it's believed that could be fixed.
We would plan to later lift this restriction.
Currently any number of items may constrain the hidden type of an opaque. E.g.:
#![feature(type_alias_impl_trait)]
type Tait = impl Sized;
fn wrap(x: ()) -> Tait { x }
fn unwrap(x: Tait) -> () { x }
There are many use-cases for this.
However, we propose that, for now, only one item may constrain any single opaque type to a particular hidden type.
This restriction is somewhat arbitrary. We have the machinery to allow this. However, adding this restriction will for now help us to more easily craft helpful error messages.
We would plan to later lift this restriction.
The main virtues of this proposal are twofold:
One of the major pain points of TAIT has been the presence of surprising cycle errors within the defining scope due to current implementation limitations surrounding the leakage of auto traits.
Under this proposal, these surprising cycle errors will disappear entirely under the new solver, even after we lift the restrictions that we plan to lift.
This proposal is forward compatible with future work that would allow the hidden type to be constrained within the same crate but outside of the defining scope using a new syntax. E.g.:
#![feature(type_alias_impl_trait)]
#![feature(todo_define_tait_anywhere_in_crate)]
use taits::*;
mod taits {
type Tait<T> = impl Sized;
}
fn define<T>()
where
constrains(Tait<T>)
{}
One useful property of such future work is that those who wish to not rely on the signature restriction and wish to always explicitly annotate which functions may constrain the hidden type of some opaque may do so simply by placing their TAITs in a submodule as above.
Thanks to Oli (@oli) and Michael Goulet (@compiler-errors) for helpful discussions and insights on this topic.
All errors and omissions remain those of the author alone.
Failed to normalize async_fn_in_trait ICE for indirect recursion of async trait method calls" #112047async_fn_in_trait and return_type_notation cause awkward awaits" #112569None.
-
Any changes
Be notified of any changes
-
Mention me
Be notified of mention me
-
Unsubscribe
Subscribe