# ghc-typelits-natnormalise

GHC typechecker plugin for types of kind GHC.TypeLits.Nat http://www.clash-lang.org/

Version on this page: | 0.3 |

LTS Haskell 8.23: | 0.5.3 |

Stackage Nightly 2017-07-25: | 0.5.3 |

Latest on Hackage: | 0.5.3 |

**Christiaan Baaij**

**christiaan.baaij@gmail.com**

#### Module documentation for 0.3

# ghc-typelits-natnormalise

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.

## Changes

# Changelog for the `ghc-typelits-natnormalise`

package

## 0.5.3 *May 15th 2017*

Add support for GHC 8.2

## 0.5.2 *January 15th 2017*

Fixes bugs: * Reification from SOP to Type sometimes loses product terms

## 0.5.1 *September 29th 2016*

Fixes bugs: * Cannot solve an equality for the second time in a definition group

## 0.5 *August 17th 2016*

Solve simple inequalities, i.e.:

`a <= a + 1`

`2a <= 3a`

*`1 <= a^b`

## 0.4.6 *July 21th 2016*

- Reduce "x^(-y) * x^y" to 1
- Fixes bugs: * Subtraction in exponent induces infinite loop

## 0.4.5 *July 20th 2016*

Fixes bugs: * Reifying negative exponent causes GHC panic

## 0.4.4 *July 19th 2016*

Fixes bugs: * Rounding error in

`logBase`

calculation

## 0.4.3 *July 18th 2016*

Fixes bugs: * False positive: "f :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)"

## 0.4.2 *July 8th 2016*

Find more unifications:

`(2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]`

`a^d * a^e ~ a^c ==> [c := d + e]`

*`x+5 ~ y ==> [x := y - 5]`

, but only when`x+5 ~ y`

is a given constraint

## 0.4.1 *February 4th 2016*

Find more unifications: *

`F x y k z ~ F x y (k-1+1) z`

==> [k := k], where`F`

can be any type function

## 0.4 *January 19th 2016*

- Stop using 'provenance' hack to create conditional evidence (GHC 8.0+ only)
- Find more unifications:
*
`F x + 2 - 1 - 1 ~ F x`

==> [F x := F x], where`F`

can be any type function with result`Nat`

.

## 0.3.2

Find more unifications:

`(z ^ a) ~ (z ^ b) ==> [a := b]`

`(i ^ a) ~ j ==> [a := round (logBase i j)]`

, when`i`

and`j`

are integers, and`ceiling (logBase i j) == floor (logBase i j)`

.

## 0.3.1 *October 19th 2015*

Find more unifications:

`(i * a) ~ j ==> [a := div j i]`

, when`i`

and`j`

are integers, and`mod j i == 0`

.`(i * a) + j ~ k ==> [a := div (k-j) i]`

, when`i`

,`j`

, and`k`

are integers, and`k-j >= 0`

and`mod (k-j) i == 0`

.

## 0.3 *June 3rd 2015*

- Find more unifications:
*
`<TyApp xs> + x ~ 2 + x ==> [<TyApp xs> ~ 2]`

- Fixes bugs:
*Unifying*Unifying`a*b ~ b`

now returns`[a ~ 1]`

; before it erroneously returned`[a ~ ]`

, which is interpred as`[a ~ 0]`

...`a+b ~ b`

now returns`[a ~ 0]`

; before it returned the undesirable, though equal,`[a ~ ]`

## 0.2.1 *May 6th 2015*

Update

`Eq`

instance of`SOP`

: Empty SOP is equal to 0

## 0.2 *April 22nd 2015*

Finds more unifications:

`(2 + a) ~ 5 ==> [a := 3]`

`(3 * a) ~ 0 ==> [a := 0]`

## 0.1.2 *April 21st 2015*

Don't simplify expressions with negative exponents

## 0.1.1 *April 17th 2015*

Add workaround for https://ghc.haskell.org/trac/ghc/ticket/10301

## 0.1 *March 30th 2015*

- Initial release