That example is a straw man. First, all reasonably strong type systems support polymorphism well enough to handle that case trivially. Second, type inference is a thing, so a lot of code in strongly-typed languages even looks the same as your second code example.

I'm not saying you can't come up with a fair example to support your argument. I will say, though, that it's going to be a lot harder to do so, and that such examples only rarely come up in practice. The argument for flexibility at the cost of guarantees of correctness used to be a good one, but it has weakened significantly with time, and before long will cease to be valid at all.

Guaranteed correctness has a cost in the form of extra specification needed to get things done.

This is simply untrue. Take an example in Haskell:

    > show 23
    "23"
    > show (4,5)
    "(4,5)"
    > show (Just 2.34, Nothing, [2..5], 'c')
    "(Just 2.34,Nothing,[2,3,4,5],'c')"

This works for all types which are members of the class Show. We can even derive new instances for Show for our own new data types automatically:

    > data Foo = Foo Int Float deriving (Show)
    > show (Foo 3 4)
    "Foo 3 4.0"

But what happens if we omit the instance of Show from our definition?

    > data Bar = Bar Char Bool
    > show (Bar 'a' True)

    <interactive>:12:1:
        No instance for (Show Bar) arising from a use of `show'
        Possible fix: add an instance declaration for (Show Bar)
        In the expression: show (Bar 'a' True)
        In an equation for `it': it = show (Bar 'a' True)

We get all the benefits of safety guarantees with minimal extra work. This form of automatic derivation works for many type classes in the standard libraries but in the cases where it doesn't work we simply define a few methods which are specified in the class's definition. None of this is any more than what you'd need to do in a dynamic language but you get all the extra benefits of compile time safety.