This is quite similar to units (e.g. F# units of measure) or taints (Perl, for tracing user input and detecting unsafe usage). A large part of the point of the

This is quite similar to units (e.g. F# units of measure) or taints (Perl, for tracing user input and detecting unsafe usage). A large part of the point of these systems is that you can write code which generalizes across the different subtypes (different units, tainted vs untainted values) yet it still passes through invariants by default (values calculated from tainted input are themselves tainted, a unit-quantified value multiplied by a scalar retains its unit, and so on). I've done similar things with syntax trees in compilers. With multiple passes, you have a representation for the output of the parser, then you might do type annotation, rewrites due to coercion etc., symbol binding and overload resolution, constant expression evaluation, and so on in separate passes. If the input and output trees for each pass have different types, it's easier to keep track of what's going on, of what invariants hold for any given tree node, or indeed which node types are permissible to exist in the input or output of a pass (e.g. you don't want unbound overload calls after overload resolution). One problem is that tags probably aren't enough when you're dealing with data structures rather than simple zero-dimensional values. Some methods shouldn't be called, or some fields shouldn't be accessed, if a value has a type with the wrong tag. But if you have a wholly different type, then you can end up reimplementing a lot of the same logic, once per type, simply to get the types to flow through. One solution I've used a couple of times for the tree problem is tree grammars. That is, a data structure which encodes a description of a valid tree and can encode invariants like nodes of type T need to have attributes of type Y with values satisfying predicate P, and between N and M children of type U, V or W, and so on. The grammar is defined in terms of an abstract supertype, and the concrete subtypes have the grammar specific to their phase baked in. This is a hybrid between static and dynamic typing, a compromise necessary for languages like Java without much expressiveness in the type domain.