Total means that the function must always return a value. In the presence of coinductive types and corecursive functions, a total function can run forever but must always be producing values when asked. e.g. an infinite stream of prime numbers can be produced by a corecursive, total function. You can use this to embed Turing complete computations in languages like Agda or Coq[1], they just must be declared as such up front. Much like IO must be declared up front in (idiomatic) Haskell. And much like you can unsafePerformIO in Haskell, Idris and Agda have their own escape hatches as the sibling comment mentions.

[1] https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_T...