"Guarded" negative occurrences in definition of inductive types, always bad? I know how some negative occurrences can definitively be bad:

data False

data Bad a = C (Bad a -&gt; a)

selfApp :: Bad a -&gt; a
selfApp (x@(C x')) = x' x

yc :: (a -&gt; a) -&gt; a
yc f = selfApp $ C (\x -&gt; f (selfApp x))

false :: False
false = yc id


However, I am not sure whether:


all inductive types with negative occurences can turn wrong ;
if so, there is a known mechanical way of doing so ;


For instance, I've been fighting trying to make this type go wrong:

type Not a = a -&gt; False

data Bad2 a = C2 (Bad2 (Not a) -&gt; a)


Any pointer to literature on this subject would be appreciated.
The reason for the ban on negative occurrences can be understood by analogy with the Knaster-Tarski theorem. This theorem says that

if $L$ is a complete lattice and $f : L \to L$ is a monotone function on $L$, then the set of fixed points of $f$ is also a complete lattice. In particular, there is a least fixed point $\mu{f}$ and a greatest fixed point $\nu f$.

In traditional model theory, lattices $L$ can be viewed as propositions, and the order relation $p \leq q$ can be understood as entailment (i.e., that $q$'s truth is entailed by $p$'s truth).
When we move from model theory to proof theory, lattices generalize to categories. Types can be seen as the objects of a category $\mathbb{C}$, and a map $e : P \to Q$ represents a proof that $Q$ can be derived from $Q$.
When we try to interpret types defined by recursive equations, e.e., $\mathbb{N} = \mu \alpha.\;1 + \alpha$, the obvious thing to do is to look for a generalization of the Knaster-Tarski theorem. So instead of a monotone function on a lattice, we know want a functor $F : \mathbb{C} \to \mathbb{C}$, which sends objects to objects, but generalizes the monotonicity condition so that every map $e : P \to Q$ gets a map $F(e) : F(P) \to F(Q)$ (with the coherence conditions that $F$ sends identities to identities and preserves compositions so that $F(g \circ f) = F(g) \circ F(f)$).
So if you want an inductive datatype $\mu \alpha.\;F(\alpha)$, you also need to supply a functorial action on terms for the type operator $F$ in order to be assured that the fixed point you want exists. The strict positivity condition in Agda and Coq is a syntactic condition that implies this semantic constraint. Loosely speaking, it says that if you build a type operator from sums and products, then you can always cook up the functorial action, and so any type formed in this way should have a fixed point.
In dependently-typed languages, you also have indexed and parameterized types, so your real task is more complicated. Bob Atkey (who has blogged about this here and here) tells me that a good place to look for the story is:

Structural Induction and Coinduction in a Fibrational Setting,  Claudio Hermida and Bart Jacobs 1997.
Fibrational Induction Rules for Initial Algebras, Neil Ghani, Patricia Johann, and Clement Fumex 2010.

As Andrej notes, fundamentally whether or not a negative occurence is okay or not depends on what your model of type theory. Basically, when you have a recursive definition, you are looking for a fixed point, and there are a lot of fixed-point theorems in mathematics.
One which I, personally, have made a lot of use of is Banach's fixed point theorem, which says that if you have a strictly contractive function on a metric space, then it has a unique fixed point. This idea was introduced into semantics by (IIRC) Maurice Nivat, and was extensively studied by America and Rutten, and was recently connected by Birkedal and his collaborators to a popular operational technique called &quot;step-indexing&quot;.

Solving Reflexive Domain Equations in a Category of Complete Metric Spaces, Pierre America and Jan J. M. M. Rutten 1989.
The Category-Theoretic Solution of Recursive Metric-space Equations, Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. 2010.

This gives rise to type theories where negative occurences in recursive types are permitted, but only when the negative occurences occur under a special &quot;guardedness&quot; type constructor. This idea was introduced by Hiroshi Nakano, and the connection to Banach's theorem was made both by myself and Nick Benton, as well as Lars Birkedal and his coauthors.

A Modality for Recursion, Hiroshi Nakano, 2000.
Ultrametric Semantics of Reactive Programs, Nick Benton and Neel Krishnaswami, 2011.
A metric model of guarded recursion, Lars Birkedal, Jan Schwinghammer, and Kristian Støvring, 2010.