Better treatment of unbound implicits

Now uses the elaborator to generate any necessary extra bindings, using
the same machinery as pattern match elaboration. The end result is that
you no longer need 'using' in a lot of cases (it is still useful if you
want to give explicit types, of course). e.g. this now works as it
stands:

  data Elem : a -> Vect n a -> Type where
       Here : Elem x (x :: xs)
       There : Elem x xs -> Elem x (y :: xs)

  isElem : DecEq a => (x : a) -> (xs : _) -> Maybe (Elem x xs)

This should also reduce the number of weird "no such variable" errors
signfificantly. In particular, it fixes #1354
Type class resolution fix

Check whether any errors introduced by a match are unrecoverable, rather
than merely checking if any more errors are introduced. Otherwise, in
some circumstances (where other problems are resolved by the match) we
might get a type class resolved where it shouldn't be, leading to
mysterious errors later.

Fixes #1365