Derive KnownNat constraints from other KnownNat constraints

Version on this page:0.2.4
LTS Haskell 21.22:0.7.10
Stackage Nightly 2023-11-30:0.7.10
Latest on Hackage:0.7.10

See all snapshots ghc-typelits-knownnat appears in

BSD-2-Clause licensed by Christiaan Baaij
This version can be pinned in stack with:ghc-typelits-knownnat-0.2.4@sha256:58dbfc1ec0392866dfd13aa4d897375a55baa5c3c5a6d899cb32fe79b65a51c2,4572

Module documentation for 0.2.4


Build Status Hackage Hackage Dependencies

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


Changelog for the ghc-typelits-knownnat package

0.2.4 April 10th 2017

  • New features:
    • Derive constraints for unary functions via a KnownNat1 instance; thanks to @nshepperd #11
    • Use type-substituted [G]iven KnownNats (partial solve for #13)

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


  • 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