Type level tic tac toe using match types

TicTacToe.Scala

sealed trait Bool
object Bool:
    sealed trait True extends Bool
    sealed trait False extends Bool
    
sealed trait Nat
object Nat:
    sealed trait _0 extends Nat
    sealed trait Succ[N <: Nat] extends Nat

    type _1 = Succ[_0]
    type _2 = Succ[_1]

object TicTacToe:
    sealed trait T3Player
    object T3Player:
        sealed trait O extends T3Player
        sealed trait X extends T3Player

    sealed trait T3Result
    object T3Result:
        sealed trait Win[P <: T3Player] extends T3Result
        sealed trait Tie extends T3Result
        sealed trait Invalid extends T3Result

    type V = T3Player | Unit

    type T3Row = (V, V, V)
    type EmptyT3Row = (Unit, Unit, Unit)
    type T3Board = (T3Row, T3Row, T3Row)
    type EmptyT3Board = (EmptyT3Row, EmptyT3Row, EmptyT3Row)

    type PlayResult = T3Result | T3Board

    type ReplaceRow[R <: Tuple, P <: T3Player, X <: Nat] <: Tuple | Unit = (R, X) match
        case (EmptyTuple, _) => Unit
        case (T3Player *: _, Nat._0) => Unit
        case (Unit *: nextR, Nat._0) => P *: nextR
        case (t *: nextR, Nat.Succ[nextX]) => ReplaceRow[nextR, P, nextX] match
            case Id[res] => res match
                case Unit => Unit
                case Tuple => t *: ReplaceRow[nextR, P, nextX]

    type ReplaceBoard[T <: Tuple, P <: T3Player, Y <: Nat, X <: Nat] <: Tuple | Unit = (T, Y) match
        case (EmptyTuple, _) => Unit
        case (row *: nextT, Nat._0) => ReplaceRow[row, P, X] *: nextT
        case (row *: nextT, Nat.Succ[nextY]) => 
            ReplaceBoard[nextT, P, nextY, X] match
                case Id[res] => res match
                    case Unit => Unit
                    case Tuple => row *: res

    type Id[X] = X

    type Rw[X] = (X, X, X)

    type HasWon[B <: T3Board, P <: T3Player] <: Bool = B match
        case ((P,P,P), _, _) => Bool.True
        case (_, (P,P,P), _) => Bool.True
        case (_, _, (P,P,P)) => Bool.True
        case ((P,_,_), (P,_,_), (P,_,_)) => Bool.True
        case ((_,P,_), (_,P,_), (_,P,_)) => Bool.True
        case ((_,_,P), (_,_,P), (_,_,P)) => Bool.True
        case ((P,_,_), (_,P,_), (_,_,P)) => Bool.True
        case ((_,_,P), (_,P,_), (P,_,_)) => Bool.True
        case _ => Bool.False


    type HasEmpty[B <: Tuple] <: Bool = B match
        case Unit *: _ => Bool.True
        case (h *: t) *: next => HasEmpty[h *: t] match
            case Bool.True => Bool.True
            case _ => HasEmpty[next]
        case _ *: next => HasEmpty[next]

    type ExecuteMove[B <: T3Board, P <: T3Player, Y <: Nat, X <: Nat] <: PlayResult = 
        ReplaceBoard[B, P, Y, X] match
            case Id[b] => b match
                case T3Board => (HasWon[b, T3Player.X], HasWon[b, T3Player.O]) match
                    case (Bool.True, Bool.True) => T3Result.Invalid
                    case (Bool.True, _) => T3Result.Win[T3Player.X]
                    case (_, Bool.True) => T3Result.Win[T3Player.O]
                    case _ => HasEmpty[b] match
                        case Bool.True => b & T3Board
                        case _ => T3Result.Tie
                case _ => T3Result.Invalid

    sealed trait Move
    sealed trait Mv[P <: T3Player, Y <: Nat, X <: Nat] extends Move

    type >>>[B <: T3Board, M <: Move] = M match
        case Mv[p, y, x] => ExecuteMove[B, p, y, x]

    trait Show[X]:
        def show: String

    object Show:
        // Note -- produces string, not just type class
        def apply[T](using sh: Show[T]): String = sh.show

        given u: Show[Unit] with { def show: String = " "}
        given x: Show[T3Player.X] with { def show: String = "X" }
        given o: Show[T3Player.O] with { def show: String = "O" }
        given win[X <: T3Player](using x: Show[X]): Show[T3Result.Win[X]] with { def show: String = s"${x.show} wins!"}
        given tie: Show[T3Result.Tie] with { def show: String = "Tie!" }
        given inv: Show[T3Result.Invalid] with { def show: String = "Invalid move!"}
        given all[A,B,C,D,E,F,G,H,I](using a:Show[A],b:Show[B],c:Show[C],d:Show[D],e:Show[E],f:Show[F],g:Show[G],h:Show[H],i:Show[I]): Show[((A,B,C),(D,E,F),(G,H,I))] with {
            def show: String = s""" ${a.show} | ${b.show} | ${c.show} \n---+---+---\n ${d.show} | ${e.show} | ${f.show} \n---+---+---\n ${g.show} | ${h.show} | ${i.show} """
        }
   
object Main:
    def main(args: Array[String]): Unit =
        import TicTacToe.*         
        import Nat.*
        import T3Player.*

        type Res = EmptyT3Board 
            >>> Mv[O, _0, _0]
            >>> Mv[X, _1, _1]
            >>> Mv[O, _1, _0]
            >>> Mv[X, _2, _0]
            >>> Mv[O, _2, _1]
            // Uncomment line below to show win
            // >>> Mv[X, _0, _2]

        println(Show[Res])