<div dir="ltr">Using the `instance` keyword declares the projection function an instance. That's almost never what you want. You can use it to model super classes, but it's much less efficient than using `{{...}}`. Suppose you have<div><br></div><div>instance</div><div>  EqA : Eq Bla</div><div>  EqA = ...</div><div><br></div><div>  OrdA : Ord Bla</div><div>  OrdA = ...</div><div><br></div><div>with a super class `instance` field `Ord.super : Ord A -> Eq A`. Now you have two possible instances for `Eq A`: `EqA` and `Ord.super OrdA`. They are definitionally equal but instance search still needs to go through the trouble of finding and comparing them. This leads to at least quadratic (possibly exponential?) slowdowns in the depth of the super class hierarchy.</div><div><br></div><div>You get the same problem when you open a record with `instance` fields: the original projection and the specialised field are both (definitionally equal) instances.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Aug 1, 2017 at 2:20 PM, Andreas Nuyts <span dir="ltr"><<a href="mailto:andreas.nuyts@cs.kuleuven.be" target="_blank">andreas.nuyts@cs.kuleuven.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
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 `{{...}}`.<br>
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?<br>
<br>
The docs have an example about making a sub-typeclass: <a href="http://agda.readthedocs.io/en/v2.5.2/language/record-types.html#instance-fields" rel="noreferrer" target="_blank">http://agda.readthedocs.io/en/<wbr>v2.5.2/language/record-types.h<wbr>tml#instance-fields</a><br>
but I would expect this to work equally well by using the `instance` keyword instead of `{{...}}`.<br>
<br>
Best,<br>
Andreas<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div>