# ghc-typelits-natnormalise

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

LTS Haskell 16.16: | 0.7.2 |

Stackage Nightly 2020-09-27: | 0.7.2 |

Latest on Hackage: | 0.7.2 |

BSD-2-Clause licensed by

**Christiaan Baaij**Maintained by

**christiaan.baaij@gmail.com**#### Module documentation for 0.7.2

This version can be pinned in stack with:

`ghc-typelits-natnormalise-0.7.2@sha256:0fc48a3744aa25e5e53a054a8bb1fe6410752e497f446d75db9bd67bb258d05e,3495`

# ghc-typelits-natnormalise

A type checker plugin for GHC that can solve *equalities* and *inequalities*
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.7.2 *March 9 2020*

- Fixes #44 infinite loop due to boxed equality

## 0.7.1 *February 6th 2020*

- Add support for GHC 8.10.1-alpha2
- Fixes #23: Can’t figure out
`+`

commutes in some contexts on GHC 8.6.3 - Fixes #28: Using the solver seems to break GHC
- Fixes #34: inequality solver mishandles subtraction

## 0.7 *August 26th 2019*

- Require KnownNat constraints when solving with constants

## 0.6.2 *July 10th 2018*

- Add support for GHC 8.6.1-alpha1
- Solve larger inequalities from smaller inequalities, e.g.
`a <= n`

implies`a <= n + 1`

## 0.6.1 *May 9th 2018*

- Stop solving
`x + y ~ a + b`

by asking GHC to solve`x ~ a`

and`y ~ b`

as this leads to a situation where we find a solution that is not the most general. - Stop using the smallest solution to an inequality to solve an equality, as this leads to finding solutions that are not the most general.
- Solve smaller inequalities from larger inequalities, e.g.
`1 <= 2*x`

implies`1 <= x`

`x + 2 <= y`

implies`x <= y`

and`2 <= y`

## 0.6 *April 23rd 2018*

- Solving constraints with
`a-b`

will emit`b <= a`

constraints. e.g. solving`n-1+1 ~ n`

will emit a`1 <= n`

constraint.- If you need subtraction to be treated as addition with a negated operarand
run with
`-fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers`

, and the`b <= a`

constraint won’t be emitted. Note that doing so can lead to unsound behaviour.

- If you need subtraction to be treated as addition with a negated operarand
run with
- Try to solve equalities using smallest solution of inequalities:
- Solve
`x + 1 ~ y`

using`1 <= y`

=>`x + 1 ~ 1`

=>`x ~ 0`

- Solve
- Solve inequalities using simple transitivity rules:
`2 <= x`

implies`1 <= x`

`x <= 9`

implies`x <= 10`

- Solve inequalities using
*simple*monotonicity of addition rules:`2 <= x`

implies`2 + 2*x <= 3*x`

- Solve inequalities using
*simple*monotonicity of multiplication rules:`1 <= x`

implies`1 <= 3*x`

- Solve inequalities using
*simple*monotonicity of exponentiation rules:`1 <= x`

implies`2 <= 2^x`

- Solve inequalities using powers of 2 and monotonicity of exponentiation:
`2 <= x`

implies`2^(2 + 2*x) <= 2^(3*x)`

## 0.5.10 *April 15th 2018*

- Add support for GHC 8.5.20180306

## 0.5.9 *March 17th 2018*

- Add support for GHC 8.4.1

## 0.5.8 *January 4th 2018*

- Add support for GHC 8.4.1-alpha1

## 0.5.7 *November 7th 2017*

- Solve inequalities such as:
`1 <= a + 3`

## 0.5.6 *October 31st 2017*

- Fixes bugs:
`(x + 1) ~ (2 * y)`

no longer implies`((2 * (y - 1)) + 1) ~ x`

## 0.5.5 *October 22nd 2017*

- Solve inequalities when their normal forms are the same, i.e.
`(2 <= (2 ^ (n + d)))`

implies`(2 <= (2 ^ (d + n)))`

- Find more unifications:
`8^x - 2*4^x ~ 8^y - 2*4^y ==> [x := y]`

## 0.5.4 *October 14th 2017*

- Perform normalisations such as:
`2^x * 4^x ==> 8^x`

## 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

- Rounding error in

## 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
`a*b ~ b`

now returns`[a ~ 1]`

; before it erroneously returned`[a ~ ]`

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

… - Unifying
`a+b ~ b`

now returns`[a ~ 0]`

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

- Unifying

## 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

Depends on 7 packages

*(full list with versions)*:Used by 8 packages in

**nightly-2020-09-16***(full list with versions)*:A service provided by
FP Complete