Strong static typing is pretty much an unmitigated win.

OK, program in a language where an array's size is an immutable part of its type. No casting, no autoconversion, no manual conversion. Now write reusable functions which operate on arrays.

Remember that a string is a kind of array, and inherits all of the same properties.

This feels like a straw man argument against static typing. No statically typed language I use suffers from this because they have great data structures and generics.

Languages such as Rust that lean on inference are an absolute joy to program in.

Actually, Rust arrays have the size as part of their type, and without type-level-integers, there is a lot of pain around them. :(

That said, there's the solution: type level integers.

(That also said, Rust's String type isn't an array, because it's mutable, so the size can't be a part of the type)

Fortunately, Liquid Haskell already exists.

I wouldn't say it's production quality yet... But it's a work in progress, and achieves far more than you are requesting here.

You can also go with Agda for full on dependent typing.

Or Idris, which is (IMO) more practically useful than Agda.

The big advantage to liquid types, a la liquid haskell, is that you get far more inference than you can get in full dependent typing.

I still think liquid haskell is too immature (Integer is not a good theory for Int, type classes aren't handled well, etc), but the promise is fascinating if the issues get worked out.

That's just an argument against languages with broken arrays. I'm guessing you've been doing a lot of Java lately?

Even Java has a sane typing system if you stay away from arrays (use ArrayList for crying out loud) but beyond Java, there is a wealth of languages with very good static type systems (Scala, Kotlin, Ceylon).

Or how about one in which "upper case letter" is a static type. A string of all upper case characters is statically declared; we don't have to iterate at run-time to check it character-by-character any more, wee!

Division by zero is passe; we just define a type that excludes zero, and make the division operator's denominator of that type.

There is a non-zero integral type in Haskell, I believe.

Yeah, I heard PG built ARC in Emojilisp after giving up on Racket ;) If I were to chose, I would choose Emojilisp too! Haskellers will certainly prefer Emojicode.

Still has mutation.