Implemented isinstance inference

[mostafa-abdullah]

There's a conceptual problem with the inference of isinstance. See the following example:

def f(x):
    if isinstance(x, A):
         return x.f()
    else:
        return x + 2

The type of variable x in the then part is A, while it is int in the else part. As a result, the type of function argument x is inferred to be the super-type of both, which is object. As a result, a function call like f("string") will be allowed because string <: object, which makes it unsound.

What do you think?

[mostafa-abdullah]

I think to solve this problem, the type of argument needs to be Union[int, A]

[marcoeilers]

So to summarize (from my point of view) what we just discussed:

• This function is an unfortunate special case; it can only be typed properly without getting dead code if we have union types. But that's a problem with the function, not with the handling of isinstance.
• The type of x needs to be a subtype of int. In general, anything that happens in the function and isn't guarded by an isinstance (and that includes the else block) must work with the normal type of x.
• The type of x in the then-branch can be assumed to be A, no matter what it is outside the branch ( guess unless it is something more general outside; otherwise we'd get weird behavior if someone does if isinstance(x, object) for no reason).
• If we give x the type int, the then branch is dead code. That's better than assigning an invalid type to x.
• Obviously, having dead code like this isn't great. We could either decide not to allow this (and add a constraint that the normal type of x has to be a supertype of A in this case), in which case we wouldn't be able to type this function. Or we could add a soft constraint that says the same thing, so that we avoid creating dead code if possible. In this case that wouldn't be possible, but we would still be able to type the function.

[mostafa-abdullah]

Implemented isinstance as agreed.

The overall type of the variable compared in the isinstance test is inferred from only the else branch (and of course the rest of the program).

The isinstance test is currently limited to a simple test like the following:

if isinstance(x, y):
    pass

Where x is a variable. Doing conjunction or disjunction in the isinstance test (like isinstance(x,y) or isinstance(x,z)) is NOT possible.

Example:

class A:
    def f(self):
        return 1

class B:
    def g(self):
        return 1

def f(x):
    if isinstance(x, A):
        res = x.f()
    elif isinstance(x, B):
        res = x.g()
    else:
        res = x + 1
    return res

f := Callable[[int], int]

TODO: use built in types in isinstance test.

[marcoeilers]

Does the TODO mean that we can't currently do something like if isinstance (x, int): ...? If so, why is that more difficult? Also, I assume when you say doing conjunctions etc is not possible, you mean that we don't change the type of the variable in question in those cases, but users can still write that code (and will simply have to manually cast the variable to a different type in the following block)? Or do we crash or report an error?

Otherwise, looks good to me.

[mostafa-abdullah]

Does the TODO mean that we can't currently do something like if isinstance (x, int): ...?

Yes this is not currently supported.

If so, why is that more difficult?

The reason is that in every function call subtype axioms are added between the types of the arguments the corresponding ones in the function definition, however we don't have Z3 types for built-ins like int. To get it working, we need to have z3 constants corresponding to the built-in types in our context, however they will conflict with the stub functions int(x), float(x), str(x), etc. We can also special case this by ignoring these axioms in an isinstance call. What do you think?

you mean that we don't change the type of the variable in question in those cases, but users can still write that code (and will simply have to manually cast the variable to a different type in the following block)?

Yes exactly. We do nothing and the user must cast the variables.