`ml-kem-0.2.1` incorrect overflow error

[lcnr]

the crate ml-kem-0.2.1 compiles with the old solver but errors with new

error[E0275]: overflow evaluating the requirement `<P as PkeParams>::NttVectorSize == _`
   --> src/param.rs:206:26
    |
206 |     type NttVectorSize = EncodedPolynomialVectorSize<U12, P::K>;
    |                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`ml_kem`)

relies on rust-lang/rust#147266 to avoid an ICE.

It's got some very cursed where-clauses, here's a self-contained (only typenum) example:

use typenum::*;
use std::ops::{Add, Div, Mul, Rem, Sub};
pub trait ParameterSet {
    type K;
    type Du: VectorEncodingSize<Self::K>;
    type Dv: EncodingSize;
}

pub trait EncodingSize {
    type EncodedPolynomialSize;
    type ValueStep;
    type ByteStep;
}
impl<D> EncodingSize for D
where
    D: Mul<U8> + Gcd<U8> + Mul<U32>,
    Prod<D, U8>: Div<Gcf<D, U8>>,
    EncodingUnit<D>: Div<D> + Div<U8>,
{
    type EncodedPolynomialSize = Prod<D, U32>;
    type ValueStep = Quot<EncodingUnit<D>, D>;
    type ByteStep = Quot<EncodingUnit<D>, U8>;
}

pub trait VectorEncodingSize<K>: EncodingSize {
    type EncodedPolynomialVectorSize;
}
impl<D, K> VectorEncodingSize<K> for D
where
    D: EncodingSize,
    D::EncodedPolynomialSize: Mul<K>,
    Prod<D::EncodedPolynomialSize, K>:
        Div<K, Output = D::EncodedPolynomialSize> + Rem<K, Output = U0>,
{
    type EncodedPolynomialVectorSize = Prod<D::EncodedPolynomialSize, K>;
}

type EncodingUnit<D> = Quot<Prod<D, U8>, Gcf<D, U8>>;
pub type EncodedPolynomialVectorSize<D, K> =
    <D as VectorEncodingSize<K>>::EncodedPolynomialVectorSize;
pub type EncodedPolynomialSize<D> = <D as EncodingSize>::EncodedPolynomialSize;
type EncodedUSize<P> = EncodedPolynomialVectorSize<<P as ParameterSet>::Du, <P as ParameterSet>::K>;
type EncodedVSize<P> = EncodedPolynomialSize<<P as ParameterSet>::Dv>;

fn foo<P>()
where
    P: ParameterSet,
    U384: Mul<P::K>,
    Prod<U384, P::K>: Add<U32> + Div<P::K, Output = U384> + Rem<P::K, Output = U0>,
    EncodedUSize<P>: Add<EncodedVSize<P>>,
    Sum<EncodedUSize<P>, EncodedVSize<P>>: Sub<EncodedUSize<P>, Output = EncodedVSize<P>>,
    EncodedPolynomialVectorSize<U12, P::K>: Add<U32>,
    Sum<EncodedPolynomialVectorSize<U12, P::K>, U32>:
        Sub<EncodedPolynomialVectorSize<U12, P::K>, Output = U32>,
{
}
fn main() {}

[theemathas]

Minimized-ish:

use std::ops::{Add, Mul};
use typenum::{Prod, U12, U32, U384};

pub fn foo<K>()
where
    U384: Mul<K>,
    Prod<Prod<U12, U32>, K>: Add<U32>,
{
}

[theemathas]

Minimized to not depend on typenum:

pub trait Mul1 {
    type Output;
}
pub trait MyAdd {}
trait IsMyU1 {}

pub struct Dummy;
pub struct MyU2;
pub struct MyU1;
pub struct MyUTerm;

impl MyAdd for MyUTerm {}

impl Mul1 for MyU2
where
    MyU1: IsMyU1,
{
    type Output = Dummy;
}

impl IsMyU1 for MyU1 where MyUTerm: MyAdd {}

pub trait Trait<T> {
    type Output;
}

pub fn foo<K>()
where
    Dummy: Trait<K>,
    <<MyU2 as Mul1>::Output as Trait<K>>::Output: MyAdd,
{
}

[theemathas]

Cleaned up a bit:

struct MarkedStruct;
pub trait MarkerTrait {}
impl MarkerTrait for MarkedStruct {}

struct ChainStruct;
trait ChainTrait {}
impl ChainTrait for ChainStruct where MarkedStruct: MarkerTrait {}

pub struct FooStruct;
pub trait FooTrait {
    type Output;
}
pub struct FooOut;
impl FooTrait for FooStruct
where
    ChainStruct: ChainTrait,
{
    type Output = FooOut;
}
type FooOutAlias = <FooStruct as FooTrait>::Output;

pub trait Trait<T> {
    type Output;
}

pub fn foo<K>()
where
    FooOut: Trait<K>,
    <FooOutAlias as Trait<K>>::Output: MarkerTrait,
{
}

[lcnr]

Thank you so much ❤️