Compiler fails to see an existing trait implementation for an indirectly referred type

[newpavlov]

I get compilation errors for a typenum-based code which can be minimized to this snippet (playground):

use core::ops::Add;
use typenum::{Sum, Unsigned, U8};

pub type TagSize = U8;

pub type TagSizePlus1 = typenum::Add1<TagSize>; // does not work
// pub type TagSizePlus1 = typenum::U9; // works

pub fn foo<N>()
where
    N: Add<TagSizePlus1>,
    Sum<N, TagSizePlus1>: Unsigned,
{
    // code
}

Add1<A> is an alias for <A as Add<B1>>::Output; and Sum<A, B> is an alias for <A as Add<B>>::Output;

The snippet results in the following compilation error:

error[E0277]: cannot add `UInt<UInt<UInt<UInt<UTerm, B1>, B0>, B0>, B1>` to `N`
  --> src/lib.rs:10:1
   |
10 | / pub fn foo<N>()
11 | | where
12 | |     N: Add<TagSizePlus1>,
13 | |     Sum<N, TagSizePlus1>: Unsigned,
   | |___________________________________^ no implementation for `N + UInt<UInt<UInt<UInt<UTerm, B1>, B0>, B0>, B1>`

But replacing Sub1<SomeSize> with U9 (an alias for UInt<UInt<UInt<UInt<UTerm, B1>, B0>, B0>, B1>) works just fine!

It looks like the compiler successfully resolves Add1<SomeSize> to UInt<UInt<UInt<UInt<UTerm, B1>, B0>, B0>, B1>, but then for some reason gets tripped while resolving the bounds and is unable to see that the bound on N which allows the addition.

Potentially relevant issue: #79629

[newpavlov]

Further simplification of the example:

pub trait Proxy {
    type Target;
}

impl Proxy for u32 {
    type Target = u64;
}

pub trait Op<T> {
    type Result;
}

fn foo<T>()
where
    T: Op<<u32 as Proxy>::Target>,
    <T as Op<<u32 as Proxy>::Target>>::Result: Sized,
{
}

It fails with:

error[E0277]: the trait bound `T: Op<u64>` is not satisfied
  --> src/lib.rs:13:1
   |
13 | / fn foo<T>()
14 | | where
15 | |     T: Op<<u32 as Proxy>::Target>,
16 | |     <T as Op<<u32 as Proxy>::Target>>::Result: Sized,
   | |_____________________________________________________^ the trait `Op<u64>` is not implemented for `T`

error[E0277]: the trait bound `T: Op<u64>` is not satisfied
  --> src/lib.rs:13:4
   |
13 | fn foo<T>()
   |    ^^^ the trait `Op<u64>` is not implemented for `T`