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) '
and
' 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.
| Package Version | Update ID | Released | Package Hub Version | Platforms | Subpackages |
|---|---|---|---|---|---|
| 0.5.3-bp150.1.3 info | GA Release | 2018-07-30 | 15 |
|
|