Believing that any technology has no cost is poor engineering IMO. There are costs to that rigidity, and they're rather self-evident.

If you believe there are no diminishing returns, I'm interested to hear your reply to the author's question about why we don't all use Agda or Idris.

Defining types is easy and enhances code readability until you go too far. Some type declarations in Haskell or highly templated C++ are hard to read.

I really don't think it does that. Most refactoring is not like that. It is about changing things at a deeper level than just the type.

I don't think they enhance code readability - I think they make it worse. I never look at the type when I am reading code, it just gets in the way.