On the Unofficial FAQ on the official Idris wiki (official in that it is on the language's git repo), it is stated that
in a total language [e.g. Idris] we don't have undefined and non-terminating terms so we need not worry about evaluating them.
However, the following definition for ones (using List instead of Stream) certainly seems non-terminating:
ones: List Int
ones = 1 :: ones
-- ...
printLn(head ones) -- seg fault!
So, I'm not sure if the wiki entry is mistaken, or if I misunderstand the context. Note the Stream workaround is already described in the Idris tutorial.
Idris is only total if you ask it to be total. You may write one of %default total, %default covering, or %default partial (the default), and all declarations afterwards will take on the given totality annotation:
%default total
-- implicitly total
ones1 : List Int
ones1 = 1 :: ones1
-- ERROR: ones1 is not total
-- total
ZNeverHeardOfIt : Nat -> Nat
ZNeverHeardOfIt (S n) = n
-- ERROR: missing cases in ZNeverHeardOfIt
covering
natRoulette : Nat -> Nat
natRoulette Z = Z
natRoulette (S n) = natRoulette (S (S n))
-- covering means all possible inputs are covered by an equation
-- but the function isn't checked for termination
-- natRoulette has cases for all inputs, but it might go into an infinite loop
-- it's morally equivalent to just partial, as a function that loops forever
-- on an input isn’t very different from one missing the case
-- it just gets the compiler to complain more
partial
ones : List Int
ones = 1 :: ones
-- no checks at all
-- Idris, being strict, needs to evaluate ones strictly before it can evaluate ones.
-- Oh wait, that's impossible. Idris promptly vanishes in a segfault.