Agreeing with you: I'm only familiar with Idris insofar as I've watched talks on it, but my recollection is that its implementation inference is a search across

Agreeing with you: I'm only familiar with Idris insofar as I've watched talks on it, but my recollection is that its implementation inference is a search across pre-listed implementations. Edwin Brady says that that's surprisingly useful. I believe him and look forward to trying it out some time soon, but it is not as magical as we might guess.