Type Invariants for Haskell

Multi-parameter type classes, functional dependencies, and re-cently GADTs and open type families open up opportunities to use complex type-level programming to let GHC’s type checker verify various properties of your programs. But type-level code is special in that its correctness is crucial to the safety of the program; so except in those cases simple enough for the type checker to see trivially that the code is correct (or harmless), type-level programs need to come with a specification of their properties together with their proof. In this article, we propose an extension to Haskell that allows the specification of invariants for type classes and open type fam-ilies, together with accompanying evidence that those invariants hold. To accommodate the open nature of type classes and type families, the evidence itself needs to be open and every subcase o