For example, how would you write a function that answers the mean value of an array of numbers? You could define Array.Length to be of type NonNegativeInteger, but that still includes 0. Alternatively, you'd have to define a NonEmptyArray type that excludes arrays of length 0, but that seems less than useful.
The thing is that, instead of redefining everything yourself, you could use a library that provides you with a set of predicates to compose and build the refinement you need. There are also much sophisticated ways to do this, like Liquid Haskell.
I think the usefulness of a specific NonEmptyArray type is controversial, and I would say such types could be extremely useful. AFAIK there have been discussions if Haskell's Prelude (part of the standard library providing a name space for convenient functions and types, similar to the functions you get in e.g. Python like map, zip, filter, range, etc.) should be more save by not advocating too generic types and functions like the standard `map`, `head` and `tail` implementations.
Functions like `head` and `tail` can be seen as problematic as they can fail and cause runtime errors (the head and tail of an empty list cause a runtime error), but I do not think they already changed that (or if it's even a topic of discussion at the moment).
It's a little bit a matter of taste. Think about Unix' "head" program that by default prints maximal 10 lines of a file. How should we deal with the following?
$ touch empty.txt
$ head -n1 empty.txt
You can look at the NaN value as an implementation of Option / Maybe, where it means None. It even behaves like it should, short-circuiting any normal operations with it to also produce NaN. Too bad Fortran and C lack sum types to surface that properly on the type level.