[Agda] Recursive instance search limited in depth

[Dominique Devriese]

2013/10/2 Dominique Devriese <dominique.devriese at cs.kuleuven.be>:
> Non-linear parametric instances
> could probably be easily abused to decide equality of types, which I
> think we want to avoid.

On second thought, this point might be moot.  If I remember correctly,
there is a discussion of tricks for (semi-)deciding type equality
using type class instances in the HList paper, but I should re-check
what features they require precisely...

Dominique