GHC typechecker plugin for types of kind GHC.TypeLits.Nat.
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-ofSOP (Sum-of-Products) form, and then perform a simple syntactic equality.
For example, this solver can prove the equality between:
(x + 2)^(y + 2)
and
4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^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.
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-ofSOP (Sum-of-Products) form, and then perform a simple syntactic equality.
For example, this solver can prove the equality between:
(x + 2)^(y + 2)
and
4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2
Because the latter is actually the SOP normal form of the former.
To use the plugin, add
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
To the header of your file.