Solving constraints during type inference
summary
GHC implements Pottier and Rémy’s generate-and-solve architecture: a constraint generator that walks the syntax tree and a smaller, subtler solver that resolves equalities, class constraints and implication constraints. The talk argues this reduces order-dependence and isolates complexity, shows how level numbers prevent illegal unifications, and explains evidence/coercion generation and elaboration to System F using mutable unification variables. Concrete numbers: ~11,000 LOC for generation, ~6,000 for the solver, ~9,000 for error handling. The implementation is production-ready and scales to GADTs and quantified constraints.
AI-written summary · about
chapters (7)
- 0:00Introduction and monads
- 1:41Program elaboration
- 5:22The constraint approach
- 10:10Generating constraints
- 16:02Constraint solving
- 19:05Level numbers and implications
- 26:28Advanced topics and Q&A
related talks
30mConstrained generation of well-typed programs
01h 02mType Inference in GHC
35mThe Mastermind behind Refinement Types
18mConcrete Type Inference for Code Optimization using Machine Learning with SMT S...
19mType Inference Logics
56mOn Type-Based Techniques for Program Manipulation
01h 38mGHC Core Optimisations
20mGenerating Well-Typed Terms that are not "Useless"