Order instances by specificity for reflection

[plt-amy]

When using getInstances to implement evil, incoherent metaprograms using instance search as hints, it would be quite handy to support specialisations out of the box. This wouldn't change the behaviour of actually solving instance metas, but it would make it easier to use getInstances to implement e.g. hint databases, which I think is a pretty common use-case.

As a concrete example, I implemented an extensionality tactic for the 1Lab, which uses getInstances to filter a space of hints, then picks the first result (or a default if there are none). We have instances like

_ : Extensionality (A → B)
_ : Extensionality (A × B)

which are quite generic, and so can really be returned in any order. But it's possible to write more specific instances like Extensionality (A / R → B), which would reduce to equality at the inclusions of elements of A (rather than extensionality over the whole quotient). However, since instance candidates are returned by name order, we can't rely on the quotient instance being picked over the generic function instance.

It would be possible to implement this sorting in user-space, e.g. by implementing a comparison function for Terms or attaching numeric weights to the instances; but both of these solutions would be slower than implementing this on the Agda side, especially if accurate term comparisons are desired (since then you'd be constantly round-tripping between quoting and unquoting to check whether types are substitution instances).

The concrete proposal is to change getInstanceCandidates so that the list is sorted by "strict specificity": Y is strictly more specific than X if Y is a substitution instance of X, but X is not a substitution instance of Y. Doing this sorting on the entry point for reflection means that it doesn't affect the solving of ordinary instance metas. I guess the main questions are:

• What do others think (e.g. @jespercockx who originally implemented getInstances)? If getInstances is our answer to "hint databases" then I think returning instance candidates in specificity order is a clear win, since it's a very lightweight way of specifiying that one hint should take priority over another: just give it a more constrained type.

• Is it actually possible to implement the strict specificity order efficiently? I think it's possible to do this with the conversion checker (go under implicit pis in the type Y so that its variables are rigid, instantiate the type X so that we have flexible metavariables, and check for leqType), but it might be necessary to use the LHS unifier.

  It might also be possible to implement the specificity ordering without actually computing a unifier, by doing a clever comparison on the Terms themselves. But I'm too tired to think about that right now.

[jespercockx]

I agree that this would be a good idea. I don't think there is an efficient way to implement the specificity order with the way instance search is implemented now, but that's just because the way instance search is implemented now is pretty simplistic. A better way to implement it would be to have a kind of case tree for finding instances belonging to a type, and then the instances that are more deeply nested in this tree are more specific. Also note that (at least for top-level instances), the specificity order depends only on the instances and not on the context where instance search is called, so if it proves to be very inefficient then we could cache it.