找出
导致未解决元的原因的最佳方法是什么？有没有办法通过扩展所有可解决的通配符将所有未解决的元（并且只有未解决的元）变成洞？
如果不出意外，将未解决的元更改为一个洞会使有关未解决的元的消息消失吗？因为那时我想我可以尝试将每个通配符和每个隐式参数更改为漏洞，直到消息消失，然后找出导致问题的哪一个......
一种方法（不一定是最好的）是替换所有隐式的带有显式下划线的参数：
f {_} {_} {_} (x {_} {_} {_})
这个答案来自Agda邮件列表：https://lists.chalmers.se/pipermail/agda/2012/004123.html