Dependent types

So, why are you not using dependent types yet? Do you like your programs randomly crashing?

>>23

instead of crashing, in Idris you have, print "Attempt to divide by zero!"

You have to use choose only on user input. For non-user input you might not need to do that (so you will not need to have any print "Attempt to divide by zero!").

which is literally no different than catching the exception and doing that

Except that you might forget to catch said exception. "b-buuut the compiler will warn me!" - what if you pass a provably non-zero divisor? You will have to still catch the exception, which is retarded.
Also, try to think of it from another way: what if you are dividing by a value that you think that will never be 0 but in reality it might be 0? You will simply not get any compile time warning that you fucked up in languages with non-dependent types.