Type Checker

The mypy type checker checks if a program has type errors and infers the types of variables and expressions. It is implemented as an AST visitor.

The mypy.checker.TypeChecker class (in mypy/checker.py) takes as an input a semantically analyzed file AST (instance of nodes.MypyFile). It produces a dict from AST expression nodes to types (the _type_maps attribute).

Type checking expressions happens in mypy.checkexpr.ExpressionChecker (in mypy/checkexpr.py). It also binds attribute references in the AST to the target attribute/method. This can only be done in type checking, since we need the inferred static type of receiver objects to find the target attribute.

A simple example

Consider this simple program:

x = 1
x + "a"

Here's a line-by-line analysis of what happens during type checking.

x = 1

• Infer type builtins.int for 1 (trivial)
• Infer type builtins.int for x

x + "a"

• Infer type builtins.int for x (from type inferred above)
• Infer type builtins.str for "a" (trivial)
• Look up type of x.__add__ by finding the type of __add__ in the symbol table of class builtins.int (callable type int → int)
• Check the operand types against the type of x.__add__: report error

(The reality is slightly more complicated -- the type of x.__add__ is an overloaded callable, with multiple variant signatures.)

Basic inference of types

Each subexpression AST node is assigned an inferred type. For example, for expression

  foo(bar, x.y) 

the type checker will infer types for 4 subexpressions: foo, bar, x, x.y and foo(bar, x.y). It type check arguments types against the type of foo (which is likely a CallableType), and the type of entire expression is derived from the return type of the type of foo.

Attribute expressions with Any receiver types are special, and cannot be bound during type checking. Instead, the type of expression x.y is just Any if the type of x is Any.

Type inference of generic types

When inferring generic types, mypy uses bidirectional local type inference. This means that expression type inference first tries to use the "type context" to infer any type variables. If this doesn't succeed, mypy falls back to using the types of subexpressions for type inference.

The type context is the "expected" type for an expression. For example, in an assignment statement the type of the LHS is the type context for the RHS. In a function call, the declared formal argument type (from a type signature) is used as a type context for inferring the type of the actual argument in a call expression.

This example relies on type context to infer the type of a list expression:

x: list[object] = [1]

The type context for [1] is list[object] (from the declared type of the LHS), and this directs mypy to infer type list[object] as the type of [1] instead of list[int]. Note that since list is invariant, the latter type would generate a type error due to incompatible types in assignment.

In this cases mypy uses the operand types (list item types) to infer the type of a list expression, since there is no type context (the type of x is being inferred here):

x = [1]

Now the type of [1] is inferred as list[int], and this type is propagated as the inferred type of x.

Type checking with Any types

Type compatibility in mypy is different from languages such as Java. The Any type is compatible with every other type, and vice versa. This is in addition to normal nominal subtyping, which is similar to Java.

Examples:

• int is compatible with Any
• Any is compatible with int
• list[int] is compatible with list[Any]
• list[Any] is compatible with list[int]
• list[int] is compatible with Sequence[Any] (subtyping + Any types)

TODO describe type operations

More about type compatibility

int, float and other built-in types are (mostly) not special. Python has no equivalent to the primitive types in Java. However, as a special case, int is treated as compatible with float even though there is no subclass relationship (this is for convenience only and dictated by PEP 484).

Mypy also support structural subtyping through protocols.

Join and Meet

Inside the type checker, two important operation are performed on the types: join and meet.

Intuitively, given two types X and Y, one can think of join(X, Y) as a type that we don't know whether it is X or Y, and meet(X, Y) is a type that we know to be compatible with both X and Y. However, join and meet only approximate this notion.

The hierarchy of classes and types in Python is generally built along a lattice. Consider the following classes:

class A:
    def foo(self): pass
class B:
    def bar(self): pass
class AB(A, B):
    pass

This hierarchy can be depicted as follows (where X -> Y mean "X is a subtype of Y", often written X <: Y):

object <- A
  ^       ^
  |       |
  B  <-  AB 

Most of mypy's type system can be put into such diagrams.

Given such a structure, join(X, Y) mean "take the closest common ancestor of X and Y". meet(X, Y) mean "take the closest common descendant of X and Y". So in the above example, join(A, B) will be object. meet(A, B) is somewhat more problematic, since we don't know at every point what are all the possible classes that inherit from both A and B. Instead, we can look at a similar example, involving Union:

Union[A, B, C] <- Union[B, C]  <- C
  ^                ^
  |                |
Union[A, B]   <-   B 
  ^
  |
  A

This diagram shows that meet(Union[A, B], Union[B, C]) is simply B. (In this diagram, join(A, B) will be Union[A, B]. This is the most precise join possible, but mypy does not take this approach, since it will make type checking much slower (or even non-terminating), and will force mypy to emit long and incomprehensible error messages; Unions usually do not have direct counterpart in the source code).

The join operation is applied, for example. In list literals:

x = [A(), B()]

An element in the list x is either A or B. If there is no other common base class, it must be object (we could infer Union[A, B], but for largely historical reasons mypy doesn't do this).

The meet operation is usually related to flow of control:

def foo(x: Union[A, B, AB]):
    if isinstance(x, B):
       # here x is meet(Union[A, B, AB], B) which is Union[B, AB]
       ...

Inside mypy there's a type named UninhabitedType which is the meet of all other types combined (this type is sometimes called Bottom, Bot or Nothing in the literature). For this type, given some other type T, it holds that join(Bot, T) = T, and meet(Bot, T) = Bot.

Meet and join are commutative operations: meet(A, B) = meet(B, A) and join(A, B) = join(B, A).

Constraint solver

Mypy uses a fairly simple constraint solver to solve values for type variables in calls to generic functions.

Consider this example generic function:

T = TypeVar("T")

def f(x: T, y: Sequence[T]) -> list[T]:
    return [x, y[0]]

Now let's see what happens when we type check this call:

f(1, [bool])

We first match the inferred argument types (int and list[bool]) to the types in the signature (T and Sequence[T]) and produce these constraints:

• T :> int
• T :> bool

Here :> means "RHS is compatible with the LHS". We find the most specific (based on certain criteria) type that matches these constraints by calculating a type join (see above for more about joins):

• T = join(int, bool) = int

Note that bool is a subclass of int in Python!

Now we substitute T with int in the signature of f to infer the type of f in the call expression:

Callable[[int, Sequence[int]], list[int]]