Yes, I think another simpler way to do it is to have a set theoretic interpretation of types with subtyping. In which case, we can check that a variable can be

Yes, I think another simpler way to do it is to have a set theoretic interpretation of types with subtyping. In which case, we can check that a variable can be type-asserted to a given subtype. A (sub)type being a set of propositions (i.e. defines a set of values).