A length-safe insertion sort.

isort.idr

insert : Ord a => a -> Vect n a -> Vect (1 + n) a
insert x [] = [x]
insert x (y::ys) with (x <= y)
  | True = x::y::ys
  | False = y::insert x ys 

isort : Ord a => Vect n a -> Vect n a
isort [] = []
isort (x::xs) = insert x (isort xs)

This isn't tail-recursive, so careful on memory usage!