<div dir="ltr">It&#39;s very nice! Also much faster than the previous implementation, I have examples that uses a lot of instance arguments that run 5x faster now, not to mention that you can leave out all the silly specialisations like Eq (List Nat).<div>

<br></div><div>I had to do a bit of work to get constructor classes (like Monad and Functor) to work:</div><div><br></div><div>I lifted the restriction on recursive instances when there are metas in the goal. The reason for this is that you get instance constraints like Monad _M, with a side constraint _M Nat == IO Nat. To avoid the looping behaviour you described in the release notes I prevent instance search from instantiating insufficiently constrained metas, but allow it to instantiate _M in the example above.</div>

<div><br></div><div>Unless someone has found any big issues, I want to merge this into master.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jul 11, 2014 at 7:32 PM, Ulf Norell <span dir="ltr">&lt;<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Awesome work. For now, I put it in a branch &#39;classes&#39; in the main repo and granted you commit rights. I will try it out on UlfNorell/agda-prelude, which uses a lot of instance arguments.<span class="HOEnZb"><font color="#888888"><br>

<div><br>
</div><div>/ Ulf</div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jul 11, 2014 at 12:26 PM, Guillaume Brunerie <span dir="ltr">&lt;<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>&gt;</span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello all,<br>
<br>
As some of you know, I started working on recursive instance search<br>
during the previous AIM and the code is now available on my GitHub<br>
here : <a href="https://github.com/guillaumebrunerie/agda" target="_blank">https://github.com/guillaumebrunerie/agda</a> (should I open a pull<br>
request against the official Agda?)<br>
<br>
The main outstanding issue is that there is no termination check yet<br>
so if you’re not careful when defining your instances you can easily<br>
make Agda loop.<br>
Also, I haven’t really thought about namespace management, for<br>
instance &#39;hiding&#39; does not hide instances (but serialization should<br>
work, though).<br>
<br>
I copy-pasted the relevant part of the CHANGELOG below (I borrowed<br>
part of the text in issue 938) and you can also look at the two files<br>
test/succeed/RecursiveInstanceSearch{,Level}.agda to see some more<br>
advanced examples of recursive instance search.<br>
<br>
Of course I welcome any feedback/bug reports.<br>
<br>
Cheers,<br>
Guillaume<br>
<br>
<br>
<br>
<br>
* Instance search is now more efficient and recursive (see issue 938)<br>
  (but without termination check yet)<br>
<br>
  A new keyword `instance&#39; has been introduced (in the style of<br>
  `abstract&#39; and  `private&#39;) which must now be used for every<br>
  definition/postulate that has to be taken into account during instance<br>
  resolution. For example:<br>
<br>
    {-# OPTIONS --copatterns #-}<br>
<br>
    record RawMonoid (A : Set) : Set where<br>
      field<br>
        nil  : A<br>
        _++_ : A -&gt; A -&gt; A<br>
    open RawMonoid<br>
<br>
    instance<br>
      rawMonoidList : {A : Set} -&gt; RawMonoid (List A)<br>
      rawMonoidList = record { nil = []; _++_ = List._++_ }<br>
<br>
      -- using copatterns to define this recursive instance:<br>
<br>
      rawMonoidMaybe : {A : Set} {{m : RawMonoid A}} -&gt; RawMonoid (Maybe A)<br>
      nil rawMonoidMaybe = nothing<br>
      _++_ rawMonoidMaybe nothing mb = mb<br>
      _++_ rawMonoidMaybe ma nothing = ma<br>
      _++_ (rawMonoidMaybe {{m}}) (just a) (just b) = just (_++_ m a b)<br>
<br>
  Moreover, each type of an instance must end in (something that reduces<br>
  to) a named type (e.g. a record, a datatype or a postulate). This<br>
  allows us to build a simple index structure<br>
<br>
    data/record name  --&gt;  possible instances<br>
<br>
  that speeds up instance search.<br>
<br>
  Instance search takes into account all local bindings and all global<br>
  &#39;instance&#39; bindings and the search is recursive. For instance,<br>
  searching for<br>
<br>
    ? : RawMonoid (Maybe (List A))<br>
<br>
  will consider the candidates {rawMonoidList, rawMonoidMaybe}, fail to<br>
  unify the first one, succeeding with the second one<br>
<br>
    ? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))<br>
<br>
  and continue with goal<br>
<br>
    ?m : RawMonoid (List A)<br>
<br>
  This will then find<br>
<br>
    ?m = rawMonoidList {A = A}<br>
<br>
  and putting together we have the solution.<br>
<br>
  Be careful that there is no termination check for now, you can easily<br>
  make Agda loop by declaring the identity function as an instance. But<br>
  it shouldn’t be possible to make Agda loop by only declaring<br>
  structurally recursive instances (whatever that means).<br>
<br>
  Additionally:<br>
<br>
  * Uniqueness of instances is up to definitional equality (see issue 899)<br>
<br>
  * Instance search will not be attempted if there are unsolved metas in<br>
    the goal. The issue is that trying to typecheck [? ++ ?] would<br>
    generate a constraint of type `RawMonoid ?&#39; to be solved by instance<br>
    search, but unification with `rawMonoidMaybe&#39; will succeed and<br>
    generate a new constraint of type `RawMonoid ?2&#39; to be solved by<br>
    instance search, and so on, so Agda would loop.<br>
<br>
    As a special case, if none of the instances declared for that type<br>
    is recursive, then instance search is attempted as usual even if<br>
    there are unsolved metas (no risk of looping here).<br>
<br>
  * Instances of the following form are allowed:<br>
<br>
        Π-level : {n : ℕ} {A : Set} {B : A → Set}<br>
                  {{_ : (a : A) → has-level n (B a)}}<br>
                  → has-level n ((a : A) → B a)<br>
<br>
      When searching recursively for an instance of type `(a : A) →<br>
      has-level n (B a)&#39;, a lambda will automatically be introduced and<br>
      instance search will search for something of type `has-level n (B<br>
      a)&#39; in the context extended by `a : A&#39;.<br>
<br>
  * There is no longer any attempt to solve irrelevant metas by instance<br>
    search<br>
<br>
  * Constructors of records and datatypes are automatically added to the<br>
    instance table<br>
_______________________________________________<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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>