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

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 -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers #-}

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 allow-negated-numbers 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 n-1 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 @(n-1) (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 "run-length encoded" vector, containing the value and
-- the number of repetitions
data Elem :: Type -> Nat -> Type where
    (:*) :: t -> Times n -> Elem t n

-- | A length-indexed 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:

(n-l)+m ~ (n+m)-l

because:

x  :: Elem t l
xs :: OptVector t (n-l)
ys :: OptVector t m

In this case it's okay to add

{-# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers #-}

if you can convince yourself you will never be able to construct a:

xs :: OptVector t (n-l)

where n-l is a negative number.