Here is a little list of drawbacks of static type systems with features like you describe (parametric types, ADTs...): Type dependency hell (banana, monkey, jungle, etc), having to fight/convince the type inferencer to accept any but the simplest things, having to type many things twice.
Looking at Haskell, "almost everything is inferred" is a lie in my experience. You are encouraged to write code using higher-order and highly parametric functions. If you do, the error messages you'll get if you don't annotate are plain sick. Another problem is that the type system provides no convenient escape hatches, while it's not powerful enough for typical programs. Many "successful" example designs I've seen are either _really_ simplistic (to the point where it's obvious that the better design wasn't chosen simply because the type system makes it really inconvenient), or have some _really_ terrible internals hacking in it (which might be the largest part, be impossible to understand by most developers, and break with the next compiler version).
Looking at C++, a practical example is vector. It's a useful tool (automatic memory management), and very likely to be all over in your function signatures. This is very bad in terms of modularity / reusability, because your functions are not defined using reasonably general types (pointers to arrays).
Many of these very real pains just aren't there with Python code, which has better modularity at the cost of being a little sloppier.
These days I look at static types mostly as tools for generating fast machine code (I doubt that much more than C types is needed here) and as tools for enabling nice syntax (OOP protocols like in Python can do that too, but they are very dirty). These things however are only needed at the very optimized parts of your average project.
So I think a good way in many cases is to go the Python route, and check types dynamically at strategic points to assert value integrity and enable transition to highly optimized (with static types) routines.