General Terms Algorithms, Languages

We report on an extension of Haskell with open type-level func-tions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key techni-cal challenge of entailment checking; and we give a novel, decid-able, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use