Solving Constraints During Type Inference - WITS'24

Explore the intricacies of type inference in GHC through this 33-minute conference talk from ACM SIGPLAN's WITS'24. Delve into Simon Peyton Jones' comprehensive overview of GHC's unique approach to type inference, which employs Pottier and Rémy's method of generating and solving constraints separately. Gain insights into key concepts such as bidirectional type inference, implication constraints, level numbers and promotion, evidence generation, and quantified constraints. Learn how these elements work together to create a robust type inference engine, and understand the challenges and solutions encountered during its implementation. Discover how GHC's approach supports advanced features like type abstraction and GADTs, and explore the interplay between type-level and term-level evidence generation.

[WITS'24] Solving constraints during type inference