Add :refine (:ref) command for refining a hole

Like :ps, but instead of a recursive search, it simply applies the
function given and fills in other arguments *by unification only*.

(In particular, this means it will fail if any implicit arguments need
other arguments, rather than the return type, in order to be solved by
unification).

So, this will work:

append : (n, m : Nat) -> Vect n a -> Vect m a -> Vect (n + m) a
append Z m [] ys = ys
append (S k) m (x :: xs) ys = x :: ?append_rhs1

*testref> :ref 6 append_rhs1 append
append k m ?append_rhs2 ?append_rhs3

But this will not:

vZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
vZipWith f [] [] = []
vZipWith f (x :: xs) (y :: ys) = f x y :: ?vZipWith_rhs1

*Vect> :ref 18 vZipWith_rhs1 vZipWith
?vZipWith_rhs1

...because unification alone is not enough to work out the implicit
arguments a and b (even if there is only one thing that will work, it
needs a deeper proof search to find it).