Support Flow Typing in TypeChecker

[DavePearce]

Currently, the type checker does not support flow typing. For example, this fails to type check:

assert:
   forall(int[] xs, any i):
       if:
          i is int
       then:
          xs[i] is int

In principle, the theorem prover can handle this easily enough. But, its not even getting passed the type checker right now.

The key question is where do we resolve this in TypeChecker? Some observations:

• At the moment, TypeChecker determines its type using Expr.getReturnType() which, for a variable access, returns the type given by the corresponding VariableDeclaration.
• WyalFileParseris responsible for connecting VariableAccess expressions with VariableDeclarations.

In principle, we could update WyalFileParser to be flow sensitive and to introduce some AliasDeclarations as it encounters them (i.e. when it sees x is int). The problem is how it determines what the appropriate type for the alias declaration is. An easy example:

assert:
   forall(any i):
       if:
           i is int
       then:
           (0 < i) || (i <= 0)

When i is int is encountered then we create an alias declaration. But, what about here:

assert:
   forall(int|null i):
       if:
           !(i is null)
       then:
           (0 < i) || (i <= 0)

Ok, it can determine the alias declaration as i is !null if it tracks the sign. What about this case:

assert:
   forall(int|null i):
       if:
           !(i is null || i >= 0)
       then:
           0 < i

Perhaps it works if the type checker just views it as this (again by tracking sign):

assert:
   forall(int|null i):
       if:
           !(i is null) && (i < 0)
       then:
           0 < i

These cases are all one reason why we separated variables out into their "versions", in order that those version can be typed differently according to their usage.

[DavePearce]

Right, some further points after a little bit of investigation:

The theorem prover itself is quite happy handling flow typing. Disable the type checker, and the above all pass.

This certainly makes me ponder whether or not the type checker is actually needed. Some mitigating factors:

1. The type checker is needed to resolve function invocations, etc.
2. Ideally, we want to avoid duplicating the code in getReturnType().
3. The parser could introduce alias declarations, but this might cause problems with retyping.

Overall, hmmm...

... I suppose we could introduce an interface for expression typing. Say, ExpressionTyper or TypeInference ?

One of the advantages here is that getReturnType(TypeSystem) currently has that ugly parameter (which is necessary for extracting readable array types, etc) and we could get rid of it. A TypeInference could then be part of a TypeSystem perhaps?

Another advantage here is that TypeInference instances could be composable in some way ...