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, if you don't mind impredicativity, 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.