How to rewrite a function body in Idris so that the type corresponds to the function signature and the whole thing compiles

I would like for this to compile:

foo: Vect n String -> Vect n String
foo {n} xs = take n xs

This fails to compile because the compiler cannot unify n with n + m. I understand that this is because of the signature of take for Vect's but I cannot figure out how to go about showing the compiler that they can be unified if m = 0.

Solution

Just to add to the previous answer, one other possibility is to do the rewrite inline using the existing plusZeroRightNeutral lemma from the library:

foo: Vect n String -> Vect n String
foo {n} xs = let xs' : Vect (n + 0) String
                     = rewrite (plusZeroRightNeutral n) in xs in
                 take n xs'

The difficulty Idris is having in unification is because it is unwilling to infer the m in the application of take:

take : (n : Nat) -> Vect (n + m) a -> Vect n a

You've given it a Vect n String where it wanted a Vect (n + m) a - it has happily unified the a with the String, because Vect is a type constructor, but is unwilling to unify n with n + m because, in general, it can't invert functions. You and I can tell that m has to be zero, but Idris is not so clever.