Open lcnr opened 12 months ago
I dont understand what is overlap for this https://blog.rust-lang.org/inside-rust/2023/12/22/trait-system-refactor-initiative.html
coherence checking exists to check that there are no two impls which would apply to the same types. In the blog post, impl<T: Overflow + Copy> MayOverlap for T {}
and impl<T> MayOverlap for Wrapper<T> {}
would overlap if Wrapper<u32>
would implement Copy
. As this is not the case, it successfully compiles. If this is still unclear, please open a thread on zulip about this.
Compiling the typenum crate requires non-fatal overflow.
The overflow happens when checking for overlap of
impl<M: Integer, N> PartialDiv<N> for M
withimpl<Ul, Bl, Ur, Br> PartialDiv<UInt<Ur, Br>> for UInt<Ul, Bl>
The overflow happens for bothUInt<?ul, ?bl>: Div<UInt<?ur, ?br>>
andUInt<?ul, ?bl>: Rem<UInt<?ur, ?br>>
.They result in a nested
(): PrivateDiv<UInt<?ul, ?bl>, UInt<?ur, ?br>, UTerm, UTerm, <<UInt<?ul, ?bl> as Len>::Output as Sub<B1>>::Output>
goal.<UInt<?ul, ?bl> as Len>::Output as Sub<B1>>::Output
cannot be normalized, so it remains as an ambiguous alias. The goal is therefore equivalent to(): PrivateDiv<UInt<?ul, ?bl>, UInt<?ur, ?br>, UTerm, UTerm, ?d0>
.This results in the nested goal
(): PrivateDivIf<UInt<?ul, ?bl>, UInt<?ur, ?br>, UTerm, TrimOut<UInt<UTerm, GetBitOut<UInt<?ul, ?bl>, ?d0>>>, ?d0, Compare<TrimOut<UInt<UTerm, GetBitOut<UInt<?ul, ?bl>, ?d0>>>, UInt<?ur, ?br>>>
As all of the associated types are yet again unknowable:
(): PrivateDivIf<UInt<?ul, ?bl>, UInt<?ur, ?br>, UTerm, ?d1, ?d0, ?d2>
We then try to apply
impl<N, D, Q, R, Ui, Bi> PrivateDivIf<N, D, Q, R, UInt<Ui, Bi>, Less> for ()
which results in the nested goal(): PrivateDiv<UInt<?ul, ?bl>, UInt<?ur, ?br>, UTerm, ?d1, Sub1<UInt<?ui, ?bi>>>
.Note that the inference variables are unconstrained in
Sub1<UInt<?ui, ?bi>>
as we equate theUInt<Ui, Bi>
from the signature with?d0
from the goal, which is ambiguous. We can therefore treat the new goal as(): PrivateDiv<UInt<?ul, ?bl>, UInt<?ur, ?br>, UTerm, ?d1, ?d3>
. This will clearly go on forever.In the old solver this ended up being ambiguous due to the
match_fresh_trait_refs
check. We then consider the impls to be disjoint asUInt<?ul, ?br>: Integer
can trivially be disproven.Note that non-fatal overflow for typenum is especially bad here as all 6
PrivateDivIf
impls apply to the(): PrivateDivIf<UInt<?ul, ?bl>, UInt<?ur, ?br>, UTerm, ?d1, ?d0, ?d2>
goal and 3 of them result in (probably) cyclic nested goals. This means that every 2 steps we have a blowup of 3, resulting in a growth of up to3^(1/2*recursion_depth)
.