Idris' opt-in totality is a weird beast since those opts are extralinguistic. I really consider it to be a downside when a language is turing complete these day

Idris' opt-in totality is a weird beast since those opts are extralinguistic. I really consider it to be a downside when a language is turing complete these days—I'd rather Idris just use a partiality monad. So, maybe I'm just using the power of wishful thinking with my characterization above.