Restrictions needed on ADT for totality

Question

In the paper Total Functional Programming by D.A. Turner three rules are given for a programming language to remain total:

1. complete case analysis
2. covariant type recursion (type constructor should not appear in negative position in a constructor argument)
3. structural recursion

But with these rules I can still have an infinite loop:

data Fix f = Fix (f (Fix f))
data Bad r = Bad (r -> r)

bad :: Fix Bad -> Fix Bad
bad b =
  case b of
    Fix t ->
      case t of
        Bad f -> f b

nonTotal = bad (Fix (Bad bad))

Where is my mistake? Should all type variables also only appear covariantly? Or is the "covariant type recursion" condition more strict?