Alright.. What I meant to say was,

Types don't enforce all meaning ie., the enforcement of contracts through types go only as far as they mean something to the problem you are applying it to. It does not cover all the complexities of the problem, or the way the code is changed in the future.

EDIT: This is also why it is easy (and nice) to implement parsers in strictly typed functional languages, because parsers are well studied theoretically. The problems in the real world are not studied well enough for contracts enforced via types to work completely.

Types don't enforce meaning, types are a tool I use to enforce consistency of meaning along certain important dimensions. I actually find that even more important when the situation is messy, because I'm likely to initially mischaracterize some aspects of it initially and when I go to change things it's very useful to be told what's now inconsistent.

I get what you are saying. What I'm trying to say is typing takes too much from me, in terms of complexity over-head, that I'm better without. I found this is true in practice now. As I said before, I write tests to do what you say types do - for me, that is enforcing meaning. Types do allow for easy refactoring, and I think that is weakness for untyped languages.

> The above function enforces that getting a user can fail and you must contact the outside world to get a user.

That seems sort of backwards. It enforces that the caller be able to handle failure (and similar for IO). It may well be that "getting a user" doesn't do either (e.g. `pure (pure defaultUser)`)