> in a lot of cases, those types that I wrote will be replaced by more dynamic representation (e.g. strings) at some point. I would love to see a type system that lets me subtype string, restrict the domain, and automatically (with some hints from the programmer) get functions on my type based on string functions the compiler can prove would result in my type.

I've only seen type systems that work like this on numbers, and usually only a very few integers at that.