Reworking TypeTestClosure

[DavePearce]

Currently, we need to rework the way that TypeTestClosure operates. The problem is that it replaced references to VariableDeclaration with those for updated VariableDeclarations. This is no longer viable (I believe) because the current model does not make it easy to replace existing facts which are "in the future".

[DavePearce]

One useful solution is be to maintain a separate typing environment for existential variables. This environment is initialised when a variable is pulled out of an exists truth. The following rules employs the TypeSystem.inferType() method and would be affected in some way:

• CongruenceClosure. This is used to infer types tests from equalities. For example, if x == y and x is int and y is int|null we might infer y is int.
• EqualityCaseAnalysis. Used for reducing equalities to true and expanded record or array equalities. Likewise, it's used for handling negated equalities as well.
• TypeTestClosure. Used for reducing types tests. For example, if x is int then x is bool reduces to false. Also for extracting type invariants, etc.

The key challenge is that these rules make use of TypeSystem.inferType(), but this provides a static view of types based on their VariableDeclarations.