Shared via Rust Playground

playground.rs

#![feature(optin_builtin_traits)]
use std::marker::PhantomData;

struct Nil;
struct Cons<H, T>(H, T);

struct Pair<A, B>(A, B);

trait Lookup_<S, Env> { type Type; }
type Lookup<S, Env> = <() as Lookup_<S, Env>>::Type;

trait NotKeyMatch {}
impl NotKeyMatch for .. {}
impl<K, V> !NotKeyMatch for (K, Pair<K, V>) {}

impl<K, X, XS>
Lookup_<K, Cons<X, XS>> for ()
where (): Lookup_<K, XS>, (K, X): NotKeyMatch
{ type Type = Lookup<K, XS>; }

impl<K, V, XS>
Lookup_<K, Cons<Pair<K, V>, XS>> for ()
{ type Type = V; }

trait Eval_<T, Env> { type Type; }
type Eval<T, Env> = <() as Eval_<T, Env>>::Type;

struct App<F, A>(PhantomData<(F, A)>);
struct Fn<X, E>(PhantomData<(X, E)>);
struct Ref<X>(PhantomData<X>);
struct Subst<X, E, R>(PhantomData<(X, E, R)>);

trait NotAction {}
impl NotAction for .. {}
impl<X, E> NotAction for Fn<X, E> {}
impl<F, A> !NotAction for App<F, A> {}
impl<X> !NotAction for Ref<X> {}
impl<X, E, R> !NotAction for Subst<X, E, R> {}

impl<T, Env>
Eval_<T, Env> for ()
where T: NotAction
{ type Type = T; }

trait Apply_<F, A> { type Type; }
type Apply<F, A> = <() as Apply_<F, A>>::Type;

impl<X, E, A>
Apply_<Fn<X, E>, A> for ()
{ type Type = Subst<X, E, A>; }

impl<F, A, Env>
Eval_<App<F, A>, Env> for ()
where ():
Eval_<F, Env> +
Eval_<A, Env> +
Apply_<Eval<F, Env>, Eval<A, Env>> +
Eval_<Apply<Eval<F, Env>, Eval<A, Env>>, Env>
{ type Type = Eval<Apply<Eval<F, Env>, Eval<A, Env>>, Env>; }

impl<X, E, R, Env>
Eval_<Subst<X, E, R>, Env> for ()
where (): Eval_<E, Cons<Pair<X, R>, Env>>
{ type Type = Eval<E, Cons<Pair<X, R>, Env>>; }

impl<X, Env>
Eval_<Ref<X>, Env> for ()
where (): Lookup_<X, Env>
{ type Type = Lookup<X, Env>; }


fn foo<F, A, Env>() 
where ():
Eval_<F, Env> +
Eval_<A, Env> +
Apply_<Eval<F, Env>, Eval<A, Env>> +
Eval_<Apply<Eval<F, Env>, Eval<A, Env>>, Env>
{}
/////////////////////////////////
struct X;
type Id = Fn<X, Ref<X>>;
type Temp = Eval<Apply<Eval<Id, Nil>, Eval<bool, Nil>>, Nil>;
type Temp2 = Eval<App<Id, bool>, Nil>;
type Temp3 = Eval<Subst<X, Ref<X>, bool>, Nil>;

//type Temp2 = Lookup<bool, Cons<Pair<bool, u32>, Nil>>;
type Bool = Eval<App<Id, bool>, Nil>;

fn main() {
    //foo::<Id, bool, Nil>();
    let x: bool = PhantomData::<Bool>;
    //let y: Bool = true;
}