# ghc-typelits-knownnat

Derive KnownNat constraints from other KnownNat constraints http://clash-lang.org/

LTS Haskell 8.20: | 0.2.4 |

Stackage Nightly 2017-06-26: | 0.3 |

Latest on Hackage: | 0.3 |

**Christiaan Baaij**

**christiaan.baaij@gmail.com**

#### Module documentation for 0.2.4

- GHC
- GHC.TypeLits

# ghc-typelits-knownnat

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*a corresponding`KnownNat`

constraint; or`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
$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol
```

and corresponding `KnownNat2`

instance:

```
instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where
type KnownNatF2 "TestFunctions.Max" = MaxSym0
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.

## Changes

# Changelog for the `ghc-typelits-knownnat`

package

## 0.3 *May 15th 2017*

GHC 8.2.1 support: Underlying representation for

`KnownNat`

in GHC 8.2 is`Natural`

, meaning users of this plugin will need to update their code to use`Natural`

for GHC 8.2 as well.

## 0.2.4 *April 10th 2017*

New features:

*Derive constraints for unary functions via a*Use type-substituted [G]iven KnownNats (partial solve for #13)`KnownNat1`

instance; thanks to @nshepperd #11

## 0.2.3 *January 15th 2017*

Solve normalised literal constraints, i.e.: *

`KnownNat (((addrSize + 1) - (addrSize - 1))) ~ KnownNat 2`

## 0.2.2 *September 29th 2016*

New features: * Derive smaller constraints from larger constraints when they differ by a single variable, i.e.

`KnownNat (a + b), KnownNat b`

implies`KnownNat a`

.

## 0.2.1 *August 19th 2016*

Fixes bugs: * Source location of derived wanted constraints is, erroneously, always set to line 1, column 1

## 0.2 *August 17th 2016*

New features:

*Handle*Handle custom, user-defined, type-level operations * Thanks to Gabor Greif (@ggreif): derive smaller from larger constraints, i.e.`GHC.TypeLits.-`

`KnownNat (n+1)`

implies`KnownNat n`

## 0.1.2

New features: Solve "complex" KnownNat constraints involving arbitrary type-functions, as long as there is a given KnownNat constraint for this type functions.

## 0.1.1 *August 11th 2016*

Fixes bug: panic on a non-given KnownNat constraint variable

## 0.1 *August 10th 2016*

- Initial release