# 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 11.14: 0.5.10 Stackage Nightly 2018-06-20: 0.6.1 Latest on Hackage: 0.6.1

See all snapshots `ghc-typelits-natnormalise` appears in

Maintained by

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

``{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}``

# Changelog for the `ghc-typelits-natnormalise` package

## 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.
• Try to solve equalities using smallest solution of inequalities: * Solve `x + 1 ~ y` using `1 <= y` => `x + 1 ~ 1` => `x ~ 0`
• 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

## 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 ~ ]`

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