Satisfying theorems is generally for the purpose of friendliness, by ensuring consistency. In this case, they had two options:

(a) be consistent as if the language had type-level literals, which resulted in nicer code in the usual case, but some unsafety on unchecked edge cases, or

(b) give more safety, but force everyone to check for the empty list even when they don't need to.

They went with (a) - it's the type of decision Haskell is (I'd argue incorrectly) criticized for not doing - people complain about having to prove things to their compiler. Of course, in hindsight, and given the language ecosystem now (and that option (b) is instead consistent with all the monad-centric libraries, etc.), (b) seems like a better choice. Which one is better could just as easily change again if empty lists became distinguished at the type-level in Prelude in the future. This is also something that would either crash, or be similarly inconsistent (just return null, causing eventual crashes instead) in any other language. It's notable, though, that the community is making effort to fix these tiny inconsistencies, rather than punting on it for backwards compatibility, as so many other ecosystems do.

Partly. Tsuyoshi Ito's answer on that page is IMO better than the original: `head` mattered at a time when pattern matching didn't exist; but today the only reason to use `head` is to form some sort of pointfree expression operating on lists that you've already filtered to be not-null. That is, you're doing `map (transform . head) . takeWhile (not . null)` or something, or maybe `takeWhile` is replaced with `filter` or so. If you cannot assert that the list is non-null then you have to handle two branches, and this code will generally look clearer if you pull it into a `where` clause and write it with pattern matching rather than with an adjusted `head` followed immediately by an appropriate `maybe` function.

With `[a] -> Maybe a`, it's not so bad if you use `catMaybes` from Data.Maybe.

map transform . catMaybes . map safeHead

Even better with mapMaybe:

    map transform . mapMaybe safeHead

In other words, it's this way because people want to emulate an unfriendly language, used on another domain where terseness is even more important than in Haskell code.

That does not make it a good choice. Just a kind of default, but it's a bad default.

isn't that just saying that 'head' shouldn't return [] on an empty list, because [] has a type which is never the type of what 'head' should return? that's separate from why 'head's type isn't [a] -> Maybe a.