Regarding natural numbers, and inductive types (ie. initial algebras of some form) in general, impredicative encodings are inconvenient, as they only specify weakly initial algebras, rather than initial ones. This means that while one can define functions by recursion on natural numbers, it is not possible to prove things by induction (indeed, induction is not derivable for impredicative encodings). It is not even possible to show that the (impredicatively encoded) booleans $true$ and $false$ are different! As far as I understand, this is why Cedille adds some kind of parametricity on top of their impredicative definitions, in order to regain the possibility to do proofs by induction. Note also the other answer by Mike Shulman, regarding the fact that in a setting where you have a primitive identity type, you can use it to "carve out" better-behaved types out of the standard impredicative encodings, letting you regain induction.
Moreover, the computational behaviour of impredicative encodings is quite impractical, as the reduction rules you get for the recursor are not the ones you could hope for (typically, you do not have that $rec_{\mathbb{N}}(P,b_0,b_{S},S\ n) \rightarrow b_S\ n \ rec_{\mathbb{N}}(P,b_0,b_{S},n) $ for an open $n$). This is linked with the standard weirdness that the predecessor function on Church-encoded natural numbers executes in a number of steps proportional to the size of the integer. For more about this, you can go look up the original paper by Paulin-Mohring on adding inductive types to Coq, where she motivates a great deal her addition.
Finally, using impredicativity where only much weaker principles would suffice is also questionable. Not only because this feels like using a bazooka to kill a fly, but also because in practice (proof-relevant) impredicativity is incompatible with many principles, typically classical ones (this is why impredicative Set is not part of default Coq any more). Moreover, if you care about foundations, giving a good account of (proof-relevant) impredicativity is hard, because Polymorphism is not set-theoretic (here polymorphism is pretty much the same thing as proof-relevant impredicativity), so there are no models of it which interprets types as sets.
There is one situation where these impredicative definitions pose much less problems though, namely that of proof-irrelevant impredicativity, ie. defining a proposition in an impredicative way. Indeed:
- you do not care about induction principles for these, because you do not want to distinguish two inhabitants of a proposition (which is exactly what induction gives you);
- you should not care too much about computational content, again because the less you look at computation in proof-irrelevant types, the better;
- proof-irrelevant impredicativity has set-theoretic models (if you interpret the impredicative sort as the two-element set), and it is in general easier to model.
In practice, in Coq for instance, you can still define propositions by induction, but this is usually seen as just a convenience to talk about an impredicatively-defined proposition, that could easily be desugared. Indeed, Coq by default only generates non-dependent recursors, but no dependent induction principle, and if you look at the set-theoretic models of CIC by Werner (as far as I know, the state of the art), he models inductive types, but does not handle inductive propositions, saying those can just be impredicatively encoded.
