This is why Gosu has, for example, covariant generics. Yes, it is unsound. But it is simple and good enough.
Type systems should be there to help us write code, in particular to support things like IDEs. Correctness is great as far as it goes, but it turns out it doesn't go too far and you get 90% of the correctness benefit with, hey, look at that, 10% of the effort and complexity.
But seriously, what is the point of having a typesystem which is not sound? Nobody is going to mind if you create another dynamic language ala Python, but design a type system (and force your users to use it) if it doesn't provide the protection against fucking up the types?
Static type systems (particularly explicit rather than inferred ones) have multiple goals: as a form of documentation; as a way of specifying interfaces so pieces can be more reliably developed independently because the seam isn't just in documentation or peoples' heads or a bunch of unit tests; as a way of designing an app (when program = data + algorithms, some people like to start with the shape of the data); and finally as a way of proving more things about the code.
I'd submit that the historical actual use of types doesn't emphasize the proof nature of types nearly as much as academic CS does. Unsound type systems are common in practical languages. And I believe that isn't accidental: because, with all the other things types are used for, you need an expressive type system, and that in turn means it is either going to be complex and sound, or simple and unsound (i.e. with escape valves like typecasting and runtime type errors - I'm considering compile-time type analysis only).
"what is the point of having a typesystem which is not sound?"
Because it gives plenty of benefits even when it's not "sound". What your suggesting is that there should never be any language between dynamic languages and haskell. Clearly there are many people who find type systems highly useful even if they don't go as far as haskell.
He just told you; to assist the IDE, things like automated refactoring, something Ruby still doesn't have to any reasonable degree. Type systems don't have to be perfect to be damn useful, if you like type systems.
This is why Gosu has, for example, covariant generics. Yes, it is unsound. But it is simple and good enough.
Type systems should be there to help us write code, in particular to support things like IDEs. Correctness is great as far as it goes, but it turns out it doesn't go too far and you get 90% of the correctness benefit with, hey, look at that, 10% of the effort and complexity.
http://www.jwz.org/doc/worse-is-better.html