In John Mitchell's book "The Foundations of Programming Languages", he considers a typed lambda calculus with unit, exponential, product, (binary) coproduct types, and arbitrary recursive types (p126). Later in the book he shows how to construct models of all these types. (I'm pretty new to all of this, but I assume this is a pretty standard system.)
It looks as though it is not possible to extend this system with a 0 type for the following reason:
Let $\sigma$ be $\mu t.t\to 0$. $\mbox{unfold}: \sigma \to \sigma \to 0$ and $\mbox{fold}: (\sigma \to 0)\to \sigma$. Then $W(\mbox{unfold})(\mbox{fold}(W(\mbox{unfold}))): 0$, where $W = \lambda xy.xyy$.
From this you can prove all equations between terms (e.g. from the existence of a closed term $t:0$, $\lambda x.t:A \to 0$ is an isomorphism between any type $A$ and $0$.)
A natural thought would be to work in a linear or affine type theory where the $W$ combinator isn't allowed, and which therefore might allow solutions to type equations like $\sigma = \sigma \to 0$.
My questions is: Is the resulting type theory consistent, and can anyone explain to me how to go about constructing models? (References would also be welcome, but the papers I've looked at so far have generally presupposed more knowledge than I have).