idris - idris 不可能的模式

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

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

以下要点提供了完整的代码段：

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

任何帮助表示赞赏。

最佳答案

我已经在freenode Idris社区与人们交谈，他们向我解释说
荒谬的模式需要一个明确的不可能的情况才能检测到那实际上是不可能的。举个例子：

hasEmptyZero : HasEmpty Zero -> Void
hasEmptyZero HasEps impossible

在此放置构造函数HasEps有助于Idris检测到它不能用于构造类型HasEmpty Zero的值。完整的（有效的）代码如下：

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