Reverse an Idris Vect

Reverse.idr

module Main 

rev : Vect n a -> Vect n a
rev Nil = Nil
rev (x :: xs) = (rev xs) ++ (x :: Nil)

main : IO ()
main = putStrLn $ show $ rev [1,2,3]

fails to compile with

hello.idr:5:5:When elaborating right hand side of rev:
Can't unify
        Vect (n + 1) a
with
        Vect (S n) a

Specifically:
        Can't unify
                plus n 1
        with
                S n