Type level integer with phantom types in Rust.

int.rs

use std::marker::PhantomData;

#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum Z {}
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct S<Z>(PhantomData<Z>);

/// `Int<M, N>` represents an integer `M - N`.
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub struct Int<M, N>(i64, PhantomData<(M, N)>);

impl<M, N> std::fmt::Debug for Int<M, N> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.debug_tuple("Int").field(&self.0).finish()
    }
}

impl Int<Z, Z> {
    /// Constructs a zero value.
    pub fn zero() -> Self {
        Int(0, PhantomData)
    }
}

impl<M, N> Int<M, N> {
    /// Casts into an `i64`.
    pub fn as_i64(self) -> i64 {
        self.0
    }

    /// Gets the successor value.
    pub fn succ(self) -> Int<S<M>, N> {
        Int(self.0 + 1, PhantomData)
    }

    /// Gets the predecessor value.
    pub fn pred(self) -> Int<M, S<N>> {
        Int(self.0 - 1, PhantomData)
    }

    /// Adds `self` and `other`.
    pub fn add<K>(self, other: Int<N, K>) -> Int<M, K> {
        Int(self.0 + other.0, PhantomData)
    }

    /// Substracts `other` from `self`.
    pub fn sub<K>(self, other: Int<K, N>) -> Int<M, K> {
        Int(self.0 - other.0, PhantomData)
    }

    /// Checks whether two integers equal as type-level.
    pub fn eq<K, L>(self, other: Int<K, L>) -> IntEq<M, N, K, L> {
        IntEq(self.0 == other.0, PhantomData)
    }
}

/// Whether two integers equal.
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct IntEq<M, N, K, L>(bool, PhantomData<(M, N, K, L)>);

impl<M, N, K, L> std::fmt::Debug for IntEq<M, N, K, L> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.debug_tuple("IntEq").field(&self.0).finish()
    }
}

impl<PM, PN, K, L> Prop for IntEq<S<PM>, S<PN>, K, L>
where
    IntEq<PM, PN, K, L>: Prop,
{
    type Res = <IntEq<PM, PN, K, L> as Prop>::Res;
}
impl<PN, PK, PL> Prop for IntEq<Z, S<PN>, S<PK>, S<PL>>
where
    IntEq<Z, S<PN>, S<PK>, S<PL>>: Prop,
{
    type Res = <IntEq<Z, S<PN>, S<PK>, S<PL>> as Prop>::Res;
}
impl<PM, PK, PL> Prop for IntEq<S<PM>, Z, S<PK>, S<PL>>
where
    IntEq<S<PM>, Z, S<PK>, S<PL>>: Prop,
{
    type Res = <IntEq<S<PM>, Z, S<PK>, S<PL>> as Prop>::Res;
}
impl Prop for IntEq<Z, Z, Z, Z> {
    type Res = True;
}
impl<N> Prop for IntEq<Z, S<N>, Z, Z> {
    type Res = False;
}
impl<L> Prop for IntEq<Z, Z, Z, S<L>> {
    type Res = False;
}

/// Single truth.
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub struct True;
/// Situation that occurs an absurdity when provided a truth.
pub type False = fn(True) -> !;

/// Type class for `True` and `False`.
pub trait Bool {}
impl Bool for True {}
impl Bool for False {}

/// Proposition type class that determines whether the question is satisfied.
pub trait Prop {
    type Res : Bool;
}

usage.rs

fn accepts_only_eq<M, N, K, L, P>(_: Int<M, N>, _: Int<K, L>, _: P)
where
    P: Prop<Res = True>,
{
}

fn main() {
    let x = Int::zero().succ().pred();
    let y = Int::zero();
    accepts_only_eq(x, y, x.eq(y));
    // this should occur an error
    // accepts_only_eq(x, y.succ(), x.eq(y.succ()));
}