There are also some things that I'm not sure are reasonable at all in something like Java/C++ without writing a lot of code. For example: https://www.chrisstucchio.com/blog/2014/type_safe_vector_add...
Java is in an interesting place in that its type system is rudimentary but not unpowerful. C is a more useful didactic target---there really do exist invariants which can be encoded in Haskell types but could never be encoded in C types!
Another huge target is parametricity. You can write Java code which is "maybe sort of parametric" but it really isn't and subsequently you can never trust it because of the existence of things like global reference equality and hash codes (in the least).
Finally, there are expressivity concerns. Java cannot encode as many things in its type language as something like Agda (to make a clear comparison). You can simply note that Java's type equality is nowhere nearly as developed as Agda's!
As an example of using Java to indicate a fairly non-trivial invariant and comparing that implementation to Scala, Haskell, and C# consider Tony Morris' challenge
http://tonymorris.github.io/blog/posts/understanding-practic...
x = r_[:n].reshape((3, -1, n/15))[:, :2].sum(axis=-1)
y = x + randn(m, 1, 2)
z = y - r_[:7]
I suppose this may have been tackled in Haskell in the Repa library, but I'd need to read papers like
http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf
to know. Hence my question if we could lift this into the type system in a conventional language, but I don't think it's possible in a general way.