Idris random shuffle

import Prelude.Vect
import Effect.Random

extractAt : (n : Fin (S k)) -> Vect (S k) a -> (a, Vect k a)
extractAt n xs = (Vect.index n xs, Vect.deleteAt n xs)

extractRandom : Vect (S k) a -> { [RND] } Eff (a, Vect k a)
extractRandom {k} xs = return $ extractAt !(rndFin k) xs

shuffle : Vect n a -> { [RND] } Eff (Vect n a)
shuffle xs = go [] xs where
    go : Vect n a -> Vect m a -> { [RND] } Eff (Vect (n + m) a)
    go {n} res [] = rewrite plusZeroRightNeutral n in return res
    go {n} {m = S m} tmp rest = rewrite sym $ plusSuccRightSucc n m in do
        (e, new) <- extractRandom rest
        go (e :: tmp) new

extractSome : (n : Nat) -> Vect (n + m) a -> { [RND] } Eff (Vect n a)
extractSome n xs = return $ take n !(shuffle xs)