Trait bound inference seems to have trouble with implied higher-ranked trait bounds that become redundant when generic parameters are supplied

[Zistack]

I tried this code:

pub trait Add <Lhs, Rhs>
{
	type Output;

	fn add (&self, lhs: Lhs, rhs: Rhs) -> Self::Output;
}

pub trait Adds <Lhs, Rhs>:
	Add <Lhs, Rhs, Output = <Self as Adds <Lhs, Rhs>>::Output>
	+ for <'a> Add <Lhs, &'a Rhs, Output = <Self as Adds <Lhs, Rhs>>::Output>
	+ for <'a> Add <&'a Lhs, Rhs, Output = <Self as Adds <Lhs, Rhs>>::Output>
	+ for <'a, 'b> Add <&'a Lhs, &'b Rhs, Output = <Self as Adds <Lhs, Rhs>>::Output>
{
	type Output;
}

impl <Lhs, Rhs, O, T> Adds <Lhs, Rhs> for T
where T:
	Add <Lhs, Rhs, Output = O>
	+ for <'a> Add <Lhs, &'a Rhs, Output = O>
	+ for <'a> Add <&'a Lhs, Rhs, Output = O>
	+ for <'a, 'b> Add <&'a Lhs, &'b Rhs, Output = O>
{
	type Output = O;
}

pub trait AddsMonoid <X>: Adds <X, X, Output = X>
{
}

impl <X, T> AddsMonoid <X> for T
where T: Adds <X, X, Output = X>
{
}

pub trait AdditionIsCommutative
{
}

pub trait ComAdd <Lhs, Rhs>:
	Add <Lhs, Rhs, Output = <Self as ComAdd <Lhs, Rhs>>::Output>
	+ Add <Rhs, Lhs, Output = <Self as ComAdd <Lhs, Rhs>>::Output>
	+ AdditionIsCommutative
{
	type Output;
}

impl <Lhs, Rhs, O, T> ComAdd <Lhs, Rhs> for T
where T:
	Add <Lhs, Rhs, Output = O>
	+ Add <Rhs, Lhs, Output = O>
	+ AdditionIsCommutative
{
	type Output = O;
}

pub trait ComAdds <Lhs, Rhs>:
	ComAdd <Lhs, Rhs, Output = <Self as ComAdds <Lhs, Rhs>>::Output>
	+ for <'a> ComAdd <Lhs, &'a Rhs, Output = <Self as ComAdds <Lhs, Rhs>>::Output>
	+ for <'a> ComAdd <&'a Lhs, Rhs, Output = <Self as ComAdds <Lhs, Rhs>>::Output>
	+ for <'a, 'b> ComAdd <&'a Lhs, &'b Rhs, Output = <Self as ComAdds <Lhs, Rhs>>::Output>
{
	type Output;
}

impl <Lhs, Rhs, O, T> ComAdds <Lhs, Rhs> for T
where T:
	ComAdd <Lhs, Rhs, Output = O>
	+ for <'a> ComAdd <Lhs, &'a Rhs, Output = O>
	+ for <'a> ComAdd <&'a Lhs, Rhs, Output = O>
	+ for <'a, 'b> ComAdd <&'a Lhs, &'b Rhs, Output = O>
{
	type Output = O;
}

pub trait ComAddsMonoid <X>: ComAdds <X, X, Output = X>
{
}

impl <X, T> ComAddsMonoid <X> for T
where T: ComAdds <X, X, Output = X>
{
}

I expected this to compile.

Instead I get the following error:

   Compiling numeric-algebras v0.1.0 (/home/zistack/Projects/numeric-algebras)
error[E0284]: type annotations needed: cannot satisfy `for<'b, 'a> <T as Add<&'b X, &'a X>>::Output == X`
  --> src/lib.rs:80:13
   |
80 | impl <X, T> ComAddsMonoid <X> for T
   |             ^^^^^^^^^^^^^^^^^ cannot satisfy `for<'b, 'a> <T as Add<&'b X, &'a X>>::Output == X`
   |
note: required for `T` to implement `for<'a, 'b> ComAdd<&'a X, &'b X>`
  --> src/lib.rs:40:11
   |
40 | pub trait ComAdd <Lhs, Rhs>:
   |           ^^^^^^
note: required for `T` to implement `ComAdds<X, X>`
  --> src/lib.rs:57:11
   |
57 | pub trait ComAdds <Lhs, Rhs>:
   |           ^^^^^^^
note: required by a bound in `ComAddsMonoid`
  --> src/lib.rs:76:30
   |
76 | pub trait ComAddsMonoid <X>: ComAdds <X, X, Output = X>
   |                              ^^^^^^^^^^^^^^^^^^^^^^^^^^ required by this bound in `ComAddsMonoid`

For more information about this error, try `rustc --explain E0284`.
error: could not compile `numeric-algebras` (lib) due to previous error

Incidentally, if I change the last bit to

impl <X, T> ComAddsMonoid <X> for T
where T: Adds <X, X, Output = X> + AdditionIsCommutative
{
}

it compiles just fine. This leads me to believe that the issue is somehow related to how the various bounds implied by ComAdds <X, X, Output = X> are becoming redundant with each other due to Lhs and Rhs being the same.

Meta

rustc --version --verbose:

rustc 1.73.0-nightly (864bdf784 2023-07-25)