ghc-typelits-knownnat-0.3: Derive KnownNat constraints from other KnownNat constraints

GHC.TypeLits.KnownNat.Solver

Description

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