Type Inference in GHC
summary
GHC performs type inference in two phases: gathering then solving — it traverses code to emit a set of typed equations and class constraints, then runs a solver. The solver is unification-based for plain types and uses instance lookup to turn class constraints into givens. Pattern matching and GADTs introduce implication/existential constraints that must be solved locally, which makes some valid programs hard for the solver to find even though the approach generally works and is what GHC emits as equations.
AI-written summary · about
chapters (6)
- 0:00Start
- 15:09Instantiation
- 21:38Failure Cases
- 22:09Infinite Type
- 22:52Types in Haskell
- 38:25Type Checking a Pattern Matching
related talks
39mEverything You Always Wanted to Know About Type Inference
33mSolving constraints during type inference
19mType Inference Logics
34mType inference for application spines
01h 35mSecrets of the GHC Typechecker in 100 Type Declarations
49mMaking sense of the Haskell type system
30mConstrained generation of well-typed programs
56mOn Type-Based Techniques for Program Manipulation