[Agda] Instance fields

[Martin Stone Davis]

record R : Set where
   field instance fooI : Foo
   field {{fooF}} : Foo

For code outside of R, both R.fooI and R.fooF are of type R -> Foo, but 
only R.fooI is subject to instance search. When you're writing code 
inside the record R, fooF is also subject to instance search because 
there it's an instance argument. I should mention that, in practice, 
there are some caveats having to do with eta-expansion, as the code 
below demonstrates.


it : ∀ {a} {A : Set a} {{x : A}} → A
it {{x}} = x

record Foo : Set where
   no-eta-equality

record RNEEI : Set where
   no-eta-equality
   field instance fooI : Foo -- if "instance" is removed, then bar1 
fails (because there are no instances)
   field {{fooR}} : Foo

record REEI : Set where
   field fooI : Foo -- if "instance" is added, then bar2 fails (because 
there are too many instances)
   field {{fooR}} : Foo

bar1 : {{_ : RNEEI}} → Foo
bar1 = it -- works because RNEEI.fooI is subject to instance search

bar2 : {{_ : REEI}} → Foo
bar2 = it -- works because REEI.fooR is an instance argument made 
available by eta-expansion


On 08/01/2017 05:20 AM, Andreas Nuyts wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda