A type checker plugin for GHC that can solve /equalities/ of types of kind
'Nat', where these types are either:
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.