Overflow when checking trait bound on a custom Add implementation

Question

I'm trying to make a zero cost abstraction library that adds units to values, to ensure computations homogeneity at compile time.

The core type is:

pub struct QuantifiedValue<T, U: Unit> {
    _m: core::marker::PhantomData<U>,
    inner: T,
}

Unit is essentially a marker trait with various compile time and type level constructs.

pub trait Unit {
    type Dimension: dimension::Dimension;
    type ComposedUnitNumerator: list::StandardUnitList;
    type ComposedUnitDenominator: list::StandardUnitList;
    const NAME: &'static str;
    const SYMBOL: &'static str;
}

The idea is that units are a ZST, and most of the times a composition of standard units, that can be written as followed:

pub struct Composed<N: crate::list::StandardUnitList, D: crate::list::StandardUnitList>(
    core::marker::PhantomData<(N, D)>
);

I'm using a classic Nil - Cons<Unit, Tail> approach for type level lists of standard units, and a unit is basically a numerator and a denominator which are standard unit lists.

For the sake of the example, a standard unit is defined:

pub struct Second;
impl StandardUnit for Second {
    type Dimension = crate::dimension::Time;
    const NAME: &'static str = "second";
    const SYMBOL: &'static str = "s";
}

And of course, standard units can also be considered units:

impl<U: StandardUnit> crate::Unit for U {
    type Dimension = <U as StandardUnit>::Dimension;
    type ComposedUnitNumerator = crate::list::Cons<Self, crate::list::Nil>;
    type ComposedUnitDenominator = crate::list::Nil;
    const NAME: &'static str = <U as StandardUnit>::NAME;
    const SYMBOL: &'static str = <U as StandardUnit>::SYMBOL;
}

Now, to my problem. I'm trying to implement ops::Add on any two quantified value where the inner types implement add, and the units are the same:

impl<Lhs, Rhs, Output, U1, U2> core::ops::Add<QuantifiedValue<Rhs, U2>> for QuantifiedValue<Lhs, U1>
where
    Lhs: core::ops::Add<Rhs, Output = Output>,
    U1: Unit,
    U2: Unit,
    (U1, U2): unit_comparison::SameUnit,
{
    type Output = QuantifiedValue<Output, U1>;
    fn add(self, rhs: QuantifiedValue<Rhs, U2>) -> Self::Output {
        QuantifiedValue::new(self.inner + rhs.inner)
    }
}

For two units to be the same (SameUnit trait), we need to check that the first numerator combined with the second denominator contains the same elements as the second numerator combined with the first denominator:

impl<U1, U2> SameUnit for (U1, U2)
where 
    U1: crate::Unit,
    U2: crate::Unit,
    (
        <U1::ComposedUnitNumerator as crate::list::StandardUnitList>::Merged<U2::ComposedUnitDenominator>,
        <U2::ComposedUnitNumerator as crate::list::StandardUnitList>::Merged<U1::ComposedUnitDenominator>,
    ): crate::list::SameSuList,
{}

The Merged associated type allows to concatenate lists at compile time:

impl StandardUnitList for Nil {
    type Merged<Other: StandardUnitList> = Other;
}

impl<U: StandardUnit, T: StandardUnitList> StandardUnitList for Cons<U, T> {
    type Merged<Other: StandardUnitList> = Cons<U, T::Merged::<Other>>;
}

We can then check if two lists are the same (SameSuList) (for now, they also need the same order):

impl SameSuList for (Nil, Nil) {}

impl<U, T1, T2> SameSuList for (Cons<U, T1>, Cons<U, T2>)
where 
    U: StandardUnit,
    T1: StandardUnitList,
    T2: StandardUnitList,
    (T1, T2): SameSuList,
{}

However, the following sample code does not work:

fn main()
    let distance = unit::QuantifiedValue::<_, unit::Metre>::new(100.0);

    let distance_sum = distance + distance;
}

This gives a compile error, basically saying that there is an attempt at creating way too big Cons<_, Cons<_, ...>> lists:

error[E0275]: overflow evaluating the requirement `(unit::list::Cons<_, _>, unit::list::Cons<_, _>): unit::list::SameSuList`
  --> src/main.rs:22:33
   |
22 |     let distance_sum = distance + distance;
   |                                 ^
   |
   = help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`hermes`)
   = note: required for `(unit::list::Cons<_, unit::list::Cons<_, _>>, unit::list::Cons<_, unit::list::Cons<_, _>>)` to implement `unit::list::SameSuList`
   = note: 124 redundant requirements hidden
   = note: required for `(Cons<Metre, Cons<_, Cons<_, Cons<_, Cons<_, Cons<_, Cons<_, Cons<_, Cons<_, Cons<_, ...>>>>>>>>>>, ...)` to implement `unit::list::SameSuList`
   = note: required for `(Metre, _)` to implement `unit::unit_comparison::SameUnit`
   = note: required for `QuantifiedValue<{float}, Metre>` to implement `Add<QuantifiedValue<_, _>>`
   = note: the full name for the type has been written to '/home/eclipse/dev/rust/hermes/target/debug/deps/hermes-f8b4ac971711d09d.long-type-2041869883332433735.txt'
   = note: consider using `--verbose` to print the full type name to the console

I've pin pointed the issue down to the Merged associated type, whenever I compare only the numerators in the SameUnit implementation without performing the merge, it works fine. I'm wondering how this is the case, as I've done a small group of tests on the Merged associated type that works fine.

My reasoning here is that the type checker would see my attempt at an add, and perform the following:

• Check for the add impl
• Check if f32: ops::Add<f32> which is ok
• Check if (Metre, Metre): SameUnit
• Check if (Metre::Num::Merged<Metre::Denom>, Metre::Num::Merged<Metre::Denom>): SameSuList
• Check if (Cons<Metre, Nil>, Cons<Metre, Nil>): SameSuList
• Check if (Nil, Nil): SameSuList
• All good to go!

However, I get the overflow. What is going on here ?

Here is a link to the playground with the bare minimal example for those who want to play with it: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=22a17f176cb939a7ac2d18a03df7a39f

Thanks in advance, cheers

Answer 1

While experimenting with similar code a while ago I came up with a stupid workaround which I am sure can be improved. When something with recursion like

trait T {}

impl<A> T for A where A: T {}

fails to compile (this example doesn't, but more advanced cases often do), you can add some indirection, which hinders the compiler from going into a loop for some reason:

trait T {}

impl<A> T for A where A: THelper<<A as NotObviousUnit>::Unit> {}

trait NotObviousUnit {
    type Unit;
}

impl<A> NotObviousUnit for A {
    type Unit = ();
}

trait THelper<A> {}

impl<A> THelper<()> for A
where
    A: T
{}

The THelper trait exists to avoid adding extra type parameters to the T trait.

In this case, building on the minimal example you provided, this becomes: (playground)

fn main() {
    let distance1 = QuantifiedValue::<_, Metre> {
        inner: 100.0,
        _m: core::marker::PhantomData,
    };
    let distance2 = QuantifiedValue::<_, Metre> {
        inner: 100.0,
        _m: core::marker::PhantomData,
    };
    let distance_sum = distance1 + distance2;
}

pub struct QuantifiedValue<T, U: Unit> {
    _m: core::marker::PhantomData<U>,
    inner: T,
}

pub trait Unit {
    type ComposedUnitNumerator: StandardUnitList;
    type ComposedUnitDenominator: StandardUnitList;
    const NAME: &'static str;
    const SYMBOL: &'static str;
}

pub trait StandardUnit {
    const NAME: &'static str;
    const SYMBOL: &'static str;
}

impl<U: StandardUnit> crate::Unit for U {
    type ComposedUnitNumerator = Cons<Self, Nil>;
    type ComposedUnitDenominator = Nil;
    const NAME: &'static str = <U as StandardUnit>::NAME;
    const SYMBOL: &'static str = <U as StandardUnit>::SYMBOL;
}

pub struct Metre;
impl StandardUnit for Metre {
    const NAME: &'static str = "metre";
    const SYMBOL: &'static str = "m";
}

pub trait StandardUnitList {
    type Merged<Other: StandardUnitList>: StandardUnitList;
}

pub struct Nil;

impl StandardUnitList for Nil {
    type Merged<Other: StandardUnitList> = Other;
}

pub struct Cons<U: StandardUnit, T: StandardUnitList>(core::marker::PhantomData<(U, T)>);

impl<U: StandardUnit, T: StandardUnitList> StandardUnitList for Cons<U, T> {
    type Merged<Other: StandardUnitList> = Cons<U, T::Merged::<Other>>;
}

pub trait SameSuList {}

impl SameSuList for (Nil, Nil) {}

impl<U, T1, T2> SameSuList for (Cons<U, T1>, Cons<U, T2>)
where 
    U: StandardUnit,
    T1: StandardUnitList,
    T2: StandardUnitList,
    (T1, T2): SameSuListHelper<<T1 as NotObvious>::Unit>,
{}

trait NotObvious {
    type Unit;
}
impl<A> NotObvious for A {
    type Unit = ();
}

trait SameSuListHelper<A> {}

impl<A> SameSuListHelper<()> for A
where
    A: SameSuList,
{}

pub trait SameUnit {}

impl<U1, U2> SameUnit for (U1, U2)
where 
    U1: crate::Unit,
    U2: crate::Unit,
    (
        <U1::ComposedUnitNumerator as StandardUnitList>::Merged<U2::ComposedUnitDenominator>,
        <U2::ComposedUnitNumerator as StandardUnitList>::Merged<U1::ComposedUnitDenominator>,
    ): SameSuList,
{}

impl<Lhs, Rhs, Output, U1, U2> core::ops::Add<QuantifiedValue<Rhs, U2>> for QuantifiedValue<Lhs, U1>
where
    Lhs: core::ops::Add<Rhs, Output = Output>,
    U1: Unit,
    U2: Unit,
    (U1, U2): SameUnit,
{
    type Output = QuantifiedValue<Output, U1>;
    fn add(self, rhs: QuantifiedValue<Rhs, U2>) -> Self::Output {
        QuantifiedValue {
            inner: self.inner + rhs.inner,
            _m: core::marker::PhantomData,
        }
    }
}

(Note that I also had to create two different copies of distance, as the types don't implement Clone or Copy currently)