Prototype Fixing false E0581/E0582 errors in the next solver - #162745
enginespot wants to merge 2 commits into
Conversation
|
Thanks for the pull request, and welcome! The Rust Project has assigned @khyperia (or someone else) to review your changes, you should hear from them (or someone else) within the next two weeks. Please see the contribution instructions and our LLM policy for more information. Why was this reviewer chosen?The reviewer was selected based on:
|
This comment has been minimized.
This comment has been minimized.
b47fc22 to
7a8b709
Compare
This comment has been minimized.
This comment has been minimized.
|
This needs significant discussion with the types team; Zulip is the right place for that. I'll leave this open for now, but am going to mark this as experimental. It is not going to be reviewed without discussion. |
7a8b709 to
8010641
Compare
|
This PR changes rustc_public cc @oli-obk, @celinval, @ouz-a, @makai410 Some changes occurred to the CTFE machinery changes to the core type system cc @lcnr
cc @rust-lang/clippy changes to the core type system cc @lcnr |
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
8010641 to
4c74fed
Compare
|
This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
|
The job Click to see the possible cause of the failure (guessed by this bot) |
Accept callable outputs determined by complete input types and independent projection equalities with the next solver enabled globally. Check the requirements for normalization and function-item lifetime generalization. Use associated-item and supertrait declarations to prove nested type equalities, trait bounds, and outlives goals. Preserve quantified premises without recursively proving the well-formedness of an established source. Carry alternative region conditions through canonical responses, MIR, borrow checking, and closure requirements.
Cover higher-ranked outputs, nested declaration equalities, GATs, scoped premises, and actual calls through function items, pointers, and trait objects, including cross-crate uses and missing-premise rejection. Exercise recursive declaration premises from COM object traits and verify that quantified Self types retain their lifetime requirements. Update the affected diagnostics and test region-constraint rollback.
4c74fed to
02c25f8
Compare
I’m addressing a class of E0581/E0582 errors under
-Znext-solver=globally: rustc rejects a callable signature even though its input types and existing constraints determine its output. This affects bothFnbounds and function pointer types.I’ll start with a callback that returns the same associated type it receives, then show how equalities and nested declarations support more involved signatures and actual calls. The later examples explain which restrictions still apply. Code snippets reuse earlier definitions; examples described as errors should be compiled separately.
Using the same associated type for input and output
The following
applypassesvalueto a callback and returns the result. Both sides useT::View, but the previous check rejected the callable bound.Why this was rejected
View<'a>does not necessarily use'a. These two implementations illustrate the distinction:Substituting each implementation into the callback bound gives:
For
Borrowed, the input is a reference whose type retains'a. ForErased, the input is always(), regardless of how'ais instantiated. A generic input written asT::View<'a>therefore does not establish that'acan be recovered from that type.In both cases, the complete input type still determines the output type. For
Borrowed, both are&'a u32; forErased, both are(). In the latter case, the output no longer depends on'aeither, so there is no need to recover it.What the change allows
I changed the check to recognize complete input types reused in the output. In
apply, both sides areT::View<'b>, so determining the output does not require recovering'bfrom the projection. The generic definition now passes the check, and both calls below are accepted:The call to
f(value)insideapplyis checked using the same type relationship. These examples exercise that call with both a reference and().Using an equality between different associated types
The input and output may use different projections. In this example, the callback takes
T::Viewand returnsU::View, while a separatewhereclause requires the two types to be equal for every'b:I use the independent
T: Family<View<'b> = U::View<'b>>bound to establish the equality when checking the callable bound. TheFn(...) -> ...binding being checked cannot serve as proof of its own validity.When normalizing the input and output, both occurrences of
'bremain bound by the same quantifier. Any additional requirements introduced by normalization must also hold.For a concrete call, another type can define
Viewas the same reference type:Inside the generic function, the equality comes from the
View<'b> = U::View<'b>bound. At this call site, both projections are&u32. ReplacingAlsoBorrowedwithErasedwould give&u32on one side and()on the other, so the equality would fail and the call would still be rejected.Wrapping the result
The output can also contain the reused type inside a wrapper such as
Option:The equality determines
U::View<'b>, which also determinesOption<U::View<'b>>. The check can recognize a reused type within the output; it does not require the entire output to be identical to the entire input. Any additional references in the output still need their lifetimes checked separately.Following equalities through associated type declarations
A function’s
whereclause may provide an equality indirectly through a declaration. Here, the relevant equality appears in the declaration ofCarrier::Assoc:Substituting the declared relationships reduces the return type to the input type:
The previous implementation did not fully use this relationship. I extended the solver to follow associated item and supertrait declarations for the current goal. Here, that establishes
<T as Identity>::Output = T, allowing the body to returnvaluedirectly.The search follows the relationship needed for that goal. If a declaration carries additional
whereclauses, their requirements must also be checked; extracting an equality does not discard its premises.Using the function through pointers and callbacks
The same
identityfunction can be used through a function pointer. This requires checking both the pointer type itself and the coercion of the function item to that type:The type of
frequires it to be callable for every'b. I therefore check thatidentitysatisfies its declaration’s requirements for every such lifetime before allowing the coercion. The resulting pointer can then be called withf(value).The declared equality can also establish the return type when calling through
Box<dyn Fn>:Adding the following implementations for
Borrowedmakes both forms available for concrete calls:Using lifetime bounds already provided by declarations
Avoiding redundant bounds
An associated type declaration can provide lifetime relationships as well as type equalities:
The function does not explicitly require
'a: 'r, but that relationship follows from the declaration:I use this declared relationship in the relevant checks, allowing
shortento omit a redundant'a: 'rbound. The solver can also use such a relationship when it needs to proveT: 'rbefore normalizing an associated type.One complete proof is enough
A lifetime requirement can have more than one possible proof. In this example, the bound on
Dprovides a sufficient one:The two possible derivations are:
The return type requires
T: 'r. The proof throughDestablishes that, so there is no need to require'a: 'ras well.Both premises of that proof,
T: 'band'b: 'r, must hold together. TakingT: 'afrom the first path and'b: 'rfrom the second would not proveT: 'r.I preserve these alternatives only when the candidate proofs agree on their type and const results. A candidate producing
u32cannot be merged with one producingboolmerely because both have satisfiable lifetime conditions.The remaining conditions are carried through to borrow checking. Requirements that a closure passes to its enclosing context are preserved as well; determining the return type does not discharge those requirements.
Cases that remain rejected
Unrelated projections or independent lifetimes
Using the same lifetime argument does not establish a relationship between two projections. This bound provides no equality between
T::View<'a>andU::View<'a>, so it still produces E0582:Even with an equality, substitution must preserve the corresponding lifetime. The independent
'aand'bbelow still cause E0582:The equality establishes
T::View<'a> = U::View<'a>. It does not establishT::View<'a> = U::View<'b>. Variables in nestedfor<...>binders likewise retain their own scopes; matching names do not make them interchangeable.An additional reference in the output
Reusing the input type does not justify an additional output reference whose lifetime has no independent basis:
Substituting
Erasedmakes the distinction explicit:The input is still just
(), but the output now includes a reference that depends on'a. The generic bound does not establish that lifetime dependency, so it still produces E0582.Unsatisfied requirements on an associated type
The following associated type normalizes to
(), but its declaration restricts its lifetime argument to'static:The
for<'a>bound must hold for every'a, whileStaticOnly::View<'a>requires'a: 'static. I retain that requirement during normalization, somissing_requirementremains rejected. Replacing the output with()cannot erase the condition under which the associated type is valid.A function that only supports restricted lifetimes
A function may return its input type and still impose a lifetime restriction. Here,
restrictedexplicitly requires'a: 'static:The coercion in
bad_pointerstill produces a type mismatch. The pointer must be callable for every'a, but the function has a narrower requirement. Matching input and output types does not remove that restriction.A circular equality is not an independent normalization proof
Suppose the only available equalities are:
These state that the two projections are equal. Reversing the first equality does not add evidence. The solver cannot treat a return to the original goal as proof that it has determined the normalization result.
I preserve recursive reasoning supported by established premises, and the solver does not need to expand declarations unrelated to the current goal. Some mutually recursive projections with no determinable normalization result can still reach the recursion limit. The two equations above illustrate the relationship; they do not imply that every program containing such equalities will overflow.
Changes to the compiler
I changed several checks to support the examples above:
whereclauses are available, they use independent equalities to normalize the input and output while checking the required lifetime conditions.for<'a>only when the relevant declaration requirements hold for every'a.A behavior change with assumptions-on-binders
The accepted examples above use
-Znext-solver=globally; they do not require-Zassumptions-on-binders. When that additional mode is enabled, the change also checks lifetime requirements that remain after leaving a quantified scope.Two cases in
tests/ui/assumptions_on_binders/test-infra-works.rscan be described as follows:T: Traitalone cannot prove the remaining requirement. Both cases were previously accepted, and existing FIXME comments already identified that acceptance as incorrect. I changed the test fromcheck-passtocheck-failbecause preserving and checking those lifetime requirements now rejects the two cases.Scope and related issues
This output dependency analysis applies to the next solver when enabled globally. It uses complete types and established equalities while preserving projection opacity and checking any additional output lifetimes.
T::Native<'a>: Not<Output = T::Native<'a>>. Reusing a complete input type also applies to this associated output constraint. The original minimal example now passes type checking with the next solver enabled globally.