UndecidableInstances is used in more libraries than you would think. In general, it doesn't inpact safety although certain programs may fail to compile because

UndecidableInstances is used in more libraries than you would think. In general, it doesn't inpact safety although certain programs may fail to compile because the compiler gives up after a while. However, this won't result in the acceptance of ill typed programs. Ultimately, the compiler is just acting like any other language run time -- at some point, your Python interpreter will give up (run time type error), your browser will give up (that annoying stop script pop up), and your operating system will give up (out of memory exception). Also, your link indicates idris's type system is Turing complete.