# ghc-typelits-knownnat

Derive KnownNat constraints from other KnownNat constraints

LTS Haskell 22.22: | 0.7.10 |

Stackage Nightly 2024-05-20: | 0.7.10 |

Latest on Hackage: | 0.7.10 |

**Christiaan Baaij**

**[email protected]**

`ghc-typelits-knownnat-0.7.10@sha256:d65df5c90f482a006eb5fe3701f59a5130cc4338e00620dd46a5bab5ceadeb03,5036`

#### Module documentation for 0.7.10

- GHC
- GHC.TypeLits

*(full list with versions)*:

**lts-21.22**

*(full list with versions)*:

# 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
`KnownNat`

constraint; or - a corresponding
`KnownNat<N>`

instance for the type function

- a matching given

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.

## Changes

# Changelog for the `ghc-typelits-knownnat`

package

## 0.7.10 *November 14th 2023*

- Work around GHC issue 23109

## 0.7.9 *October 10th 2023*

- Support for GHC 9.8.1

## 0.7.8 *February 20th 2023*

- Support for GHC-9.6.0.20230210

## 0.7.7 *October 10th 2022*

- Add support for GHC 9.4

## 0.7.6 *June 18th 2021*

- Add support for GHC 9.2.0.20210422

## 0.7.5 *February 10th 2021*

- Raise upper limit for TH dep to allow building on ghc-9.0.1

## 0.7.4 *January 1st 2021*

- Add support for GHC 9.0.1-rc1

## 0.7.3 *July 25th 2020*

## 0.7.2 *February 6th 2020*

- Add support for GHC 8.10.0-alpha2

## 0.7.1 *October 8th 2019*

## 0.7 *August 26th 2018*

- Solve “known” type-level Booleans, also inside
`If`

(GHC 8.6+)

## 0.6 *September 14th 2018*

- Move
`KnownNat2`

instances for`Div`

and`Mod`

from`ghc-typelits-extra`

to`ghc-typelits-knownnat`

## 0.5 *May 9th 2018*

- Fix Inferred constraint is too strong #19

## 0.4.2 *April 15th 2018*

- Add support for GHC 8.5.20180306

## 0.4.1 *March 17th, 2018*

- Add support for GHC 8.4.1

## 0.4 *January 4th, 2018*

- Add partial GHC 8.4.1-alpha1 support
- Drop
`singletons`

dependency #15`KnownNatN`

classes no longer have the`KnownNatFN`

associated type family

## 0.3.1 *August 17th 2017*

- Fix testsuite for GHC 8.2.1

## 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:

## 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`

.

- Derive smaller constraints from larger constraints when they differ by a single variable, i.e.

## 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
`GHC.TypeLits.-`

- Handle custom, user-defined, type-level operations
- Thanks to Gabor Greif (@ggreif): derive smaller from larger constraints, i.e.
`KnownNat (n+1)`

implies`KnownNat n`

- Handle

## 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