The general consensus in the community afaik, is that

  head :: [a] -> a

in Prelude was a mistake, and the default should be to return a Maybe/Optional. Beginners are generally advised to avoid head, and all other partial functions in the Prelude, such as tail and the indexing operator, wherever possible, and rely on pattern matching instead, which is generally sufficient and more idiomatic for the relevant use cases. I agree that having the option to use a partial function is useful, escape hatches are important, but it shouldn't be the go to.

Nonempty was just a simple example. You're right that it's not very commonly used (probably because it's not in Prelude), but the general culture of writing type safe interfaces and pushing guarantees to compile time %100 is a thing. A commonly used, more complicated example might be Servant, which is a web library which statically ensures your implementation meets an API spec.

Well, since the Prelude was never changed to at least add an alternative headMaybe, perhaps it was not seen as a deep enough mistake.

Yes, I am aware that the Haskell community generally tries to push more guarantees to compile time, and that Haskell's ease of defining and using new types equivalent to existing ones but that signify some property helps a lot in this.

Still, there is some limit to this. For example, you have many libraries adding measurement units for Haskell, and many libraries doing linear algebra. But you won't find too many people doing linear algebra with measurement units, because the types of intermediate results explode too much (e.g. a type-safe unit-of-measurement matrix multiplication of 3x3 matrices has 18 type parameters, with complicated restrictions between them).

Definitely don't disagree!

> How many functions have you seen, in Haskell, that take Nonempty a versus taking [a]?

Most take Foldable or Traversable.

When it's relevant your functions can be specialized into Nonempty.

We've been using this approach in Typescript. It's more palatable than Haskell since you can express an array that has at least one element as a variadic tuple `[T, ... T]`. Having the possibility to encode invariants in types is very useful, although it gets harder at times since TS chokes when you push it to its limits. Note that this happens in an old Meteor codebase that was completely JS a year and a half ago.

What complications would it have produced? Eg Elm has `List.head : List a -> Maybe a` and it's just fine I think?

In practice I've found that it leads to writing code that you know is unreachable, but you can't prove it to the compiler.

If you know the list can't be empty, can't you prove that to the compiler by using a non-empty list type?

Good point! last time I used elm i didn't know what a nonempty list was.