There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones.
Maybe you know this, but this is a well known correspondence (as in academically from decades ago, but barely mentioned in industry): https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
The types you write in code describe program properties to be proven and the type checker tries to create a proof that those properties are true for all inputs and outputs. Tests as you say only check a small number of inputs/outputs in comparison. It's very similar to mathematics where checking if a conjecture holds for a few values is a poor substitute to a rigorous proof.
I wouldn't say using a "unit test" is ever really a viable option for me. Property-based tests subsume unit tests.
So no, Coq and other "total" programing languages (agda, idris, F*) may not be turing complete in the usual sense because the two things are contradictory, but they are much better: you can simulate a turing machine as a server which will be provably always making progress in finite time.
See this paper for some more insights:
https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....
Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris).
I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
[0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
(Contrast with long compile times which are incompressible)