Repository navigation
Overflow evaluating well-formedness requirement with empty trait bound on associated type #148349
Description
rustc 1.91.0 as well as nightly (1.93.0-nightly (2025-10-30 d5419f1e97b90741d518)) produce an overflow error when using a where clause on an associated type when the bound in the where clause is empty. While this is a pathological example, this did occur in auto-generated code (e.g. in verus).
trait SomeBound {}
trait T where
Self::Assoc:,
// this works:
//Self::Assoc: SomeBound
{
type Assoc;
}I expected this to compile successfully (and indeed it did on Rust 1.88).
On nightly and with 1.91 (rustc 1.91.0 (f8297e351 2025-10-28)), I get the following error:
Compiling playground v0.0.1 (/playground)
error[E0275]: overflow evaluating the requirement `<Self as T>::Assoc well-formed`
--> src/lib.rs:4:5
|
4 | Self::Assoc:,
| ^^^^^^^^^^^
|
note: required by a bound in `T`
--> src/lib.rs:4:5
|
3 | trait T where
| - required by a bound in this trait
4 | Self::Assoc:,
| ^^^^^^^^^^^ required by this bound in `T`
For more information about this error, try `rustc --explain E0275`.
error: could not compile `playground` (lib) due to 1 previous error
Activity
theemathas commentedon Nov 1, 2025
Bisection result:
theemathas commentedon Nov 1, 2025
Probably #140208 (comment)
cc @compiler-errors @lcnr
lcnr commentedon Nov 3, 2025
This is an intended change, we did not expect much breakage from it however. cc @rust-lang/types
Is this challenging to work around on in verus? My current tendency is to close this as intended, we could stop the lowering as explicit
WellFormedclauses inpredicates_ofbut instead only check that these empty where-clauses are well-formed in item WF check to avoid this breakage here..jackh726 commentedon Nov 3, 2025
I'm very curious if there is a simple fix to
verus.Given that there is breakage here (while we did the FCP in #140208 under the presumption of no breakage), I feel a bit conflicted about just closing as intended. On one hand, this has been stable for a couple releases now. On the other hand, #140208 didn't have great motivation other than just not wanted to try to support it in the new solver.
I think if there is a quick and simple fix to
verusand we can get that landed, let's just do that. A simple fix in the compiler, regardless, would also not be the worst idea - if it's local and well thought out. I'd probably be happy to get it landed orthogonally.I guess, I'm not happy to just close this as intended breakage - I want some defined resolution to this.
dschoepe commentedon Nov 3, 2025
Yes, this was easy to fix in verus by omitting empty bounds in the part that generates such code, but I figured I'd report it anyway.
BoxyUwU commentedon Nov 3, 2025
I don't think the justification for making wf goals not be coinductive was "dont want to put effort into it in the new solver", it was more of a "we're not sure that this is theoretically sound" iirc. I would like to keep treating them as not coinductive which means either treating this as intended breakage or no longer lowering
Ty:,bounds towf(Ty).Making
Ty:not lower towf(Ty)seems fairly reasonable to me but I don't know if we might for some reason want to ensure thatTysticks around after hir ty lowering which would make it problematic to drop altogetherlcnr commentedon Nov 4, 2025
I think we do want to check that these types are well-formed. We don't have to add these requirements to
predicates_of/ theparam_envhowever, we could lower them separately and then explicitly prove them in when checking that item WF