Copyright  (C) 20152016 University of Twente 2017 QBayLogic B.V. 

License  BSD2 (see the file LICENSE) 
Maintainer  Christiaan Baaij <christiaan.baaij@gmail.com> 
Safe Haskell  None 
Language  Haskell2010 
Extensions 

A type checker plugin for GHC that can solve equalities of types of kind
Nat
, where these types are either:
 Typelevel naturals
 Type variables
 Applications of the arithmetic expressions
(+,,*,^)
.
It solves these equalities by normalising them to sortof
SOP
(SumofProducts) 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.