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.

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.

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.

The reason that type theorists avoid it in favor of adding inductive types as primitive definitions 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. (You need this 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.)

If you're okay with impredicativity, I don't think there are any semantic issues (though I think there may be technical issues related to decidability of typechecking).

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.