Half baked idea: Inference command?

gistfile1.txt

foo : (xs : Vect n a) -> (ys : Vect m a) -> ?noIdea
foo xs ys = xs ++ ys

Currently this gives:

Can't unify
        Vect (n + m) a
with
        ?noIdea

Instead: how about the elaborator noting this is an incomplete type, and making the unification errors visible to the \o command, meaning that solving the metavaraiable would give:

foo : (xs : Vect n a) -> (ys : Vect m a) -> Vect (n + m) a 
foo xs ys = xs ++ ys