有没有比 :set showimplicits 更有用的信息来追踪统一错误？我目前正在得到这个并且不知道从这里去哪里：
问问题
25 次
1 回答
2
不幸的是，简短的回答是“不，不是真的”。但是，我不喜欢看到糟糕的错误消息，所以如果您可以提供更多详细信息，也许我们可以研究和改进。
更长的答案是 Idris 在这里报告错误的方式存在问题，我希望发生的事情与此类似：https ://github.com/idris-lang/Idris-dev/issues/2126
我注意到您只显示了统一错误的第二个“特定”部分。真正的问题很可能出在第一部分。由于统一失败可能是暂时的，并且可能会在详细说明者获得更多信息时得到解决，因此当出现额外信息时（通常来自术语的其他部分），错误消息会得到更新。这里发生的情况是，第一次尝试失败的部分现在可以了，但其他部分仍然损坏。
现在，我建议忽略“特别”位并查看第一部分（我想这可能很大）。否则，如果您的程序的相关部分很容易解释，那么邮件列表中的某个人可能会提供帮助。
不过，我最终会解决相关问题...
于 2015-05-20T23:52:05.500 回答