Package Info


GHC typechecker plugin for types of kind GHC.TypeLits.Nat


A type checker plugin for GHC that can solve /equalities/ 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:

' (x + 2)^(y + 2) '


' 4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2 '

Because the latter is actually the 'SOP' normal form of the former.

To use the plugin, add the

' OPTIONS_GHC -fplugin GHC.TypeLits.Normalise '

Pragma to the header of your file.

License: BSD-2-Clause



Package Version Update ID Released Package Hub Version Platforms Subpackages
0.5.3-bp150.1.3 info GA Release 2018-07-30 15
  • AArch64
  • ppc64le
  • x86-64
  • ghc-ghc-typelits-natnormalise
  • ghc-ghc-typelits-natnormalise-devel