ghc-typelits-knownnat
Derive KnownNat constraints from other KnownNat constraints
| LTS Haskell 24.18: | 0.7.13 |
| Stackage Nightly 2025-11-03: | 0.8.2 |
| Latest on Hackage: | 0.8.2 |
ghc-typelits-knownnat-0.8.2@sha256:6e9ef33bd2cf462e7d66f5b28608c0156007947b3a7a95fd5b90bfa4a0365d1e,5993Module documentation for 0.8.2
- 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
KnownNatconstraint - Type-level naturals
- Applications of the arithmetic expression:
{+,-,*,^} - Type functions, when there is either:
- a matching given
KnownNatconstraint; 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.