ghc-typelits-natnormalise

A type checker plugin for GHC that can solve equalities and inequalities of types of kind Nat, where these types are either: Type-level naturals Type variables Applications of the arithmetic expressions (+,-,*,^). It solves these equalities by normalising them to sort-of SOP (Sum-of-Products) form, and then perform a simple syntactic equality. For example, this solver can prove the equality between: and Because the latter is actually the SOP normal form of the former. To use the plugin, add the Pragma to the header of your file.