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

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Warnings:

'ghc-options: -O0' is not needed. Use the --disable-optimization configure flag.

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 constraint
Type-level naturals
Applications of the arithmetic expression: +,-,*,^
Type functions, when there is either:

a matching given KnownNat constraint; or
a 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]

Properties

Versions	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.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.2), ghc-prim (>=0.4.0.0 && <0.8), 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.18), transformers (>=0.5.2.0 && <0.6) [details]
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 2021-02-10T10:04:57Z

Modules

[Index] [Quick Jump]

GHC
- TypeLits
  - GHC.TypeLits.KnownNat
    - GHC.TypeLits.KnownNat.Solver

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.5.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

ChristiaanBaaij, QBayLogic

For package maintainers and hackage trustees

edit package information

Readme for ghc-typelits-knownnat-0.7.5

[back to package description]

ghc-typelits-knownnat

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 constraint
Type-level naturals
Applications of the arithmetic expression: {+,-,*,^}
Type functions, when there is either:
- a matching given KnownNat constraint; or
- a corresponding KnownNat<N> instance for the type function

To elaborate the latter points, given the type family Min:

type family Min (a :: Nat) (b :: Nat) :: Nat where
  Min 0 b = 0
  Min a b = If (a <=? b) a b

the plugin can derive a KnownNat (Min x y + 1) constraint given only a KnownNat (Min x y) constraint:

g :: forall x y . (KnownNat (Min x y)) => Proxy x -> Proxy y -> Integer
g _ _ = natVal (Proxy :: Proxy (Min x y + 1))

And, given the type family Max:

type family Max (a :: Nat) (b :: Nat) :: Nat where
  Max 0 b = b
  Max a b = If (a <=? b) b a

and corresponding KnownNat2 instance:

instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where
  natSing2 = let x = natVal (Proxy @a)
                 y = natVal (Proxy @b)
                 z = max x y
             in  SNatKn z
  {-# INLINE natSing2 #-}

the plugin can derive a KnownNat (Max x y + 1) constraint given only a KnownNat x and KnownNat y constraint:

h :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer
h _ _ = natVal (Proxy :: Proxy (Max x y + 1))

To use the plugin, add the

OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver

Pragma to the header of your file.