idris-lang/Idris-dev — pull request #1764 by ziman (2014-12-05 01:45:59+00:00)
Title: 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