Add pkg-config gc flags to llvm Makefile

This makes building work for systems which have gc installed in a
non-standard location.  The invocation was pulled from
https://github.com/schani/clojurec/pull/2, and then modified based on
https://github.com/idris-lang/Idris-dev/pull/428#issuecomment-26302460.
Fix parser for :def REPL command
Remove bad Applicative constraints from neweffects
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
Merge pull request #1363 from bmsherman/parseDef

Fix parser for :def REPL command
Merge pull request #1364 from puffnfresh/neweffects-bad-constraints

Remove bad Applicative constraints from neweffects
Remove some needless 'using' blocks

since the elaborator is now cleverer
No need for 'using' in HVect
Ensure erasure happens under 'force'

Fixes #1367
I'm not yet convinced there isn't still potentially a similar problem
under other forms of ProjCase, but since these only arise in unusual
circumstances at the moment there isn't a problem *yet*!
windows executables should end with .exe
Highlight prover output for ideslave
Update CHANGELOG for unbound implicits
Highlight differing implicits in errors

But only if there are otherwise no visible differences in the error
Merge pull request #1368 from Heather/clean

windows executables should end with .exe
Merge pull request #1369 from david-christiansen/prover-output-color

Highlight prover output for ideslave
Make prover better at IDESlave protocol

Instead of returning strings that comprise results, return actions that
complete them. This makes handling which requests are completed much easier.
Keep type arguments of = when unelaborating

This allows more informative error messages when the mismatch is in the
type arguments to =.
Support multiple let bindings

This sort of thing now works:

  test : Nat -> Nat
  test n = let foo = n
               S k = plus foo foo
              in k

The bindings must be aligned, and the keyword 'in' (indented however you
like within the 'test' block) terminates the list.

Pattern match alternatives are also supported, for quickly catching
failures:

  test2 : Nat -> Nat
  test2 n = let foo = n
                S k = plus foo foo
                    | Z => 42
              in k

Fixes #1362
Remove commented out code