# ghc-typelits-knownnat: Derive KnownNat constraints from other KnownNat constraints

A type checker plugin for GHC that can derive "complex" `KnownNat`

constraints from other simple/variable `KnownNat`

constraints. i.e. without
this plugin, you must have both a `KnownNat n`

and a `KnownNat (n+2)`

constraint in the type signature of the following function:

f :: forall n . (KnownNat n, KnownNat (n+2)) => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))

Using the plugin you can omit the `KnownNat (n+2)`

constraint:

f :: forall n . KnownNat n => Proxy n -> Integer f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))

The plugin can derive `KnownNat`

constraints for types consisting of:

Type variables, when there is a corresponding

`KnownNat`

constraintType-level naturals

Applications of the arithmetic expression: +,-,*,^

Type functions, when there is either:

a matching given

`KnownNat`

constraint; ora corresponding

`KnownNat<N>`

instance for the type function

To use the plugin, add the

OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver

Pragma to the header of your file.

[Skip to Readme]

Versions [faq] | 0.1, 0.1.1, 0.2, 0.2.1, 0.2.2, 0.2.3, 0.2.4, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.5, 0.5.1, 0.6, 0.7, 0.7.1, 0.7.2 |
---|---|

Change log | CHANGELOG.md |

Dependencies | base (>=4.9 && <5), ghc (>=8.0.1 && <8.4), ghc-tcplugins-extra (>=0.2), ghc-typelits-natnormalise (>=0.5.2 && <0.6), singletons (>=2.2 && <2.4), template-haskell (>=2.11.0.0 && <2.13), transformers (>=0.5.2.0 && <0.6) [details] |

License | BSD-2-Clause |

Copyright | Copyright © 2016, University of Twente, 2017 QBayLogic |

Author | Christiaan Baaij |

Maintainer | christiaan.baaij@gmail.com |

Revised | Revision 1 made by ChristiaanBaaij at 2017-08-16T09:37:33Z |

Category | Type System |

Home page | http://clash-lang.org/ |

Source repo | head: git clone https://github.com/clash-lang/ghc-typelits-knownnat.git |

Uploaded | by ChristiaanBaaij at 2017-05-15T08:30:25Z |

Distributions | Arch:0.7.2, LTSHaskell:0.6, NixOS:0.7.2, Stackage:0.6 |

Downloads | 11871 total (470 in the last 30 days) |

Rating | (no votes yet) [estimated by Bayesian average] |

Your Rating | |

Status | Docs available [build log] Last success reported on 2017-05-15 [all 1 reports] |

## Flags

Name | Description | Default | Type |
---|---|---|---|

deverror | Enables | Disabled | Manual |

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

## Downloads

- ghc-typelits-knownnat-0.3.tar.gz [browse] (Cabal source package)
- Package description (revised from the package)

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.