I do development in both statically and dynamically typed languages; speaking personally, I really value the added documentation that types provide beyond a certain program size.

Static types also can enhance a language's tooling; look at Hoogle for Haskell, Pursuit for PureScript, or Fancy Search for Elm, for example. I can ask these type-directed search engines "hey, is there a function that takes a String and returns an Int", and Hoogle will tell me length satisfies those requirements. Idris' type-directed search goes a step further - I can ask it "hey, is there a function that takes a vector of length N and a vect of length M and returns a vector of length N+M", and it'll tell me that ++ is how you append two vectors. It's a great tool for exploring a new language! That being said, there are similar things in some dynamic languages - Smalltalk's method finder comes to mind - but they seem more common in statically typed languages, especially descendents of ML.

It seems that one can tend to spend more time fighting with the borrow checker than actually solving real problems.

I definitely had this reaction when I started playing with Rust last year! But as a sometimes C programmer, I began to realize that the problems the borrow checker is pointing out - memory leaks and shared mutable references - are definitely real problems worth solving! I didn't see a lot of false positives from the borrow checker during my experiementation, but I know there are blind spots (eg. IIRC it's impossible to write a double linked list in safe Rust).

On a side note, if anyone from dynamic land is looking to dip their toe into static waters, especially if you know JavaScript, I highly recommend checking out Elm. Its compiler is very friendly and helps you along, and I feel like the speed of development compares to that of JS, even though it's statically typed.