Why are recursive types seldomly seen in dependent type theory?
The point of inductive types is precisely that you get normalization. Unrestricted recursive types simply lead to non-normalizing terms.
Given any type $A$, we may inhabit $A$ with a non-normalizing term as follows. Consider the recursive type
$$D = D \to A.$$
The term $\omega \mathrel{{:}{=}} \lambda d : D . d \; d$ has type $D \to A$ and it also has type $D$, since they are equal. Therefore $\omega \; \omega$ has type $A$, and in addition $\omega \; \omega$ reduces to itself, giving a non-normalizing term.
If instead of $D = D \to A$ we have just $D \cong D \to A$ then an easy adaptation of the above argument leads to the same conclusion. You just have to coerce $d$ to have type $D \to A$.
Is this bad? If you're using type theory to write programs then it probably isn't that bad. It's actually kind of cool. But if you're using type theory to do reasoning, i.e., you want ot use types as propositions, then it's bad because every type has an inhabitant and so every propostion has a proof. It just depends on what you want from type theory.
What are the rules for recursive types?
$\newcommand{\Type}{\mathsf{Type}}$
Let us try to formulate the rules for recursive types. A reasonable attempt goes along the same lines as what you've suggested:
$$\frac{\Gamma, X : \Type \vdash F(X) : \Type}{\Gamma\vdash \mu X . F(X) : \Type}$$
$$\frac{\Gamma \vdash e : F(\mu X . F(X))}{\Gamma \vdash S(e) : \mu X . F(X)}$$
$$\frac{\Gamma, y : \mu X . F(X) \vdash C(y) : \Type \qquad
\Gamma, x : F(\mu X . F(X)) \vdash f(x) : C(S(x)) \quad
\Gamma \vdash u : \mu X . F(X)
}{\Gamma \vdash \mathsf{rec}_F([x . f(x)], u) : C(u)}$$
We shouldn't forget to ask about equations that we expect to hold. The $\beta$-rule would be
$$\mathsf{rec}_F([x . f(x)], S(e)) = f(e)$$
and let us throw in an $\eta$-rule
$$S(\mathsf{rec}_F([x . x], u)) = u.$$
The $\eta$-rule says that if we take apart $u : \mu X . F(X)$ and put it back together, we will get $u$.
So far we have a map $S : F(\mu X . F(X)) \to \mu X . F(X)$, but we also want $R : \mu X . F(X) \to F(\mu X . F(X))$ together with
$$S(R(u)) = u \qquad\text{and}\qquad R(S(e)) = e \tag{1}$$
These say that $S$ and $R$ form an isomorphism between $F(\mu X . F(X))$ and $\mu X . F(X)$. We can get such an $R$, namely
$$R \mathbin{{:}{=}} \lambda y : F(\mu X . F(X)) . \mathsf{rec}_F([x . x], y).$$
Indeed, we have by the $\beta$-rule
$$R(S(e)) = \mathsf{rec}_F([x . x], S(e)) = e$$
and by the $\eta$-rule
$$S(R(u)) = S(\mathsf{rec}_F([x . x], u) = u.$$
We could have started with having $S$ and $R$ satisfying equations (1), and that would allow us to derive the eliminator as
$$\mathsf{rec}_F ([x . f(x)], u) = f(R(u)).$$
Such an eliminator satisfies the $\beta$-rule and the $\eta$-rule, quite obviously. This should give us pause. We discovered that our rules say precisely that $\mu X . F(X)$ is isomorphic to $F(\mu X . F(X))$ and nothing else. This is not good, because the rules should fix the meaning of $\mu X . F(X)$ up to equivalence of types.
To see that the rules are no good, consider the case $F(X) = X$. Every type is a fixed point of $F$, and our rules say nothing about which one $\mu X . X$ should be. Indeed, we can take an arbitrary type $A$ and set $R$ and $S$ to be the identity maps. That will satisfy all the rules for $\mu X . X$.
We should somehow state which fixed point of $F$ we have in mind when we write down $\mu X . F(X)$. a reasonable choice would be to ask for the smallest or initial one. But what does that mean? In category theory it means that there is a unique homomorphism from the algebra $S : F(\mu X . F(X)) \to \mu X . F(X)$ to any other $F$-algebra. Here we rely on the fact that $F$ is a functor so that we can reasonably talk about $F$ applied to a map. But our $F$ is not going to be a functor in general because it might break covariance (try to extend $F(X) = X \to X$ so that it takes $f : A \to B$ to some $F(f) : F(A) \to F(B)$ and you will see what the problem is). We are stuck, as we have no good criterion for picking one of possible fixed points of $F$!
The way out is to decompose $F : \Type \to \Type$ according to covariant and contravariant arguments,
$$F : \Type \times \Type^{\mathrm{op}} \to \Type.$$
For example $F(X) = X \to X$ becomes $F(X_1, X_2) = X_2 \to X_1$. But now it's not clear what a fixed point of $F$ might be. All this leads to Freyd's notion of algebraically compact categories and a beautiful theory surrounding them. The theory can be applied to categorical models of programming languages to explain how recursive types work there. When we throw in dependent types, then as far as I know, things break and nobody knows what to do. But I would love to be proved wrong!
The sort of recursive types we spoke about here goes under the name isorecursive types. The other option are equirecursive types, see the same link.
