A tactic language doesn't need to be total, since it's only run at compile-time, so no errors can leak into the resulting proof/program. The worst that can happen is the compiler hangs.
Coq comes with "ltac", which is a horrible imperative language that leads to very fragile proofs. On the other hand, mtac is just Coq's normal, total FP language ("gallina"). A monad is used to wrap up general recursion, so that gallina can be used un-changed.
During compilation, these monadic values are forced, which either leads to a value or causes the compiler to hang. This is a really nice compromise, since you can write Haskell-style FP code which "obviously terminates", without having to prove that it terminates, you still have access to all of the nice dependent type machinery, and the end result (the program, not the meta-program) is guaranteed to be total (unlike, say, an Idris function which turns off the totality checker).
What are you referring to? Data/codata checking works with local type inference.
Huh?
inf = Cons 1 inf> Each recursive function call must be on a syntactic subcomponent of its formal parameter.
But it doesn't. But you can't actually use that to get a nonterminating program, because you can't recurse over it:
> Ordinary recursion is not legal over codata, because it might not terminate.