Is there such a thing as "recursively dependent types"? Specifically, I would like a dependent type theory containing a type $A(x)$ which depends on a variable $x: A(z)$, where $z$ is a particular constant of type $A(z)$.


This may be more "impredicative" than some type-theorists would like, but from the perspective of semantics in locally cartesian closed categories, I can't see any reason it would be a problem: the type $A$ comes with a display map to $A\_z$, while $A\_z$ itself is the pullback of this display map along a particular morphism $z \colon 1\to A\_z$. But I want to know whether a corresponding syntax exists.



Recursively dependent types?
If $z$ is a constant, it's completely unproblematic, but it's troublesome if $z$ is a variable. Here's a simple example: suppose $A$ is a type operator of kind $\mathbb{N} \to \star$, defined as follows: 


$\matrix{
 A(z) & = & \mathbb{N} \\\ 
 A(n + 1) & = & \mathbb{N} \times A(n) }$ 


Then it's obviously the case that $z : A(z)$. 


OTOH, if $z$ is a variable, on the other hand, then you'll run into the difficulty that the standard well-formedness rule for contexts says that for $\Gamma, x:A$ to be a well-formed context, then $\Gamma \vdash A$ -- that is, $A$ should be well-formed with respect to the variables in $\Gamma$. 


Now, there's nothing semantically wrong about adding fixed point operators at every kind. That is, have type operators with kinds like $\mu : (\star \to \star) \to \star$, or $\mu' : ((\star \to \star) \to (\star \to \star)) \to \star \to \star$ or $\mu'' : ((\mathbb{N} \to \star) \to (\mathbb{N} \to \star)) \to \mathbb{N} \to \star$. This kinds of dependency, where the dependent index can vary at every level of a data structure, are very useful when programming in type theory. For example, we might define the type of lists of type $A$, indexed by length in the following way:


$\array{nil & : & list(z) \\\
 cons & : & \forall n:\mathbb{N}.\; A \to list(n) \to list(n+1)}
$


So here, $list$ is the least fixed point of a type operator of kind $(\mathbb{N} \to \star) \to (\mathbb{N} \to \star)$. However, most type theories avoid adding the generic operator (like $\mu''$ above) in favor of only permitting inductive types as primitive definitions. 


This is partly for philosophical reasons, and partly for pragmatic reasons involving not wanting to require supplying a well-ordering at each elimination of a recursive type. This is necessary to avoid being able to use a recursive type like $\mu \alpha.\; \alpha \to \alpha$ to introduce general recursion and inconsistency into the type theory. However, this complicates typechecking quite a bit -- if you're not very careful, you can lose decidability of typechecking. (In particular, in an inconsistent context, you can cook up with a bogus well-order using the local contradiction, and then use that to tip a conversion rule based on blind $\beta$-reduction into going into an infinite loop. This is not a problem for consistency, but it can annoy users.) 


If you're okay with impredicativity, I don't think there are any semantic issues related to consistency, though. 


