Type Tests for Negation Types

[DavePearce]

The following from TypeEquals_Valid_57 fails at JVM verification time:

type nat is (int x) where x >= 0

function f(int|null x) -> nat:
    //
    if x is !nat:
        return 0
    else:
        return x

The reason is not completely clear. The bytecode looks like this:

         0: aload_0
         1: getstatic     #22                 // Field constant$1:Lwyjc/runtime/WyType;
         4: swap
         5: invokevirtual #12                 // Method wyjc/runtime/WyType.is:(Ljava/lang/Object;)Lwyjc/runtime/WyBool;
         8: invokevirtual #34                 // Method wyjc/runtime/WyBool.value:()Z
        11: ifne          22
        14: aload_0
        15: checkcast     #28                 // class java/math/BigInteger
        18: astore_0
        19: goto          41
        22: aload_0
        23: astore_0
        24: aload_0
        25: invokestatic  #31                 // Method nat$typeof:(Ljava/math/BigInteger;)Z
        28: ifeq          34
        31: goto          14
        34: getstatic     #1                  // Field constant$0:Ljava/math/BigInteger;
        37: areturn
        38: goto          43
        41: aload_0
        42: areturn
        43: return

The problem is that, on the true branch, it needs to perform a checkcast before calling nat$typeof(). For some reason it's not doing that. The type test being used should be against !int. So, on the true branch, it shouldn't need to check the invariant. In fact, it should be checking the invariant on the false branch and, if the invariant doesn't hold, branching back to the true branch.