stricter hidden type wf-check [based on #115008] by lcnr · Pull Request #121679 · rust-lang/rust (original) (raw)

I have strong feelings here and believe we should not support this behavior.

Regarding the complexity. My main concern is not the behavior of check_opaque_meets_bounds. I strongly believe that the following statement should be true:

We should always be able to assume, and verify, that all types are well-formed in the current context.

Allowing these patterns breaks this assumption at the point where we define the nested opaque type. This is fragile in two ways:

We will have to be careful when emitting WF constraints to avoid this breakage going forward. As shown by this PR. It is very subtle why my approach broke the wf-nested.rs tests while your approach in #115008 did not. Your approach only emits WellFormed obligations when relating opaques. We therefore avoid checking well-formedness of nested opaques as we eagerly replaced the nested opaque with an inference variable in project_and_unify_type:

This is not done in the new solver. We'd have to work around it there to continue to support this, for example by also eagerly replacing opaques with inference variables.

Even more importantly, we have to worry about accidentally leaking the non-wf type to somewhere which accepts well-formed types. We already have multiple unsoundnesses caused by a lack of WF checks, e.g. #98117. I do not want to make it more difficult to fix such issues as that may end up forcing nested opaques to be well-formed.

Supporting this pattern by amending the environment while defining nested opaque types seems a lot more acceptable. However, I believe that doing so is far from trivial.

Finally, I don't think this behavior is (very) desirable or consistent with the rest of Rust. I feel like "this was accepted as a valid defining use in #106038" is mostly irrelevant as the concern in #106038 (comment) ended up mostly slipping through and there hasn't been any official team approval of this behavior.This diverges from the behavior of where-clauses where such reasoning is not supported:

trait Id { type Ty; } impl Id for () { type Ty = X; }

fn test() where (): Id<&'static T>, // (): Id<&'static T, Ty = &'static T> // both of these bounds error {}

I do agree that supporting the following is generally desirable:

fn id(s: &T) -> &T { s } fn test() -> impl Fn(&T) -> impl Sized { id }

However, even this is imo not a strong argument to not land this PR as is. We currently do not support defining higher-ranked opaque types at all. Trying to do so always errors. I will push against any such attempts until the new solver is exclusively used as I am very much unsure how to soundly handle this when using semantic lookup for the opaque type storage.

Once implied bounds are explicitly handled and checked (necessary to fix #25860), we can support the above pattern without needing to support non-wf types as the type would now only be used inside of the Binder with the right bounds.

This breaking change is not necessary for the soundness fix here and thus I prefer to at least have it in a separate PR.

I don't. I consider the breakage for RPIT to have already been FCP'd as part of #115008.

However this is still a regression:

trait Id { type Ty; } impl Id for () { type Ty = X; } fn test() -> impl Id<&'static T, Ty = impl Sized> {}

We should probably ignore the wf-check nested RPIT, similar to nested TAIT.

We could separate the removal of the nested TAIT special-case into a separate PR, but given that the added WF-checks during borrowck reduce the breakage caused by that I don't think such a split is desirable. I personally don't have the energy and motivation to first land the approach of #115008 and then move the WF-checks, breaking wf-nested.rs in a separate PR.