Is there a denotational semantics for System $F_\omega$ in literature that supports both recursive types and general recursion?
I'm looking for a model of Ralf Hinze's variant of System $F_\omega$ [4]. It has a term-level fixed point combinator $$\mathit{fix} : \forall X:*.~(X\rightarrow X)\rightarrow X$$ and type-level fixed point combinators $$\mu_\kappa : (\kappa\rightarrow\kappa)\rightarrow\kappa.$$ Neither the ideal model the the interval model seems to fit.
In the ideal model [1], the convertibility rule $$\mu_\kappa T\leftrightarrow T(\mu_\kappa T)$$ is not sound, because not all ideal functions have fixed points.
In the interval model [2], it is not clear how to make the term-abstraction and term-application rules sound. Martini's interval model for $F$ [3] restricts types to maximal intervals, but such a restriction would leave the inhabited type $$\mu_*(\lambda X.~X)\rightarrow\mu_*(\lambda X.~X)$$ without any meaning.
[1] MacQueen, Plotkin, Sethi. An ideal model for recursive polymorphic types.
[2] Cartwright. Types as intervals.
[3] Martini. An interval model for second order lambda calculus.
[4] Hinze. Polytypic values possess polykinded types.
