I agree that this is where we should be headed; it seems to me that Liquid Haskell, which was submitted to HN recently[1], could actually do what you need, since it uses an SMT solver to check for preconditions.
The casting function could specify the valid input values, and force the programmer to handle the rest of the cases when the input type is wider.
The casting function could specify the valid input values, and force the programmer to handle the rest of the cases when the input type is wider.
[1] https://news.ycombinator.com/item?id=13125328