Recursively dependent types? 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.
 A: 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. 
A: Mike, if you consider that locally cartesian closed categories
provide the canonical semantics for dependent type theories then
you may as well just use sets, for which any function
$p:A\to X$ provides a dependent type $A[x]=\{a|p((a)=x\}$.
Not only is this a very dull notion of dependent type,
but it gives no account of the way in which $A{x]$ might depend
"continuously" on $x$,
something that we probably need to understand in order to
give a meaning to the word "recursive".
(Local, relative or ordinary) cartesian closure is needed to
interpret function- or Pi-types, which do not feature in your
question.  The appropriate arena is a category with some finite
limits and something infinitary to capture the recursion.
A class of display maps is a class of morphisms that is
closed under (composition with isomorphisms and) pullback against
arbitrary maps in the category.
This categorical notion is equivalent to that of a dependent type
theory in the basic algebraic sense, ie with types, terms, equations
and structural rules.
As I believe you are more comfortable with a categorical language,
you can solve your problem in that setting and then use the equivalence
to reformulate it symbolically.
In particular, the class of display maps includes
- all isomorphisms iff the type theory includes singleton dependent types;
- composites iff the type theory has Sigma types;
- inclusions of diagonals and hence all maps iff the type theory has
  equality types;
- relative cartesian closure corresponds to Pi types.
I had originally interpreted your "recursively dependent" types
to mean an infinite chain of dependencies, and hence of display maps.
For that you would want the class of displays to be closed under
cofiltered limits.
Neel, on the other hand, read it as a fixed point equation,
which we can interpret categorically as the fixed point of a functor.
Unsurprisingly, domain theory would be a useful setting in which
to look for models of these situations.
Indeed
my PhD thesis
introduced classes of display maps in order to study dependent types
in domain theory, 
and you might like to look at the last chapter for investigations
of appropriate notions of displays of domains.
For the theory of display maps and their equivalence with dependent
types, my thesis was completely superseded by 
Chapter VIII
of my book, "Practical Foundations of Mathematics" (CUP 1999).
For the interpretation of dependent types in domain theory,
Martin Hyland and Andrew Pitts gave a comprehensive account in
their paper
The Theory of Constructions: Categorical Semantics and
Topos-Theoretic Models in
Categories in Computer Science and Logic
edited by John Gray and Andre Scedrov, 
AMS Contemporary Mathematics 92 (1989).
