Type level quicksort

tlsort.idr

  qsort : Ord a => List a -> List a
  qsort [] = []
  qsort (x :: xs) = let (l, r) = partition (< x) xs in
                        assert_total (qsort l ++ x :: qsort r) -- assert totality otherwise it won't reduce in the type
  
  data Singleton : a -> Type where
       MkSingleton : Singleton x
  
  t_qsort : Ord a => (xs : List a) -> Singleton (qsort xs)
  t_qsort xs = MkSingleton
  
  {-
  *tlsort> t_qsort [1,6,9,2,4,7,3,5,8]
  MkSingleton : Singleton [1, 2, 3, 4, 5, 6, 7, 8, 9]
  -}