The thing to realize is that at the end of the day, all you are doing is reducing bugs, and while your type system (IMO) really can help reduce bugs, it will never catch all bugs. There is still value in a function declaring that its argument is of type User (and not defensively checking it) even if it is theoretically possible, in the presence of a bug, though unlikely, that the argument is not really a User. The function has said what its precondition is, and (assuming you are validating any data that comes over the network or from an untyped source), this precondition will in practice be checked 99% of the time. If a bug happens to line up with a hole in the type system, you’ll just have to debug and fix it.