Copyright | (C) 2016, University of Twente |
---|---|

License | BSD2 (see the file LICENSE) |

Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |

Safe Haskell | Trustworthy |

Language | Haskell2010 |

Extensions | TupleSections |

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 only derive `KnownNat`

constraints consisting of:

- Type-level naturals
- Type variables
- Applications of the arithmetic expression:
`{+,*,^}`

i.e. it *cannot* derive a `KnownNat (n-1)`

constraint from a `KnownNat n`

constraint

To use the plugin, add the

OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver

Pragma to the header of your file.

# Documentation

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 only derive `KnownNat`

constraints consisting of:

- Type-level naturals
- Type variables
- Applications of the arithmetic expression:
`{+,*,^}`

.

i.e. it *cannot* derive a `KnownNat (n-1)`

constraint from a `KnownNat n`

constraint

To use the plugin, add the

OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver

Pragma to the header of your file.