<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>