What is the greatest limitation of Haskell's type system? The greatest limitation in Haskell's type system is it only does Haskell's type system.
I totally agree. Almost two years of working in Haskell has convinced me of the benefit of static type analysis. It can catch a lot of bugs. But Haskell's type system also increases the amount of code and the surface area of your interface. The types become a point of coupling. They become hard to change without changing everything that uses them.
This rigidity is where their power comes from, and also their annoyance. Well-chosen types can stabilize a system in a good way. Mistakes in the types, or changes in their requirements, stabilize the system in a bad way.
I would love to see a type checker that could handle non-discriminated union types (Haskell has discriminated unions, which force you to box and unbox values, adding to code size and coupling to the types). It would be nice to have the type checker say "Function foo takes either a String or a Number, but on line 34 you pass it a String or Number or HashMap."
Another type of analysis I would like to see is whether a function is pure, does IO, or accesses mutable state. You can tag all basic IO operations as IO. Then anything that calls one of those operations also gets the tag IO. Similarly for mutable state. Haskell makes IO a type so that it can be statically checked, because Haskell only does type checking. It is not really a type, though, and does not need static type analysis.
Another great advantage of static checking in a dynamic language is that the definition of functions can change at any time. So function foo could compile, but with a warning that it calls function bar incorrectly. When you correct function bar, the warning goes away automatically.
Those are some ideas I had watching that video and thinking about static analysis in Clojure. I am quite excited.