Невозможные шаблоны в Идрисе

Question

Я изучаю Идриса, и я застрял на очень простой лемме, которая показывает, что для типа данных не существует определенного индекса. Я пытался использовать невозможные картины, но Идрис отказывается их со следующим сообщением об ошибке:

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

Полный кусок кода доступен в следующей сути:

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

Любой помощь приветствуется.

Answer 1

Я разговаривал с людьми в сообществе freenode Идрис, и они объяснили мне, что для абсурдного шаблона нужен явный невозможный случай, чтобы обнаружить, что это действительно невозможно. В качестве примера:

hasEmptyZero : HasEmpty Zero -> Void 
hasEmptyZero HasEps impossible 

Здесь положить конструктор HasEps помогает Идрис обнаружить, что он не может быть использован для построения значения типа HasEmpty Zero. Полный (рабочий) код приведен в следующем виде:

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