> Yes, you can work around the limitations of a static type system, either by finding another solution (lenses) or by making functions more specific (assume all keys are strings), but that doesn't mean the limitations disappear. It just means you're working around them.

I'm less concerned about the theoretical limitations of types that you seem to be talking about and more interested in looking at concrete real-world applications where you think you need dynamic types and seeing exactly what we can do to address them with a type system. I know there exist things that are difficult or maybe impossible to define types for (the Y combinator for instance, or possibly this assoc-in). My argument is that you don't need this power. I don't care whether difficult to type things exist, I care about whether real-world problems require them. I have yet to encounter one that I felt requires the same amount of dynamic typing power that you seem to be arguing for.

See this thread for some concrete examples:

https://www.reddit.com/r/haskell/comments/792nl4/clojure_vs_...