From 23a0b3aa35eff1056ad3b160aaadaee5bb9c4a07 Mon Sep 17 00:00:00 2001
From: Melody Horn <melody@boringcactus.com>
Date: Sat, 13 Mar 2021 11:37:27 -0700
Subject: add types to this type-level programming clusterfuck

also make the numbers count down instead of up in AddQueens, which changes where the infinite recursion lives but doesn't fix it
---
 src/main.rs | 309 +++++++++++++++++++++++++++++++++++-------------------------
 1 file changed, 179 insertions(+), 130 deletions(-)

(limited to 'src')

diff --git a/src/main.rs b/src/main.rs
index 7612805..2de2e3a 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -4,50 +4,60 @@
 //! [source 2](https://sdleffler.github.io/RustTypeSystemTuringComplete/)
 use std::marker::PhantomData;
 
-struct Nil;
-struct Cons<X, XS>(PhantomData<X>, PhantomData<XS>);
-
-trait First {
-    type X;
+trait Typed {
+    type Type;
 }
 
-impl First for Nil {
-    type X = Nil;
+struct ListType<T>(PhantomData<T>);
+
+struct Nil<T>(PhantomData<T>);
+impl<T> Typed for Nil<T> { type Type = ListType<T>; }
+struct Cons<X, XS>(PhantomData<X>, PhantomData<XS>);
+impl<T, X: Typed<Type=T>, XS: Typed<Type=ListType<T>>> Typed for Cons<X, XS> { type Type = ListType<T>; }
+
+trait First<T>: Typed<Type=ListType<T>> {
+    type X: Typed<Type=T>;
 }
 
-impl<X, XS> First for Cons<X, XS> {
+impl<T, X: Typed<Type=T>, XS: Typed<Type=ListType<T>>> First<T> for Cons<X, XS> {
     type X = X;
 }
 
-trait ListConcat {
-    type C;
+trait ListConcat<X> {
+    type C: Typed<Type=ListType<X>>;
 }
 
-impl<X> ListConcat for (Nil, X) {
+impl<T, X: Typed<Type=ListType<T>>> ListConcat<T> for (Nil<T>, X) {
     type C = X;
 }
 
-impl<A, As, Bs> ListConcat for (Cons<A, As>, Bs) where (As, Bs): ListConcat {
-    type C = Cons<A, <(As, Bs) as ListConcat>::C>;
+impl<T, A: Typed<Type=T>, As: Typed<Type=ListType<T>>, Bs: Typed<Type=ListType<T>>> ListConcat<T> for (Cons<A, As>, Bs)
+    where (As, Bs): ListConcat<T> {
+    type C = Cons<A, <(As, Bs) as ListConcat<T>>::C>;
 }
 
-trait ListConcatAll {
-    type L;
+trait ListConcatAll<T>: Typed<Type=ListType<ListType<T>>> {
+    type L: Typed<Type=ListType<T>>;
 }
 
-impl ListConcatAll for Nil {
-    type L = Nil;
+impl<T> ListConcatAll<T> for Nil<ListType<T>> {
+    type L = Nil<T>;
 }
 
-impl<Chunk, Rest> ListConcatAll for Cons<Chunk, Rest> where Rest: ListConcatAll, (Chunk, <Rest as ListConcatAll>::L): ListConcat {
-    type L = <(Chunk, <Rest as ListConcatAll>::L) as ListConcat>::C;
+impl<T, Chunk: Typed<Type=ListType<T>>, Rest: Typed<Type=ListType<ListType<T>>>> ListConcatAll<T> for Cons<Chunk, Rest>
+    where Rest: ListConcatAll<T>, (Chunk, <Rest as ListConcatAll<T>>::L): ListConcat<T> {
+    type L = <(Chunk, <Rest as ListConcatAll<T>>::L) as ListConcat<T>>::C;
 }
 
+struct BoolType;
+
 struct True;
+impl Typed for True { type Type = BoolType; }
 struct False;
+impl Typed for False { type Type = BoolType; }
 
-trait Not {
-    type B;
+trait Not: Typed<Type=BoolType> {
+    type B: Typed<Type=BoolType>;
 }
 
 impl Not for True {
@@ -59,7 +69,7 @@ impl Not for False {
 }
 
 trait Or {
-    type B;
+    type B: Typed<Type=BoolType>;
 }
 
 impl Or for (True, True) {
@@ -78,15 +88,15 @@ impl Or for (False, False) {
     type B = False;
 }
 
-trait AnyTrue {
-    type T;
+trait AnyTrue: Typed<Type=ListType<BoolType>> {
+    type T: Typed<Type=BoolType>;
 }
 
-impl AnyTrue for Nil {
+impl AnyTrue for Nil<BoolType> {
     type T = False;
 }
 
-impl<More> AnyTrue for Cons<True, More> {
+impl<More: Typed<Type=ListType<BoolType>>> AnyTrue for Cons<True, More> {
     type T = True;
 }
 
@@ -94,174 +104,207 @@ impl<List> AnyTrue for Cons<False, List> where List: AnyTrue {
     type T = <List as AnyTrue>::T;
 }
 
-struct Z;
-struct S<N>(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>;
+struct NatType;
+
+struct N0;
+impl Typed for N0 { type Type = NatType; }
+struct N1;
+impl Typed for N1 { type Type = NatType; }
+struct N2;
+impl Typed for N2 { type Type = NatType; }
+struct N3;
+impl Typed for N3 { type Type = NatType; }
+struct N4;
+impl Typed for N4 { type Type = NatType; }
+struct N5;
+impl Typed for N5 { type Type = NatType; }
+struct N6;
+impl Typed for N6 { type Type = NatType; }
+struct N7;
+impl Typed for N7 { type Type = NatType; }
+struct N8;
+impl Typed for N8 { type Type = NatType; }
+
+trait Succ: Typed<Type=NatType> {
+    type N: Typed<Type=NatType>;
+}
+
+impl Succ for N1 { type N = N0; }
+impl Succ for N2 { type N = N1; }
+impl Succ for N3 { type N = N2; }
+impl Succ for N4 { type N = N3; }
+impl Succ for N5 { type N = N4; }
+impl Succ for N6 { type N = N5; }
+impl Succ for N7 { type N = N6; }
+impl Succ for N8 { type N = N7; }
 
 trait PeanoEqual {
-    type T;
+    type T: Typed<Type=BoolType>;
 }
 
-impl PeanoEqual for (Z, Z) {
+impl PeanoEqual for (N0, N0) {
     type T = True;
 }
 
-impl<A> PeanoEqual for (S<A>, Z) {
+impl<A, N: Succ<N=A>> PeanoEqual for (N, N0) {
     type T = False;
 }
 
-impl<B> PeanoEqual for (Z, S<B>) {
+impl<B, N: Succ<N=B>> PeanoEqual for (N0, N) {
     type T = False;
 }
 
-impl<A, B> PeanoEqual for (S<A>, S<B>) where (A, B): PeanoEqual {
+impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoEqual for (SA, SB) where (A, B): PeanoEqual {
     type T = <(A, B) as PeanoEqual>::T;
 }
 
 trait PeanoLT {
-    type T;
+    type T: Typed<Type=BoolType>;
 }
 
-impl PeanoLT for (Z, Z) {
+impl PeanoLT for (N0, N0) {
     type T = False;
 }
 
-impl<X> PeanoLT for (S<X>, Z) {
+impl<X, SX: Succ<N=X>> PeanoLT for (SX, N0) {
     type T = False;
 }
 
-impl<X> PeanoLT for (Z, S<X>) {
+impl<X, SX: Succ<N=X>> PeanoLT for (N0, SX) {
     type T = True;
 }
 
-impl<A, B> PeanoLT for (S<A>, S<B>) where (A, B): PeanoLT {
+impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoLT for (SA, SB) where (A, B): PeanoLT {
     type T = <(A, B) as PeanoLT>::T;
 }
 
 trait PeanoAbsDiff {
-    type C;
+    type C: Typed<Type=NatType>;
 }
 
-impl PeanoAbsDiff for (Z, Z) {
-    type C = Z;
+impl PeanoAbsDiff for (N0, N0) {
+    type C = N0;
 }
 
-impl<B> PeanoAbsDiff for (Z, S<B>) {
-    type C = S<B>;
+impl<B, SB: Succ<N=B>> PeanoAbsDiff for (N0, SB) {
+    type C = SB;
 }
 
-impl<A> PeanoAbsDiff for (S<A>, Z) {
-    type C = S<A>;
+impl<A, SA: Succ<N=A>> PeanoAbsDiff for (SA, N0) {
+    type C = SA;
 }
 
-impl<A, B> PeanoAbsDiff for (S<A>, S<B>) where (A, B): PeanoAbsDiff {
+impl<A, B, SA: Succ<N=A>, SB: Succ<N=B>> PeanoAbsDiff for (SA, SB) where (A, B): PeanoAbsDiff {
     type C = <(A, B) as PeanoAbsDiff>::C;
 }
 
-trait Range {
-    type Xs;
+trait Range: Typed<Type=NatType> {
+    type Xs: Typed<Type=ListType<NatType>>;
 }
 
-impl Range for Z {
-    type Xs = Nil;
+impl Range for N0 {
+    type Xs = Nil<NatType>;
 }
 
-impl<N> Range for S<N> where N: Range {
+impl<N, SN: Succ<N=N>> Range for SN where N: Range {
     type Xs = Cons<N, N::Xs>;
 }
 
 fn accepts_true(_: True) {}
-fn legal_compare(x: <(S<Z>, S<Z>) as PeanoEqual>::T) {
+fn legal_compare(x: <(N1, N1) as PeanoEqual>::T) {
     accepts_true(x)
 }
 
-trait Apply {
-    type R;
+struct Fn1Type<X, R>(PhantomData<X>, PhantomData<R>);
+
+trait Apply<T> {
+    type R: Typed<Type=T>;
 }
 
-struct Conj1<List>(PhantomData<List>);
+struct Conj1<List: Typed<Type=ListType<T>>, T>(PhantomData<List>);
+impl<T, List: Typed<Type=ListType<T>>> Typed for Conj1<List, T> { type Type = Fn1Type<T, ListType<T>>; }
 
-impl<List, X> Apply for (Conj1<List>, X) {
+impl<T, List: Typed<Type=ListType<T>>, X: Typed<Type=T>> Apply<ListType<T>> for (Conj1<List, T>, X) {
     type R = Cons<X, List>;
 }
 
-trait Map {
-    type Ys;
+trait Map<T> {
+    type Ys: Typed<Type=ListType<T>>;
 }
 
-impl<F> Map for (F, Nil) {
-    type Ys = Nil;
+impl<T1, T2, F: Typed<Type=Fn1Type<T1, T2>>> Map<T2> for (F, Nil<T1>) {
+    type Ys = Nil<T2>;
 }
 
-impl<F, X, Xs> Map for (F, Cons<X, Xs>) where (F, X): Apply, (F, Xs): Map {
-    type Ys = Cons<<(F, X) as Apply>::R, <(F, Xs) as Map>::Ys>;
+impl<T1, T2, F: Typed<Type=Fn1Type<T1, T2>>, X: Typed<Type=T1>, Xs: Typed<Type=ListType<T1>>> Map<T2> for (F, Cons<X, Xs>)
+    where (F, X): Apply<T2>, (F, Xs): Map<T2> {
+    type Ys = Cons<<(F, X) as Apply<T2>>::R, <(F, Xs) as Map<T2>>::Ys>;
 }
 
-trait MapCat {
-    type Zs;
+trait MapCat<T> {
+    type Zs: Typed<Type=ListType<T>>;
 }
 
-impl<F> MapCat for (F, Nil) {
-    type Zs = Nil;
+impl<T1, T2, F: Typed<Type=Fn1Type<T1, ListType<T2>>>> MapCat<T2> for (F, Nil<T1>) {
+    type Zs = Nil<T2>;
 }
 
-impl<F, Xs> MapCat for (F, Xs) where (F, Xs): Map, <(F, Xs) as Map>::Ys: ListConcatAll {
-    type Zs = <<(F, Xs) as Map>::Ys as ListConcatAll>::L;
+impl<T1, T2, F: Typed<Type=Fn1Type<T1, ListType<T2>>>, Xs: Typed<Type=ListType<T1>>> MapCat<T2> for (F, Xs)
+    where (F, Xs): Map<ListType<T2>>, <(F, Xs) as Map<ListType<T2>>>::Ys: ListConcatAll<T2> {
+    type Zs = <<(F, Xs) as Map<ListType<T2>>>::Ys as ListConcatAll<T2>>::L;
 }
 
-trait AppendIf {
-    type Zs;
+trait AppendIf<T> {
+    type Zs: Typed<Type=ListType<T>>;
 }
 
-impl<X, Ys> AppendIf for (True, X, Ys) {
+impl<T, X: Typed<Type=T>, Ys: Typed<Type=ListType<T>>> AppendIf<T> for (True, X, Ys) {
     type Zs = Cons<X, Ys>;
 }
 
-impl<X, Ys> AppendIf for (False, X, Ys) {
+impl<T, X: Typed<Type=T>, Ys: Typed<Type=ListType<T>>> AppendIf<T> for (False, X, Ys) {
     type Zs = Ys;
 }
 
-trait Filter {
-    type Ys;
+trait Filter<T> {
+    type Ys: Typed<Type=ListType<T>>;
 }
 
-impl<F> Filter for (F, Nil) {
-    type Ys = Nil;
+impl<T, F: Typed<Type=Fn1Type<T, BoolType>>> Filter<T> for (F, Nil<T>) {
+    type Ys = Nil<T>;
 }
 
-impl<F, X, Xs> Filter for (F, Cons<X, Xs>) where (F, X): Apply, (F, Xs): Filter, (<(F, X) as Apply>::R, X, <(F, Xs) as Filter>::Ys): AppendIf {
-    type Ys = <(<(F, X) as Apply>::R, X, <(F, Xs) as Filter>::Ys) as AppendIf>::Zs;
+impl<T, F: Typed<Type=Fn1Type<T, BoolType>>, X: Typed<Type=T>, Xs: Typed<Type=ListType<T>>> Filter<T> for (F, Cons<X, Xs>)
+    where (F, X): Apply<BoolType>, (F, Xs): Filter<T>,
+          (<(F, X) as Apply<BoolType>>::R, X, <(F, Xs) as Filter<T>>::Ys): AppendIf<T> {
+    type Ys = <(<(F, X) as Apply<BoolType>>::R, X, <(F, Xs) as Filter<T>>::Ys) as AppendIf<T>>::Zs;
 }
 
-struct Queen<X, Y>(PhantomData<X>, PhantomData<Y>);
-struct Queen1<X>(PhantomData<X>);
+struct QueenType;
+
+struct Queen<X: Typed<Type=NatType>, Y: Typed<Type=NatType>>(PhantomData<X>, PhantomData<Y>);
+impl<X, Y> Typed for Queen<X, Y> { type Type = QueenType; }
+struct Queen1<X: Typed<Type=NatType>>(PhantomData<X>);
+impl<X> Typed for Queen1<X> { type Type = Fn1Type<NatType, QueenType>; }
 
-impl<X, Y> Apply for (Queen1<X>, Y) {
+impl<X: Typed<Type=NatType>, Y: Typed<Type=NatType>> Apply<QueenType> for (Queen1<X>, Y) {
     type R = Queen<X, Y>;
 }
 
 trait QueensInRow {
-    type Queens;
+    type Queens: Typed<Type=ListType<QueenType>>;
 }
 
-impl<N, X> QueensInRow for (N, X) where N: Range, (Queen1<X>, <N as Range>::Xs): Map {
-    type Queens = <(Queen1<X>, <N as Range>::Xs) as Map>::Ys;
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>> QueensInRow for (N, X)
+    where N: Range, (Queen1<X>, <N as Range>::Xs): Map<QueenType> {
+    type Queens = <(Queen1<X>, <N as Range>::Xs) as Map<QueenType>>::Ys;
 }
 
 trait Threatens {
-    type T;
+    type T: Typed<Type=BoolType>;
 }
 
-impl<Ax, Ay, Bx, By> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
+impl<Ax: Typed<Type=NatType>, Ay: Typed<Type=NatType>, Bx: Typed<Type=NatType>, By: Typed<Type=NatType>> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
     where (Ax, Bx): PeanoEqual + PeanoAbsDiff, (Ay, By): PeanoEqual + PeanoAbsDiff,
           (<(Ax, Bx) as PeanoEqual>::T, <(Ay, By) as PeanoEqual>::T): Or,
           (<(Ax, Bx) as PeanoAbsDiff>::C, <(Ay, By) as PeanoAbsDiff>::C): PeanoEqual,
@@ -274,84 +317,90 @@ impl<Ax, Ay, Bx, By> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
     ) as Or>::B;
 }
 
-struct Threatens1<A>(PhantomData<A>);
+struct Threatens1<A: Typed<Type=QueenType>>(PhantomData<A>);
+impl<A> Typed for Threatens1<A> { type Type = Fn1Type<QueenType, BoolType>; }
 
-impl<A, B> Apply for (Threatens1<A>, B) where (A, B): Threatens {
+impl<A: Typed<Type=QueenType>, B: Typed<Type=QueenType>> Apply<BoolType> for (Threatens1<A>, B)
+    where (A, B): Threatens {
     type R = <(A, B) as Threatens>::T;
 }
 
 trait Safe {
-    type T;
+    type T: Typed<Type=BoolType>;
 }
 
-impl<Config, Queen> Safe for (Config, Queen)
-    where (Threatens1<Queen>, Config): Map,
-          <(Threatens1<Queen>, Config) as Map>::Ys: AnyTrue,
-          <<(Threatens1<Queen>, Config) as Map>::Ys as AnyTrue>::T: Not {
-    type T = <<<(Threatens1<Queen>, Config) as Map>::Ys as AnyTrue>::T as Not>::B;
+impl<Config: Typed<Type=ListType<QueenType>>, Queen: Typed<Type=QueenType>> Safe for (Config, Queen)
+    where (Threatens1<Queen>, Config): Map<BoolType>,
+          <(Threatens1<Queen>, Config) as Map<BoolType>>::Ys: AnyTrue,
+          <<(Threatens1<Queen>, Config) as Map<BoolType>>::Ys as AnyTrue>::T: Not {
+    type T = <<<(Threatens1<Queen>, Config) as Map<BoolType>>::Ys as AnyTrue>::T as Not>::B;
 }
 
-struct Safe1<Config>(PhantomData<Config>);
+struct Safe1<Config: Typed<Type=ListType<QueenType>>>(PhantomData<Config>);
 
-impl<Config, Queen> Apply for (Safe1<Config>, Queen) where (Config, Queen): Safe {
+impl<Config: Typed<Type=ListType<QueenType>>, Queen> Apply<BoolType> for (Safe1<Config>, Queen)
+    where (Config, Queen): Safe {
     type R = <(Config, Queen) as Safe>::T;
 }
 
 trait AddQueen {
-    type Cs;
+    type Cs: Typed<Type=ListType<QueenType>>;
 }
 
-impl<N, X, C> AddQueen for (N, X, C)
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, C: Typed<Type=ListType<QueenType>>> AddQueen for (N, X, C)
     where (N, X): QueensInRow,
-          (Safe1<C>, <(N, X) as QueensInRow>::Queens): Filter,
-          <(Conj1<C>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys: Map {
-    type Cs = <<(Conj1<C>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys as Map>::Ys;
+          (Safe1<C>, <(N, X) as QueensInRow>::Queens): Filter<QueenType>,
+          <(Conj1<C, QueenType>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter<QueenType>>::Ys: Map<QueenType> {
+    type Cs = <<(Conj1<C, QueenType>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter<QueenType>>::Ys as Map<QueenType>>::Ys;
 }
 
-struct AddQueen2<N, X>(PhantomData<N>, PhantomData<X>);
+struct AddQueen2<N: Typed<Type=NatType>, X: Typed<Type=NatType>>(PhantomData<N>, PhantomData<X>);
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>> Typed for AddQueen2<N, X> { type Type = Fn1Type<ListType<QueenType>, ListType<QueenType>>; }
 
-impl<N, X, C> Apply for (AddQueen2<N, X>, C) where (N, X, C): AddQueen {
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, C: Typed<Type=ListType<QueenType>>> Apply<ListType<QueenType>> for (AddQueen2<N, X>, C)
+    where (N, X, C): AddQueen {
     type R = <(N, X, C) as AddQueen>::Cs;
 }
 
 trait AddQueenToAll {
-    type CsPrime;
+    type CsPrime: Typed<Type=ListType<ListType<QueenType>>>;
 }
 
-impl<N, X, Cs> AddQueenToAll for (N, X, Cs) where (AddQueen2<N, X>, Cs): MapCat {
-    type CsPrime = <(AddQueen2<N, X>, Cs) as MapCat>::Zs;
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> AddQueenToAll for (N, X, Cs)
+    where (AddQueen2<N, X>, Cs): MapCat<ListType<QueenType>> {
+    type CsPrime = <(AddQueen2<N, X>, Cs) as MapCat<ListType<QueenType>>>::Zs;
 }
 
 trait AddQueensIf {
-    type CsPrime;
+    type CsPrime: Typed<Type=ListType<ListType<QueenType>>>;
 }
 
-impl<N, X, Cs> AddQueensIf for (False, N, X, Cs) {
+impl<N: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> AddQueensIf for (N, N0, Cs) {
     type CsPrime = Cs;
 }
 
-impl<N, X, Cs> AddQueensIf for (True, N, X, Cs)
-    where (N, X, Cs): AddQueenToAll,
-          (N, S<X>, <(N, X, Cs) as AddQueenToAll>::CsPrime): AddQueens {
-    type CsPrime = <(N, S<X>, <(N, X, Cs) as AddQueenToAll>::CsPrime) as AddQueens>::CsPrime;
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>, SX: Succ<N=X>> AddQueensIf for (N, SX, Cs)
+    where (N, SX, Cs): AddQueenToAll,
+          (N, X, <(N, SX, Cs) as AddQueenToAll>::CsPrime): AddQueens {
+    type CsPrime = <(N, X, <(N, SX, Cs) as AddQueenToAll>::CsPrime) as AddQueens>::CsPrime;
 }
 
 trait AddQueens {
-    type CsPrime;
+    type CsPrime: Typed<Type=ListType<ListType<QueenType>>>;
 }
 
-impl<N, X, Cs> AddQueens for (N, X, Cs)
-    where (X, N): PeanoLT,
-          (<(X, N) as PeanoLT>::T, N, X, Cs): AddQueensIf {
-    type CsPrime = <(<(X, N) as PeanoLT>::T, N, X, Cs) as AddQueensIf>::CsPrime;
+impl<N: Typed<Type=NatType>, X: Typed<Type=NatType>, Cs: Typed<Type=ListType<ListType<QueenType>>>> AddQueens for (N, X, Cs)
+    where (N, X, Cs): AddQueensIf {
+    type CsPrime = <(N, X, Cs) as AddQueensIf>::CsPrime;
 }
 
 trait Solution {
-    type C;
+    type C: Typed<Type=ListType<QueenType>>;
 }
 
-impl<N> Solution for N where (N, Z, Cons<Nil, Nil>): AddQueens, <(N, Z, Cons<Nil, Nil>) as AddQueens>::CsPrime: First {
-    type C = <<(N, Z, Cons<Nil, Nil>) as AddQueens>::CsPrime as First>::X;
+impl<N: Typed<Type=NatType>> Solution for N
+    where (N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>): AddQueens, <(N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>) as AddQueens>::CsPrime: First<ListType<QueenType>> {
+    type C = <<(N, N, Cons<Nil<QueenType>, Nil<ListType<QueenType>>>) as AddQueens>::CsPrime as First<ListType<QueenType>>>::X;
 }
 
 fn solve() -> <N6 as Solution>::C {
-- 
cgit v1.2.3