On my bike ride back from the office, I started thinking about my earlier statement about subsumption and that the new system would lose the static guarantee that an instance of a subtype with strengthened invariant is used as a supertype. Maybe we actually can do better in some cases. The important questions are: Where does subsumption happen? What class are we compiling?
First, though, I should emphasize that static analysis of what class will be contained in a certain variable at runtime is pretty difficult. It is easy to construct a program where the runtype type depends on some condition or might even be (pseudo-)random. In those cases, some sort of sum type should be used for the variable. So even within one method or one class, a certain amount of flow analysis has to be done. With debug information, the static types of all fields, parameters and local variables should be available without having to do inference, though.
Now let’s consider what class we are compiling. If we are compiling the subclass with the strengthened invariant itself, then it is reasonable to assume that adding a new invariant may break binary compatibility, so the entire project should be recompiled, or at least re-checked (in the case of the Java API). The same should probably apply if we are compiling a superclass or subclass of the class with the strengthened invariant.
If we are compiling a class other than the subclass with the strengthened precondition, then unless subsumption happens within the class being compiled, it has to happen either during a method call to another class or after returning a value.
Does this help us? I don’t know yet. It seems like it should be possible to figure out the possible types of a variable whose method is called, at least using sum types, which may be too general. Figuring out the class of the caller is probably impossible, though, at least using incremental compilation.
I think, even after these additional considerations, I’m getting back to the point that we cannot get a static guarantee with incremental compilation, without considering the whole program.
