A Quick Look at Impredicativity
summary
A design called Quick Look phase adds a localized instantiation pass to GHC that discovers impredicative instantiations by peeking at arguments and nested applications, turning guarded instantiation into simple equality and falling back to monomorphic instantiation when needed. The prototype integrates with type classes, type families, GADTs and visible type application, requires only 450 lines added to GHC’s ~90k-line typechecker, and succeeds on many previously untypable examples.
AI-written summary · about
chapters (13)
- 0:00Intro
- 1:31System F
- 2:08Impredicative Inference
- 2:55The Swamp
- 3:19Quick Look Example
- 5:00Guardedness
- 6:44QL May Guess No Information
- 7:14Looking at the Result
- 8:21When to Stop Quick Looking?
- 9:49Our Goals
- 10:54Localised
- 11:30More in the Paper
- 12:34Quick Look Impredicativity
related talks
34mType inference for application spines
01h 02mType Inference in GHC
28mImplicit modules, a middle step towards modular implicits
30mDotty and types: the story so far
28mQuotient Polymorphism
21mRefinement Type Refutations
23mImpredicative Observational Equality
22mIntensional Analysis of Typed Template Haskell Quotations