sealed trait Nat { type N <: Nat }
sealed trait S[P <: Nat] extends Nat { type N = S[P] }
sealed trait Z extends Nat { type N = Z }

sealed trait Pred[A <: Nat] { type Out <: Nat }
object Pred {
    def apply[A <: Nat](implicit pred: Pred[A]): Aux[A, pred.Out] = pred
    type Aux[A <: Nat, B <: Nat] = Pred[A] { type Out = B }
    implicit def pred[B <: Nat]: Aux[S[B], B] = new Pred[S[B]] { type Out = B }
}

sealed trait LT[A <: Nat, B <: Nat]
object LT {
    def apply[A <: Nat, B <: Nat](implicit lt: LT[A, B]): LT[A, B] = lt

    implicit def lt1[B <: Nat] = new LT[Z, S[B]] { }
    implicit def lt2[A <: Nat, B <: Nat](implicit lt: LT[A, B]) =
        new LT[S[A], S[B]] { }
}

sealed trait LTEQ[A <: Nat, B <: Nat]
object LTEQ {
    def apply[A <: Nat, B <: Nat](implicit lteq: LTEQ[A, B]): LTEQ[A, B] = lteq

    implicit def lteq1 = new LTEQ[Z, Z] { }
    implicit def lteq2[B <: Nat] = new LTEQ[Z, S[B]] { }
    implicit def lteq3[A <: Nat, B <: Nat](implicit lteq: LTEQ[A, B]) =
        new LTEQ[S[A], S[B]] { }
}

sealed trait Max[A <: Nat, B <: Nat] { type Out <: Nat }
object Max {
    def apply[A <: Nat, B <: Nat](implicit max: Max[A, B]): Aux[A, B, max.Out] = max

    type Aux[A <: Nat, B <: Nat, C <: Nat] = Max[A, B] { type Out = C }

    implicit def maxAux0[A <: Nat, B <: Nat]
        (implicit lteq: LTEQ[A, B]): Aux[A, B, B] = new Max[A, B] { type Out = B }
    implicit def maxAux1[A <: Nat, B <: Nat]
        (implicit lt: LT[B, A]): Aux[A, B, A] = new Max[A, B] { type Out = A }
}

object NonRecursiveTrees {
    sealed trait Tree[+A]
    case class Leaf[+A](value: A) extends Tree[A]
    case class Node[+A](left: Tree[A], right: Tree[A]) extends Tree[A]
    type WithDepth[+A, B <: Nat] = A { type Depth = B }

    def leaf[A](value: A): WithDepth[Leaf[A], Z] =
        new Leaf(value) { type Depth = Z }
    def node[A, L <: Nat, R <: Nat]
        (left: WithDepth[Tree[A], L], right: WithDepth[Tree[A], R])
        (implicit max: Max[L, R]): WithDepth[Node[A], S[max.Out]] =
        new Node(left, right) { type Depth = S[max.Out] }

    implicit class TreeOps[A, DL <: Nat](val lhs: WithDepth[Tree[A], DL]) {
        def ~[B <: A, DR <: Nat](rhs: WithDepth[Tree[B], DR])
            (implicit max: Max[DL, DR]) = node[A, DL, DR](lhs, rhs)
        def ~[B <: A](rhs: B): WithDepth[Tree[A], S[DL]] =
            new Node(lhs, new Leaf(rhs)) { type Depth = S[DL] }
    }
    implicit class LeafOps[A](val lhs: A) {
        def ~[B <: A, D <: Nat]
            (rhs: WithDepth[Tree[B], D]): WithDepth[Tree[A], S[D]] =
            new Node(new Leaf(lhs), rhs) { type Depth = S[D] }
        def ~[B <: A](rhs: B): WithDepth[Tree[A], S[Z]] =
            new Node(new Leaf(lhs), new Leaf(rhs)) { type Depth = S[Z] }
    }
}