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.

[oli-obk]

@rfcbot merge

[rfcbot]

Team member @oli-obk has proposed to merge this. The next step is review by the rest of the tagged team members:

• @BoxyUwU
• @aliemjay
• @compiler-errors
• @jackh726
• @lcnr
• @nikomatsakis
• @oli-obk
• @spastorino

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

See this document for info about what commands tagged team members can give me.

[jackh726]

What's the decision here? To adopt to rule as stated in the OP?

[oli-obk]

Yes.

[lcnr]

in case somebody wants to look at the cases where non-defining uses in the defining scope cause issues¹:

• non-defining use in defining scope: region params trait-system-refactor-initiative#74
• non-defining use in defining scope: projection goal with nested item bound trait-system-refactor-initiative#69
• non-defining use in defining scope, how to handle trait-system-refactor-initiative#40
• opaque types in the defining scope auto trait candidate trait-system-refactor-initiative#32 (you can't prove auto trait bounds for opaques in their defining scope without defining them)

Footnotes

1. i mostly opened these issues to avoid forgetting about them myself, they lack a lot of background info ↩

[nikomatsakis]

@rfcbot reviewed

…

On Mon, May 27, 2024, at 4:09 AM, Rust RFC bot wrote: Team member @oli-obk <https://github.com/oli-obk> has proposed to merge this. The next step is review by the rest of the tagged team members: • @BoxyUwU <https://github.com/BoxyUwU> • @aliemjay <https://github.com/aliemjay> • @compiler-errors <https://github.com/compiler-errors> • @jackh726 <https://github.com/jackh726> • @lcnr <https://github.com/lcnr> • @nikomatsakis <https://github.com/nikomatsakis> • @oli-obk <https://github.com/oli-obk> • @spastorino <https://github.com/spastorino> No concerns currently listed. Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up! See this document <https://github.com/rust-lang/rfcbot-rs/blob/master/README.md> for info about what commands tagged team members can give me. — Reply to this email directly, view it on GitHub <#117861 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABF4ZXZBJR6U5LZ4WV5BGLZEMH5ZAVCNFSM6AAAAAA7IREAAWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMZTGI2DIMZYHE>. You are receiving this because you were mentioned.Message ID: ***@***.***>

[rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[rfcbot]

The final comment period, with a disposition to merge, as per the review above, is now complete.

As the automated representative of the governance process, I would like to thank the author for their work and everyone else who contributed.

This will be merged soon.

[oli-obk]

Actually, need to finish the impl that actually enforces this