[Agda] Instance fields

[Andreas Nuyts]

Hi,

In a record type declaration, there are two ways in which we can make a 
field 'instance': either by using the `instance` keyword, or by wrapping 
the name in `{{...}}`.
I know that the latter makes the field an instance argument of the 
constructor, and the former does not. But are they otherwise different, 
and if so, how?

The docs have an example about making a sub-typeclass: 
http://agda.readthedocs.io/en/v2.5.2/language/record-types.html#instance-fields
but I would expect this to work equally well by using the `instance` 
keyword instead of `{{...}}`.

Best,
Andreas