Description
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)? IfgetInstancesis 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
Yso that its variables are rigid, instantiate the typeXso that we have flexible metavariables, and check forleqType), 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
Termsthemselves. But I'm too tired to think about that right now.