Type coercion does not equal weak typing -- I submit JS and Perl as examples where types are strong but there is a coercion protocol dependent on which types an operator expects around it.
If it were type coercion, we would expect the add function to have either of these two behaviours:
- coerce the input arguments to strings, i.e. implicitly accept two strings and return another string
- coerce the input arguments to integers, i.e. implicitly accept two integers and return an integer
Of course, in Javascript it is implemented as a function that takes the theoretical "Any" type and decides what do do at runtime. But in a statically type language, the equivalent mechanism would be dynamic/multiple dispatch (or a static overload, possibly in combination with a generic/template method) -- not type coercion.
Sometimes useful, but the type system ends up offering few meaningful protections as a consequence.
However, C does allow you to write code that can not proven to be legal with respect to the formal system of the language and get it to compile, I think that is what you are referring to.
But just because you can write an invalid program does not mean the type system doesn't exist or is flawed. I can also write an invalid Haskell program.
The difference between these two would be that the haskell program can be proven to contain only operations that map to well-defined operations in the formal language model by an automated process, while the same can not be done for C in the general case.
However, just because you can not always prove conformance to a formal model using automated means, doesn't mean that no formal model exists (because it does!).