Right, so we essentially say that the provided example doesn't refute the "it works if it compiles" slogan. It just works according to the provided specificatio

Right, so we essentially say that the provided example doesn't refute the "it works if it compiles" slogan. It just works according to the provided specification expressed in the types, and it so happened that the specification was not specific enough. 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).