Agda-style record syntax

This patch adds a nice Agda-style way of defining records. This is a (contrived) example:
```Idris
||| A vector wrapper.
||| @ a An implicit param.
||| @ n An explicit param.
record C : {a : Type} -> (n : Nat) -> Type where
  constructor MkC

  ||| A rather unhelpful implicit because it can't be inferred.
  {unhelpfulField : a}

  ||| The wrapped vector.
  xs : Vect n a
```
Behind the scenes, the above generates the following type:
```Idris
MkC : (n : Nat) -> Vect n a -> C n
```
Shortcomings:
* no docstrings for fields and parameters
  * currently, the record pipeline seems to just ignore this info (old-style records suffer from this as well)
  * should be relatively straightforward to fix
* no tactic implicit fields, just plain implicits
* the `constructor` clause is mandatory because it syntactically disambiguates old-style records from Agda-style records. Maybe we should find a better way to do this and allow automatic `MkT` constructor naming.
* free variables in fields won't get turned into unbound implicits