Micah (1) [Avatar] Offline

In Section 11.2.2, Executing Infinite Processes, run is defined as follows:

data InfIO : Type where
  Do : IO a -> (a -> Inf InfIO) -> InfIO

run : InfIO -> IO ()
run (Do action cont) = do res <- action
                          run (cont res)

The book says that this function is not total, but when I check it in the repl it says that it is total.

Which is correct?