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]
Flags
Manual Flags
Name | Description | Default |
---|---|---|
deverror | Enables `-Werror` for development mode and TravisCI | Disabled |
Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info
Downloads
- ghc-typelits-knownnat-0.7.12.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Versions [RSS] | 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, 0.7.3, 0.7.4, 0.7.5, 0.7.6, 0.7.7, 0.7.8, 0.7.9, 0.7.10, 0.7.12 |
---|---|
Change log | CHANGELOG.md |
Dependencies | base (>=4.9 && <5), ghc (>=8.0.1 && <9.12), ghc-prim (>=0.4.0.0 && <0.12), ghc-tcplugins-extra (>=0.3.1), ghc-typelits-natnormalise (>=0.7.1 && <0.8), integer-gmp (>=0.5.1.0), template-haskell (>=2.11.0.0 && <2.23), transformers (>=0.5.2.0 && <0.7) [details] |
Tested with | ghc ==8.0.2, ghc ==8.2.2, ghc ==8.4.4, ghc ==8.6.5, ghc ==8.8.4, ghc ==8.10.7, ghc ==9.0.2, ghc ==9.2.8, ghc ==9.4.7, ghc ==9.6.3, ghc ==9.8.2, ghc ==9.10.1 |
License | BSD-2-Clause |
Copyright | Copyright © 2016 , University of Twente, 2017-2018, QBayLogic B.V., 2017 , Google Inc. |
Author | Christiaan Baaij |
Maintainer | christiaan.baaij@gmail.com |
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 2024-05-22T20:14:14Z |
Distributions | Arch:0.7.8, LTSHaskell:0.7.12, NixOS:0.7.12, Stackage:0.7.12 |
Reverse Dependencies | 33 direct, 32 indirect [details] |
Downloads | 22125 total (105 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs available [build log] Last success reported on 2024-05-22 [all 1 reports] |