Graciously handle Drop impls introducing more generic parameters than the ADT

[BoxyUwU]

Follow up to #110577
Fixes #126378
Fixes #126889

Motivation

A current issue with the way we check drop impls do not specialize any of their generic parameters is that when the Drop impl introduces more generic parameters than are present on the ADT, we fail to prove any bounds involving those parameters. This can be demonstrated with the following code on stable which fails due to the fact that <T as Trait>::Assoc == U is not present in Foos ParamEnv even though arguably there is no reason it cannot compiler:

struct Foo<T: Trait>(T);

trait Trait {
    type Assoc;
}

impl<T: Trait<Assoc = U>, U: ?Sized> Drop for Foo<T> {
    //~^ ERROR: `Drop` impl requires `<T as Trait>::Assoc == U` but the struct ...
    fn drop(&mut self) {}
}

fn main() {}

I think the motivation for supporting this code is somewhat lacking, it might be useful in practice for deeply nested associated types where you might want to be able to write:
where T: Trait<Assoc: Other<AnotherAssoc: MoreTrait<YetAnotherAssoc: InnerTrait<Final = U>>>>
in order to be able to just use U in the function body instead of writing out the whole nested associated type. Regardless I don't think there is really any reason to not support this code and it is relatively easy to support it.

What I find slightly more compelling is the fact that when defining a const parameter const N: u8 we desugar that to having a where clause requiring the constant N is typed as u8 (ClauseKind::ConstArgHasType). As we always desugar const parameters to have these bounds, if we attempt to prove that some const parameter N is of type u8 and there is no bound on N in the enviroment that generally indicates usage of an incorrect ParamEnv (this has caught a bug already).

Given that, if we write the following code:

#![feature(associated_const_equality)]
struct Foo<T: Trait>(T);

trait Trait {
    const ASSOC: usize;
}

impl<T: Trait<ASSOC = N>, const N: usize> Drop for Foo<T> {
    fn drop(&mut self) {}
}

fn main() {}

The Drop impl would have this desugared where clause about N being of type usize, and if we were to try to prove that where clause in Foo's ParamEnv we would ICE as there would not be any ConstArgHasType in the environment (which generally indicates improper ParamEnv usage. As this is otherwise well formed code (the T: Trait<ASSOC = N> causes N to be constrained) we have to handle this somehow and I believe the only principled way to support this is the changes I have made to dropck.rs that would cause these code examples to compiler (Perhaps we could just throw out all ConstArgHasType where clauses from the predicates we prove but that makes me nervous even if it might actually be okay).

The changes

Currently the way dropck.rs works is that take the ParamEnv of the ADT and instantiate it with the generic arguments used on the self ty of the impl. We then instantiate the predicates of the drop impl with the identity params to the impl, e.g. in the original example <T as Trait>::Assoc == U stays as <T as Trait>::Assoc == U. We then attempt to prove all the where clauses in the instantiated env of the self type ADT.

This PR changes us to first instantiate the impl with infer vars, then we equate the self type (with infer vars as its generic arguments) with the self type as written by the user. This causes all generic parameters on the impl that are constrained via associated type/const equality bounds to be left as inference variables while all other parameters are still Ty/Const/Region

Finally when instantiating the predicates on the impl, instead of using the identity arguments, we use the list of inference variables of which some have been inferred to the impl parameters. In practice this means that we wind up proving <T as Trait>::Assoc == ?x which can succeed just fine. In the const generics example we would wind up trying to prove ConstArgHasType(?x: usize) instead of ConstArgHasType(N: usize) which avoids the ICE as it is expected to encounter goals of the form ?x: usize.

At a higher level the way I justify/think about this is that as we are proving goals in the environment of the ADT (Foo in the above examples), we do not expect to encounter generic parameters from a different environment so we must "deal with them" somehow. In this PR we handle them by replacing them with inference variables as they should either actually be unconstrained (and we will error later) or they are constrained to be equal to some associated type/const.

To go along with this it would be nice if we were not instantiating the adt's env with the generic arguments to the ADT in the Drop impl as it would make it clearer we are proving bounds in the adt's env instead of the Drop impl's. Instead we would map the predicates on the drop impl to be valid in the environment of the adt. In practice this causes diagnostic regressions as all of the generic parameters in errors refer to the ones defined on the adt; attempting to map these back to the ones on the impl, while possible, is involved as writing a TypeFolder over FulfillmentError is non trivial.

Edge cases

There are some subtle interactions here:

One is that we should not allow <T as Trait>::Assoc == U to be present on the Drop if U is constrained by the self type of the impl and the bound is not present in the ADT's environment. demonstrated with the following code:

trait Trait {
    type Assoc;
}

struct Foo<T: Trait, U: ?Sized>(T, U);

impl<T: Trait<Assoc = U>, U: ?Sized> Drop for Foo<T, U> {
    //~^ ERROR: `Drop` impl requires `<T as Trait>::Assoc == U`
    fn drop(&mut self) {}
}

fn main() {}

This is tested at tests/ui/dropck/constrained_by_assoc_type_equality_and_self_ty.rs.

Another weirdness is that we permit the following code to compile now:

struct Foo<T>(T);

impl<'a, T: 'a> Drop for Foo<T> {
    fn drop(&mut self) {}
}

This is caused by the fact that we permit unconstrained lifetime parameters in trait implementations as long as they are not used in associated types (so we do not wind up erroring on this code like we perhaps ought to), combined with the fact that as we are now proving T: '?x instead of T: 'a which allows proving the bound via '?x= 'empty wheras previously it would have failed.

This is tested as part of tests/ui/dropck/reject-specialized-drops-8142.rs.

---

r? @compiler-errors

[compiler-errors]

cool beans

[compiler-errors]

This is a pretty simple extension to the new dropck algorithm that was introduced in #110577, however, it's probably worth FCPing because of a few subtleties pointed out in the PR description. This seems rock solid tho, thanks for the detailed PR description.

@rfcbot fcp merge

[rfcbot]

Team member @compiler-errors 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.

[BoxyUwU]

WHOO WE DID IT !

[compiler-errors]

@rfcbot review

[compiler-errors]

r=me on the code changes

[nikomatsakis]

I'm having a hard time understanding what the change does. Is this a good summary, @BoxyUwU ?

• Given a struct S<P> where WC_S with parameters P
• and a impl<Q> Drop for S<R> where WC_I
• try to prove forall<P> { WC_S => exists<Q> { S<P> = S<R>, WC_I } }

This would correspond to

• using the ParamEnv from the struct (i.e., forall<P> { WC_S => ... })
• instantiating the impl arguments Q with inference variables (exists<Q>)
• proving the self type is equal (S<P> = S<R>) and impl where-clauses (WC_I)

[compiler-errors]

@nikomatsakis: Yes exactly.

[nikomatsakis]

@rfcbot reviewed

OK, that makes sense to me.

[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.

[compiler-errors]

uwu

@bors r+ rollup

[bors]

📌 Commit 6a00008 has been approved by compiler-errors

It is now in the queue for this repository.