TAIT decision on "may define implies must define"

[traviscross]

Nominating for T-lang to decide whether to adopt the following restriction for the stabilization of TAIT:

At least until the new trait solver is stabilized, any item that is allowed to define the hidden type of some opaque type must define the hidden type of that opaque type.

If adopted, we would call this the "may define implies must define" restriction.

For the purposes of this question, please set aside how we know whether an item is allowed to define the hidden type; this question is invariant to the details of that.

This restriction leaves space for the new trait solver. That solver will consider more uses of the opaque type to be defining and it will implement lazy normalization. Given this, items that may define the hidden type but do not present the potential for differences between the old and new solver that we would prefer to avoid so as to ease the stabilization of the new trait solver.

With this restriction, TAIT becomes roughly equivalent to RPIT with respect to many of the relevant challenges.

The effect of this restriction would be to reject the following code:

#![feature(type_alias_impl_trait)]

type Tait = impl Sized;
fn define() -> Tait {} // Defines the hidden type.
fn passthrough(x: Tait) -> Tait { // Allowed to define but does not.
    // ~^ ERROR Any item that may define a hidden type must define that hidden type.
    x
}

Please set aside how we know that define and passthrough are both allowed to define the hidden type of the opaque. There are many ways that could be notated, and that question is orthogonal to this restriction.

Whether or not this restriction could be lifted later is a question of what is possible under the new trait solver and of what other rules we might decide to adopt that may make this more or less possible. Adopting this restriction now does not in and of itself close the door to possibly permitting this later.

This rule was described and proposed in the 2023-11-08 T-lang Mini-TAIT design meeting (minutes): rust-lang/lang-team#233.

Related

• opaque types in the defining scope auto trait candidate trait-system-refactor-initiative#32
• non-defining use in defining scope, how to handle trait-system-refactor-initiative#40
• non-defining use in defining scope: projection goal with nested item bound trait-system-refactor-initiative#69
• non-defining use in defining scope: region params trait-system-refactor-initiative#74

[lcnr]

This issue has been lang nominated for 3 months and is adding uncertainty to the new trait solver work and blocking refactorings of the old solver. I currently do not know how to sensibly support non-defining uses of opaque types inside of their defining scope.

As an alternative to needing to fully decide this as @rust-lang/lang, it would also work to delegate officially delegate this decision to t-types instead. Discussing why this restriction exists and how or whether it could be avoided seems very much like the responsibility of the types team after all.

[oli-obk]

I'm going to overrule any language concerns due to critical implementation concerns, which thoroughly puts this into T-types territory. T-lang can still review this and give advice or opinions when they get to this issue.