In total dependently typed languages, general recursion is forbidden, since this can allow for non-terimination. However, dependently typed language can still describe Turing-complete computations (without running them), using free monads (see also here).
However, recursion is not the only source of non-termination in dependently typed languages. Having $Set : Set$ allows for Girard's paradox, inductive data types must be strictly positive, since otherwise we can write an interpreter for the untyped lambda calculus.
I'm wondering, is there an equivalent of the General Recursion monad for describing (but not running) computations involving $Set : Set$ or non-strictly positive data types? Or is there a way that we can express these in terms of a general-recursion monad?