Idris中的不可能模式

Question

我正在學習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有助於伊德里斯檢測，它不能被用於構建HasEmpty Zero類型的值。完整的（工作）代碼在以下要點：

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