idris-lang/Idris-dev — pull request #1676 by edwinb (2014-10-25 22:25:20+00:00)
Title: Proper error for missing eliminator

...just a Msg, but it's better than an INTERNAL ERROR