Haskell is a big language, so GHC’s type inference engine is also big: it consists of 50,000 lines of Haskell, and another 42,000 lines of comments.
In this talk I give an overview of how it works, including
- A sketch of how Trees That Grow is applied to GHC
- How elaboration works: as well as checking for type-correctness, the type inference engine must produces an elaborated program, with type and dictionary abstractions and applications.
- The idea of separating generating constraints from solving constraints, including the key idea of implication constraints.
- How level numbers work.
This talk is part of the 2023 GHC Contributors Workshop. That link takes you to a page that has videos of all the other talks – highly recommended.