ghc-typelits-natnormalise
GHC typechecker plugin for types of kind GHC.TypeLits.Nat
| Version on this page: | 0.3.1 |
| LTS Haskell 20.24: | 0.7.8 |
| Stackage Nightly 2023-06-04: | 0.7.8 |
| Latest on Hackage: | 0.7.8 |
Maintained by christiaan.baaij@gmail.com
This version can be pinned in stack with:
ghc-typelits-natnormalise-0.3.1@sha256:32bad1f6c489f4ce4fafe4208d4b22aa9ddb041f5d0b17743e3d3744419c346d,2572Module 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.
To use the plugin, add
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
To the header of your file.