-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Derive KnownNat constraints from other KnownNat constraints
--   
--   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 use the plugin, add the
--   
--   
--   OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver
--   
--   
--   Pragma to the header of your file.
@package ghc-typelits-knownnat
@version 0.7.13

-- | Some "magic" classes and instances to get the
--   GHC.TypeLits.KnownNat.Solver type checker plugin working.
--   
--   
Usage
--   
--   Let's say you defined a closed type family Max:
--   
--   
--   import Data.Type.Bool (If)
--   import GHC.TypeLits
--   
--   type family Max (a :: Nat) (b :: Nat) :: Nat where
--     Max 0 b = b
--     Max a b = If (a <=? b) b a
--   
--   
--   if you then want the GHC.TypeLits.KnownNat.Solver to solve
--   KnownNat constraints over Max, given just
--   KnownNat constraints for the arguments of Max, then
--   you must define:
--   
--   
--   {-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,
--                MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,
--                TypeApplications, TypeFamilies, TypeOperators,
--                UndecidableInstances #-}
--   
--   import Data.Proxy            (Proxy (..))
--   import GHC.TypeLits.KnownNat
--   
--   instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where
--     natSing2 = let x = natVal (Proxy a)
--                    y = natVal (Proxy b)
--                    z = max x y
--                in  SNatKn z
--     {-# INLINE natSing2 #-}
--   
--   
--   
FAQ
--   
--   
1. GHC.TypeLits.KnownNat.Solver does not seem to find the
--   corresponding KnownNat2 instance for my type-level
--   operation
--   
--   At the Core-level, GHCs internal mini-Haskell, type families that only
--   have a single equation are treated like type synonyms.
--   
--   For example, let's say we defined a closed type family Max:
--   
--   
--   import Data.Type.Bool (If)
--   import GHC.TypeLits
--   
--   type family Max (a :: Nat) (b :: Nat) :: Nat where
--     Max a b = If (a <=? b) b a
--   
--   
--   Now, a Haskell-level program might contain a constraint
--   
--   
--   KnownNat (Max a b)
--   
--   
--   , however, at the Core-level, this constraint is expanded to:
--   
--   
--   KnownNat (If (a <=? b) b a)
--   
--   
--   GHC.TypeLits.KnownNat.Solver never sees any reference to the
--   Max type family, so it will not look for the corresponding
--   KnownNat2 instance either. To fix this, ensure that your
--   type-level operations always have at least two equations. For
--   Max this means we have to redefine it as:
--   
--   
--   type family Max (a :: Nat) (b :: Nat) :: Nat where
--     Max 0 b = b
--     Max a b = If (a <=? b) b a
--   
module GHC.TypeLits.KnownNat

-- | Singleton natural number
newtype SNatKn (f :: Symbol)
SNatKn :: Natural -> SNatKn (f :: Symbol)

-- | Class for arithmetic functions with one argument.
--   
--   The Symbol f must correspond to the fully qualified name
--   of the type-level operation. Use nameToSymbol to get the fully
--   qualified TH Name as a Symbol
class KnownNat1 (f :: Symbol) (a :: Nat)
natSing1 :: KnownNat1 f a => SNatKn f

-- | Class for arithmetic functions with two arguments.
--   
--   The Symbol f must correspond to the fully qualified name
--   of the type-level operation. Use nameToSymbol to get the fully
--   qualified TH Name as a Symbol
class KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat)
natSing2 :: KnownNat2 f a b => SNatKn f

-- | Class for arithmetic functions with three arguments.
--   
--   The Symbol f must correspond to the fully qualified name
--   of the type-level operation. Use nameToSymbol to get the fully
--   qualified TH Name as a Symbol
class KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat)
natSing3 :: KnownNat3 f a b c => SNatKn f

-- | Singleton version of Bool
data SBool (b :: Bool)
[SFalse] :: SBool 'False
[STrue] :: SBool 'True

-- | Get the Bool value associated with a type-level Bool
--   
--   Use boolVal if you want to perform the standard boolean
--   operations on the reified type-level Bool.
--   
--   Use boolSing if you need a context in which the type-checker
--   needs the type-level Bool to be either True or
--   False
--   
--   
--   f :: forall proxy b r . KnownBool b => r
--   f = case boolSing @b of
--     SFalse -> -- context with b ~ False
--     STrue  -> -- context with b ~ True
--   
boolVal :: forall (b :: Bool) proxy. KnownBool b => proxy b -> Bool
class KnownBool (b :: Bool)
boolSing :: KnownBool b => SBool b

-- | A type "representationally equal" to SBool, used for simpler
--   implementation of constraint-level functions that need to create
--   instances of KnownBool
newtype SBoolKb (f :: Symbol)
SBoolKb :: Bool -> SBoolKb (f :: Symbol)

-- | Class for ternary functions with a Natural result.
--   
--   The Symbol f must correspond to the fully qualified name
--   of the type-level operation. Use nameToSymbol to get the fully
--   qualified TH Name as a Symbol
class KnownNat2Bool (f :: Symbol) (a :: Bool) (b :: k) (c :: k)
natBoolSing3 :: KnownNat2Bool f a b c => SNatKn f

-- | Class for binary functions with a Boolean result.
--   
--   The Symbol f must correspond to the fully qualified name
--   of the type-level operation. Use nameToSymbol to get the fully
--   qualified TH Name as a Symbol
class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k)
boolNatSing2 :: KnownBoolNat2 f a b => SBoolKb f

-- | Convert a TH Name to a type-level Symbol
nameToSymbol :: Name -> TypeQ
instance (GHC.Internal.TypeNats.KnownNat a, GHC.Internal.TypeNats.KnownNat b) => GHC.TypeLits.KnownNat.KnownBoolNat2 "GHC.Internal.Data.Type.Ord.OrdCond" a b
instance (GHC.Internal.TypeNats.KnownNat a, GHC.Internal.TypeNats.KnownNat b) => GHC.TypeLits.KnownNat.KnownBoolNat2 "GHC.Internal.Data.Type.Ord.<=?" a b
instance GHC.TypeLits.KnownNat.KnownBool 'GHC.Types.False
instance GHC.TypeLits.KnownNat.KnownBool 'GHC.Types.True
instance (GHC.Internal.TypeNats.KnownNat a, GHC.Internal.TypeNats.KnownNat b) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.Internal.TypeNats.^" a b
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y, (1 GHC.Internal.Data.Type.Ord.<= y) GHC.Types.~ (() :: Constraint)) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.Internal.TypeNats.Mod" x y
instance (GHC.Internal.TypeNats.KnownNat x, GHC.Internal.TypeNats.KnownNat y, (1 GHC.Internal.Data.Type.Ord.<= y) GHC.Types.~ (() :: Constraint)) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.Internal.TypeNats.Div" x y
instance (GHC.Internal.TypeNats.KnownNat a, GHC.Internal.TypeNats.KnownNat b, (b GHC.Internal.Data.Type.Ord.<= a) GHC.Types.~ (() :: Constraint)) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.Internal.TypeNats.-" a b
instance (GHC.Internal.TypeNats.KnownNat a, GHC.Internal.TypeNats.KnownNat b) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.Internal.TypeNats.+" a b
instance (GHC.Internal.TypeNats.KnownNat a, GHC.Internal.TypeNats.KnownNat b) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.Internal.TypeNats.*" a b
instance (GHC.TypeLits.KnownNat.KnownBool a, GHC.Internal.TypeNats.KnownNat b, GHC.Internal.TypeNats.KnownNat c) => GHC.TypeLits.KnownNat.KnownNat2Bool "GHC.Internal.Data.Type.Bool.If" a b c

-- | 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
--   
--   
--   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.
module GHC.TypeLits.KnownNat.Solver

-- | 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.
plugin :: Plugin
