<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <div class="moz-text-html" lang="x-unicode"> Thanks. A little
      experiment shows that `bar2` works regardless of whether its
      argument is explicit, implicit or instance.<br>
      <br>
      So I conclude that declaring a field `{{foo}}` of a record type R
      does two things:<br>
      * It makes the corresponding argument to the constructor,
      implicit;<br>
      * Whenever an argument of type R is in the context, its `foo`
      field becomes available for instance search upon eta-expansion.<br>
      <br>
      Andreas<br>
      <br>
      <div class="moz-cite-prefix">On 02-08-17 01:50, <a
          class="moz-txt-link-abbreviated"
          href="mailto:agda-request@lists.chalmers.se">agda-request@lists.chalmers.se</a>
        wrote:<br>
      </div>
      <blockquote type="cite"
        cite="mid:mailman.43269.1501631446.12045.agda@lists.chalmers.se">
        <pre wrap="">Date: Tue, 1 Aug 2017 11:18:11 -0700
From: Martin Stone Davis <a class="moz-txt-link-rfc2396E" href="mailto:martin.stone.davis@gmail.com"><martin.stone.davis@gmail.com></a>
To: <a class="moz-txt-link-abbreviated" href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>
Subject: Re: [Agda] Instance fields
Message-ID: <a class="moz-txt-link-rfc2396E" href="mailto:5fb4917c-30a0-4e44-1dda-32984d88b633@gmail.com"><5fb4917c-30a0-4e44-1dda-32984d88b633@gmail.com></a>
Content-Type: text/plain; charset=utf-8; format=flowed

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</pre>
      </blockquote>
      <br>
    </div>
  </body>
</html>