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


-- | A collection of data types for type-level programming
--   
--   A collection of data types for type-level programming
@package type-combinators
@version 0.1.2.1


-- | Type-level <tt>Monoid</tt>, defined as an open type family.
module Type.Family.Monoid


-- | Reexports the kind <a>Constraint</a>, as well as some conveniences for
--   working with <a>Constraint</a>s.
module Type.Family.Constraint

-- | The empty <a>Constraint</a>.
type ØC = (() :: Constraint)
class IffC b t f => Iff (b :: Bool) (t :: Constraint) (f :: Constraint) where type family IffC b t f :: Constraint
data Constraint :: BOX
instance t => Type.Family.Constraint.Iff 'GHC.Types.True t f
instance f => Type.Family.Constraint.Iff 'GHC.Types.False t f


-- | Convenient aliases and type families for working with type-level
--   lists.
module Type.Family.List
type Ø = '[]
type (:<) = (:)

-- | Type-level singleton list.
type Only a = '[a]

-- | Appends two type-level lists.

-- | Type-level list snoc.

-- | Takes a type-level list of <a>Constraint</a>s to a single
--   <a>Constraint</a>, where <tt>ListC cs</tt> holds iff all elements of
--   <tt>cs</tt> hold.

-- | Map an <tt>(f :: k -&gt; l)</tt> over a type-level list <tt>(as ::
--   [k])</tt>, giving a list <tt>(bs :: [l])</tt>.

-- | Map a list of <tt>(fs :: [k -&gt; l])</tt> over a single <tt>(a ::
--   k)</tt>, giving a list <tt>(bs :: [l])</tt>.
(==) :: Eq a => a -> a -> Bool


-- | Type-level natural numbers, along with frequently used type families
--   over them.
module Type.Family.Nat
data N
Z :: N
S :: N -> N

-- | Convenient aliases for low-value Peano numbers.
type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
type N9 = S N8
type N10 = S N9

-- | A type family to compute Boolean equality. Instances are provided only
--   for <i>open</i> kinds, such as <tt>*</tt> and function kinds.
--   Instances are also provided for datatypes exported from base. A
--   poly-kinded instance is <i>not</i> provided, as a recursive definition
--   for algebraic kinds is generally more useful.
instance GHC.Show.Show Type.Family.Nat.N
instance GHC.Classes.Ord Type.Family.Nat.N
instance GHC.Classes.Eq Type.Family.Nat.N


-- | Convenient type families for working with type-level <tt>Maybe</tt>s.
module Type.Family.Maybe

-- | Take a <tt>Maybe Constraint</tt> to a <tt>Constraint</tt>.

-- | Map over a type-level <tt>Maybe</tt>.

-- | A type family to compute Boolean equality. Instances are provided only
--   for <i>open</i> kinds, such as <tt>*</tt> and function kinds.
--   Instances are also provided for datatypes exported from base. A
--   poly-kinded instance is <i>not</i> provided, as a recursive definition
--   for algebraic kinds is generally more useful.


-- | Type-level pairs and triples, along with some convenient aliases and
--   type families over them.
module Type.Family.Tuple
type (#) = (,)


-- | The <a>Known</a> class, among others in this library, use an
--   associated <a>Constraint</a> to maintain a bidirectional chain of
--   inference.
--   
--   For instance, given evidence of <tt>Known Nat n</tt>, if <tt>n</tt>
--   later gets refined to <tt>n'</tt>, we can correctly infer <tt>Known
--   Nat n'</tt>, as per the type instance defined for <tt>KnownC Nat (S
--   n')</tt>.
module Type.Class.Known

-- | Each instance of <a>Known</a> provides a canonical construction of a
--   type at a particular index.
--   
--   Useful for working with singleton-esque GADTs.
class KnownC f a => Known (f :: k -> *) (a :: k) where type family KnownC f a :: Constraint KnownC (f :: k -> *) (a :: k) = ØC
known :: Known f a => f a
instance forall (k :: BOX) (a :: k) (b :: k). (a ~ b) => Type.Class.Known.Known ((Data.Type.Equality.:~:) a) b


-- | A type <tt>t</tt> that is a <tt><a>Witness</a> p q t</tt> provides a
--   <a>Constraint</a> entailment of <tt>q</tt>, given that <tt>p</tt>
--   holds.
--   
--   The <a>Witness</a> class uses an associated <a>Constraint</a>
--   <tt>WitnessC</tt> to maintain backwards inference of <a>Witness</a>
--   instances with respect to type refinement. See the <a>Known</a> class
--   for more information.
--   
--   Heavily inspired by ekmett's constraints library:
--   <a>http://hackage.haskell.org/package/constraints</a>
--   
--   The code provided here does not <i>quite</i> subsume the
--   <tt>constraints</tt> library, as we do not give classes and instances
--   for representing the standard library's class heirarchy and instance
--   definitions.
module Type.Class.Witness

-- | A reified <a>Constraint</a>.
data Wit :: Constraint -> *
Wit :: Wit c
data Wit1 :: (k -> Constraint) -> k -> *
Wit1 :: Wit1 c a

-- | Reified evidence of <a>Constraint</a> entailment.
--   
--   Given a term of <tt>p :- q</tt>, the Constraint <tt>q</tt> holds if
--   <tt>p</tt> holds.
--   
--   Entailment of <a>Constraint</a>s form a <a>Category</a>:
--   
--   <pre>
--   &gt;&gt;&gt; id  :: p :- p
--   
--   &gt;&gt;&gt; (.) :: (q :- r) -&gt; (p :-&gt; q) -&gt; (p :- r)
--   </pre>
data (:-) :: Constraint -> Constraint -> *
Sub :: (p => Wit q) -> p :- q
[getSub] :: p :- q -> p => Wit q
type (:-:) = Bij (:-)

-- | A general eliminator for entailment.
--   
--   Given a term of type <tt>t</tt> with an instance <tt>Witness p q
--   t</tt> and a term of type <tt>r</tt> that depends on <a>Constraint</a>
--   <tt>q</tt>, we can reduce the Constraint to <tt>p</tt>.
--   
--   If <tt>p</tt> is <tt>ØC</tt>, i.e. the empty <a>Constraint</a>
--   <tt>()</tt>, then a Witness <tt>t</tt> can completely discharge the
--   Constraint <tt>q</tt>.
class WitnessC p q t => Witness (p :: Constraint) (q :: Constraint) (t :: *) | t -> p q where type family WitnessC p q t :: Constraint WitnessC p q t = ØC
(\\) :: (Witness p q t, p) => (q => r) -> t -> r

-- | Convert a <a>Witness</a> to a canonical reified entailment.
entailed :: Witness p q t => t -> p :- q

-- | Convert a <a>Witness</a> to a canonical reified <a>Constraint</a>.
witnessed :: Witness ØC q t => t -> Wit q

-- | An entailment <tt>p :- q</tt> is a Witness of <tt>q</tt>, given
--   <tt>p</tt>.

-- | A type equality <tt>a <a>:~:</a> b</tt> is a Witness that <tt>(a ~
--   b)</tt>.

-- | If the constraint <tt>c</tt> holds, there is a canonical construction
--   for a term of type <tt><a>Wit</a> c</tt>, viz. the constructor
--   <tt>Wit</tt>.

-- | Constraint chaining under <tt>Maybe</tt>.
(/?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r
qed :: Maybe (a :~: a)
impossible :: a -> Void
data Dec a
Proven :: a -> Dec a
Refuted :: (a -> Void) -> Dec a
class DecEquality (f :: k -> *)
decideEquality :: DecEquality f => f a -> f b -> Dec (a :~: b)
decCase :: Dec a -> (a -> r) -> ((a -> Void) -> r) -> r
data Bij p a b
Bij :: p a b -> p b a -> Bij p a b
[fwd] :: Bij p a b -> p a b
[bwd] :: Bij p a b -> p b a
($->) :: Bij p a b -> p a b
(<-$) :: Bij p a b -> p b a
type (<->) = Bij (->)
(<->) :: p a b -> p b a -> Bij p a b
(<?>) :: r <-> s -> Dec r -> Dec s
instance Control.Category.Category (Type.Class.Witness.:-)
instance Type.Class.Witness.Witness Type.Family.Constraint.ØC c (Type.Class.Witness.Wit c)
instance Type.Class.Witness.Witness p q (p Type.Class.Witness.:- q)
instance forall (k :: BOX) (a :: k) (b :: k). Type.Class.Witness.Witness Type.Family.Constraint.ØC (a ~ b) (a Data.Type.Equality.:~: b)
instance c => Type.Class.Known.Known Type.Class.Witness.Wit c
instance forall (k :: BOX) (p :: k -> k -> *). Control.Category.Category p => Control.Category.Category (Type.Class.Witness.Bij p)


-- | A <tt>singleton</tt>-esque type for representing lengths of type-level
--   lists, irrespective of the actual types in that list.
module Data.Type.Length
data Length :: [k] -> *
LZ :: Length Ø
LS :: !(Length as) -> Length (a :< as)
lOdd :: Length as -> Bool
lEven :: Length as -> Bool
instance forall (k :: BOX) (as :: [k]). GHC.Classes.Eq (Data.Type.Length.Length as)
instance forall (k :: BOX) (as :: [k]). GHC.Classes.Ord (Data.Type.Length.Length as)
instance forall (k :: BOX) (as :: [k]). GHC.Show.Show (Data.Type.Length.Length as)
instance Type.Class.Known.Known Data.Type.Length.Length Type.Family.List.Ø
instance forall (k :: BOX) (a :: k) (as :: [k]). Type.Class.Known.Known Data.Type.Length.Length as => Type.Class.Known.Known Data.Type.Length.Length (a Type.Family.List.:< as)


-- | Higher order functors, foldables, and traversables, along with their
--   indexed variants. (oh, and bifunctors tacked on for good measure.)
module Type.Class.HFunctor
class HFunctor (t :: (k -> *) -> l -> *)

-- | Take a natural transformation to a lifted natural transformation.
map' :: HFunctor t => (forall (a :: k). f a -> g a) -> t f b -> t g b
class HIxFunctor (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i
imap' :: HIxFunctor i t => (forall (a :: k). i b a -> f a -> g a) -> t f b -> t g b
class HFoldable (t :: (k -> *) -> l -> *)
foldMap' :: (HFoldable t, Monoid m) => (forall (a :: k). f a -> m) -> t f b -> m
class HIxFoldable (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i
ifoldMap' :: (HIxFoldable i t, Monoid m) => (forall (a :: k). i b a -> f a -> m) -> t f b -> m
class (HFunctor t, HFoldable t) => HTraversable (t :: (k -> *) -> l -> *)
traverse' :: (HTraversable t, Applicative h) => (forall (a :: k). f a -> h (g a)) -> t f b -> h (t g b)
class (HIxFunctor i t, HIxFoldable i t) => HIxTraversable (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i
itraverse' :: (HIxTraversable i t, Applicative h) => (forall (a :: k). i b a -> f a -> h (g a)) -> t f b -> h (t g b)
class HBifunctor (t :: (k -> *) -> (l -> *) -> m -> *)
bimap' :: HBifunctor t => (forall (a :: k). f a -> h a) -> (forall (a :: l). g a -> i a) -> t f g b -> t h i b


-- | Two type combinators for working with conjunctions: A <i>fanout</i>
--   combinator '(:&amp;:)', and a <i>par</i> combinator '(:*:)'.
--   
--   These are analogous to '(&amp;&amp;&amp;)' and '(***)' from
--   <a>Arrow</a>, respectively.
module Data.Type.Conjunction
data (:&:) (f :: k -> *) (g :: k -> *) :: k -> *
(:&:) :: !(f a) -> !(g a) -> (f :&: g) a
fanFst :: (f :&: g) a -> f a
fanSnd :: (f :&: g) a -> g a
uncurryFan :: (f a -> g a -> r) -> (f :&: g) a -> r
curryFan :: ((f :&: g) a -> r) -> f a -> g a -> r
data (:*:) (f :: k -> *) (g :: l -> *) :: (k, l) -> *
(:*:) :: !(f a) -> !(g b) -> (f :*: g) (a # b)
parFst :: (f :*: g) p -> f (Fst p)
parSnd :: (f :*: g) p -> g (Snd p)
uncurryPar :: (forall a b. (p ~ (a # b)) => f a -> g b -> r) -> (f :*: g) p -> r
curryPar :: ((f :*: g) (a # b) -> r) -> f a -> g b -> r
_fst :: (a # b) :~: (c # d) -> a :~: c
_snd :: (a # b) :~: (c # d) -> b :~: d
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *) (a :: k). (GHC.Classes.Eq (f a), GHC.Classes.Eq (g a)) => GHC.Classes.Eq ((Data.Type.Conjunction.:&:) f g a)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *) (a :: k). (GHC.Classes.Ord (f a), GHC.Classes.Ord (g a)) => GHC.Classes.Ord ((Data.Type.Conjunction.:&:) f g a)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *) (a :: k). (GHC.Show.Show (f a), GHC.Show.Show (g a)) => GHC.Show.Show ((Data.Type.Conjunction.:&:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (p :: (,) k k1). (GHC.Classes.Eq (f (Type.Family.Tuple.Fst p)), GHC.Classes.Eq (g (Type.Family.Tuple.Snd p))) => GHC.Classes.Eq ((Data.Type.Conjunction.:*:) f g p)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (p :: (,) k k1). (GHC.Classes.Ord (f (Type.Family.Tuple.Fst p)), GHC.Classes.Ord (g (Type.Family.Tuple.Snd p))) => GHC.Classes.Ord ((Data.Type.Conjunction.:*:) f g p)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (p :: (,) k k1). (GHC.Show.Show (f (Type.Family.Tuple.Fst p)), GHC.Show.Show (g (Type.Family.Tuple.Snd p))) => GHC.Show.Show ((Data.Type.Conjunction.:*:) f g p)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *). Type.Class.Witness.DecEquality f => Type.Class.Witness.DecEquality (f Data.Type.Conjunction.:&: g)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *) (a :: k). (Type.Class.Known.Known f a, Type.Class.Known.Known g a) => Type.Class.Known.Known (f Data.Type.Conjunction.:&: g) a
instance forall (k :: BOX) (f :: k -> *). Type.Class.HFunctor.HFunctor ((Data.Type.Conjunction.:&:) f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.HFunctor.HFoldable ((Data.Type.Conjunction.:&:) f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.HFunctor.HTraversable ((Data.Type.Conjunction.:&:) f)
instance Type.Class.HFunctor.HBifunctor (Data.Type.Conjunction.:&:)
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (s :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (t :: GHC.Prim.Constraint) (f :: k -> *) (g :: k -> *) (a :: k). (Type.Class.Witness.Witness p q (f a), Type.Class.Witness.Witness s t (g a)) => Type.Class.Witness.Witness (p, s) (q, t) ((Data.Type.Conjunction.:&:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (p :: (,) k k1) (a :: k) (b :: k1). (p ~ (a Type.Family.Tuple.# b), Type.Class.Known.Known f a, Type.Class.Known.Known g b) => Type.Class.Known.Known (f Data.Type.Conjunction.:*: g) p
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.HFunctor.HFunctor ((Data.Type.Conjunction.:*:) f)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.HFunctor.HFoldable ((Data.Type.Conjunction.:*:) f)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.HFunctor.HTraversable ((Data.Type.Conjunction.:*:) f)
instance Type.Class.HFunctor.HBifunctor (Data.Type.Conjunction.:*:)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *). (Type.Class.Witness.DecEquality f, Type.Class.Witness.DecEquality g) => Type.Class.Witness.DecEquality (f Data.Type.Conjunction.:*: g)
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (s :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (t :: GHC.Prim.Constraint) (f :: k -> *) (g :: k1 -> *) (x :: (,) k k1) (a :: k) (b :: k1). (Type.Class.Witness.Witness p q (f a), Type.Class.Witness.Witness s t (g b), x ~ (a Type.Family.Tuple.# b)) => Type.Class.Witness.Witness (p, s) (q, t) ((Data.Type.Conjunction.:*:) f g x)


-- | Two type combinators for working with disjunctions: A <i>branch</i>
--   combinator '(:+:)', and a <i>choice</i> combinator '(:|:)'.
--   
--   These are analogous to '(+++)' and '(|||)' from <a>Arrow</a>,
--   respectively.
module Data.Type.Disjunction
data (:+:) (f :: k -> *) (g :: k -> *) :: k -> *
L :: !(f a) -> (f :+: g) a
R :: !(g a) -> (f :+: g) a
(>+<) :: (f a -> r) -> (g a -> r) -> (f :+: g) a -> r
data (:|:) (f :: k -> *) (g :: l -> *) :: Either k l -> *
L' :: !(f a) -> (f :|: g) (Left a)
R' :: !(g b) -> (f :|: g) (Right b)
(>|<) :: (forall a. (e ~ Left a) => f a -> r) -> (forall b. (e ~ Right b) => g b -> r) -> (f :|: g) e -> r
instance forall (k :: BOX) (f :: k -> *). Type.Class.HFunctor.HFunctor ((Data.Type.Disjunction.:+:) f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.HFunctor.HFoldable ((Data.Type.Disjunction.:+:) f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.HFunctor.HTraversable ((Data.Type.Disjunction.:+:) f)
instance Type.Class.HFunctor.HBifunctor (Data.Type.Disjunction.:+:)
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> *) (g :: k -> *) (a :: k). (Type.Class.Witness.Witness p q (f a), Type.Class.Witness.Witness p q (g a)) => Type.Class.Witness.Witness p q ((Data.Type.Disjunction.:+:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *) (g :: k -> *) (a :: k1). Type.Class.Known.Known f a => Type.Class.Known.Known (f Data.Type.Disjunction.:|: g) ('Data.Either.Left a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (b :: k1). Type.Class.Known.Known g b => Type.Class.Known.Known (f Data.Type.Disjunction.:|: g) ('Data.Either.Right b)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.HFunctor.HFunctor ((Data.Type.Disjunction.:|:) f)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.HFunctor.HFoldable ((Data.Type.Disjunction.:|:) f)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.HFunctor.HTraversable ((Data.Type.Disjunction.:|:) f)
instance Type.Class.HFunctor.HBifunctor (Data.Type.Disjunction.:|:)
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k1 -> *) (g :: k -> *) (a :: k1). Type.Class.Witness.Witness p q (f a) => Type.Class.Witness.Witness p q ((Data.Type.Disjunction.:|:) f g ('Data.Either.Left a))
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> *) (g :: k1 -> *) (b :: k1). Type.Class.Witness.Witness p q (g b) => Type.Class.Witness.Witness p q ((Data.Type.Disjunction.:|:) f g ('Data.Either.Right b))


-- | A <tt>singleton</tt>-esque type for representing indices in a
--   type-level list.
module Data.Type.Index
data Index :: [k] -> k -> *
IZ :: Index (a :< as) a
IS :: !(Index as a) -> Index (b :< as) a
type (∈) a as = Elem as a
class Elem (as :: [k]) (a :: k)
elemIndex :: Elem as a => Index as a
instance forall (k :: BOX) (as :: [k]) (a :: k). GHC.Classes.Eq (Data.Type.Index.Index as a)
instance forall (k :: BOX) (as :: [k]) (a :: k). GHC.Classes.Ord (Data.Type.Index.Index as a)
instance forall (k :: BOX) (as :: [k]) (a :: k). GHC.Show.Show (Data.Type.Index.Index as a)
instance forall (k :: BOX) (a :: k) (as :: [k]). Data.Type.Index.Elem (a Type.Family.List.:< as) a
instance forall (k :: BOX) (b :: k) (as :: [k]) (a :: k). Data.Type.Index.Elem as a => Data.Type.Index.Elem (b Type.Family.List.:< as) a
instance forall (k :: BOX) (a :: k) (as :: [k]). Type.Class.Known.Known (Data.Type.Index.Index (a Type.Family.List.:< as)) a
instance forall (k :: BOX) (b :: k) (as :: [k]) (a :: k). Type.Class.Known.Known (Data.Type.Index.Index as) a => Type.Class.Known.Known (Data.Type.Index.Index (b Type.Family.List.:< as)) a


-- | A <a>QuasiQuoter</a> for the <a>Index</a> type.
module Data.Type.Index.Quote
ix :: QuasiQuoter
parseIxExp :: String -> Q Exp
parseIxPat :: String -> Q Pat


-- | A type combinator for type-level <tt>Maybe</tt>s, lifting <tt>(f :: k
--   -&gt; *)</tt> to <tt>(Option f :: Maybe k -&gt; *)</tt>.
module Data.Type.Option
data Option (f :: k -> *) :: Maybe k -> *
Nothing_ :: Option f Nothing
Just_ :: !(f a) -> Option f (Just a)

-- | Eliminator for <tt><a>Option</a> f</tt>.
option :: (forall a. (m ~ Just a) => f a -> r) -> ((m ~ Nothing) => r) -> Option f m -> r

-- | We can take a natural transformation of <tt>(forall x. f x -&gt; g
--   x)</tt> to a natural transformation of <tt>(forall mx. <a>Option</a> f
--   mx -&gt; <a>Option</a> g mx)</tt>.
instance Type.Class.HFunctor.HFunctor Data.Type.Option.Option
instance Type.Class.HFunctor.HFoldable Data.Type.Option.Option
instance Type.Class.HFunctor.HTraversable Data.Type.Option.Option
instance forall (k :: BOX) (f :: k -> *). Type.Class.Known.Known (Data.Type.Option.Option f) 'GHC.Base.Nothing
instance forall (k :: BOX) (f :: k -> *) (a :: k). Type.Class.Known.Known f a => Type.Class.Known.Known (Data.Type.Option.Option f) ('GHC.Base.Just a)
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> *) (x :: GHC.Base.Maybe k) (a :: k). (Type.Class.Witness.Witness p q (f a), x ~ 'GHC.Base.Just a) => Type.Class.Witness.Witness p q (Data.Type.Option.Option f x)


-- | <a>Sum</a> is a type combinators for representing disjoint sums of
--   indices <tt>(as :: [k])</tt> of a single functor @(f :: k -&gt; *).
--   Contrast to the many-functors-one-index <tt>FSum</tt>
module Data.Type.Sum
data Sum (f :: k -> *) :: [k] -> *
InL :: !(f a) -> Sum f (a :< as)
InR :: !(Sum f as) -> Sum f (a :< as)

-- | There are no possible values of the type <tt>Sum f Ø</tt>.
nilSum :: Sum f Ø -> Void
decomp :: Sum f (a :< as) -> Either (f a) (Sum f as)
injectSum :: Index as a -> f a -> Sum f as
inj :: (a ∈ as) => f a -> Sum f as
prj :: (a ∈ as) => Sum f as -> Maybe (f a)
index :: Index as a -> Sum f as -> Maybe (f a)
instance Type.Class.HFunctor.HFunctor Data.Type.Sum.Sum
instance Type.Class.HFunctor.HIxFunctor Data.Type.Index.Index Data.Type.Sum.Sum
instance Type.Class.HFunctor.HFoldable Data.Type.Sum.Sum
instance Type.Class.HFunctor.HIxFoldable Data.Type.Index.Index Data.Type.Sum.Sum
instance Type.Class.HFunctor.HTraversable Data.Type.Sum.Sum
instance Type.Class.HFunctor.HIxTraversable Data.Type.Index.Index Data.Type.Sum.Sum
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> *) (a :: k). Type.Class.Witness.Witness p q (f a) => Type.Class.Witness.Witness p q (Data.Type.Sum.Sum f '[a])
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> *) (a :: k) (b :: k) (as :: [k]). (Type.Class.Witness.Witness p q (f a), Type.Class.Witness.Witness p q (Data.Type.Sum.Sum f (b Type.Family.List.:< as))) => Type.Class.Witness.Witness p q (Data.Type.Sum.Sum f (a Type.Family.List.:< (b Type.Family.List.:< as)))


-- | <a>FSum</a> is a type combinators for representing disjoint sums of
--   many functors <tt>(fs :: [k -&gt; *])</tt> at a single index <tt>(a ::
--   k)</tt>. As opposed to one-functor-many-indices <tt>Sum</tt>.
module Data.Type.Sum.Dual
data FSum :: [k -> *] -> k -> *
FInL :: !(f a) -> FSum (f :< fs) a
FInR :: !(FSum fs a) -> FSum (f :< fs) a

-- | There are no possible values of the type <tt>FSum Ø a</tt>.
nilSumF :: FSum Ø a -> Void

-- | Decompose a non-empty FSum into either its head or its tail.
decompF :: FSum (f :< fs) a -> Either (f a) (FSum fs a)

-- | Inject an element into an FSum.
injF :: (f ∈ fs) => f a -> FSum fs a

-- | Project an implicit index out of an FSum.
prjF :: (f ∈ fs) => FSum fs a -> Maybe (f a)

-- | Inject an element into an FSum with an explicitly specified Index.
injectFSum :: Index fs f -> f a -> FSum fs a

-- | Project an explicit index out of an FSum.
indexF :: Index fs f -> FSum fs a -> Maybe (f a)

-- | Map over the single element in an FSum with a function that can handle
--   any possible element, along with the element's index.
imapF :: (forall f. Index fs f -> f a -> f b) -> FSum fs a -> FSum fs b

-- | Fun fact: Since there is exactly one element in an FSum, we don't need
--   the <tt>Monoid</tt> instance!
ifoldMapF :: (forall f. Index fs f -> f a -> m) -> FSum fs a -> m

-- | Another fun fact: Since there is exactly one element in an FSum, we
--   require only a <tt>Functor</tt> instance on <tt>g</tt>, rather than
--   <tt>Applicative</tt>.
itraverseF :: Functor g => (forall f. Index fs f -> f a -> g (f b)) -> FSum fs a -> g (FSum fs b)
instance Type.Family.List.ListC (GHC.Base.Functor Type.Family.List.<$> fs) => GHC.Base.Functor (Data.Type.Sum.Dual.FSum fs)
instance Type.Family.List.ListC (Data.Foldable.Foldable Type.Family.List.<$> fs) => Data.Foldable.Foldable (Data.Type.Sum.Dual.FSum fs)
instance (Type.Family.List.ListC (GHC.Base.Functor Type.Family.List.<$> fs), Type.Family.List.ListC (Data.Foldable.Foldable Type.Family.List.<$> fs), Type.Family.List.ListC (Data.Traversable.Traversable Type.Family.List.<$> fs)) => Data.Traversable.Traversable (Data.Type.Sum.Dual.FSum fs)


-- | A collection of simple type combinators, such as <tt>Identity</tt>
--   <a>I</a>, <tt>Constant</tt> <a>C</a>, <tt>Compose</tt> '(:.:)', left
--   unnest <a>LL</a>, right unnest <a>RR</a>, the <tt>S Combinator</tt>
--   <a>SS</a>, etc.
module Data.Type.Combinator
data (:.:) (f :: l -> *) (g :: k -> l) :: k -> *
Comp :: f (g a) -> (f :.: g) a
[getComp] :: (f :.: g) a -> f (g a)
data (:..:) (f :: m -> *) (g :: k -> l -> m) :: k -> l -> *
Comp2 :: f (g a b) -> (f :..: g) a b
data IT :: (k -> *) -> k -> *
IT :: f a -> IT f a
[getIT] :: IT f a -> f a
data I :: * -> *
I :: a -> I a
[getI] :: I a -> a
newtype LL (a :: k) (f :: l -> *) (g :: k -> l)
LL :: f (g a) -> LL
[getLL] :: LL -> f (g a)
newtype RR (g :: k -> l) (f :: l -> *) (a :: k)
RR :: f (g a) -> RR
[getRR] :: RR -> f (g a)
newtype SS (f :: k -> l -> *) (g :: k -> l) :: k -> *
SS :: f a (g a) -> SS f g a
[getSS] :: SS f g a -> f a (g a)
data CT :: * -> (k -> *) -> l -> *
CT :: r -> CT r f a
[getCT] :: CT r f a -> r
data C :: * -> k -> *
C :: r -> C r a
[getC] :: C r a -> r
newtype Join f a
Join :: f a a -> Join f a
[getJoin] :: Join f a -> f a a
newtype Flip p b a
Flip :: p a b -> Flip p b a
[getFlip] :: Flip p b a -> p a b
flipped :: (f a b -> g c d) -> Flip f b a -> Flip g d c
newtype Cur (p :: (k, l) -> *) :: k -> l -> *
Cur :: p (a # b) -> Cur p a b
[getCur] :: Cur p a b -> p (a # b)
data Uncur (p :: k -> l -> *) :: (k, l) -> *
Uncur :: p a b -> Uncur p (a # b)
[getUncur] :: Uncur p (a # b) -> p a b
newtype Cur3 (p :: (k, l, m) -> *) :: k -> l -> m -> *
Cur3 :: p '(a, b, c) -> Cur3 p a b c
[getCur3] :: Cur3 p a b c -> p '(a, b, c)
data Uncur3 (p :: k -> l -> m -> *) :: (k, l, m) -> *
Uncur3 :: p a b c -> Uncur3 p '(a, b, c)
[getUncur3] :: Uncur3 p '(a, b, c) -> p a b c
instance forall (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (b :: k1) (a :: k). GHC.Show.Show (p a b) => GHC.Show.Show (Data.Type.Combinator.Flip p b a)
instance forall (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (b :: k1) (a :: k). GHC.Classes.Ord (p a b) => GHC.Classes.Ord (Data.Type.Combinator.Flip p b a)
instance forall (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (b :: k1) (a :: k). GHC.Classes.Eq (p a b) => GHC.Classes.Eq (Data.Type.Combinator.Flip p b a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *) (g :: k -> k1) (a :: k). GHC.Classes.Eq (f (g a)) => GHC.Classes.Eq ((Data.Type.Combinator.:.:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *) (g :: k -> k1) (a :: k). GHC.Classes.Ord (f (g a)) => GHC.Classes.Ord ((Data.Type.Combinator.:.:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *) (g :: k -> k1) (a :: k). GHC.Show.Show (f (g a)) => GHC.Show.Show ((Data.Type.Combinator.:.:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (f :: k2 -> *) (g :: k -> k1 -> k2) (a :: k) (b :: k1). GHC.Classes.Eq (f (g a b)) => GHC.Classes.Eq ((Data.Type.Combinator.:..:) f g a b)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (f :: k2 -> *) (g :: k -> k1 -> k2) (a :: k) (b :: k1). GHC.Classes.Ord (f (g a b)) => GHC.Classes.Ord ((Data.Type.Combinator.:..:) f g a b)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (f :: k2 -> *) (g :: k -> k1 -> k2) (a :: k) (b :: k1). GHC.Show.Show (f (g a b)) => GHC.Show.Show ((Data.Type.Combinator.:..:) f g a b)
instance forall (k :: BOX) (f :: k -> *) (a :: k). GHC.Classes.Eq (f a) => GHC.Classes.Eq (Data.Type.Combinator.IT f a)
instance forall (k :: BOX) (f :: k -> *) (a :: k). GHC.Classes.Ord (f a) => GHC.Classes.Ord (Data.Type.Combinator.IT f a)
instance forall (k :: BOX) (f :: k -> *) (a :: k). GHC.Show.Show (f a) => GHC.Show.Show (Data.Type.Combinator.IT f a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Type.Combinator.I a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Type.Combinator.I a)
instance GHC.Show.Show a => GHC.Show.Show (Data.Type.Combinator.I a)
instance forall (k :: BOX) (k1 :: BOX) (a :: k) (f :: k1 -> *) (g :: k -> k1). GHC.Classes.Eq (f (g a)) => GHC.Classes.Eq (Data.Type.Combinator.LL a f g)
instance forall (k :: BOX) (k1 :: BOX) (a :: k) (f :: k1 -> *) (g :: k -> k1). GHC.Classes.Ord (f (g a)) => GHC.Classes.Ord (Data.Type.Combinator.LL a f g)
instance forall (k :: BOX) (k1 :: BOX) (a :: k) (f :: k1 -> *) (g :: k -> k1). GHC.Show.Show (f (g a)) => GHC.Show.Show (Data.Type.Combinator.LL a f g)
instance forall (k :: BOX) (k1 :: BOX) (g :: k -> k1) (f :: k1 -> *) (a :: k). GHC.Classes.Eq (f (g a)) => GHC.Classes.Eq (Data.Type.Combinator.RR g f a)
instance forall (k :: BOX) (k1 :: BOX) (g :: k -> k1) (f :: k1 -> *) (a :: k). GHC.Classes.Ord (f (g a)) => GHC.Classes.Ord (Data.Type.Combinator.RR g f a)
instance forall (k :: BOX) (k1 :: BOX) (g :: k -> k1) (f :: k1 -> *) (a :: k). GHC.Show.Show (f (g a)) => GHC.Show.Show (Data.Type.Combinator.RR g f a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> k1 -> *) (g :: k -> k1) (a :: k). GHC.Classes.Eq (f a (g a)) => GHC.Classes.Eq (Data.Type.Combinator.SS f g a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> k1 -> *) (g :: k -> k1) (a :: k). GHC.Classes.Ord (f a (g a)) => GHC.Classes.Ord (Data.Type.Combinator.SS f g a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> k1 -> *) (g :: k -> k1) (a :: k). GHC.Show.Show (f a (g a)) => GHC.Show.Show (Data.Type.Combinator.SS f g a)
instance forall (k :: BOX) (k1 :: BOX) r (f :: k -> *) (a :: k1). GHC.Classes.Eq r => GHC.Classes.Eq (Data.Type.Combinator.CT r f a)
instance forall (k :: BOX) (k1 :: BOX) r (f :: k -> *) (a :: k1). GHC.Classes.Ord r => GHC.Classes.Ord (Data.Type.Combinator.CT r f a)
instance forall (k :: BOX) (k1 :: BOX) r (f :: k -> *) (a :: k1). GHC.Show.Show r => GHC.Show.Show (Data.Type.Combinator.CT r f a)
instance forall (k :: BOX) r (a :: k). GHC.Classes.Eq r => GHC.Classes.Eq (Data.Type.Combinator.C r a)
instance forall (k :: BOX) r (a :: k). GHC.Classes.Ord r => GHC.Classes.Ord (Data.Type.Combinator.C r a)
instance forall (k :: BOX) r (a :: k). GHC.Show.Show r => GHC.Show.Show (Data.Type.Combinator.C r a)
instance forall (k :: BOX) (f :: k -> k -> *) (a :: k). GHC.Classes.Eq (f a a) => GHC.Classes.Eq (Data.Type.Combinator.Join f a)
instance forall (k :: BOX) (f :: k -> k -> *) (a :: k). GHC.Classes.Ord (f a a) => GHC.Classes.Ord (Data.Type.Combinator.Join f a)
instance forall (k :: BOX) (f :: k -> k -> *) (a :: k). GHC.Show.Show (f a a) => GHC.Show.Show (Data.Type.Combinator.Join f a)
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k1 -> *) (g :: k -> k1) (a :: k). Type.Class.Witness.Witness p q (f (g a)) => Type.Class.Witness.Witness p q ((Data.Type.Combinator.:.:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k2 -> *) (g :: k -> k1 -> k2) (a :: k) (b :: k1). Type.Class.Witness.Witness p q (f (g a b)) => Type.Class.Witness.Witness p q ((Data.Type.Combinator.:..:) f g a b)
instance Type.Class.HFunctor.HFunctor Data.Type.Combinator.IT
instance Type.Class.HFunctor.HFoldable Data.Type.Combinator.IT
instance Type.Class.HFunctor.HTraversable Data.Type.Combinator.IT
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> *) (a :: k). Type.Class.Witness.Witness p q (f a) => Type.Class.Witness.Witness p q (Data.Type.Combinator.IT f a)
instance forall (k :: BOX) (f :: k -> *) (a :: k). GHC.Num.Num (f a) => GHC.Num.Num (Data.Type.Combinator.IT f a)
instance GHC.Base.Functor Data.Type.Combinator.I
instance GHC.Base.Applicative Data.Type.Combinator.I
instance GHC.Base.Monad Data.Type.Combinator.I
instance Data.Foldable.Foldable Data.Type.Combinator.I
instance Data.Traversable.Traversable Data.Type.Combinator.I
instance Type.Class.Witness.Witness p q a => Type.Class.Witness.Witness p q (Data.Type.Combinator.I a)
instance GHC.Num.Num a => GHC.Num.Num (Data.Type.Combinator.I a)
instance forall (k :: BOX) (k1 :: BOX) (a :: k1). Type.Class.HFunctor.HFunctor (Data.Type.Combinator.LL a)
instance forall (k :: BOX) (k1 :: BOX) (a :: k1). Type.Class.HFunctor.HFoldable (Data.Type.Combinator.LL a)
instance forall (k :: BOX) (k1 :: BOX) (a :: k1). Type.Class.HFunctor.HTraversable (Data.Type.Combinator.LL a)
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (a :: k) (f :: k1 -> *) (g :: k -> k1). Type.Class.Witness.Witness p q (f (g a)) => Type.Class.Witness.Witness p q (Data.Type.Combinator.LL a f g)
instance forall (k :: BOX) (k1 :: BOX) (g :: k1 -> k). Type.Class.HFunctor.HFunctor (Data.Type.Combinator.RR g)
instance forall (k :: BOX) (k1 :: BOX) (g :: k1 -> k). Type.Class.HFunctor.HFoldable (Data.Type.Combinator.RR g)
instance forall (k :: BOX) (k1 :: BOX) (g :: k1 -> k). Type.Class.HFunctor.HTraversable (Data.Type.Combinator.RR g)
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (g :: k -> k1) (f :: k1 -> *) (a :: k). Type.Class.Witness.Witness p q (f (g a)) => Type.Class.Witness.Witness p q (Data.Type.Combinator.RR g f a)
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> k1 -> *) (g :: k -> k1) (a :: k). Type.Class.Witness.Witness p q (f a (g a)) => Type.Class.Witness.Witness p q (Data.Type.Combinator.SS f g a)
instance Type.Class.HFunctor.HFunctor (Data.Type.Combinator.CT r)
instance Type.Class.HFunctor.HFoldable (Data.Type.Combinator.CT r)
instance Type.Class.HFunctor.HTraversable (Data.Type.Combinator.CT r)
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) r (f :: k -> *) (a :: k1). Type.Class.Witness.Witness p q r => Type.Class.Witness.Witness p q (Data.Type.Combinator.CT r f a)
instance forall (k :: BOX) (k1 :: BOX) r (f :: k -> *) (a :: k1). GHC.Num.Num r => GHC.Num.Num (Data.Type.Combinator.CT r f a)
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) r (a :: k). Type.Class.Witness.Witness p q r => Type.Class.Witness.Witness p q (Data.Type.Combinator.C r a)
instance forall (k :: BOX) r (a :: k). GHC.Num.Num r => GHC.Num.Num (Data.Type.Combinator.C r a)
instance forall (k :: BOX) (f :: k -> k -> *) (a :: k). Type.Class.Known.Known (f a) a => Type.Class.Known.Known (Data.Type.Combinator.Join f) a
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> k -> *) (a :: k). Type.Class.Witness.Witness p q (f a a) => Type.Class.Witness.Witness p q (Data.Type.Combinator.Join f a)
instance forall (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (b :: k1) (a :: k). Type.Class.Known.Known (p a) b => Type.Class.Known.Known (Data.Type.Combinator.Flip p b) a
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> k1 -> *) (b :: k1) (a :: k). Type.Class.Witness.Witness p q (f a b) => Type.Class.Witness.Witness p q (Data.Type.Combinator.Flip f b a)
instance forall (k :: BOX) (k1 :: BOX) (p :: (,) k1 k -> *) (a :: k1) (b :: k). Type.Class.Known.Known p (a Type.Family.Tuple.# b) => Type.Class.Known.Known (Data.Type.Combinator.Cur p a) b
instance forall (k :: BOX) (k1 :: BOX) (q :: GHC.Prim.Constraint) (r :: GHC.Prim.Constraint) (p :: (,) k k1 -> *) (a :: k) (b :: k1). Type.Class.Witness.Witness q r (p (a Type.Family.Tuple.# b)) => Type.Class.Witness.Witness q r (Data.Type.Combinator.Cur p a b)
instance forall (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (q :: (,) k k1) (a :: k) (b :: k1). (Type.Class.Known.Known (p a) b, q ~ (a Type.Family.Tuple.# b)) => Type.Class.Known.Known (Data.Type.Combinator.Uncur p) q
instance forall (k :: BOX) (k1 :: BOX) (r :: GHC.Prim.Constraint) (s :: GHC.Prim.Constraint) (p :: k -> k1 -> *) (q :: (,) k k1) (a :: k) (b :: k1). (Type.Class.Witness.Witness r s (p a b), q ~ (a Type.Family.Tuple.# b)) => Type.Class.Witness.Witness r s (Data.Type.Combinator.Uncur p q)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: (,,) k1 k2 k -> *) (a :: k1) (b :: k2) (c :: k). Type.Class.Known.Known p '(a, b, c) => Type.Class.Known.Known (Data.Type.Combinator.Cur3 p a b) c
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (q :: GHC.Prim.Constraint) (r :: GHC.Prim.Constraint) (p :: (,,) k k1 k2 -> *) (a :: k) (b :: k1) (c :: k2). Type.Class.Witness.Witness q r (p '(a, b, c)) => Type.Class.Witness.Witness q r (Data.Type.Combinator.Cur3 p a b c)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: k -> k1 -> k2 -> *) (q :: (,,) k k1 k2) (a :: k) (b :: k1) (c :: k2). (Type.Class.Known.Known (p a b) c, q ~ '(a, b, c)) => Type.Class.Known.Known (Data.Type.Combinator.Uncur3 p) q
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (r :: GHC.Prim.Constraint) (s :: GHC.Prim.Constraint) (p :: k -> k1 -> k2 -> *) (q :: (,,) k k1 k2) (a :: k) (b :: k1) (c :: k2). (Type.Class.Witness.Witness r s (p a b c), q ~ '(a, b, c)) => Type.Class.Witness.Witness r s (Data.Type.Combinator.Uncur3 p q)


-- | Types for working with (and under) existentially and universally
--   quantified types.
--   
--   The <a>Some</a> type can be very useful when working with type-indexed
--   GADTs, where defining instances for classes like <a>Read</a> can be
--   tedious at best, and frequently impossible, for the GADT itself.
module Data.Type.Quantifier
data Some (f :: k -> *) :: *
Some :: f a -> Some f

-- | An eliminator for a <a>Some</a> type.
--   
--   Consider this function akin to a Monadic bind, except instead of
--   binding into a Monad with a sequent function, we're binding into the
--   existential quantification with a universal eliminator function.
--   
--   It serves as an explicit delimiter in a program of where the type
--   index may be used and depended on, and where it may not.
--   
--   NB: the result type of the eliminating function may not refer to the
--   universally quantified type index <tt>a</tt>.
some :: Some f -> (forall a. f a -> r) -> r
withSome :: (forall a. f a -> r) -> Some f -> r
onSome :: (forall a. f a -> g b) -> Some f -> Some g
type Some2 f = Some (Some :.: f)
data All (f :: k -> *) :: *
All :: (forall (a :: k). f a) -> All f
[instAll] :: All f -> forall (a :: k). f a

-- | A data type for natural transformations.
data (:->) (f :: k -> *) (g :: k -> *)
NT :: (forall a. f a -> g a) -> f :-> g
data (:-->) (p :: k -> l -> *) (q :: k -> l -> *)
NT2 :: (forall a b. p a b -> q a b) -> p :--> q


-- | Type combinators for type-level lists, lifting <tt>(f :: k -&gt;
--   *)</tt> to <tt>(Prod f :: [k] -&gt; *)</tt>, as well as its
--   constructions, manipulations, and eliminations.
--   
--   <a>Prod</a> is similar in nature to a few others in the Haskell
--   ecosystem, such as:
--   
--   Oleg's <tt>HList</tt>, from
--   <a>http://hackage.haskell.org/package/HList</a>, and
--   
--   Kenneth Foner's <tt>ConicList</tt>, from
--   <a>http://hackage.haskell.org/package/IndexedList-0.1.0.1/docs/Data-List-Indexed-Conic.html</a>.
module Data.Type.Product
data Prod (f :: k -> *) :: [k] -> *
Ø :: Prod f Ø
(:<) :: !(f a) -> !(Prod f as) -> Prod f (a :< as)

-- | Construct a two element Prod. Since the precedence of (:&gt;) is
--   higher than (:&lt;), we can conveniently write lists like:
--   
--   <pre>
--   &gt;&gt;&gt; a :&lt; b :&gt; c
--   </pre>
--   
--   Which is identical to:
--   
--   <pre>
--   &gt;&gt;&gt; a :&lt; b :&lt; c :&lt; Ø
--   </pre>

-- | Build a singleton Prod.
only :: f a -> Prod f '[a]

-- | snoc function. insert an element at the end of the list.
(>:) :: Prod f as -> f a -> Prod f (as >: a)
head' :: Prod f (a :< as) -> f a
tail' :: Prod f (a :< as) -> Prod f as

-- | Get all but the last element of a non-empty Prod.
init' :: Prod f (a :< as) -> Prod f (Init' a as)

-- | Get the last element of a non-empty Prod.
last' :: Prod f (a :< as) -> f (Last' a as)
reverse' :: Prod f as -> Prod f (Reverse as)
append' :: Prod f as -> Prod f bs -> Prod f (as ++ bs)

-- | A Prod of simple Haskell types.
type Tuple = Prod I

-- | Singleton Tuple.
only_ :: a -> Tuple '[a]

-- | Cons onto a Tuple.

-- | Snoc onto a Tuple.
(>::) :: Tuple as -> a -> Tuple (as >: a)
onHead' :: (f a -> f b) -> Prod f (a :< as) -> Prod f (b :< as)
onTail' :: (Prod f as -> Prod f bs) -> Prod f (a :< as) -> Prod f (a :< bs)
uncurry' :: (f a -> Prod f as -> r) -> Prod f (a :< as) -> r
curry' :: (l ~ (a :< as)) => (Prod f l -> r) -> f a -> Prod f as -> r
index :: Index as a -> Prod f as -> f a
instance Type.Class.HFunctor.HFunctor Data.Type.Product.Prod
instance Type.Class.HFunctor.HIxFunctor Data.Type.Index.Index Data.Type.Product.Prod
instance Type.Class.HFunctor.HFoldable Data.Type.Product.Prod
instance Type.Class.HFunctor.HIxFoldable Data.Type.Index.Index Data.Type.Product.Prod
instance Type.Class.HFunctor.HTraversable Data.Type.Product.Prod
instance forall (k :: BOX) (f :: k -> *). Type.Class.Known.Known (Data.Type.Product.Prod f) Type.Family.List.Ø
instance forall (k :: BOX) (f :: k -> *) (a :: k) (as :: [k]). (Type.Class.Known.Known f a, Type.Class.Known.Known (Data.Type.Product.Prod f) as) => Type.Class.Known.Known (Data.Type.Product.Prod f) (a Type.Family.List.:< as)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Witness.Witness Type.Family.Constraint.ØC Type.Family.Constraint.ØC (Data.Type.Product.Prod f Type.Family.List.Ø)
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (s :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (t :: GHC.Prim.Constraint) (f :: k -> *) (a :: k) (as :: [k]). (Type.Class.Witness.Witness p q (f a), Type.Class.Witness.Witness s t (Data.Type.Product.Prod f as)) => Type.Class.Witness.Witness (p, s) (q, t) (Data.Type.Product.Prod f (a Type.Family.List.:< as))


-- | A <tt>singleton</tt>-esque type for representing Peano natural
--   numbers.
module Data.Type.Nat
data Nat :: N -> *
Z_ :: Nat Z
S_ :: !(Nat n) -> Nat (S n)

-- | <tt><a>Z_</a></tt> is the canonical construction of a <tt><a>Nat</a>
--   Z</tt>.

-- | If <tt>n</tt> is a canonical construction of <tt>Nat n</tt>,
--   <tt><a>S_</a> n</tt> is the canonical construction of <tt>Nat (S
--   n)</tt>.

-- | A <tt>Nat n</tt> is a <a>Witness</a> that there is a canonical
--   construction for <tt>Nat n</tt>.
_Z :: Z :~: Z
_S :: x :~: y -> S x :~: S y
_s :: S x :~: S y -> x :~: y
_ZneS :: Z :~: S x -> Void

-- | A proof that <a>Z</a> is also a right identity for the addition of
--   type-level <a>Nat</a>s.
addZ :: Nat x -> (x + Z) :~: x
addS :: Nat x -> Nat y -> S (x + y) :~: (x + S y)
(.+) :: Nat x -> Nat y -> Nat (x + y)
(.*) :: Nat x -> Nat y -> Nat (x * y)
(.^) :: Nat x -> Nat y -> Nat (x ^ y)
nat :: Nat n -> Int
n0 :: Nat N0
n1 :: Nat N1
n2 :: Nat N2
n3 :: Nat N3
n4 :: Nat N4
n5 :: Nat N5
n6 :: Nat N6
n7 :: Nat N7
n8 :: Nat N8
n9 :: Nat N9
n10 :: Nat N10
instance GHC.Classes.Eq (Data.Type.Nat.Nat n)
instance GHC.Classes.Ord (Data.Type.Nat.Nat n)
instance GHC.Show.Show (Data.Type.Nat.Nat n)
instance Type.Class.Known.Known Data.Type.Nat.Nat 'Type.Family.Nat.Z
instance Type.Class.Known.Known Data.Type.Nat.Nat n => Type.Class.Known.Known Data.Type.Nat.Nat ('Type.Family.Nat.S n)
instance Type.Class.Witness.Witness Type.Family.Constraint.ØC (Type.Class.Known.Known Data.Type.Nat.Nat n) (Data.Type.Nat.Nat n)
instance Data.Type.Equality.TestEquality Data.Type.Nat.Nat
instance Type.Class.Witness.DecEquality Data.Type.Nat.Nat


-- | A <tt>singleton</tt>-esque type for representing members of finite
--   sets.
module Data.Type.Fin
data Fin :: N -> *
FZ :: Fin (S n)
FS :: !(Fin n) -> Fin (S n)

-- | Gives the list of all members of the finite set of size <tt>n</tt>.
fins :: Nat n -> [Fin n]
fin :: Fin n -> Int

-- | There are no members of <tt>Fin Z</tt>.
finZ :: Fin Z -> Void
weaken :: Fin n -> Fin (S n)

-- | Map a finite set to a lower finite set without one of its members.
without :: Fin n -> Fin n -> Maybe (Fin (Pred n))
class (<=) (x :: N) (y :: N)
weakenN :: (<=) x y => Fin x -> Fin y

-- | Take a <a>Fin</a> to an existentially quantified <a>Nat</a>.
finNat :: Fin x -> Some Nat

-- | A <tt>Fin n</tt> is a <a>Witness</a> that <tt>n &gt;= 1</tt>.
--   
--   That is, <tt><a>Pred</a> n</tt> is well defined.
instance GHC.Classes.Eq (Data.Type.Fin.Fin n)
instance GHC.Classes.Ord (Data.Type.Fin.Fin n)
instance GHC.Show.Show (Data.Type.Fin.Fin n)
instance x Data.Type.Fin.<= x
instance (x Data.Type.Fin.<= y) => x Data.Type.Fin.<= 'Type.Family.Nat.S y
instance (n' ~ Type.Family.Nat.Pred n) => Type.Class.Witness.Witness Type.Family.Constraint.ØC ('Type.Family.Nat.S n' ~ n) (Data.Type.Fin.Fin n)


-- | A <a>QuasiQuoter</a> for the <a>N</a> kind and the <a>Nat</a> type.
module Data.Type.Nat.Quote
n :: QuasiQuoter
parseNatExp :: String -> Q Exp
parseNatPat :: String -> Q Pat
parseNatType :: String -> Q Type


-- | Type combinators for type-level lists, where we have many functors
--   with a single index.
module Data.Type.Product.Dual
data FProd (fs :: [k -> *]) :: k -> *
ØF :: FProd Ø a
(:<<) :: !(f a) -> !(FProd fs a) -> FProd (f :< fs) a

-- | Construct a two element FProd. Since the precedence of (:&gt;&gt;) is
--   higher than (:&lt;&lt;), we can conveniently write lists like:
--   
--   <pre>
--   &gt;&gt;&gt; a :&lt;&lt; b :&gt;&gt; c
--   </pre>
--   
--   Which is identical to:
--   
--   <pre>
--   &gt;&gt;&gt; a :&lt;&lt; b :&lt;&lt; c :&lt;&lt; Ø
--   </pre>

-- | Build a singleton FProd.
onlyF :: f a -> FProd '[f] a

-- | snoc function. insert an element at the end of the FProd.
(>>:) :: FProd fs a -> f a -> FProd (fs >: f) a
headF :: FProd (f :< fs) a -> f a
tailF :: FProd (f :< fs) a -> FProd fs a

-- | Get all but the last element of a non-empty FProd.
initF :: FProd (f :< fs) a -> FProd (Init' f fs) a

-- | Get the last element of a non-empty FProd.
lastF :: FProd (f :< fs) a -> Last' f fs a

-- | Reverse the elements of an FProd.
reverseF :: FProd fs a -> FProd (Reverse fs) a

-- | Append two FProds.
appendF :: FProd fs a -> FProd gs a -> FProd (fs ++ gs) a

-- | Map over the head of a non-empty FProd.
onHeadF :: (f a -> g a) -> FProd (f :< fs) a -> FProd (g :< fs) a

-- | Map over the tail of a non-empty FProd.
onTailF :: (FProd fs a -> FProd gs a) -> FProd (f :< fs) a -> FProd (f :< gs) a
uncurryF :: (f a -> FProd fs a -> r) -> FProd (f :< fs) a -> r
curryF :: (l ~ (f :< fs)) => (FProd l a -> r) -> f a -> FProd fs a -> r
indexF :: Index fs f -> FProd fs a -> f a

-- | If all <tt>f</tt> in <tt>fs</tt> are <tt>Functor</tt>s, then <tt>FProd
--   fs</tt> is a <tt>Functor</tt>.

-- | If all <tt>f</tt> in <tt>fs</tt> are <tt>Foldable</tt>s, then
--   <tt>FProd fs</tt> is a <tt>Foldable</tt>.

-- | If all <tt>f</tt> in <tt>fs</tt> are <tt>Traversable</tt>s, then
--   <tt>FProd fs</tt> is a <tt>Traversable</tt>.

-- | Map over all elements of an FProd with access to the element's index.
imapF :: (forall f. Index fs f -> f a -> f b) -> FProd fs a -> FProd fs b

-- | Fold over all elements of an FProd with access to the element's index.
ifoldMapF :: Monoid m => (forall f. Index fs f -> f a -> m) -> FProd fs a -> m

-- | Traverse over all elements of an FProd with access to the element's
--   index.
itraverseF :: Applicative g => (forall f. Index fs f -> f a -> g (f b)) -> FProd fs a -> g (FProd fs b)

-- | An empty FProd is a no-op Witness.

-- | A non-empty FProd is a Witness if both its head and tail are
--   Witnesses.
instance Type.Family.List.ListC (GHC.Base.Functor Type.Family.List.<$> fs) => GHC.Base.Functor (Data.Type.Product.Dual.FProd fs)
instance Type.Family.List.ListC (Data.Foldable.Foldable Type.Family.List.<$> fs) => Data.Foldable.Foldable (Data.Type.Product.Dual.FProd fs)
instance (Type.Family.List.ListC (GHC.Base.Functor Type.Family.List.<$> fs), Type.Family.List.ListC (Data.Foldable.Foldable Type.Family.List.<$> fs), Type.Family.List.ListC (Data.Traversable.Traversable Type.Family.List.<$> fs)) => Data.Traversable.Traversable (Data.Type.Product.Dual.FProd fs)
instance forall (k :: BOX) (a :: k). Type.Class.Known.Known (Data.Type.Product.Dual.FProd Type.Family.List.Ø) a
instance forall (k :: BOX) (f :: k -> *) (fs :: [k -> *]) (a :: k). (Type.Class.Known.Known f a, Type.Class.Known.Known (Data.Type.Product.Dual.FProd fs) a) => Type.Class.Known.Known (Data.Type.Product.Dual.FProd (f Type.Family.List.:< fs)) a
instance forall (k :: BOX) (a :: k). Type.Class.Witness.Witness Type.Family.Constraint.ØC Type.Family.Constraint.ØC (Data.Type.Product.Dual.FProd Type.Family.List.Ø a)
instance forall (k :: BOX) (p :: GHC.Prim.Constraint) (s :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (t :: GHC.Prim.Constraint) (f :: k -> *) (fs :: [k -> *]) (a :: k). (Type.Class.Witness.Witness p q (f a), Type.Class.Witness.Witness s t (Data.Type.Product.Dual.FProd fs a)) => Type.Class.Witness.Witness (p, s) (q, t) (Data.Type.Product.Dual.FProd (f Type.Family.List.:< fs) a)


-- | <a>V</a> and its combinator analog <a>VT</a> represent lists of known
--   length, characterized by the index <tt>(n :: N)</tt> in <tt><a>V</a> n
--   a</tt> or <tt><a>VT</a> n f a</tt>.
--   
--   The classic example used ad nauseum for type-level programming.
--   
--   The operations on <a>V</a> and <a>VT</a> correspond to the type level
--   arithmetic operations on the kind <a>N</a>.
module Data.Type.Vector
data VT (n :: N) (f :: k -> *) :: k -> *
ØV :: VT Z f a
(:*) :: !(f a) -> !(VT n f a) -> VT (S n) f a
type V n = VT n I
(.++) :: VT x f a -> VT y f a -> VT (x + y) f a
vrep :: Known Nat n => f a -> VT n f a
head' :: VT (S n) f a -> f a
tail' :: VT (S n) f a -> VT n f a
onTail :: (VT m f a -> VT n f a) -> VT (S m) f a -> VT (S n) f a
vDel :: Fin n -> VT n f a -> VT (Pred n) f a
imap :: (Fin n -> f a -> g b) -> VT n f a -> VT n g b
ifoldMap :: Monoid m => (Fin n -> f a -> m) -> VT n f a -> m
itraverse :: Applicative h => (Fin n -> f a -> h (g b)) -> VT n f a -> h (VT n g b)
index :: Fin n -> VT n f a -> f a
vmap :: (f a -> g b) -> VT n f a -> VT n g b
vap :: (f a -> g b -> h c) -> VT n f a -> VT n g b -> VT n h c
vfoldr :: (f a -> b -> b) -> b -> VT n f a -> b
vfoldMap' :: (b -> b -> b) -> b -> (f a -> b) -> VT n f a -> b
vfoldMap :: Monoid m => (f a -> m) -> VT n f a -> m
withVT :: [f a] -> (forall n. VT n f a -> r) -> r
withV :: [a] -> (forall n. V n a -> r) -> r
findV :: Eq a => a -> V n a -> Maybe (Fin n)
findVT :: Eq (f a) => f a -> VT n f a -> Maybe (Fin n)
newtype M ns a
M :: Matrix ns a -> M ns a
[getMatrix] :: M ns a -> Matrix ns a
vgen_ :: Known Nat n => (Fin n -> f a) -> VT n f a
vgen :: Nat n -> (Fin n -> f a) -> VT n f a
mgen_ :: Known (Prod Nat) ns => (Prod Fin ns -> a) -> M ns a
mgen :: Prod Nat ns -> (Prod Fin ns -> a) -> M ns a
onMatrix :: (Matrix ms a -> Matrix ns b) -> M ms a -> M ns b
diagonal :: VT n (VT n f) a -> VT n f a
vtranspose :: Known Nat n => VT m (VT n f) a -> VT n (VT m f) a
transpose :: Known Nat n => M (m :< (n :< ns)) a -> M (n :< (m :< ns)) a
m0 :: M Ø Int
m1 :: M '[N2] Int
m2 :: M '[N2, N4] Int
m3 :: M '[N2, N3, N4] (Int, Int, Int)
m4 :: M '[N2, N3, N4, N5] (Int, Int, Int, Int)
ppVec :: (VT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VT n f a -> ShowS
ppMatrix :: (Show a, Known Length ns) => M ns a -> IO ()
ppMatrix' :: Show a => Length ns -> Matrix ns a -> ShowS
mzipWith :: Monoid a => (a -> a -> b) -> [a] -> [a] -> [b]
zipLines :: (ShowS -> ShowS -> ShowS) -> ShowS -> ShowS -> ShowS
compose :: Foldable f => f (a -> a) -> a -> a
instance forall (k :: BOX) (n :: Type.Family.Nat.N) (f :: k -> *) (a :: k). GHC.Classes.Eq (f a) => GHC.Classes.Eq (Data.Type.Vector.VT n f a)
instance forall (k :: BOX) (n :: Type.Family.Nat.N) (f :: k -> *) (a :: k). GHC.Classes.Ord (f a) => GHC.Classes.Ord (Data.Type.Vector.VT n f a)
instance forall (k :: BOX) (n :: Type.Family.Nat.N) (f :: k -> *) (a :: k). GHC.Show.Show (f a) => GHC.Show.Show (Data.Type.Vector.VT n f a)
instance GHC.Classes.Eq (Data.Type.Vector.Matrix ns a) => GHC.Classes.Eq (Data.Type.Vector.M ns a)
instance GHC.Classes.Ord (Data.Type.Vector.Matrix ns a) => GHC.Classes.Ord (Data.Type.Vector.M ns a)
instance GHC.Show.Show (Data.Type.Vector.Matrix ns a) => GHC.Show.Show (Data.Type.Vector.M ns a)
instance GHC.Base.Functor f => GHC.Base.Functor (Data.Type.Vector.VT n f)
instance (GHC.Base.Applicative f, Type.Class.Known.Known Data.Type.Nat.Nat n) => GHC.Base.Applicative (Data.Type.Vector.VT n f)
instance (GHC.Base.Monad f, Type.Class.Known.Known Data.Type.Nat.Nat n) => GHC.Base.Monad (Data.Type.Vector.VT n f)
instance Data.Foldable.Foldable f => Data.Foldable.Foldable (Data.Type.Vector.VT n f)
instance Data.Traversable.Traversable f => Data.Traversable.Traversable (Data.Type.Vector.VT n f)
instance forall (k :: BOX) (n :: Type.Family.Nat.N) (f :: k -> *) (a :: k). Type.Class.Witness.Witness Type.Family.Constraint.ØC (Type.Class.Known.Known Data.Type.Nat.Nat n) (Data.Type.Vector.VT n f a)
instance forall (k :: BOX) (n :: Type.Family.Nat.N) (f :: k -> *) (a :: k). (GHC.Num.Num (f a), Type.Class.Known.Known Data.Type.Nat.Nat n) => GHC.Num.Num (Data.Type.Vector.VT n f a)
instance GHC.Num.Num (Data.Type.Vector.Matrix ns a) => GHC.Num.Num (Data.Type.Vector.M ns a)