伊德里斯中不可能的模式

Question

我正在学习 Idris 并且我陷入了一个非常简单的引理，该引理表明某些特定索引对于数据类型是不可能的。我尝试使用不可能的模式，但 Idris 拒绝使用以下错误消息：

RegExp.idr line 32 col 13:
hasEmptyZero prf is a valid case

完整的代码片段可在以下要点中找到：

https://gist.github.com/rodrigogribeiro/f27f1f035e5a98f506ee

任何帮助表示赞赏。

Answer 1

我曾与 freenode Idris 社区的人交谈过，他们向我解释说，荒谬的模式需要一个明确的不可能案例才能检测到它真的不可能。举个例子：

hasEmptyZero : HasEmpty Zero -> Void
hasEmptyZero HasEps impossible

在这里放置构造函数HasEps有助于 Idris 检测到它不能用于构造 type 的值HasEmpty Zero。完整（工作）代码的要点如下：

https://gist.github.com/rodrigogribeiro/5b39048df1d9ddc083ec