def getUsers(f):
        return (logged_in_users(f), logged_out_users(f))

    def userCount(f):
        return len(getUsers(f))

"Python provides many tools that can be used to solve programming woes. One such tool is its strong and readable syntax." Do you see how empty this sort of platitude is?

Similarly, one might say that a strong type system is a useful tool. That doesn't make it a panacea (and I don't think that this was the claim), but that doesn't mean one can't appreciate it as a good tool.

    def get_users(f) -> Tuple[List, List]:
       return (logged_in_users(f), logged_out_users(f))

    def user_count(f) -> int:
       return len(get_users())

    def get_users(f) -> List:
       return logged_in_users(f) + logged_out_users(f)

    def user_count(f) -> int:
       return len(get_users())

Also, you should annotate the type of your lists :)

  def get_users(f) -> Tuple[List[User], List[User]]:
    return (logged_in_users(f), logged_out_users(f))

  def user_count(f) -> int:
    logged_in_users, logged_out_users = get_users()
    return len(logged_in_users) + len(logged_out_users)

But, if that really is the reason for Maybe [a] over [a], I'd still prefer Either SomeUsefulErrorType [a].

My specification doesn't make a distinction between absent users and possible error responses because I assume that errors will be processed elsewhere and the getUsers function is applied as part of the "safe core" interface that is not concerned about error handling. If the specification was more precise (even more precise than in your suggestion, for instance, getUsers :: SafeIterable a => Foo -> a and length :: SafeIterable a => a -> Integer ), it would work differently.

The issue in the example has to do with the clarity of the intent encoded in the type signature, not the inherent issue of the type system that cannot guarantee safe runtime of the example. That's why I mentioned type constraints for specific iterables as a possible solution to the encoding problem.

A better example of the compiled-but-not-working case would be something that currently cannot be expressed well by the type system, something like async exceptions or access to closed resources (will be covered by linear types soon).

Haskell will never stop you from representing every value as String, and just throwing exceptions if the strings do not convert back, for example.

I know, not what you meant. But a custom sum type would not only allow you to return multiple different failure cases, you also wouldn't give it a `Foldable` instance with surprising semantics.

Plain old data types are seriously underrated these days.