# ghc-typelits-natnormalise

GHC typechecker plugin for types of kind GHC.TypeLits.Nat

http://www.clash-lang.org/

 Version on this page: 0.3.1 LTS Haskell 22.26: 0.7.10 Stackage Nightly 2024-06-21: 0.7.10 Latest on Hackage: 0.7.10

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

Maintained by
This version can be pinned in stack with:`ghc-typelits-natnormalise-0.3.1@sha256:32bad1f6c489f4ce4fafe4208d4b22aa9ddb041f5d0b17743e3d3744419c346d,2572`

#### Module documentation for 0.3.1

Depends on 3 packages(full list with versions):
Used by 2 packages in lts-3.22(full list with versions):

# ghc-tynat-normalise

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

## 0.1 March 30th 2015

• Initial release