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


-- | Recover type indexes and instances for your existentialized types.
--   
--   Recover type indexes and instances for your existentialized types.
@package exinst
@version 0.4


-- | Exinst is a library providing you with tools to recover type-indexed
--   types whose type-indexes have been existentialized, as well as
--   automatically deriving instances for them, as long as said type
--   indexes are singleton types (see <a>singleton</a>).
--   
--   In short, what <tt>exinst</tt> currently gives you is: For any type
--   <tt>t :: k -&gt; *</tt>, if <tt>k</tt> is a singleton type and <tt>c
--   (t a) :: <a>Constraint</a></tt> is satisfied, then you can
--   existentialize away the <tt>a</tt> parameter with <tt><a>Some1</a>
--   t</tt>, recover it later, and have <tt>c (<a>Some1</a> t)</tt>
--   automatically satisfied. Currently, up to 4 type indexes can be
--   existentialized using <a>Some1</a>, <a>Some2</a>, <a>Some3</a> and
--   <a>Some4</a> respectively.
--   
--   NOTE: This tutorial asumes some familiarity with singleton types as
--   implemented by the <a>singleton</a> library. A singleton type is, in
--   very rough terms, a type inhabited by a single term, which allows one
--   to go from its term-level representation to its type-level
--   representation and back without much trouble. A bit like the term
--   <tt>()</tt>, which is of type <tt>()</tt>. Whenever you have the type
--   <tt>()</tt> you know what that its term-level representation must be
--   <tt>()</tt>, and whenever you have the term <tt>()</tt> you know that
--   its type must be <tt>()</tt>.
module Exinst
data Some1 (f1 :: k1 -> Type)
Some1 :: !(Sing a1) -> !(f1 a1) -> Some1
some1 :: forall (f1 :: k1 -> Type) a1. SingI a1 => f1 a1 -> Some1 f1
fromSome1 :: forall (f1 :: k1 -> Type) a1. (SingI a1, SDecide k1) => Some1 f1 -> Maybe (f1 a1)
_Some1 :: forall (f1 :: k1 -> Type) a1. (SingI a1, SDecide k1) => Prism' (Some1 f1) (f1 a1)
withSome1 :: forall (f1 :: k1 -> Type) (r :: Type). Some1 f1 -> (forall a1. SingI a1 => f1 a1 -> r) -> r

-- | Like <a>withSome1</a>, but takes an explicit <a>Sing</a> besides the
--   <a>SingI</a> instance.
withSome1Sing :: forall (f1 :: k1 -> Type) (r :: Type). Some1 f1 -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r) -> r
some1SingRep :: SingKind k1 => Some1 (f1 :: k1 -> Type) -> DemoteRep k1
class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0)

-- | Runtime lookup of the <tt>c (f1 a1)</tt> instance.
dict1 :: Dict1 c f1 => Sing a1 -> Dict (c (f1 a1))
data Some2 (f2 :: k2 -> k1 -> Type)
Some2 :: !(Sing a2) -> !(Sing a1) -> !(f2 a2 a1) -> Some2
some2 :: forall (f2 :: k2 -> k1 -> Type) a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> Some2 f2
fromSome2 :: forall (f2 :: k2 -> k1 -> Type) a2 a1. (SingI a2, SDecide k2, SingI a1, SDecide k1) => Some2 f2 -> Maybe (f2 a2 a1)
_Some2 :: forall (f2 :: k2 -> k1 -> Type) a2 a1. (SingI a2, SDecide k2, SingI a1, SDecide k1) => Prism' (Some2 f2) (f2 a2 a1)
withSome2 :: forall (f2 :: k2 -> k1 -> Type) (r :: Type). Some2 f2 -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r) -> r

-- | Like <a>withSome2</a>, but takes explicit <a>Sing</a>s besides the
--   <a>SingI</a> instances.
withSome2Sing :: forall (f2 :: k2 -> k1 -> Type) (r :: Type). Some2 f2 -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r) -> r
some2SingRep :: (SingKind k2, SingKind k1) => Some2 (f2 :: k2 -> k1 -> Type) -> (DemoteRep k2, DemoteRep k1)
class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
dict2 :: Dict2 c f2 => Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
data Some3 (f3 :: k3 -> k2 -> k1 -> Type)
Some3 :: !(Sing a3) -> !(Sing a2) -> !(Sing a1) -> !(f3 a3 a2 a1) -> Some3
some3 :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> Some3 f3
fromSome3 :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1. (SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1, SDecide k1) => Some3 f3 -> Maybe (f3 a3 a2 a1)
_Some3 :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1. (SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1, SDecide k1) => Prism' (Some3 f3) (f3 a3 a2 a1)
withSome3 :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type). Some3 f3 -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r) -> r

-- | Like <a>withSome3</a>, but takes explicit <a>Sing</a>s besides the
--   <a>SingI</a> instances.
withSome3Sing :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type). Some3 f3 -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r) -> r
some3SingRep :: (SingKind k3, SingKind k2, SingKind k1) => Some3 (f3 :: k3 -> k2 -> k1 -> Type) -> (DemoteRep k3, DemoteRep k2, DemoteRep k1)
class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0)
dict3 :: Dict3 c f3 => Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
Some4 :: !(Sing a4) -> !(Sing a3) -> !(Sing a2) -> !(Sing a1) -> !(f4 a4 a3 a2 a1) -> Some4
some4 :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) => f4 a4 a3 a2 a1 -> Some4 f4
fromSome4 :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1. (SingI a4, SDecide k4, SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1, SDecide k1) => Some4 f4 -> Maybe (f4 a4 a3 a2 a1)
_Some4 :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1. (SingI a4, SDecide k4, SingI a3, SDecide k3, SingI a2, SDecide k2, SingI a1, SDecide k1) => Prism' (Some4 f4) (f4 a4 a3 a2 a1)
withSome4 :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type). Some4 f4 -> (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) => f4 a4 a3 a2 a1 -> r) -> r

-- | Like <a>withSome4</a>, but takes explicit <a>Sing</a>s besides the
--   <a>SingI</a> instances.
withSome4Sing :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type). Some4 f4 -> (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r) -> r
some4SingRep :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1) => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) -> (DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1)
class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0)
dict4 :: Dict4 c f4 => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))

-- | <a>Dict0</a> is a bit different from <a>Dict1</a>, <a>Dict2</a>, etc.
--   in that it looks up an instance for the singleton type itself, and not
--   for some other type indexed by said singleton type.
class Dict0 (c :: k0 -> Constraint)

-- | Runtime lookup of the <tt>c a0</tt> instance.
dict0 :: Dict0 c => Sing a0 -> Dict (c a0)

-- | Like <a>Product</a> from <a>Data.Functor.Product</a>, but only
--   intended to be used with kinds other than <tt>Type</tt>.
--   
--   This type is particularly useful when used in combination with
--   <a>Some1</a> as <tt><a>Some1</a> (<a>P1</a> l r)</tt>, so as to ensure
--   that <tt>l</tt> and <tt>r</tt> are indexed by the same type. Moreover,
--   <a>P1</a> already supports many common instances from <tt>base</tt>,
--   <tt>hashable</tt>, <tt>deepseq</tt>, <tt>aeson</tt>, <tt>bytes</tt>,
--   <tt>cereal</tt>, <tt>binary</tt>, and <tt>quickcheck</tt> out of the
--   box, so you can benefit from them as well.
data P1 l r (a1 :: k1)
P1 :: (l a1) -> (r a1) -> P1 l r

-- | Like <a>P1</a>, but for <tt>l</tt> and <tt>r</tt> taking two type
--   indexes.
data P2 l r (a2 :: k2) (a1 :: k1)
P2 :: (l a2 a1) -> (r a2 a1) -> P2 l r

-- | Like <a>P1</a>, but for <tt>l</tt> and <tt>r</tt> taking three type
--   indexes.
data P3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1)
P3 :: (l a3 a2 a1) -> (r a3 a2 a1) -> P3 l r

-- | Like <a>P1</a>, but for <tt>l</tt> and <tt>r</tt> taking four type
--   indexes.
data P4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1)
P4 :: (l a4 a3 a2 a1) -> (r a4 a3 a2 a1) -> P4 l r

-- | Like <a>Sum</a> from <a>Data.Functor.Sum</a>, but only intended to be
--   used with kinds other than <tt>Type</tt>.
--   
--   This type is particularly useful when used in combination with
--   <a>Some1</a> as <tt><a>Some1</a> (<a>S1</a> l r)</tt>, so as to ensure
--   that <tt>l</tt> and <tt>r</tt> are indexed by the same type. Moreover,
--   <a>S1</a> already supports many common instances from <tt>base</tt>,
--   <tt>hashable</tt>, <tt>deepseq</tt>, <tt>aeson</tt>, <tt>bytes</tt>,
--   <tt>cereal</tt>, <tt>binary</tt>, and <tt>quickcheck</tt> out of the
--   box, so you can benefit from them as well.
data S1 l r (a1 :: k1)
S1L :: (l a1) -> S1 l r
S1R :: (r a1) -> S1 l r

-- | Like <a>S1</a>, but for <tt>l</tt> and <tt>r</tt> taking two type
--   indexes.
data S2 l r (a2 :: k2) (a1 :: k1)
S2L :: (l a2 a1) -> S2 l r
S2R :: (r a2 a1) -> S2 l r

-- | Like <a>S1</a>, but for <tt>l</tt> and <tt>r</tt> taking three type
--   indexes.
data S3 l r (a3 :: k3) (a2 :: k2) (a1 :: k1)
S3L :: (l a3 a2 a1) -> S3 l r
S3R :: (r a3 a2 a1) -> S3 l r

-- | Like <a>S1</a>, but for <tt>l</tt> and <tt>r</tt> taking four type
--   indexes.
data S4 l r (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1)
S4L :: (l a4 a3 a2 a1) -> S4 l r
S4R :: (r a4 a3 a2 a1) -> S4 l r

-- | The kind of constraints, like <tt>Show a</tt>
data Constraint :: *

-- | Values of type <tt><a>Dict</a> p</tt> capture a dictionary for a
--   constraint of type <tt>p</tt>.
--   
--   e.g.
--   
--   <pre>
--   <a>Dict</a> :: <a>Dict</a> (<a>Eq</a> <a>Int</a>)
--   </pre>
--   
--   captures a dictionary that proves we have an:
--   
--   <pre>
--   instance <a>Eq</a> 'Int
--   </pre>
--   
--   Pattern matching on the <a>Dict</a> constructor will bring this
--   instance into scope.
data Dict (a :: Constraint) :: Constraint -> *
[Dict] :: Dict a

-- | The singleton kind-indexed data family.

-- | A <a>SingI</a> constraint is essentially an implicitly-passed
--   singleton. If you need to satisfy this constraint with an explicit
--   singleton, please see <a>withSingI</a>.
class SingI k (a :: k)