Lambda calculus on Rust types

lambda.rs

trait Lam<X> {
    type Result;
}

struct True0;
struct True1<X>(X);

struct False0;
struct False1<X>(X);

// \x. \y. x
impl<X> Lam<X> for True0 {
    type Result = True1<X>;
}
impl<X, Y> Lam<Y> for True1<X> {
    type Result = X;
}

// \x. \y. y
impl<X> Lam<X> for False0 {
    type Result = False1<X>;
}
impl<X, Y> Lam<Y> for False1<X> {
    type Result = Y;
}

struct And0;
struct And1<X>(X);

impl<X> Lam<X> for And0 {
    type Result = And1<X>;
}
impl<X, Y> Lam<Y> for And1<X>
where
    X: Lam<Y>,
    <X as Lam<Y>>::Result: Lam<X>,
{
    type Result = <<X as Lam<Y>>::Result as Lam<X>>::Result;
}

struct If0;
struct IfCond<Cond>(Cond);
struct IfCondT<Cond, T>(Cond, T);

impl<Cond> Lam<Cond> for If0 {
    type Result = IfCond<Cond>;
}
impl<Cond, T> Lam<T> for IfCond<Cond> {
    type Result = IfCondT<Cond, T>;
}

impl<Cond, T, F> Lam<F> for IfCondT<Cond, T>
where
    Cond: Lam<T>,
    <Cond as Lam<T>>::Result: Lam<F>
{
    type Result = <<Cond as Lam<T>>::Result as Lam<F>>::Result;
}

struct Identity;
impl<X> Lam<X> for Identity {
    type Result = X;
}

struct Xx;
impl<X> Lam<X> for Xx
where
    X: Lam<X>
{
    type Result = <X as Lam<X>>::Result;
}

type Identity2 = <Xx as Lam<Identity>>::Result;
static T0: Identity2 = Identity;

type Bool = True0;
type OnTrue = i32;
type OnFalse = String;

type I32 = <
    <<If0 as Lam<Bool>>::Result as Lam<OnTrue>>::Result
    as Lam<OnFalse>
>::Result;
static I32Value: I32 = 100_i32;

// -- Uncommenting this leads to infinite recursion in the compiler
// type InfiniteRecursion = <Xx as Lam<Xx>>::Result;
// static T1: InfiniteRecursion = Xx;