Silly natural numbers on types

nat-typefuck.rs

trait Nat {
    type Succ;
    
    const NUMERIC: u64;
}

struct S<T>(T);
struct Z;

impl Nat for Z {
    type Succ = S<Z>;
    const NUMERIC: u64 = 0;
}
impl<T: Nat> Nat for S<T> {
    type Succ = S<T>;
    const NUMERIC: u64 = 1 + <T as Nat>::NUMERIC;
}

// Traits

trait Add<R: Nat>: Nat {
    type Added: Nat;
}

trait Mul<R: Nat>: Nat {
    type Multiplied: Nat;
}

trait Pow<R: Nat>: Nat {
    type Raised: Nat;
}

// Adding

impl<T: Nat> Add<Z> for T {
    type Added = T;
}
impl<T: Nat + Add<R>, R: Nat> Add<S<R>> for T {
    type Added = S<<T as Add<R>>::Added>;
}

// Multiplying

impl<T: Nat> Mul<Z> for T {
    type Multiplied = Z;
}
impl<T, R> Mul<S<R>> for T
where
    T: Nat + Mul<R> + Add<<T as Mul<R>>::Multiplied>,
    R: Nat
{
    type Multiplied = < T as Add< <T as Mul<R>>::Multiplied > >::Added;
}

// Raising

impl<T: Nat> Pow<Z> for T {
    type Raised = S<Z>;
}

impl<T, R> Pow<S<R>> for T
where
    T: Nat + Pow<R> + Mul< <T as Pow<R>>::Raised >,
    R: Nat,
{
    type Raised = < T as Mul< <T as Pow<R>>::Raised > >::Multiplied;
}

// Testing

fn main() {
    type _1 = S<Z>;
    type _2 = S<_1>;
    type _3 = S<_2>;
    type _4 = S<_3>;
    type _5 = S<_4>;
    
    type _8 = < _4 as Mul<_2> >::Multiplied;
    type _64 = < _8 as Pow<_2> >::Raised;
    
    dbg!(_64::NUMERIC);
    
    dbg!(_1::NUMERIC, _2::NUMERIC, _3::NUMERIC);
    dbg!(
        <_1 as Add<_2>>::Added::NUMERIC,
        <_2 as Add<_3>>::Added::NUMERIC,
    );
    
    dbg!(
        < <_3 as Mul<_3>>::Multiplied as Add< <_4 as Mul<_4>>::Multiplied > >::Added::NUMERIC
    );
    dbg!(
        <_3 as Pow<_2>>::Raised::NUMERIC
    );
}