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.
Treating subtraction as addition with a negated number
If you are absolutely sure that your subtractions can never lead to (a locally) negative number, you can ask the plugin to treat subtraction as addition with a negated operand by additionally adding:
{# OPTIONS_GHC fpluginopt GHC.TypeLits.Normalise:allownegatednumbers #}
to the header of your file, thereby allowing to use associativity and commutativity rules when proving constraints involving subtractions. Note that this option can lead to unsound behaviour and should be handled with extreme care.
When it leads to unsound behaviour
For example, enabling the allownegatednumbers feature would allow you to prove:
(n  1) + 1 ~ n
without a (1 <= n)
constraint, even though when n is set to 0 the
subtraction n1
would be locally negative and hence not be a natural number.
This would allow the following erroneous definition:
data Fin (n :: Nat) where FZ :: Fin (n + 1) FS :: Fin n > Fin (n + 1) f :: forall n . Natural > Fin n f n = case of 0 > FZ x > FS (f @(n1) (x  1)) fs :: [Fin 0] fs = f <$> [0..]
When it might be Okay
This example is taken from the mezzo library.
When you have:
  Singleton type for the number of repetitions of an element. data Times (n :: Nat) where T :: Times n   An element of a "runlength encoded" vector, containing the value and  the number of repetitions data Elem :: Type > Nat > Type where (:*) :: t > Times n > Elem t n   A lengthindexed vector, optimised for repetitions. data OptVector :: Type > Nat > Type where End :: OptVector t 0 (:) :: Elem t l > OptVector t (n  l) > OptVector t n
And you want to define:
  Append two optimised vectors. type family (x :: OptVector t n) ++ (y :: OptVector t m) :: OptVector t (n + m) where ys ++ End = ys End ++ ys = ys (x : xs) ++ ys = x : (xs ++ ys)
then the last line will give rise to the constraint:
(nl)+m ~ (n+m)l
because:
x :: Elem t l xs :: OptVector t (nl) ys :: OptVector t m
In this case it's okay to add
{# OPTIONS_GHC fpluginopt GHC.TypeLits.Normalise:allownegatednumbers #}
if you can convince yourself you will never be able to construct a:
xs :: OptVector t (nl)
where nl is a negative number.