Restrictions needed on ADT for totality
The constraint


  
  covariant type recursion (type constructor should not appear in negative position in a constructor argument)
  


excludes this

data Bad r = Bad (r -&gt; r)
                  ^    ^--- positive position
                  ^-------- negative position


Indeed, all the occurrences of r must appear in positive position.


  Should all type variables also only appear covariantly?


Yes, precisely.

Essentially, your Fix Bad tries to generate a type $T$ isomorphic to $T \to T$. If we had that, we would have a model of the untyped $\lambda$ calculus, where terms are not normalizing ("terminating") in general.

Indeed, to apply any two terms $x, y : T$ we can exploit the isomorphism to treat $x$ as if $x : T\to T$, at which point the application $x y$ becomes feasible. As a special case, we also obtain $xx$, hence $\Omega = (\lambda x.xx)(\lambda x.xx)$ which is the archetypal non normalizing term.

To conclude let me point out that, in some advanced calculi with dependent types, covariant recursion is not enough, and you need an even stricter constraint called "strict positivity". Without that, contradictions arise. In Haskell-like languages, covariance (and the other constraints you mention) should suffice.