Type-level ordering verification

IsSorted.scala

import shapeless._
import shapeless.ops.nat.LTEq.<=
import Nat._

sealed trait ToValue[T, V] { def value: V }
def toValue[T, V](implicit tv: ToValue[T, V]): V = tv.value

object Bool {
  sealed trait Bool

  sealed trait True extends Bool
  sealed trait False extends Bool

  implicit def trueValue = new ToValue[True, Boolean] { def value = true }
  implicit def falseValue = new ToValue[False, Boolean] { def value = false }
}

object GT {
  trait GT[A <: Nat, B <: Nat]
  type >[A <: Nat, B <: Nat] = GT[A, B]

  implicit def gt1[B <: Nat] = new >[Succ[B], _0] {}
  implicit def gt2[A <: Nat, B <: Nat](implicit gt : A > B) = new >[Succ[A], Succ[B]] {}
}

object IsSorted {
  import Bool._
  import GT._

  sealed trait IsSorted[XS <: HList] { type Out <: Bool }

  implicit def hnilIsSorted = new IsSorted[HNil] { type Out = True }
  
  implicit def hcons1IsSorted[X <: Nat] = new IsSorted[X :: HNil] { type Out = True }

  implicit def hconsIsSorted[X0 <: Nat, X1 <: Nat, XS <: HList](
    implicit ev1: X0 <= X1, ev2: IsSorted[X1 :: XS]) =
      new IsSorted[X0 :: X1 :: XS] { type Out = ev2.Out }


  implicit def hconsIsNotSorted[X0 <: Nat, X1 <: Nat, XS <: HList](
    implicit ev1: X0 > X1) =
      new IsSorted[X0 :: X1 :: XS] { type Out = False }
}

import IsSorted._

type Input1 = _0 :: _4 :: _3 :: _1 :: _2 :: HNil
type Input2 = _0 :: _1 :: _2 :: _3 :: _4 :: HNil

toValue[IsSorted[Input1]#Out, Boolean] // false
toValue[IsSorted[Input2]#Out, Boolean] // true