Finding out which metas are unsolved in an Agda program

Question

What's the best way to find out what's causing unsolved metas? Is there a way to turn all unsolved metas (and only the unsolved ones) into holes, by expanding all the surrounding wildcards that are solvable?

If nothing else, does changing an unsolved meta into a hole make the message about the unsolved meta go away? Because then I guess I can try to change every wildcard and every implicit argument into holes until the message goes away and then figure out which one is causing the problems...

Answer 1

One approach (not necessarily the best) is to replace all implicit arguments with explicit underscores:

f {_} {_} {_} (x {_} {_} {_})

This answer is from the Agda mailing list: https://lists.chalmers.se/pipermail/agda/2012/004123.html