Derive KnownNat constraints from other KnownNat constraints

Version on this page:0.2.3
LTS Haskell 8.2:0.2.3
Stackage Nightly 2017-02-25:0.2.3
Latest on Hackage:0.2.3
BSD2 licensed by Christiaan Baaij
Maintained by

Module documentation for 0.2.3


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.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
comments powered byDisqus