Why Building a Python Type Checker Is So Hard

In large Python codebases, type checkers catch bugs early and power editor autocompletion and type hints. Yet they often flag code that runs perfectly in production—and as projects grow, check times can crawl, stalling CI pipelines and freezing editor feedback loops. Eliminating these headaches takes far more than just parsing type annotations.

Over the past decade, four major tech companies—Dropbox, Microsoft, Meta, and Astral—have assembled dedicated full-time engineering teams, pouring dozens of core developers into building and maintaining Python type checkers.

Written in Python, TypeScript, OCaml, and Rust, these tools all grapple with the same core tensions: deciphering Python’s fluid dynamic semantics, keeping false positives to a minimum, and delivering near-instant results for massive codebases and editors alike.

The Core Dilemma: Gradual Typing and Dynamic Semantics

Python lets developers adopt type hints incrementally: annotate a few functions today, leave the rest alone, and run the code without changes. Modern Python’s type system is built on the theory of gradual typing, introduced by Jeremy Siek and Walid Taha in 2006. For a checker, this means it must simultaneously handle code with complete and incomplete type information.

Type annotations help the checker catch incompatible operations, but unannotated or partially checked code can still blow up with a type error at runtime. Consequently, passing type checks does not guarantee the absence of runtime type errors. A “sound” type system provides an explicit guarantee: once a program passes type checking, runtime type errors of the kind guarded by the system cannot happen. This does not mean the program is free of other bugs.

 Python code
   |
   +-- Sufficient type info
   |     |
   |     v
   |   Check type compatibility
   |
   +-- Incomplete type info
         |
         v
       May fall back to Any
         |
         v
       May miss type errors

PEP 483 introduced is-consistent-with to determine whether one type can be assigned to another. It preserves standard subtyping rules: if a value of one type can be safely used where another is expected, the assignment is allowed. In addition, it allows Any to be assigned to and from any type.

When Any is involved, however, this compatibility relation lacks transitivity: just because A is consistent with B, and B is consistent with C, it does not follow that A is consistent with C.

Otherwise, because int is consistent with Any, and Any is consistent with str, the system would deduce the absurd conclusion that int can be used as str. As PEP 483 bluntly put it:

“In essence, Any declares a fallback to dynamic typing and shuts up complaints from the static checker.”

PEP 484 stated the type checker’s role just as plainly:

“Essentially, such a type checker acts as a very powerful linter.”

For developers, this trade-off manifests in two ways: working code getting flagged as erroneous (false positives), and buggy code slipping through undetected (false negatives). Checker teams must constantly tune their rules to suppress false positives while catching as many genuine errors as possible.

Curbing False Positives—and Limiting Scope

Eric Traut, the creator of pyright, once noted in the official Python typing forum that type safety is not a checker’s overarching goal—many design decisions come down to trade-offs between false positives and false negatives.

Specifications describe how rules ought to work; in practice, applying them across millions of lines of production code forces teams to untangle endless edge cases and tweak heuristics based on bug reports. With over 2,700 open issues on GitHub as of October 2026, mypy’s tracker is a living record of this relentless maintenance burden.

Ori Roth’s 2022 research paper, “Python Type Hints are Turing Complete”, proved that Python type annotations can simulate the computation of ordinary programs. As a result, what appears to be a simple check between two types can actually demand computations as complex as running a program itself.

This leads directly to undecidability: no universal algorithm exists that, given any two valid types, is guaranteed to terminate in finite time and correctly decide whether one is a subtype of the other. Specific instances can be resolved, but no algorithm can guarantee an answer in every case; even if a checker is willing to search indefinitely, there is no guarantee that search will ever halt.

For type checker implementers, this means drawing hard boundaries around analysis depth. When generics nest deeply, or when type comparisons cycle back to the same subproblem recursively, the tool must decide where to stop. That boundary keeps the checker from running indefinitely, at the cost that some legitimate type constructs may not be fully analyzed.

Mutable Containers, Decorators, and Dynamic Attributes

Beyond theoretical limitations, Python’s ability to mutate objects and functions at runtime makes static analysis even trickier:

• Type constraints on mutable containers (invariance): An int can be passed where a float is expected, but a list[int] cannot be passed to a function expecting list[float]. If the function calls append(3.14), a float would pollute a list annotated as containing integers; subsequent integer-specific operations by the caller (such as bitwise shifts) would crash. The checker must account for mutations, rather than merely verifying whether the current element types are compatible.
• Control flow branching and type narrowing: When code checks if x is not None:, the checker must trace data flow along execution paths, refining the type of x to exclude None. With complex nested loops and conditional branches, the computation required to explore analysis paths swells rapidly.
• Decorators mutating function signatures: Decorators can preserve, add, or strip function parameters. Metadata preserved by functools.wraps (such as function names and docstrings) cannot express these type transformations. ParamSpec captures an entire parameter list as a unit, and Concatenate describes prepending arguments to it, but tracking these higher-order relationships puts immense demands on the type engine.
• Dynamic attributes and monkey-patching: Classes can intercept attribute access dynamically via __getattr__, or mutate __dict__ at runtime to inject or overwrite attributes. A checker cannot learn every attribute from class definitions alone; it must account for changes at runtime.

Academic research has documented this exact friction: the paper Python 3 Types in the Wild (DLS 2020) found that real-world Python codebases heavily utilizing dynamic features trigger a flood of false positives in type checkers. Some Python code runs without issue, yet checkers cannot glean enough information from the source and annotations to confirm whether its types are compatible.

A Moving Target: Ten Years and 17 PEPs Later

Type checkers face a specification that never sits still. Every new feature can alter how tools parse code, infer types, and cache intermediate analysis results.

Since PEP 484 was introduced in 2014, the Python community has accepted more than 17 typing-related PEPs:

These PEPs have continually expanded Python’s type syntax—such as PEP 695 introducing the type alias statement in Python 3.12—while fundamentally reshaping internal checker architectures. Parsers must learn new grammar, constraint solvers must resolve new type arguments, and serialization formats for incremental caches must adapt.

Furthermore, the official typing specification often lags behind real-world demands. The specification itself admits that it was “pasted together and reorganized” from multiple PEPs and is “not necessarily a coherent whole.”

Because formal standards cannot keep up with every practical need, major tools like mypy and pyright had to blaze their own trails, creating countless undocumented, de facto standards. To resolve these divergences, the community accepted PEP 729 in 2023, establishing the Typing Council and driving conformance test suites. Even so, checker maintainers still face the ongoing task of aligning implementations case by case to iron out discrepancies.

The Ecosystem Integration Burden: Where Does Type Information Come From?

A type checker cannot operate in a vacuum: it must know what functions the standard library and thousands of third-party packages export, what arguments they accept, and what types they return.

typeshed serves as a vital central repository, maintaining type declarations for the standard library and select third-party packages. Libraries can also bundle their own inline type annotations or stub files, rather than relying entirely on typeshed.

• Over 5,300 stub files: As of September 2026, typeshed maintains 752 standard library stubs plus stub directories for 204 third-party packages, totaling more than 5,300 stub files (.pyi files containing type signatures without implementation code).
• Third-party maintenance disconnect: The vast majority of third-party stubs are not maintained by upstream library authors. Instead, over 400 volunteers across typeshed write and publish them to PyPI as separate packages (such as types-requests). When an upstream library updates its API, its corresponding stubs frequently fall out of sync.
• Gaps across popular packages: Statistics shared on the official typing forums indicate that among the top 2,000 most-downloaded packages on PyPI, only about 10% ship with typeshed stubs or dedicated stub packages (as of November 2024).

Any new type checker must parse and respect the full spectrum of type syntax across thousands of stub files in typeshed, while properly ingesting inline annotations distributed by packages. When encountering unannotated dependencies, it must decide how to degrade gracefully. Beyond the core type-checking algorithms, keeping up with ecosystem compatibility requires non-stop maintenance.

Performance and Architecture: A History of Rewrites Across Four Languages

A modern type checker must satisfy two competing performance profiles: batch CI checks that scan millions of lines concentrated in a monorepo, and interactive IDE workflows that demand sub-second latency for every keystroke.

 Architecture of Major Python Type Checkers

 +----------------------------------------------+
 | mypy (Python + C / mypyc)                    |
 | - Whole-program batch analysis               |
 +----------------------------------------------+

 +----------------------------------------------+
 | pyright (TypeScript / Node.js)               |
 | - Lazy evaluation for responsive IDE         |
 +----------------------------------------------+

 +----------------------------------------------+
 | Pyrefly / ty (Rust)                          |
 | - Multi-threaded analysis                    |
 +----------------------------------------------+

To balance the throughput needed for large monorepos with the responsiveness required by IDEs, teams took radically different architectural paths—with several ultimately opting for ground-up rewrites:

1. mypy (Python + C / mypyc): Early versions processed files sequentially, hitting severe performance bottlenecks as codebases scaled. The team later introduced incremental caching to reuse prior analysis and built a persistent daemon (dmypy) to eliminate repeated startup overhead. They also invested months in developing mypyc, a dedicated compiler that translates type-annotated Python into C extension modules, yielding a roughly 4x speedup.
2. pyright (TypeScript / Node.js): Microsoft released pyright in 2019, touting a 3x to 5x speed advantage over mypy. Engineered from day one as a language server for code editors, it relies on lazy, demand-driven evaluation—computing types only when requested—paired with a fault-tolerant parser capable of analyzing incomplete code as the user types. It soon became the underlying engine behind Pylance, VS Code’s official Python extension.
3. Pyre → Pyrefly (OCaml → Rust): Meta originally built Pyre in OCaml to type-check Instagram’s massive codebase. In 2025, Meta announced Pyrefly, a complete rewrite in Rust by a 15-person team, specifically focused on delivering real-time responsiveness for modern IDEs.
4. ty (Rust): Following Ruff and uv, Astral assembled a 10-person team to build ty, an entirely new type checker. Independent benchmarks showed check speeds 9x to 21x faster than mypy’s. Astral called ty the most complex product they had ever built, requiring deep expertise across type theory, runtime semantics, and the real-world package ecosystem.

The True Cost of Human Investment

Every challenge described above demands continuous, long-term engineering investment: triaging false positives, tracking evolving PEPs, tracing package APIs, and pushing check times down on massive codebases.

Jukka Lehtosalo, reflecting on mypy’s evolution, once observed:

“Architectural decisions made early on can cause ongoing pain years later.”

Since late 2015, Dropbox has maintained a full-time core team to develop mypy, iteratively stress-testing and refining it against millions of lines of production Python.

Here is an overview of the primary implementation languages, publicly disclosed team sizes, and development milestones across the major projects:

A Python type checker must navigate multiple conflicting constraints at once: code is often unannotated, objects mutate at runtime, specifications and third-party APIs shift constantly, and both massive monorepos and responsive editors demand near-instant answers. Engineering teams must strike a delicate balance between analysis depth, false positive rates, and raw execution speed to deliver real-time IDE feedback.

Every single false positive or momentary lag a developer experiences in their editor is tied to a web of trade-offs across type theory, data-flow analysis, package stubs, and cache architecture. These four companies have spent the past decade funding dedicated teams for a single reason: to prevent these fundamental constraints from standing in the way of everyday engineering.