#![recursion_limit = "8"]
// The field order matters 😂
struct Foo<T> {
t: T,
opt_t: Option<T>,
}
fn require_sync<T: Sync>() {}
fn main() {
require_sync::<Foo<Foo<Foo<Foo<Foo<Foo<()>>>>>>>();
}
The above code compiles with the old solver, while it requires recursion_limit = "12" for the next solver.
To prove Foo^N: Sync, we have to prove constituent nested goals Foo^N-1: Sync and Option<Foo^N-1>: Sync.
If we require depth d to prove the former, the next solver requires the depth d + 1 for the later, because we goes down one depth from Option<Foo^N-1>: Sync to its constituent goal Foo^N-1: Sync, and we hit the cache with required depth d for this nested goal.
So, the total required depth for the root goal is proportional to N with slope 2.
But for the old solver, we check the recursion limit when we actually consider the obligation and don't record/lookup the required depth for its deeply nested goals.
Therefore, the total required depth for the root goal is proportional to N with slope 1 and the next-solver requires twice more recursion limits as N grows.
This affects wgpu = "25.0.2".
This is investigated and explained by @ShoyuVanilla. zulip discussion
It's planned to add a FCW for this. #159224
The above code compiles with the old solver, while it requires
recursion_limit = "12"for the next solver.To prove
Foo^N: Sync, we have to prove constituent nested goalsFoo^N-1: SyncandOption<Foo^N-1>: Sync.If we require depth
dto prove the former, the next solver requires the depthd + 1for the later, because we goes down one depth fromOption<Foo^N-1>: Syncto its constituent goalFoo^N-1: Sync, and we hit the cache with required depth d for this nested goal.So, the total required depth for the root goal is proportional to
Nwith slope2.But for the old solver, we check the recursion limit when we actually consider the obligation and don't record/lookup the required depth for its deeply nested goals.
Therefore, the total required depth for the root goal is proportional to
Nwith slope1and the next-solver requires twice more recursion limits asNgrows.This affects
wgpu = "25.0.2".This is investigated and explained by @ShoyuVanilla. zulip discussion
It's planned to add a FCW for this. #159224