> Indeed this is true.  (Although Erlang's `dialyzer` can "propose"
> signatures for your code based on what it "sees" in its usage.)

That's remarkable for a dynamic language :)

> And I think such a use-case, of rejecting what is provably wrong, is
> of a lot of help to dynamic-typed languages, especially in cases like:

These are good examples. I agree that catching simple errors like this
would be very useful.