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


-- | Utility package for constraints
--   
--   Convenience functions and TH for working with constraints. See
--   <a>README.md</a> for example usage.
@package constraints-extras
@version 0.3.2.1

module Data.Constraint.Compose

-- | Composition for constraints.
class p (f a) => ComposeC (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1)
instance forall k2 k1 (p :: k2 -> GHC.Types.Constraint) (f :: k1 -> k2) (a :: k1). p (f a) => Data.Constraint.Compose.ComposeC p f a

module Data.Constraint.Flip

-- | Flip for constraints.
class c h g => FlipC (c :: k -> k' -> Constraint) (g :: k') (h :: k)
instance forall k k' (c :: k -> k' -> GHC.Types.Constraint) (h :: k) (g :: k'). c h g => Data.Constraint.Flip.FlipC c g h


-- | Throughout this module, we use the following GADT and <tt>ArgDict</tt>
--   instance in our examples:
--   
--   <pre>
--   {-# LANGUAGE StandaloneDeriving #-}
--   
--   data Tag a where
--     I :: Tag Int
--     B :: Tag Bool
--   deriving instance Show (Tag a)
--   
--   $(deriveArgDict ''Tag)
--   </pre>
--   
--   The constructors of <tt>Tag</tt> mean that a type variable <tt>a</tt>
--   in <tt>Tag a</tt> must come from the set { <tt>Int</tt>, <tt>Bool</tt>
--   }. We call this the "set of types <tt>a</tt> that could be applied to
--   <tt>Tag</tt>".
module Data.Constraint.Extras

-- | Morally, this class is for GADTs whose indices can be finitely
--   enumerated. An <tt><a>ArgDict</a> c f</tt> instance allows us to do
--   two things:
--   
--   <ol>
--   <li><a>ConstraintsFor</a> requests the set of constraints <tt>c a</tt>
--   for all possible types <tt>a</tt> that could be applied to
--   <tt>f</tt>.</li>
--   <li><a>argDict</a> selects a specific <tt>c a</tt> given a value of
--   type <tt>f a</tt>.</li>
--   </ol>
--   
--   Use <a>deriveArgDict</a> to derive instances of this class.
class ArgDict (c :: k -> Constraint) (f :: k -> Type) where {
    
    -- | Apply <tt>c</tt> to each possible type <tt>a</tt> that could appear in
    --   a <tt>f a</tt>.
    --   
    --   <pre>
    --   ConstraintsFor Show Tag = (Show Int, Show Bool)
    --   </pre>
    type family ConstraintsFor f c :: Constraint;
}

-- | Use an <tt>f a</tt> to select a specific dictionary from
--   <tt>ConstraintsFor f c</tt>.
--   
--   <pre>
--   argDict I :: Dict (Show Int)
--   </pre>
argDict :: (ArgDict c f, ConstraintsFor f c) => f a -> Dict (c a)

-- | "Primed" variants (<tt>ConstraintsFor'</tt>, <a>argDict'</a>,
--   <a>Has'</a>, <a>has'</a>, &amp;c.) use the <a>ArgDict</a> instance on
--   <tt>f</tt> to apply constraints on <tt>g a</tt> instead of just
--   <tt>a</tt>. This is often useful when you have data structures
--   parameterised by something of kind <tt>(x -&gt; Type) -&gt; Type</tt>,
--   like in the <tt>dependent-sum</tt> and <tt>dependent-map</tt>
--   libraries.
--   
--   <pre>
--   ConstraintsFor' Tag Show Identity = (Show (Identity Int), Show (Identity Bool))
--   </pre>
type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)

-- | Get a dictionary for a specific <tt>g a</tt>, using a value of type
--   <tt>f a</tt>.
--   
--   <pre>
--   argDict' B :: Dict (Show (Identity Bool))
--   </pre>
argDict' :: forall f c g a. Has' c f g => f a -> Dict (c (g a))
type ConstraintsForV (f :: (k -> k') -> Type) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)
argDictV :: forall f c g v. HasV c f g => f v -> Dict (c (v g))

-- | <tt>Has c f</tt> is a constraint which means that for every type
--   <tt>a</tt> that could be applied to <tt>f</tt>, we have <tt>c a</tt>.
--   
--   <pre>
--   Has Show Tag = (ArgDict Show Tag, Show Int, Show Bool)
--   </pre>
type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c)

-- | Use the <tt>a</tt> from <tt>f a</tt> to select a specific <tt>c a</tt>
--   constraint, and bring it into scope. The order of type variables is
--   chosen to work with <tt>-XTypeApplications</tt>.
--   
--   <pre>
--   -- Hold an a, along with a tag identifying the a.
--   data SomeTagged tag where
--     SomeTagged :: a -&gt; tag a -&gt; SomeTagged tag
--   
--   -- Use the stored tag to identify the thing we have, allowing us to call 'show'. Note that we
--   -- have no knowledge of the tag type.
--   showSomeTagged :: Has Show tag =&gt; SomeTagged tag -&gt; String
--   showSomeTagged (SomeTagged a tag) = has @Show tag $ show a
--   </pre>
has :: forall c f a r. Has c f => f a -> (c a => r) -> r

-- | <tt>Has' c f g</tt> is a constraint which means that for every type
--   <tt>a</tt> that could be applied to <tt>f</tt>, we have <tt>c (g
--   a)</tt>.
--   
--   <pre>
--   Has' Show Tag Identity = (ArgDict (Show . Identity) Tag, Show (Identity Int), Show (Identity Bool))
--   </pre>
type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g)

-- | Like <a>has</a>, but we get a <tt>c (g a)</tt> instance brought into
--   scope instead. Use <tt>-XTypeApplications</tt> to specify <tt>c</tt>
--   and <tt>g</tt>.
--   
--   <pre>
--   -- From dependent-sum:Data.Dependent.Sum
--   data DSum tag f = forall a. !(tag a) :=&gt; f a
--   
--   -- Show the value from a dependent sum. (We'll need 'whichever', discussed later, to show the key.)
--   showDSumVal :: forall tag f . Has' Show tag f =&gt; DSum tag f -&gt; String
--   showDSumVal (tag :=&gt; fa) = has' @Show @f tag $ show fa
--   </pre>
has' :: forall c g f a r. Has' c f g => f a -> (c (g a) => r) -> r
type HasV c f g = (ArgDict (FlipC (ComposeC c) g) f, ConstraintsForV f c g)
hasV :: forall c g f v r. HasV c f g => f v -> (c (v g) => r) -> r

-- | Given "forall a. <tt>c (t a)</tt>" (the <tt>ForallF c t</tt>
--   constraint), select a specific <tt>a</tt>, and bring <tt>c (t a)</tt>
--   into scope. Use <tt>-XTypeApplications</tt> to specify <tt>c</tt>,
--   <tt>t</tt> and <tt>a</tt>.
--   
--   <pre>
--   -- Show the tag of a dependent sum, even though we don't know the tag type.
--   showDSumKey :: forall tag f . ForallF Show tag =&gt; DSum tag f -&gt; String
--   showDSumKey ((tag :: tag a) :=&gt; fa) = whichever @Show @tag @a $ show tag
--   </pre>
whichever :: forall c t a r. ForallF c t => (c (t a) => r) -> r

-- | Allows explicit specification of constraint implication.
class Implies1 c d
implies1 :: Implies1 c d => c a :- d a

-- | <i>Deprecated: Just use <a>ArgDict</a></i>
type ArgDictV f c = ArgDict f c
instance forall k (c :: k -> GHC.Types.Constraint) (f :: k -> *) (g :: k -> *). (Data.Constraint.Extras.ArgDict c f, Data.Constraint.Extras.ArgDict c g) => Data.Constraint.Extras.ArgDict c (f GHC.Generics.:+: g)
instance forall k (c :: k -> GHC.Types.Constraint) (f :: k -> *) (g :: k -> *). (Data.Constraint.Extras.ArgDict c f, Data.Constraint.Extras.ArgDict c g) => Data.Constraint.Extras.ArgDict c (Data.Functor.Sum.Sum f g)

module Data.Constraint.Extras.TH
deriveArgDict :: Name -> Q [Dec]

-- | <i>Deprecated: Just use <a>deriveArgDict</a></i>
deriveArgDictV :: Name -> Q [Dec]
gadtIndices :: Name -> [Con] -> Q [Either Type Type]
