You still can't avoid runtime errors because of non-terminating functions. Determining whether an arbitrary function in a Turing complete language is total or n

You still can't avoid runtime errors because of non-terminating functions. Determining whether an arbitrary function in a Turing complete language is total or not is undecidable. I don't see any mention of a totality checker (which would make the language not Turing complete) either. Idris also has this.