[Agda] Recursive instance search limited in depth

[Guillaume Brunerie]

Hello,

In Dominique Devriese and Frank Piessens’s paper "On the Bright Side
of Type Classes:
Instance Arguments in Agda" they say (section 4.1) that having
recursive instance search is not desirable in Agda, because it would
be powerful and Agda should not be too powerful :-) (or at least this
is what I understood).
Is that the case or is it just that recursive instance search is more
complicated to implement?

In any case, there is another option which seems quite easy to
implement, not too powerful but probably still very useful: limit
instance search to a given depth.
There could be a flag similar to --termination-depth (maybe
--instance-search-depth) where the user specifies a number n, and then
Agda would limit instance search depth to n.

What do you think?
Is there something I’m missing or would it be accepted in Agda?

Thanks,

Guillaume