Impossible models in Idris

Question

I am studying Idris and I am stuck in a very simple lemma that shows that a particular index is not possible for a data type. I tried to use impossible templates, but Idris refuses them with the following error message:

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

The full code snippet is available as follows:

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

Any help is appreciated.

Answer 1

I am talking to people in the freenode Idris community, and they explained to me that the absurd picture needs an explicit impossible case to discover that it is really impossible. As an example:

hasEmptyZero : HasEmpty Zero -> Void
hasEmptyZero HasEps impossible

HasEps Idris , HasEmpty Zero. () :

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