Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?
I'm going to assume that by $\mathrm{Fix}$ you mean a new type constructor

$$\frac{\Gamma\vdash F:*\rightarrow *}{\Gamma\vdash \mathrm{Fix}\ F:*} $$

Along with the conversion rule $\mathrm{Fix}\ F\simeq F\ (\mathrm{Fix}\ F)$. This is often referred to as equi-recursive types as opposed to iso-recursive types, where the conversion rule does not exist, and you need additional $\mathrm{fold}$ and $\mathrm{unfold}$ constructs to use $\mathrm{Fix}$.

I'll ignore the fact that the rule for $\mathrm{Fix}$ is non-terminating on it's own, since this isn't that harmful. You question about terms

$$\Gamma\vdash t:A$$
with
$$\Gamma\vdash A:*$$

when are they sound proofs of the statement $A$?

You suggest using a "totality checker", to sidestep the need for messy rules such as positivity and various other restrictions when dealing with iso-recursive types.

The first remark is that simply checking termination of a term $t$ won't do: we can easily build a proof of $\forall n:\mathbb{N}. n = 0$ which has a normal form, but loops when applied to some natural number! So we really do need to check totality, which involves proving that $t$ will not lead to non-termination when placed in an arbitrary well-typed context.

Sadly, we don't really know how to do this, other than building back in all those nasty restrictions you want to avoid! For positivity for example, taking $\Lambda=\lambda X:*.X\rightarrow X$, then you can type
$$\vdash \lambda x:\mathrm{Fix}\ \Lambda.x\ x:\mathrm{Fix}\ \Lambda $$

which smells like trouble: your totality checker had better reject that as a theorem.

The other restrictions will crop up pretty quickly.

As a side note, if you can prove something using some "reasonable" totality checker (provably correct in HOL) then you can actually "reverse engineer" a proof in CoC + $\forall n. S\ n\neq 0$, by internalizing the totality check. This technique is similar to realizability, where there is a correspondance between provably total functions and $\Pi^0_2$ theorems.



As a side note that came up in the comments, it seems to me that when restricting $\mathrm{Fix}$ to positive type constructors, i.e. type constructors $F$ for which (for each variable $f$) there exists a term $t_f$ such that

$${A:*,B:*,f:A\rightarrow B\vdash t_f:F\ A\rightarrow F\ B} $$

then there is no encoding of $\mathbb{N}$ such that induction over $\mathbb{N}$ holds.

The rough argument for this is to encode $\mathrm{Fix}\ F$ by 
$$\forall X, (F\ X\rightarrow X) \rightarrow X$$
which is the usual encoding for positive inductive types in system F, and show that every well typed term in the system with $\mathrm{Fix}$ can be well typed in the CoC without it. Then we can conclude by the fact that CoC doesn't have any inductive definitions of $\mathbb{N}$ itself.

The encoding is a little messy, though, I think. I'd be happy to have a reference for this.