-- 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"
--   <tt>KnownNat</tt> constraints from other simple/variable
--   <tt>KnownNat</tt> constraints. i.e. without this plugin, you must have
--   both a <tt>KnownNat n</tt> and a <tt>KnownNat (n+2)</tt> constraint in
--   the type signature of the following function:
--   
--   <pre>
--   f :: forall n . (KnownNat n, KnownNat (n+2)) =&gt; Proxy n -&gt; Integer
--   f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
--   </pre>
--   
--   Using the plugin you can omit the <tt>KnownNat (n+2)</tt> constraint:
--   
--   <pre>
--   f :: forall n . KnownNat n =&gt; Proxy n -&gt; Integer
--   f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
--   </pre>
--   
--   The plugin can derive <tt>KnownNat</tt> constraints for types
--   consisting of:
--   
--   <ul>
--   <li>Type variables, when there is a corresponding <tt>KnownNat</tt>
--   constraint</li>
--   <li>Type-level naturals</li>
--   <li>Applications of the arithmetic expression: +,-,*,^</li>
--   <li>Type functions, when there is either:</li>
--   </ul>
--   
--   <ol>
--   <li>a matching given <tt>KnownNat</tt> constraint; or</li>
--   <li>a corresponding <tt>KnownNat&lt;N&gt;</tt> instance for the type
--   function</li>
--   </ol>
--   
--   To use the plugin, add the
--   
--   <pre>
--   OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver
--   </pre>
--   
--   Pragma to the header of your file.
@package ghc-typelits-knownnat
@version 0.7.12


-- | Some "magic" classes and instances to get the
--   <a>GHC.TypeLits.KnownNat.Solver</a> type checker plugin working.
--   
--   <h1>Usage</h1>
--   
--   Let's say you defined a closed type family <tt>Max</tt>:
--   
--   <pre>
--   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 &lt;=? b) b a
--   </pre>
--   
--   if you then want the <a>GHC.TypeLits.KnownNat.Solver</a> to solve
--   <a>KnownNat</a> constraints over <tt>Max</tt>, given just
--   <a>KnownNat</a> constraints for the arguments of <tt>Max</tt>, then
--   you must define:
--   
--   <pre>
--   {-# 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) =&gt; <a>KnownNat2</a> $(<a>nameToSymbol</a> ''Max) a b where
--     natSing2 = let x = natVal (Proxy <tt>a)
--                    y = natVal (Proxy </tt>b)
--                    z = max x y
--                in  <a>SNatKn</a> z
--     {-# INLINE natSing2 #-}
--   </pre>
--   
--   <h1>FAQ</h1>
--   
--   <h4>1. <a>GHC.TypeLits.KnownNat.Solver</a> does not seem to find the
--   corresponding <a>KnownNat2</a> instance for my type-level
--   operation</h4>
--   
--   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 <tt>Max</tt>:
--   
--   <pre>
--   import Data.Type.Bool (If)
--   import GHC.TypeLits
--   
--   type family Max (a :: Nat) (b :: Nat) :: Nat where
--     Max a b = If (a &lt;=? b) b a
--   </pre>
--   
--   Now, a Haskell-level program might contain a constraint
--   
--   <pre>
--   KnownNat (Max a b)
--   </pre>
--   
--   , however, at the Core-level, this constraint is expanded to:
--   
--   <pre>
--   KnownNat (If (a &lt;=? b) b a)
--   </pre>
--   
--   <a>GHC.TypeLits.KnownNat.Solver</a> never sees any reference to the
--   <tt>Max</tt> type family, so it will not look for the corresponding
--   <a>KnownNat2</a> instance either. To fix this, ensure that your
--   type-level operations always have at least two equations. For
--   <tt>Max</tt> this means we have to redefine it as:
--   
--   <pre>
--   type family Max (a :: Nat) (b :: Nat) :: Nat where
--     Max 0 b = b
--     Max a b = If (a &lt;=? b) b a
--   </pre>
module GHC.TypeLits.KnownNat

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

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

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

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

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

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

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

-- | Class for ternary functions with a Natural result.
--   
--   The <a>Symbol</a> <i>f</i> must correspond to the fully qualified name
--   of the type-level operation. Use <a>nameToSymbol</a> to get the fully
--   qualified TH Name as a <a>Symbol</a>
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 <a>Symbol</a> <i>f</i> must correspond to the fully qualified name
--   of the type-level operation. Use <a>nameToSymbol</a> to get the fully
--   qualified TH Name as a <a>Symbol</a>
class KnownBoolNat2 (f :: Symbol) (a :: k) (b :: k)
boolNatSing2 :: KnownBoolNat2 f a b => SBoolKb f

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


-- | A type checker plugin for GHC that can derive "complex"
--   <tt>KnownNat</tt> constraints from other simple/variable
--   <tt>KnownNat</tt> constraints. i.e. without this plugin, you must have
--   both a <tt>KnownNat n</tt> and a <tt>KnownNat (n+2)</tt> constraint in
--   the type signature of the following function:
--   
--   <pre>
--   f :: forall n . (KnownNat n, KnownNat (n+2)) =&gt; Proxy n -&gt; Integer
--   f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
--   </pre>
--   
--   Using the plugin you can omit the <tt>KnownNat (n+2)</tt> constraint:
--   
--   <pre>
--   f :: forall n . KnownNat n =&gt; Proxy n -&gt; Integer
--   f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
--   </pre>
--   
--   The plugin can derive <tt>KnownNat</tt> constraints for types
--   consisting of:
--   
--   <ul>
--   <li>Type variables, when there is a corresponding <tt>KnownNat</tt>
--   constraint</li>
--   <li>Type-level naturals</li>
--   <li>Applications of the arithmetic expression: <tt>{+,-,*,^}</tt></li>
--   <li>Type functions, when there is either:</li>
--   <li>a matching given <tt>KnownNat</tt> constraint; or</li>
--   <li>a corresponding <tt>KnownNat&lt;N&gt;</tt> instance for the type
--   function</li>
--   </ul>
--   
--   To elaborate the latter points, given the type family <tt>Min</tt>:
--   
--   <pre>
--   type family Min (a :: Nat) (b :: Nat) :: Nat where
--     Min 0 b = 0
--     Min a b = If (a &lt;=? b) a b
--   </pre>
--   
--   the plugin can derive a <tt>KnownNat (Min x y + 1)</tt> constraint
--   given only a <tt>KnownNat (Min x y)</tt> constraint:
--   
--   <pre>
--   g :: forall x y . (KnownNat (Min x y)) =&gt; Proxy x -&gt; Proxy y -&gt; Integer
--   g _ _ = natVal (Proxy :: Proxy (Min x y + 1))
--   </pre>
--   
--   And, given the type family <tt>Max</tt>:
--   
--   <pre>
--   type family Max (a :: Nat) (b :: Nat) :: Nat where
--     Max 0 b = b
--     Max a b = If (a &lt;=? b) b a
--   </pre>
--   
--   and corresponding <tt>KnownNat2</tt> instance:
--   
--   <pre>
--   instance (KnownNat a, KnownNat b) =&gt; KnownNat2 "TestFunctions.Max" a b where
--     natSing2 = let x = natVal (Proxy <tt>a)
--                    y = natVal (Proxy </tt>b)
--                    z = max x y
--                in  SNatKn z
--     {-# INLINE natSing2 #-}
--   </pre>
--   
--   the plugin can derive a <tt>KnownNat (Max x y + 1)</tt> constraint
--   given only a <tt>KnownNat x</tt> and <tt>KnownNat y</tt> constraint:
--   
--   <pre>
--   h :: forall x y . (KnownNat x, KnownNat y) =&gt; Proxy x -&gt; Proxy y -&gt; Integer
--   h _ _ = natVal (Proxy :: Proxy (Max x y + 1))
--   </pre>
--   
--   To use the plugin, add the
--   
--   <pre>
--   OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver
--   </pre>
--   
--   Pragma to the header of your file.
module GHC.TypeLits.KnownNat.Solver

-- | A type checker plugin for GHC that can derive "complex"
--   <tt>KnownNat</tt> constraints from other simple/variable
--   <tt>KnownNat</tt> constraints. i.e. without this plugin, you must have
--   both a <tt>KnownNat n</tt> and a <tt>KnownNat (n+2)</tt> constraint in
--   the type signature of the following function:
--   
--   <pre>
--   f :: forall n . (KnownNat n, KnownNat (n+2)) =&gt; Proxy n -&gt; Integer
--   f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
--   </pre>
--   
--   Using the plugin you can omit the <tt>KnownNat (n+2)</tt> constraint:
--   
--   <pre>
--   f :: forall n . KnownNat n =&gt; Proxy n -&gt; Integer
--   f _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2))
--   </pre>
--   
--   The plugin can derive <tt>KnownNat</tt> constraints for types
--   consisting of:
--   
--   <ul>
--   <li>Type variables, when there is a corresponding <tt>KnownNat</tt>
--   constraint</li>
--   <li>Type-level naturals</li>
--   <li>Applications of the arithmetic expression: <tt>{+,-,*,^}</tt></li>
--   <li>Type functions, when there is either:</li>
--   <li>a matching given <tt>KnownNat</tt> constraint; or</li>
--   <li>a corresponding <tt>KnownNat&lt;N&gt;</tt> instance for the type
--   function</li>
--   </ul>
--   
--   To elaborate the latter points, given the type family <tt>Min</tt>:
--   
--   <pre>
--   type family Min (a :: Nat) (b :: Nat) :: Nat where
--     Min 0 b = 0
--     Min a b = If (a &lt;=? b) a b
--   </pre>
--   
--   the plugin can derive a <tt>KnownNat (Min x y + 1)</tt> constraint
--   given only a <tt>KnownNat (Min x y)</tt> constraint:
--   
--   <pre>
--   g :: forall x y . (KnownNat (Min x y)) =&gt; Proxy x -&gt; Proxy y -&gt; Integer
--   g _ _ = natVal (Proxy :: Proxy (Min x y + 1))
--   </pre>
--   
--   And, given the type family <tt>Max</tt>:
--   
--   <pre>
--   type family Max (a :: Nat) (b :: Nat) :: Nat where
--     Max 0 b = b
--     Max a b = If (a &lt;=? b) b a
--   
--   $(genDefunSymbols [''Max]) -- creates the <tt>MaxSym0</tt> symbol
--   </pre>
--   
--   and corresponding <tt>KnownNat2</tt> instance:
--   
--   <pre>
--   instance (KnownNat a, KnownNat b) =&gt; KnownNat2 "TestFunctions.Max" a b where
--     type KnownNatF2 "TestFunctions.Max" = MaxSym0
--     natSing2 = let x = natVal (Proxy <tt> a)
--                    y = natVal (Proxy </tt> b)
--                    z = max x y
--                in  SNatKn z
--     {-# INLINE natSing2 #-}
--   </pre>
--   
--   the plugin can derive a <tt>KnownNat (Max x y + 1)</tt> constraint
--   given only a <tt>KnownNat x</tt> and <tt>KnownNat y</tt> constraint:
--   
--   <pre>
--   h :: forall x y . (KnownNat x, KnownNat y) =&gt; Proxy x -&gt; Proxy y -&gt; Integer
--   h _ _ = natVal (Proxy :: Proxy (Max x y + 1))
--   </pre>
--   
--   To use the plugin, add the
--   
--   <pre>
--   OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver
--   </pre>
--   
--   Pragma to the header of your file.
plugin :: Plugin
