Bug with Flow Typing in TypeChecker

[DavePearce]

This is a bug related to flow typing in TypeChecker as released in v0.1. The following assertion fails:

type Expr is (int|BinOp|Var this)
type BinOp is ({Expr lhs, Expr rhs} this)
type Var is ({int[] id} this)

assert:
    forall(Expr e, !int&!{int[] id}&Expr e3):
        if:
            e3 == e
            e is !int
            e is !{int[] id}
        then:
            e3.lhs is Expr

The type checker complains expected record type for e3 in e3.lhs. It should be reasonably clear that e3 has type BinOp, so it should be fine.

[DavePearce]

This is not so much a bug, as it is a simply a hole in the current implementation. Specifically, in ReadableRecordExtractor the method subtract(Type.Record, Type.Record) is not fully implemented. Some examples:

{int|null x} - {null x} ===> {int x}

{int x} - {null x} ===> {int x}

{int|null x, int y} - {null x, int y} ===> {int x, int y}

{int|null x, int y} - {null x, ...} ===> {int x, int y}

{int|null x, ... } - {null x} ===> {int x, ...}

{int|null x, ... } - {null x, int y} ===> ????

For the last case, it's really not clear what the resulting type should be...

[DavePearce]

At the moment, the essential problem is that the current implementation does this:

{T1 x, T2 y} - {T3 x, T4 y} ===> { (T1&!T3) x, (T2&!T4) y}

But, this leads to the following error (amongst other things):

{int|null x, int y} - {null x, int y} ===> { ((int|null)&!null) x, (int&!int) y }

Here, the type for y is clearly incorrect. Perhaps the translation should instead be this:

{T1 x, T2 y} - {T3 x, T4 y} ===> { (T1&!T3) x, T2 y} | { T1 x, (T2&!T4) y}