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.

Themypy.checker.TypeChecker class (inmypy/checker.py) takes as an input a semantically analyzed file AST (instance ofnodes.MypyFile). It produces a dict from AST expression nodes to types (the_type_maps attribute).

Type checking expressions happens inmypy.checkexpr.ExpressionChecker (inmypy/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.

Consider this simple program:

x=1x+"a"

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

x = 1

• Infer typebuiltins.int for1 (trivial)
• Infer typebuiltins.int forx

x + "a"

• Infer typebuiltins.int forx (from type inferred above)
• Infer typebuiltins.str for"a" (trivial)
• Look up type ofx.__add__ by finding the type of__add__ in the symbol table of classbuiltins.int (callable typeint → int)
• Check the operand types against the type ofx.__add__:report error

(The reality is slightly more complicated -- the type ofx.__add__ is anoverloaded callable, with multiple variant signatures.)

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 andfoo(bar, x.y). It type check arguments types against the type offoo (which is likely aCallableType), and the type of entire expression is derived from the return type of the type offoo.

Attribute expressions withAny receiver types are special, and cannot be bound during type checking. Instead, the type of expressionx.y is justAny if the type ofx isAny.

When inferring generic types, mypy usesbidirectional 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] islist[object] (from the declared type of the LHS), and this directs mypy to infer typelist[object] as the type of[1] instead oflist[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 ofx is being inferred here):

x= [1]

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

Type compatibility in mypy is different from languages such as Java. TheAny 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 withAny
• Any is compatible withint
• list[int] is compatible withlist[Any]
• list[Any] is compatible withlist[int]
• list[int] is compatible withSequence[Any] (subtyping +Any types)

TODO describe type operations

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 withfloat even though there is no subclass relationship (this is for convenience only anddictated by PEP 484).

Mypy also support structural subtyping through protocols.

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 ofjoin(X, Y) as a type that we don't know whether it is X or Y, andmeet(X, Y) is a type that we know to be compatible withboth X and Y. However, join and meet only approximate this notion.

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

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

This hierarchy can be depicted as follows (whereX -> Y mean "X is a subtype of Y", often writtenX <: 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 beobject.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, involvingUnion:

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 listx is either A or B. If there is no other common base class, it must beobject (we could inferUnion[A, B], but for largely historical reasons mypy doesn't do this).

The meet operation is usually related to flow of control:

deffoo(x:Union[A,B,AB]):ifisinstance(x,B):# here x is meet(Union[A, B, AB], B) which is Union[B, AB]       ...

Inside mypy there's a type namedUninhabitedType which is the meet of all other types combined (this type is sometimes calledBottom,Bot orNothing 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).

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")deff(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 andlist[bool]) to the types in the signature (T andSequence[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 thatbool is a subclass ofint in Python!

Now we substituteT withint in the signature off to infer the type off in the call expression:

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