N queen problem in the Rust type system

queen.rs

#! /usr/bin/env -S cargo +nightly -Zscript
---
[package]
edition = "2024"
[dependencies]
---

#![recursion_limit = "1024"]

use std::marker::PhantomData;

/* 
// Peano Numbers
trait Nat {}
impl Nat for Z {}
impl<N: Nat> Nat for S<N> {}

struct Z;
struct S<N: Nat>(PhantomData<N>);

type N0 = Z;
type N1 = S<N0>;
type N2 = S<N1>;
type N3 = S<N2>;
type N4 = S<N3>;
type N5 = S<N4>;
type N6 = S<N5>;
type N7 = S<N6>;
type N8 = S<N7>;

trait PeanoEqual {
    type Output: Bool;
}

impl PeanoEqual for (Z, Z) {
    type Output = True;
}

impl<N> PeanoEqual for (Z, S<N>)
where
    N: Nat,
{
    type Output = False;
}

impl<N> PeanoEqual for (S<N>, Z)
where
    N: Nat,
{
    type Output = False;
}

impl<N1, N2> PeanoEqual for (S<N1>, S<N2>)
where
    N1: Nat,
    N2: Nat,
    (N1, N2): PeanoEqual,
{
    type Output = <(N1, N2) as PeanoEqual>::Output;
}

trait PeanoLT {
    type Output: Bool;
}

impl PeanoLT for (Z, Z) {
    type Output = False;
}

impl<N: Nat> PeanoLT for (S<N>, Z) {
    type Output = False;
}

impl<N: Nat> PeanoLT for (Z, S<N>) {
    type Output = True;
}

impl<N1, N2> PeanoLT for (S<N1>, S<N2>)
where
    N1: Nat,
    N2: Nat,
    (N1, N2): PeanoLT,
{
    type Output = <(N1, N2) as PeanoLT>::Output;
}

trait PeanoAbsDiff {
    type Output: Nat;
}

impl PeanoAbsDiff for (Z, Z) {
    type Output = Z;
}

impl<N: Nat> PeanoAbsDiff for (Z, S<N>) {
    type Output = S<N>;
}

impl<N: Nat> PeanoAbsDiff for (S<N>, Z) {
    type Output = S<N>;
}

impl<N1, N2> PeanoAbsDiff for (S<N1>, S<N2>)
where
    N1: Nat,
    N2: Nat,
    (N1, N2): PeanoAbsDiff,
{
    type Output = <(N1, N2) as PeanoAbsDiff>::Output;
}
// srebmuN onaeP
*/

// Church Numbers
trait ChurchNat {
    type Succ: ChurchNat;
    type IsZero: Bool;
}

struct Zero;
struct Succ<N: ChurchNat>(PhantomData<N>);

impl ChurchNat for Zero {
    type Succ = Succ<Zero>;
    type IsZero = True;
}

impl<N: ChurchNat> ChurchNat for Succ<N> {
    type Succ = Succ<Succ<N>>;
    type IsZero = False;
}//
//

type N0 = Zero;
type N1 = Succ<N0>;
type N2 = Succ<N1>;
type N3 = Succ<N2>;
type N4 = Succ<N3>;
type N5 = Succ<N4>;
type N6 = Succ<N5>;
type N7 = Succ<N6>;
type N8 = Succ<N7>;

trait ChurchEqual {
    type Output: Bool;
}

impl ChurchEqual for (Zero, Zero) {
    type Output = True;
}

impl<N: ChurchNat> ChurchEqual for (Zero, Succ<N>) {
    type Output = False;
}

impl<N: ChurchNat> ChurchEqual for (Succ<N>, Zero) {
    type Output = False;
}

impl<N1, N2> ChurchEqual for (Succ<N1>, Succ<N2>)
where
    N1: ChurchNat,
    N2: ChurchNat,
    (N1, N2): ChurchEqual,
{
    type Output = <(N1, N2) as ChurchEqual>::Output;
}

trait ChurchLT {
    type Output: Bool;
}

impl ChurchLT for (Zero, Zero) {
    type Output = False;
}

impl<N: ChurchNat> ChurchLT for (Succ<N>, Zero) {
    type Output = False;
}

impl<N: ChurchNat> ChurchLT for (Zero, Succ<N>) {
    type Output = True;
}

impl<N1, N2> ChurchLT for (Succ<N1>, Succ<N2>)
where
    N1: ChurchNat,
    N2: ChurchNat,
    (N1, N2): ChurchLT,
{
    type Output = <(N1, N2) as ChurchLT>::Output;
}

trait ChurchAbsDiff {
    type Output: ChurchNat;
}

impl ChurchAbsDiff for (Zero, Zero) {
    type Output = Zero;
}

impl<N: ChurchNat> ChurchAbsDiff for (Zero, Succ<N>) {
    type Output = Succ<N>;
}

impl<N: ChurchNat> ChurchAbsDiff for (Succ<N>, Zero) {
    type Output = Succ<N>;
}

impl<N1, N2> ChurchAbsDiff for (Succ<N1>, Succ<N2>)
where
    N1: ChurchNat,
    N2: ChurchNat,
    (N1, N2): ChurchAbsDiff,
{
    type Output = <(N1, N2) as ChurchAbsDiff>::Output;
}
// srebmuN hcruhC

// List
struct Nil;
struct Cons<X, Xs>(PhantomData<(X, Xs)>);
// tsiL

// List functions
trait AnyTrue {
    type Output: Bool;
}

impl AnyTrue for Nil {
    type Output = False;
}

impl<L> AnyTrue for Cons<True, L> {
    type Output = True;
}

impl<L> AnyTrue for Cons<False, L>
where
    L: AnyTrue,
{
    type Output = <L as AnyTrue>::Output;
}

trait Map {
    type Output;
}

impl<F> Map for (F, Nil) {
    type Output = Nil;
}

impl<F, X, Xs> Map for (F, Cons<X, Xs>)
where
    F: Apply<X>,
    (F, Xs): Map,
{
    type Output = Cons<<F as Apply<X>>::Output, <(F, Xs) as Map>::Output>;
}

trait MapCat {
    type Output;
}

impl<F, L> MapCat for (F, L)
where
    (F, L): Map,
    <(F, L) as Map>::Output: ListConcatAll,
{
    type Output = <<(F, L) as Map>::Output as ListConcatAll>::Output;
}

trait AppendIf {
    type Output;
}

impl<X, Ys> AppendIf for (True, X, Ys) {
    type Output = Cons<X, Ys>;
}

impl<X, Ys> AppendIf for (False, X, Ys) {
    type Output = Ys;
}

trait Filter {
    type Output;
}

impl<F> Filter for (F, Nil) {
    type Output = Nil;
}

impl<F, X, Xs, FilterOutput> Filter for (F, Cons<X, Xs>)
where
    F: Apply<X>,
    (F, Xs): Filter<Output = FilterOutput>,
    (<F as Apply<X>>::Output, X, FilterOutput): AppendIf,
{
    type Output = <(<F as Apply<X>>::Output, X, <(F, Xs) as Filter>::Output) as AppendIf>::Output;
}

trait ListConcat {
    type Output;
}

impl<L2> ListConcat for (Nil, L2) {
    type Output = L2;
}

impl<X, Xs, L2> ListConcat for (Cons<X, Xs>, L2)
where
    (Xs, L2): ListConcat,
{
    type Output = Cons<X, <(Xs, L2) as ListConcat>::Output>;
}

trait ListConcatAll {
    type Output;
}

impl ListConcatAll for Nil {
    type Output = Nil;
}

impl<L, Ls> ListConcatAll for Cons<L, Ls>
where
    Ls: ListConcatAll,
    (L, <Ls as ListConcatAll>::Output): ListConcat,
{
    type Output = <(L, <Ls as ListConcatAll>::Output) as ListConcat>::Output;
}
// snoitcnuf tsiL

// Booleans
struct True;
struct False;

trait Bool {}

impl Bool for True {}
impl Bool for False {}

trait Not {
    type Output: Bool;
}

impl Not for True {
    type Output = False;
}

impl Not for False {
    type Output = True;
}

trait Or {
    type Output: Bool;
}

impl Or for (False, False) {
    type Output = False;
}

impl Or for (False, True) {
    type Output = True;
}

impl Or for (True, False) {
    type Output = True;
}

impl Or for (True, True) {
    type Output = True;
}


trait Apply<A> {
    type Output;
}

// can't quite curry and partial func app at the type level so need a helper
struct Conj1<L>(PhantomData<L>);
impl<X, L> Apply<X> for Conj1<L> {
    type Output = Cons<X, L>;
}

// Range
trait Range {
    type Output;
}

impl Range for Zero {
    type Output = Nil;
}

impl<N> Range for Succ<N>
where
    N: ChurchNat + Range,
{
    type Output = Cons<N, <N as Range>::Output>;
}
// egnaR

// Queen
struct Queen<X, Y>(PhantomData<(X, Y)>);
struct Queen1<X>(PhantomData<X>);

impl<X: ChurchNat, Y> Apply<Y> for Queen1<X> {
    type Output = Queen<X, Y>;
}

trait QueensInRow {
    type Output;
}

impl<N, X> QueensInRow for (N, X)
where
    N: Range,
    (Queen1<X>, <N as Range>::Output): Map,
{
    type Output = <(Queen1<X>, <N as Range>::Output) as Map>::Output;
}
// neeuQ

trait Threatens {
    type Output: Bool;
}

impl<Ax, Ay, Bx, By> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
where
    (Ax, Bx): ChurchEqual,
    (Ay, By): ChurchEqual,
    (Ax, Bx): ChurchAbsDiff,
    (Ay, By): ChurchAbsDiff,
    (
        <(Ax, Bx) as ChurchEqual>::Output,
        <(Ay, By) as ChurchEqual>::Output,
    ): Or,
    (
        <(Ax, Bx) as ChurchAbsDiff>::Output,
        <(Ay, By) as ChurchAbsDiff>::Output,
    ): ChurchEqual,
    (
        <(
            <(Ax, Bx) as ChurchEqual>::Output,
            <(Ay, By) as ChurchEqual>::Output,
        ) as Or>::Output,
        <(
            <(Ax, Bx) as ChurchAbsDiff>::Output,
            <(Ay, By) as ChurchAbsDiff>::Output,
        ) as ChurchEqual>::Output,
    ): Or,
{
    type Output = <(
        <(
            <(Ax, Bx) as ChurchEqual>::Output,
            <(Ay, By) as ChurchEqual>::Output,
        ) as Or>::Output,
        <(
            <(Ax, Bx) as ChurchAbsDiff>::Output,
            <(Ay, By) as ChurchAbsDiff>::Output,
        ) as ChurchEqual>::Output,
    ) as Or>::Output;
}

struct Threatens1<A>(PhantomData<A>);
impl<Qa, Qb> Apply<Qb> for Threatens1<Qa>
where
    (Qa, Qb): Threatens,
{
    type Output = <(Qa, Qb) as Threatens>::Output;
}

trait Safe {
    type Output: Bool;
}

impl<C, Q> Safe for (C, Q)
where
    (Threatens1<Q>, C): Map,
    <(Threatens1<Q>, C) as Map>::Output: AnyTrue,
    <<(Threatens1<Q>, C) as Map>::Output as AnyTrue>::Output: Not,
{
    type Output = <<<(Threatens1<Q>, C) as Map>::Output as AnyTrue>::Output as Not>::Output;
}

struct Safe1<C>(PhantomData<C>);
impl<C, Q> Apply<Q> for Safe1<C>
where
    (C, Q): Safe,
{
    type Output = <(C, Q) as Safe>::Output;
}

trait AddQueen {
    type Output;
}

impl<N, X, C> AddQueen for (N, X, C)
where
    (N, X): QueensInRow,
    (Safe1<C>, <(N, X) as QueensInRow>::Output): Filter,
    (
        Conj1<C>,
        <(Safe1<C>, <(N, X) as QueensInRow>::Output) as Filter>::Output,
    ): Map,
{
    type Output = <(
        Conj1<C>,
        <(Safe1<C>, <(N, X) as QueensInRow>::Output) as Filter>::Output,
    ) as Map>::Output;
}

struct AddQueen2<N, X>(PhantomData<(N, X)>);
impl<N, X, C> Apply<C> for AddQueen2<N, X>
where
    (N, X, C): AddQueen,
{
    type Output = <(N, X, C) as AddQueen>::Output;
}

trait AddQueenToAll {
    type Output;
}

impl<N, X, Cs> AddQueenToAll for (N, X, Cs)
where
    (AddQueen2<N, X>, Cs): MapCat,
{
    type Output = <(AddQueen2<N, X>, Cs) as MapCat>::Output;
}

trait AddQueensIf {
    type Output;
}

impl<N, X, Cs> AddQueensIf for (False, N, X, Cs) {
    type Output = Cs;
}

impl<N, X, Cs, AddQueenToAllOutput> AddQueensIf for (True, N, X, Cs)
where
    X: ChurchNat,
    (N, X, Cs): AddQueenToAll<Output = AddQueenToAllOutput>,
    (N, <X as ChurchNat>::Succ, AddQueenToAllOutput): AddQueens,
{
    type Output = <(N, <X as ChurchNat>::Succ, <(N, X, Cs) as AddQueenToAll>::Output) as AddQueens>::Output;
}

trait AddQueens {
    type Output;
}

impl<N, X, Cs, ChurchLTOutput> AddQueens for (N, X, Cs)
where
    (X, N): ChurchLT<Output = ChurchLTOutput>,
    (ChurchLTOutput, N, X, Cs): AddQueensIf,
{
    type Output = <(<(X, N) as ChurchLT>::Output, N, X, Cs) as AddQueensIf>::Output;
}

trait Solution {
    type Output;
}

impl<N, AddQueensIfOutput> Solution for N
where
    N: ChurchNat,
    (Zero, N): ChurchLT,
    (<(Zero, N) as ChurchLT>::Output, N, Zero, Cons<Nil, Nil>): AddQueensIf<Output = AddQueensIfOutput>,
    AddQueensIfOutput: First,
{
    type Output = <<(N, Zero, Cons<Nil, Nil>) as AddQueens>::Output as First>::Output;
}

trait First {
    type Output;
}

impl First for Nil {
    type Output = Nil;
}

impl<X, Xs> First for Cons<X, Xs> {
    type Output = X;
}

fn main() {

    let mut args = std::env::args().collect::<Vec<String>>();
    let _program = args.iter().skip(1);
    let arg = args.pop().expect("Enter a number between 0..=8");

    let num: u8 = arg.parse().expect("Enter a number between 0..=8");

    let ans = match num {
        0 => std::any::type_name::<<Zero as Solution>::Output>(),
        1 => std::any::type_name::<<N1 as Solution>::Output>(),
        2 => std::any::type_name::<<N2 as Solution>::Output>(),
        3 => std::any::type_name::<<N3 as Solution>::Output>(),
        4 => std::any::type_name::<<N4 as Solution>::Output>(),
        5 => std::any::type_name::<<N5 as Solution>::Output>(),
        6 => std::any::type_name::<<N6 as Solution>::Output>(),
        7 => std::any::type_name::<<N7 as Solution>::Output>(),
        8 => std::any::type_name::<<N8 as Solution>::Output>(),
        _ => panic!("Enter a number between 0..=8"),
    };

    dbg!(ans);

}