Dependent vectors in Idris

data Vec : (n : Nat) -> (t : Type) -> Type where
    Nil : Vec Z t
    (::) : t -> Vec n t -> Vec (S n) t

infixr 6 .++
(.++) : Vec n t -> Vec m t -> Vec (n + m) t
[] .++ b = b
(.++) {n = S n} {m = m} (x :: xs) y = rewrite plusSuccRightSucc n m in xs .++ (x :: y)

infixl 7 .*
(.*) : Num t => Vec n t -> Vec n t -> t
(.*) [] [] = 0
(.*) (x :: xs) (y :: ys) = (x * y) + (xs .* ys)

natVec : (n : Nat) -> Vec n Int
natVec Z = Nil
natVec (S n) = (cast n) :: natVec n

main : IO ()
main = do
    n <- fromIntegerNat . cast `map` getLine
    m <- fromIntegerNat . cast `map` getLine

    let a = natVec n
    let b = natVec m

    print $ a .* a

    --print $ a .* b
    --Error: cannot unify n with m

    --print $ (a .++ b) .* (b .++ a)
    --Error: cannot unify (n + m) with (m + n)

    print $ (a .++ b) .* (rewrite plusCommutative n m in b .++ a)

    case n `decEq` m of
        Yes eq => print $ a .* (rewrite eq in b)
        _      => return ()