But, if that really is the reason for Maybe [a] over [a], I'd still prefer Either SomeUsefulErrorType [a].
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.
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.