-- 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.2.4.0


-- | 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)
type Fail = True ~ False
class IffC b t f => Iff (b :: Bool) (t :: Constraint) (f :: Constraint) where type IffC b t f :: Constraint where {
    type family IffC b t f :: Constraint;
}
class d (c a) => Comp (d :: l -> Constraint) (c :: k -> l) (a :: k)

-- | The kind of constraints, like <tt>Show a</tt>
data Constraint :: *
instance t => Type.Family.Constraint.Iff 'GHC.Types.True t f
instance f => Type.Family.Constraint.Iff 'GHC.Types.False t f
instance forall k l (d :: l -> GHC.Types.Constraint) (c :: k -> l) (a :: k). d (c a) => Type.Family.Constraint.Comp d c a


-- | 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 KnownC f a :: Constraint type KnownC (f :: k -> *) (a :: k) = ØC where {
    type family KnownC f a :: Constraint;
    type KnownC (f :: k -> *) (a :: k) = ØC;
}
known :: Known f a => f a
instance forall k (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] :: c => Wit c
data Wit1 :: (k -> Constraint) -> k -> *
[Wit1] :: c a => 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] :: {getSub :: p => Wit q} -> p :- q
transC :: (b :- c) -> (a :- b) -> a :- c

-- | 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 WitnessC p q t :: Constraint type WitnessC p q t = ØC where {
    type family WitnessC p q t :: Constraint;
    type WitnessC p q t = ØC;
}
(\\) :: (Witness p q t, p) => (q => r) -> t -> r
(//) :: (Witness p q t, p) => t -> (q => r) -> r
infixr 0 //

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

-- | Convert a <a>Witness</a> to a canonical reified entailment.
entailed :: Witness p q t => t -> p :- q
class Fails (c :: Constraint)
failC :: Fails c => c :- Fail
absurdC :: Fails a => a :- b
class c => Const (c :: Constraint) (d :: k)
constC :: Const c d => Wit c
class f (g a) => (∘) (f :: l -> Constraint) (g :: k -> l) (a :: k)
compC :: (∘) f g a => Wit (f (g a))
class (f a, g a) => (∧) (f :: k -> Constraint) (g :: k -> Constraint) (a :: k)
conjC :: (∧) f g a => (Wit (f a), Wit (g a))
class (∨) (f :: k -> Constraint) (g :: k -> Constraint) (a :: k)
disjC :: (∨) f g a => Either (Wit (f a)) (Wit (g a))
eitherC :: forall f g a b. f a :- b -> g a :- b -> (f ∨ g) a :- b
pureC :: b => a :- b
contraC :: a :- Fail -> a :- b
class Forall (p :: k -> Constraint) (q :: k -> Constraint) where forall = pureC
forall :: Forall p q => p a :- q a
forall :: (Forall p q, q a) => p a :- q a
toEquality :: (a ~ b) :- (c ~ d) -> a :~: b -> c :~: d
commute :: (a ~ b) :- (b ~ a)
falso :: (b ~ False) :- Holds b c
top :: a :- ØC
bottom :: Fail :- c

-- | 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
infixr 0 //?
(//?+) :: (Witness p q t, p) => Either e t -> (q => Either e r) -> Either e r
infixr 0 //?+
witMaybe :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r -> Maybe r
qed :: Maybe (a :~: a)
impossible :: a -> Void
exFalso :: Wit Fail -> a
(=?=) :: TestEquality f => f a -> f b -> Maybe (a :~: b)
infix 4 =?=
class TestEquality1 (f :: k -> l -> *)
testEquality1 :: TestEquality1 f => f a c -> f b c -> Maybe (a :~: b)
(=??=) :: TestEquality1 f => f a c -> f b c -> Maybe (a :~: b)
infix 4 =??=
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
absurd :: Arrow p => p Void a
instance Control.Category.Category (Type.Class.Witness.:-)
instance forall k (c :: GHC.Types.Constraint) (d :: k). c => Type.Class.Witness.Const c d
instance forall k l (f :: l -> GHC.Types.Constraint) (g :: k -> l) (a :: k). f (g a) => (Type.Class.Witness.∘) f g a
instance forall k (f :: k -> GHC.Types.Constraint) (a :: k) (g :: k -> GHC.Types.Constraint). (f a, g a) => (Type.Class.Witness.∧) f g a
instance Type.Class.Witness.Witness Type.Family.Constraint.ØC c (Type.Class.Witness.Wit c)
instance forall k (c :: k -> GHC.Types.Constraint) (a :: k). Type.Class.Witness.Witness Type.Family.Constraint.ØC (c a) (Type.Class.Witness.Wit1 c a)
instance Type.Class.Witness.Witness p q (p Type.Class.Witness.:- q)
instance forall k (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 (c :: k -> GHC.Types.Constraint) (a :: k). c a => Type.Class.Known.Known (Type.Class.Witness.Wit1 c) a


-- | Higher order analogs of type classes from the Prelude, and quantifier
--   data types.
module Type.Class.Higher
class Eq1 (f :: k -> *) where eq1 = (==) neq1 a b = not $ eq1 a b
eq1 :: Eq1 f => f a -> f a -> Bool
eq1 :: (Eq1 f, Eq (f a)) => f a -> f a -> Bool
neq1 :: Eq1 f => f a -> f a -> Bool
(=#=) :: Eq1 f => f a -> f a -> Bool
infix 4 =#=
class Eq2 (f :: k -> l -> *) where eq2 = (==) neq2 a b = not $ eq2 a b
eq2 :: Eq2 f => f a b -> f a b -> Bool
eq2 :: (Eq2 f, Eq (f a b)) => f a b -> f a b -> Bool
neq2 :: Eq2 f => f a b -> f a b -> Bool
(=##=) :: Eq2 f => f a b -> f a b -> Bool
infix 4 =##=
class Eq3 (f :: k -> l -> m -> *) where eq3 = (==) neq3 a b = not $ eq3 a b
eq3 :: Eq3 f => f a b c -> f a b c -> Bool
eq3 :: (Eq3 f, Eq (f a b c)) => f a b c -> f a b c -> Bool
neq3 :: Eq3 f => f a b c -> f a b c -> Bool
(=###=) :: Eq3 f => f a b c -> f a b c -> Bool
infix 4 =###=
class Eq1 f => Ord1 (f :: k -> *) where compare1 = compare a <# b = compare1 a b == LT a ># b = compare1 a b == GT a <=# b = compare1 a b /= GT a >=# b = compare1 a b /= LT
compare1 :: Ord1 f => f a -> f a -> Ordering
compare1 :: (Ord1 f, Ord (f a)) => f a -> f a -> Ordering
(<#) :: Ord1 f => f a -> f a -> Bool
(>#) :: Ord1 f => f a -> f a -> Bool
(<=#) :: Ord1 f => f a -> f a -> Bool
(>=#) :: Ord1 f => f a -> f a -> Bool
class Eq2 f => Ord2 (f :: k -> l -> *) where compare2 = compare a <## b = compare2 a b == LT a >## b = compare2 a b == GT a <=## b = compare2 a b /= GT a >=## b = compare2 a b /= LT
compare2 :: Ord2 f => f a b -> f a b -> Ordering
compare2 :: (Ord2 f, Ord (f a b)) => f a b -> f a b -> Ordering
(<##) :: Ord2 f => f a b -> f a b -> Bool
(>##) :: Ord2 f => f a b -> f a b -> Bool
(<=##) :: Ord2 f => f a b -> f a b -> Bool
(>=##) :: Ord2 f => f a b -> f a b -> Bool
class Eq3 f => Ord3 (f :: k -> l -> m -> *) where compare3 = compare a <### b = compare3 a b == LT a >### b = compare3 a b == GT a <=### b = compare3 a b /= GT a >=### b = compare3 a b /= LT
compare3 :: Ord3 f => f a b c -> f a b c -> Ordering
compare3 :: (Ord3 f, Ord (f a b c)) => f a b c -> f a b c -> Ordering
(<###) :: Ord3 f => f a b c -> f a b c -> Bool
(>###) :: Ord3 f => f a b c -> f a b c -> Bool
(<=###) :: Ord3 f => f a b c -> f a b c -> Bool
(>=###) :: Ord3 f => f a b c -> f a b c -> Bool
class Show1 (f :: k -> *) where showsPrec1 = showsPrec show1 = ($ "") . shows1
showsPrec1 :: Show1 f => Int -> f a -> ShowS
showsPrec1 :: (Show1 f, Show (f a)) => Int -> f a -> ShowS
show1 :: Show1 f => f a -> String
shows1 :: Show1 f => f a -> ShowS
class Show2 (f :: k -> l -> *) where showsPrec2 = showsPrec show2 = ($ "") . shows2
showsPrec2 :: Show2 f => Int -> f a b -> ShowS
showsPrec2 :: (Show2 f, Show (f a b)) => Int -> f a b -> ShowS
show2 :: Show2 f => f a b -> String
shows2 :: Show2 f => f a b -> ShowS
class Show3 (f :: k -> l -> m -> *) where showsPrec3 = showsPrec show3 = ($ "") . shows3
showsPrec3 :: Show3 f => Int -> f a b c -> ShowS
showsPrec3 :: (Show3 f, Show (f a b c)) => Int -> f a b c -> ShowS
show3 :: Show3 f => f a b c -> String
shows3 :: Show3 f => f a b c -> ShowS
class Read1 (f :: k -> *)
readsPrec1 :: Read1 f => Int -> ReadS (Some f)
reads1 :: Read1 f => ReadS (Some f)
readMaybe1 :: Read1 f => String -> Maybe (Some f)
class Read2 (f :: k -> l -> *)
readsPrec2 :: Read2 f => Int -> ReadS (Some2 f)
reads2 :: Read2 f => ReadS (Some2 f)
readMaybe2 :: Read2 f => String -> Maybe (Some2 f)
class Read3 (f :: k -> l -> m -> *)
readsPrec3 :: Read3 f => Int -> ReadS (Some3 f)
reads3 :: Read3 f => ReadS (Some3 f)
readMaybe3 :: Read3 f => String -> Maybe (Some3 f)
class Functor1 (t :: (k -> *) -> l -> *)

-- | Take a natural transformation to a lifted natural transformation.
map1 :: Functor1 t => (forall (a :: k). f a -> g a) -> t f b -> t g b
class IxFunctor1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i
imap1 :: IxFunctor1 i t => (forall (a :: k). i b a -> f a -> g a) -> t f b -> t g b
class Foldable1 (t :: (k -> *) -> l -> *)
foldMap1 :: (Foldable1 t, Monoid m) => (forall (a :: k). f a -> m) -> t f b -> m
class IxFoldable1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i
ifoldMap1 :: (IxFoldable1 i t, Monoid m) => (forall (a :: k). i b a -> f a -> m) -> t f b -> m
class (Functor1 t, Foldable1 t) => Traversable1 (t :: (k -> *) -> l -> *)
traverse1 :: (Traversable1 t, Applicative h) => (forall (a :: k). f a -> h (g a)) -> t f b -> h (t g b)
class (IxFunctor1 i t, IxFoldable1 i t) => IxTraversable1 (i :: l -> k -> *) (t :: (k -> *) -> l -> *) | t -> i
itraverse1 :: (IxTraversable1 i t, Applicative h) => (forall (a :: k). i b a -> f a -> h (g a)) -> t f b -> h (t g b)
class Bifunctor1 (t :: (k -> *) -> (l -> *) -> m -> *)
bimap1 :: Bifunctor1 t => (forall (a :: k). f a -> h a) -> (forall (a :: l). g a -> i a) -> t f g b -> t h i b
class IxBifunctor1 (i :: m -> k -> *) (j :: m -> l -> *) (t :: (k -> *) -> (l -> *) -> m -> *) | t -> i j
ibimap1 :: IxBifunctor1 i j t => (forall (a :: k). i b a -> f a -> f' a) -> (forall (a :: l). j b a -> g a -> g' a) -> t f g b -> t f' g' b
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
(>>-) :: Some f -> (forall a. f a -> r) -> r
infixl 1 >>-
(>->) :: (forall x. f x -> Some g) -> (forall x. g x -> Some h) -> f a -> Some h
infixr 1 >->
withSome :: (forall a. f a -> r) -> Some f -> r
onSome :: (forall a. f a -> g x) -> Some f -> Some g
msome :: Monad m => f a -> m (Some f)
(>>=-) :: Monad m => m (Some f) -> (forall a. f a -> m r) -> m r
infixl 1 >>=-
data Some2 (f :: k -> l -> *) :: *
[Some2] :: f a b -> Some2 f
some2 :: Some2 f -> (forall a b. f a b -> r) -> r
(>>--) :: Some2 f -> (forall a b. f a b -> r) -> r
infixl 1 >>--
(>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h
infixr 1 >-->
withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g
msome2 :: Monad m => f a b -> m (Some2 f)
(>>=--) :: Monad m => m (Some2 f) -> (forall a b. f a b -> m r) -> m r
infixl 1 >>=--
data Some3 (f :: k -> l -> m -> *) :: *
[Some3] :: f a b c -> Some3 f
some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r
(>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r
infixl 1 >>---
(>--->) :: (forall x y z. f x y z -> Some3 g) -> (forall x y z. g x y z -> Some3 h) -> f a b c -> Some3 h
infixr 1 >--->
withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r
onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g
msome3 :: Monad m => f a b c -> m (Some3 f)
(>>=---) :: Monad m => m (Some3 f) -> (forall a b c. f a b c -> m r) -> m r
infixl 1 >>=---
data SomeC (c :: k -> Constraint) (f :: k -> *)
[SomeC] :: c a => f a -> SomeC c f
someC :: SomeC c f -> (forall a. c a => f a -> r) -> r
(>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r
infixl 1 >>~
msomeC :: (Monad m, c a) => f a -> m (SomeC c f)
(>>=~) :: Monad m => m (SomeC c f) -> (forall a. c a => f a -> m r) -> m r
infixl 1 >>=~
instance forall k (f :: k -> *). (Data.Type.Equality.TestEquality f, Type.Class.Higher.Eq1 f) => GHC.Classes.Eq (Type.Class.Higher.Some f)


-- | Type-level pairs and triples, along with some convenient aliases and
--   type families over them.
module Type.Family.Tuple
type (#) = (,)
fstCong :: (p ~ q) :- (Fst p ~ Fst q)
sndCong :: (p ~ q) :- (Snd p ~ Snd q)
fst3Cong :: (p ~ q) :- (Fst3 p ~ Fst3 q)
snd3Cong :: (p ~ q) :- (Snd3 p ~ Snd3 q)
thd3Cong :: (p ~ q) :- (Thd3 p ~ Thd3 q)
pairMapCong :: (f ~ g, a ~ b) :- ((f <$> a) ~ (g <$> b))


-- | 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]
nullCong :: (a ~ b) :- (Null a ~ Null b)
nilNotCons :: (Ø ~ (a :< as)) :- Fail

-- | Appends two type-level lists.
appendCong :: (a ~ b, c ~ d) :- ((a ++ c) ~ (b ++ d))
concatCong :: (as ~ bs) :- (Concat as ~ Concat bs)

-- | Type-level list snoc.
snocCong :: (as ~ bs, a ~ b) :- ((as >: a) ~ (bs >: b))
reverseCong :: (as ~ bs) :- (Reverse as ~ Reverse bs)
initCong :: (a ~ b, as ~ bs) :- (Init' a as ~ Init' b bs)
lastCong :: (a ~ b, as ~ bs) :- (Last' a as ~ Last' b bs)

-- | 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>.
listMapCong :: (f ~ g, as ~ bs) :- ((f <$> as) ~ (g <$> bs))

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

module Data.Type.Index.Trans
type IxList' = IxList (:~:)
type IxEnv = IxList (IxFirst (:~:))
class IxLift (t :: (k -> m -> *) -> l -> m -> *) (x :: l) where type LiftI t x :: k where {
    type family LiftI t x :: k;
}
ixLift :: IxLift t x => i (LiftI t x) y -> t i x y
data IxList (i :: k -> l -> *) :: [k] -> l -> *
[IxHead] :: !(i a b) -> IxList i (a :< as) b
[IxTail] :: !(IxList i as b) -> IxList i (a :< as) b
data IxFirst (i :: k -> l -> *) :: (k, m) -> l -> *
[IxFirst] :: !(i a b) -> IxFirst i '(a, c) b
data IxSecond (i :: k -> l -> *) :: (m, k) -> l -> *
[IxSecond] :: !(i a b) -> IxSecond i '(c, a) b
data IxOr (i :: k -> m -> *) (j :: l -> m -> *) :: Either k l -> m -> *
[IxOrL] :: !(i a b) -> IxOr i j (Left a) b
[IxOrR] :: !(j a b) -> IxOr i j (Right a) b
data IxJust (i :: k -> l -> *) :: Maybe k -> l -> *
[IxJust] :: !(i a b) -> IxJust i (Just a) b
data IxComp (i :: k -> l -> *) (j :: l -> m -> *) :: k -> m -> *
[IxComp] :: !(i a b) -> !(j b c) -> IxComp i j a c

-- | Propositional equality. If <tt>a :~: b</tt> is inhabited by some
--   terminating value, then the type <tt>a</tt> is the same as the type
--   <tt>b</tt>. To use this equality in practice, pattern-match on the
--   <tt>a :~: b</tt> to get out the <tt>Refl</tt> constructor; in the body
--   of the pattern-match, the compiler knows that <tt>a ~ b</tt>.
data (:~:) k (a :: k) (b :: k) :: forall k. k -> k -> *
[Refl] :: (:~:) k a a
instance forall m k m1 (p :: (k, m1)). p ~ '(Type.Family.Tuple.Fst p, Type.Family.Tuple.Snd p) => Data.Type.Index.Trans.IxLift Data.Type.Index.Trans.IxFirst p
instance forall m k m1 (p :: (m1, k)). p ~ '(Type.Family.Tuple.Fst p, Type.Family.Tuple.Snd p) => Data.Type.Index.Trans.IxLift Data.Type.Index.Trans.IxSecond p
instance forall m k k1 (i :: k1 -> m -> GHC.Types.*) (a :: k). Data.Type.Index.Trans.IxLift (Data.Type.Index.Trans.IxOr i) ('Data.Either.Right a)


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

-- | Take a <tt>Maybe Constraint</tt> to a <tt>Constraint</tt>.
leftCong :: (a ~ b) :- (IsLeft a ~ IsLeft b)
rightCong :: (a ~ b) :- (IsRight a ~ IsRight b)
leftNotRight :: (Left a ~ Right b) :- Fail

-- | Map over a type-level <tt>Maybe</tt>.
eitherFmapCong :: (f ~ g, a ~ b) :- ((f <$> a) ~ (g <$> b))
eitherPamfCong :: (f ~ g, a ~ b) :- ((f <&> a) ~ (g <&> b))
eitherApCong :: (f ~ g, a ~ b) :- ((f <*> a) ~ (g <*> b))
eitherAltCong :: (a ~ c, b ~ d) :- ((a <|> b) ~ (c <|> d))
fromLeftCong :: (a ~ b) :- (FromLeft a ~ FromLeft b)
fromRightCong :: (a ~ b) :- (FromRight a ~ FromRight b)


-- | 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>.
nothingCong :: (a ~ b) :- (IsNothing a ~ IsNothing b)
nothingNotJust :: (Nothing ~ Just a) :- Fail

-- | Map over a type-level <tt>Maybe</tt>.
maybeFmapCong :: (f ~ g, a ~ b) :- ((f <$> a) ~ (g <$> b))
maybePamfCong :: (f ~ g, a ~ b) :- ((f <&> a) ~ (g <&> b))
maybeApCong :: (f ~ g, a ~ b) :- ((f <*> a) ~ (g <*> b))
maybeAltCong :: (a ~ c, b ~ d) :- ((a <|> b) ~ (c <|> d))
fromJustCong :: (a ~ b) :- (FromJust a ~ FromJust b)


-- | A collection of simple type combinators, such as <tt>Identity</tt>
--   <a>I</a>, <tt>Constant</tt> <a>C</a>, <tt>Compose</tt> '(:.:)',
--   Currying/Uncurrying, etc.
module Data.Type.Combinator
data Comp1 (f :: l -> m -> *) (g :: k -> l) :: k -> m -> *
[Comp1] :: {getComp1 :: !(f (g h) a)} -> Comp1 f g h a
newtype (:.:) (f :: l -> *) (g :: k -> l) (a :: k)
Comp :: f (g a) -> (:.:)
[getComp] :: (:.:) -> f (g a)
newtype I a
I :: a -> I a
[getI] :: I a -> a
newtype C r a
C :: r -> C r a
[getC] :: C r a -> r
mapC :: (r -> s) -> C r a -> C s b
newtype Flip p b a
Flip :: p a b -> Flip p b a
[getFlip] :: Flip p b a -> p a b
flipTestEquality1 :: TestEquality (p c) => Flip p a c -> Flip p b c -> Maybe (a :~: b)
mapFlip :: (f a b -> g c d) -> Flip f b a -> Flip g d c
newtype Cur (p :: (k, l) -> *) (a :: k) (b :: l)
Cur :: p (a # b) -> Cur
[getCur] :: Cur -> p (a # b)
mapCur :: (p '(a, b) -> q '(c, d)) -> Cur p a b -> Cur q c d
data Uncur (p :: k -> l -> *) :: (k, l) -> *
[Uncur] :: {getUncur :: p a b} -> Uncur p (a # b)
mapUncur :: (p (Fst a) (Snd a) -> q b c) -> Uncur p a -> Uncur q '(b, c)
newtype Cur3 (p :: (k, l, m) -> *) (a :: k) (b :: l) (c :: m)
Cur3 :: p '(a, b, c) -> Cur3
[getCur3] :: Cur3 -> p '(a, b, c)
mapCur3 :: (p '(a, b, c) -> q '(d, e, f)) -> Cur3 p a b c -> Cur3 q d e f
data Uncur3 (p :: k -> l -> m -> *) :: (k, l, m) -> *
[Uncur3] :: {getUncur3 :: p a b c} -> Uncur3 p '(a, b, c)
mapUncur3 :: (p (Fst3 x) (Snd3 x) (Thd3 x) -> q d e f) -> Uncur3 p x -> Uncur3 q '(d, e, f)
newtype Join f a
Join :: f a a -> Join f a
[getJoin] :: Join f a -> f a a
mapJoin :: (f a a -> g b b) -> Join f a -> Join g b
data Conj (t :: (k -> *) -> l -> *) (f :: k -> m -> *) :: l -> m -> *
[Conj] :: t (Flip f b) a -> Conj t f a b
data LL (c :: k -> *) :: l -> (l -> k) -> *
[LL] :: {getLL :: c (f a)} -> LL c a f
data RR (c :: k -> *) :: (l -> k) -> l -> *
[RR] :: {getRR :: c (f a)} -> RR c f a
instance forall k k1 (p :: k -> k1 -> *) (b :: k1) (a :: k). GHC.Read.Read (p a b) => GHC.Read.Read (Data.Type.Combinator.Flip p b a)
instance forall k k1 (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 k1 (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 k1 (p :: k -> k1 -> *) (b :: k1) (a :: k). GHC.Classes.Eq (p a b) => GHC.Classes.Eq (Data.Type.Combinator.Flip p b a)
instance Data.Traversable.Traversable (Data.Type.Combinator.C r)
instance Data.Foldable.Foldable (Data.Type.Combinator.C r)
instance GHC.Base.Functor (Data.Type.Combinator.C r)
instance forall r k (a :: k). GHC.Read.Read r => GHC.Read.Read (Data.Type.Combinator.C r a)
instance forall r k (a :: k). GHC.Show.Show r => GHC.Show.Show (Data.Type.Combinator.C r a)
instance forall r k (a :: k). GHC.Classes.Ord r => GHC.Classes.Ord (Data.Type.Combinator.C r a)
instance forall r k (a :: k). GHC.Classes.Eq r => GHC.Classes.Eq (Data.Type.Combinator.C r a)
instance Data.Traversable.Traversable Data.Type.Combinator.I
instance Data.Foldable.Foldable Data.Type.Combinator.I
instance GHC.Base.Functor Data.Type.Combinator.I
instance GHC.Show.Show a => GHC.Show.Show (Data.Type.Combinator.I a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Type.Combinator.I a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Type.Combinator.I a)
instance forall l (f :: l -> GHC.Types.*) k (g :: k -> l) (a :: k). GHC.Read.Read (f (g a)) => GHC.Read.Read ((Data.Type.Combinator.:.:) f g a)
instance forall l (f :: l -> GHC.Types.*) k (g :: k -> l) (a :: k). GHC.Show.Show (f (g a)) => GHC.Show.Show ((Data.Type.Combinator.:.:) f g a)
instance forall l (f :: l -> GHC.Types.*) k (g :: k -> l) (a :: k). GHC.Classes.Ord (f (g a)) => GHC.Classes.Ord ((Data.Type.Combinator.:.:) f g a)
instance forall l (f :: l -> GHC.Types.*) k (g :: k -> l) (a :: k). GHC.Classes.Eq (f (g a)) => GHC.Classes.Eq ((Data.Type.Combinator.:.:) f g a)
instance forall k l (p :: (k, l) -> *) (a :: k) (b :: l). GHC.Classes.Eq (p (a Type.Family.Tuple.# b)) => GHC.Classes.Eq (Data.Type.Combinator.Cur p a b)
instance forall k l (p :: (k, l) -> *) (a :: k) (b :: l). GHC.Classes.Ord (p (a Type.Family.Tuple.# b)) => GHC.Classes.Ord (Data.Type.Combinator.Cur p a b)
instance forall k l (p :: (k, l) -> *) (a :: k) (b :: l). GHC.Show.Show (p (a Type.Family.Tuple.# b)) => GHC.Show.Show (Data.Type.Combinator.Cur p a b)
instance forall k l (p :: (k, l) -> *) (a :: k) (b :: l). GHC.Read.Read (p (a Type.Family.Tuple.# b)) => GHC.Read.Read (Data.Type.Combinator.Cur p a b)
instance forall l k (p :: k -> l -> *) (x :: (k, l)). GHC.Classes.Eq (p (Type.Family.Tuple.Fst x) (Type.Family.Tuple.Snd x)) => GHC.Classes.Eq (Data.Type.Combinator.Uncur p x)
instance forall l k (p :: k -> l -> *) (x :: (k, l)). GHC.Classes.Ord (p (Type.Family.Tuple.Fst x) (Type.Family.Tuple.Snd x)) => GHC.Classes.Ord (Data.Type.Combinator.Uncur p x)
instance forall l k (p :: k -> l -> *) (x :: (k, l)). GHC.Show.Show (p (Type.Family.Tuple.Fst x) (Type.Family.Tuple.Snd x)) => GHC.Show.Show (Data.Type.Combinator.Uncur p x)
instance forall l k (x :: (k, l)) (a :: k) (b :: l) (p :: k -> l -> *). (x ~ (a Type.Family.Tuple.# b), GHC.Read.Read (p a b)) => GHC.Read.Read (Data.Type.Combinator.Uncur p x)
instance forall k l m (p :: (k, l, m) -> *) (a :: k) (b :: l) (c :: m). GHC.Classes.Eq (p '(a, b, c)) => GHC.Classes.Eq (Data.Type.Combinator.Cur3 p a b c)
instance forall k l m (p :: (k, l, m) -> *) (a :: k) (b :: l) (c :: m). GHC.Classes.Ord (p '(a, b, c)) => GHC.Classes.Ord (Data.Type.Combinator.Cur3 p a b c)
instance forall k l m (p :: (k, l, m) -> *) (a :: k) (b :: l) (c :: m). GHC.Show.Show (p '(a, b, c)) => GHC.Show.Show (Data.Type.Combinator.Cur3 p a b c)
instance forall k l m (p :: (k, l, m) -> *) (a :: k) (b :: l) (c :: m). GHC.Read.Read (p '(a, b, c)) => GHC.Read.Read (Data.Type.Combinator.Cur3 p a b c)
instance forall m l k (p :: k -> l -> m -> *) (x :: (k, l, m)). GHC.Classes.Eq (p (Type.Family.Tuple.Fst3 x) (Type.Family.Tuple.Snd3 x) (Type.Family.Tuple.Thd3 x)) => GHC.Classes.Eq (Data.Type.Combinator.Uncur3 p x)
instance forall m l k (p :: k -> l -> m -> *) (x :: (k, l, m)). GHC.Classes.Ord (p (Type.Family.Tuple.Fst3 x) (Type.Family.Tuple.Snd3 x) (Type.Family.Tuple.Thd3 x)) => GHC.Classes.Ord (Data.Type.Combinator.Uncur3 p x)
instance forall m l k (p :: k -> l -> m -> *) (x :: (k, l, m)). GHC.Show.Show (p (Type.Family.Tuple.Fst3 x) (Type.Family.Tuple.Snd3 x) (Type.Family.Tuple.Thd3 x)) => GHC.Show.Show (Data.Type.Combinator.Uncur3 p x)
instance forall m l k (x :: (k, l, m)) (a :: k) (b :: l) (c :: m) (p :: k -> l -> m -> *). (x ~ '(a, b, c), GHC.Read.Read (p a b c)) => GHC.Read.Read (Data.Type.Combinator.Uncur3 p x)
instance forall k (f :: k -> k -> *) (a :: k). GHC.Classes.Eq (f a a) => GHC.Classes.Eq (Data.Type.Combinator.Join f a)
instance forall k (f :: k -> k -> *) (a :: k). GHC.Classes.Ord (f a a) => GHC.Classes.Ord (Data.Type.Combinator.Join f a)
instance forall k (f :: k -> k -> *) (a :: k). GHC.Show.Show (f a a) => GHC.Show.Show (Data.Type.Combinator.Join f a)
instance forall k (f :: k -> k -> *) (a :: k). GHC.Read.Read (f a a) => GHC.Read.Read (Data.Type.Combinator.Join f a)
instance forall l m k (f :: (l -> GHC.Types.*) -> m -> GHC.Types.*) (g :: (k -> GHC.Types.*) -> l -> GHC.Types.*). (Type.Class.Higher.Functor1 f, Type.Class.Higher.Functor1 g) => Type.Class.Higher.Functor1 (Data.Type.Combinator.Comp1 f g)
instance forall k l (f :: l -> GHC.Types.*) (g :: k -> l). Type.Class.Higher.Eq1 f => Type.Class.Higher.Eq1 (f Data.Type.Combinator.:.: g)
instance forall k l (f :: l -> GHC.Types.*) (g :: k -> l). Type.Class.Higher.Ord1 f => Type.Class.Higher.Ord1 (f Data.Type.Combinator.:.: g)
instance forall k l (f :: l -> GHC.Types.*) (g :: k -> l). Type.Class.Higher.Show1 f => Type.Class.Higher.Show1 (f Data.Type.Combinator.:.: g)
instance forall k l (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: l -> GHC.Types.*) (g :: k -> l) (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 l (f :: l -> *) (g :: k -> l). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (f Data.Type.Combinator.:.: g)
instance forall l l1 (f :: l1 -> *). Data.Type.Equality.TestEquality f => Type.Class.Witness.TestEquality1 ((Data.Type.Combinator.:.:) f)
instance GHC.Base.Applicative Data.Type.Combinator.I
instance GHC.Base.Monad 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 GHC.Classes.Eq r => Type.Class.Higher.Eq1 (Data.Type.Combinator.C r)
instance GHC.Classes.Ord r => Type.Class.Higher.Ord1 (Data.Type.Combinator.C r)
instance GHC.Show.Show r => Type.Class.Higher.Show1 (Data.Type.Combinator.C r)
instance GHC.Read.Read r => Type.Class.Higher.Read1 (Data.Type.Combinator.C r)
instance forall k (p :: GHC.Types.Constraint) (q :: GHC.Types.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 r (a :: k). GHC.Num.Num r => GHC.Num.Num (Data.Type.Combinator.C r a)
instance forall k k1 (p :: k -> k1 -> GHC.Types.*) (b :: k1). Type.Class.Witness.TestEquality1 p => Data.Type.Equality.TestEquality (Data.Type.Combinator.Flip p b)
instance forall k k1 (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: k -> k1 -> GHC.Types.*) (a :: k) (b :: k1). 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 k1 (p :: k -> k1 -> GHC.Types.*) (a :: k) (b :: k1). Type.Class.Known.Known (p a) b => Type.Class.Known.Known (Data.Type.Combinator.Flip p b) a
instance forall k k1 (p :: (k1, k) -> GHC.Types.*) (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 l (q :: GHC.Types.Constraint) (r :: GHC.Types.Constraint) (p :: (k, l) -> GHC.Types.*) (a :: k) (b :: l). 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 l k (p :: k -> l -> GHC.Types.*). Type.Class.Higher.Read2 p => Type.Class.Higher.Read1 (Data.Type.Combinator.Uncur p)
instance forall l k (p :: k -> l -> GHC.Types.*) (a :: k) (b :: l) (q :: (k, l)). (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 l k (r :: GHC.Types.Constraint) (s :: GHC.Types.Constraint) (p :: k -> l -> GHC.Types.*) (a :: k) (b :: l) (q :: (k, l)). (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 k1 l (p :: (k1, l, k) -> GHC.Types.*) (a :: k1) (b :: l) (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 l m (q :: GHC.Types.Constraint) (r :: GHC.Types.Constraint) (p :: (k, l, m) -> GHC.Types.*) (a :: k) (b :: l) (c :: m). 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 m l k (p :: k -> l -> m -> GHC.Types.*). Type.Class.Higher.Read3 p => Type.Class.Higher.Read1 (Data.Type.Combinator.Uncur3 p)
instance forall m l k (p :: k -> l -> m -> GHC.Types.*) (a :: k) (b :: l) (c :: m) (q :: (k, l, m)). (Type.Class.Known.Known (p a b) c, q ~ '(a, b, c)) => Type.Class.Known.Known (Data.Type.Combinator.Uncur3 p) q
instance forall m l k (r :: GHC.Types.Constraint) (s :: GHC.Types.Constraint) (p :: k -> l -> m -> GHC.Types.*) (a :: k) (b :: l) (c :: m) (q :: (k, l, m)). (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)
instance forall k (f :: k -> k -> GHC.Types.*). Type.Class.Higher.Eq2 f => Type.Class.Higher.Eq1 (Data.Type.Combinator.Join f)
instance forall k (f :: k -> k -> GHC.Types.*). Type.Class.Higher.Ord2 f => Type.Class.Higher.Ord1 (Data.Type.Combinator.Join f)
instance forall k (f :: k -> k -> GHC.Types.*). Type.Class.Higher.Show2 f => Type.Class.Higher.Show1 (Data.Type.Combinator.Join f)
instance forall k (f :: k -> k -> GHC.Types.*) (a :: k). Type.Class.Known.Known (f a) a => Type.Class.Known.Known (Data.Type.Combinator.Join f) a
instance forall k (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: k -> k -> GHC.Types.*) (a :: k). Type.Class.Witness.Witness p q (f a a) => Type.Class.Witness.Witness p q (Data.Type.Combinator.Join f a)


-- | 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
(.&.) :: (f a -> h b) -> (g a -> i b) -> (f :&: g) a -> (h :&: i) b
infixr 3 .&.
fanFirst :: (f a -> g a) -> (f :&: h) a -> (g :&: h) 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 (f :: k -> *) (a :: k) (g :: k -> *). (GHC.Classes.Eq (f a), GHC.Classes.Eq (g a)) => GHC.Classes.Eq ((Data.Type.Conjunction.:&:) f g a)
instance forall k (f :: k -> *) (a :: k) (g :: k -> *). (GHC.Classes.Ord (f a), GHC.Classes.Ord (g a)) => GHC.Classes.Ord ((Data.Type.Conjunction.:&:) f g a)
instance forall k (f :: k -> *) (a :: k) (g :: k -> *). (GHC.Show.Show (f a), GHC.Show.Show (g a)) => GHC.Show.Show ((Data.Type.Conjunction.:&:) f g a)
instance forall k (f :: k -> *) (a :: k) (g :: k -> *). (GHC.Read.Read (f a), GHC.Read.Read (g a)) => GHC.Read.Read ((Data.Type.Conjunction.:&:) f g a)
instance forall l k (f :: k -> *) (p :: (k, l)) (g :: l -> *). (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 l k (f :: k -> *) (p :: (k, l)) (g :: l -> *). (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 l k (f :: k -> *) (p :: (k, l)) (g :: l -> *). (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 l k (p :: (k, l)) (a :: k) (b :: l) (f :: k -> *) (g :: l -> *). (p ~ (a Type.Family.Tuple.# b), GHC.Read.Read (f a), GHC.Read.Read (g b)) => GHC.Read.Read ((Data.Type.Conjunction.:*:) f g p)
instance forall k (f :: k -> GHC.Types.*) (g :: k -> GHC.Types.*). (Type.Class.Higher.Eq1 f, Type.Class.Higher.Eq1 g) => Type.Class.Higher.Eq1 (f Data.Type.Conjunction.:&: g)
instance forall k (f :: k -> GHC.Types.*) (g :: k -> GHC.Types.*). (Type.Class.Higher.Ord1 f, Type.Class.Higher.Ord1 g) => Type.Class.Higher.Ord1 (f Data.Type.Conjunction.:&: g)
instance forall k (f :: k -> GHC.Types.*) (g :: k -> GHC.Types.*). (Type.Class.Higher.Show1 f, Type.Class.Higher.Show1 g) => Type.Class.Higher.Show1 (f Data.Type.Conjunction.:&: g)
instance forall k (f :: k -> GHC.Types.*) (a :: k) (g :: k -> GHC.Types.*). (Type.Class.Known.Known f a, Type.Class.Known.Known g a) => Type.Class.Known.Known (f Data.Type.Conjunction.:&: g) a
instance forall l (f :: l -> GHC.Types.*). Type.Class.Higher.Functor1 ((Data.Type.Conjunction.:&:) f)
instance forall l (f :: l -> GHC.Types.*). Type.Class.Higher.Foldable1 ((Data.Type.Conjunction.:&:) f)
instance forall l (f :: l -> GHC.Types.*). Type.Class.Higher.Traversable1 ((Data.Type.Conjunction.:&:) f)
instance Type.Class.Higher.Bifunctor1 (Data.Type.Conjunction.:&:)
instance forall k (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: k -> GHC.Types.*) (a :: k) (s :: GHC.Types.Constraint) (t :: GHC.Types.Constraint) (g :: k -> GHC.Types.*). (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 l k (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (Type.Class.Higher.Eq1 f, Type.Class.Higher.Eq1 g) => Type.Class.Higher.Eq1 (f Data.Type.Conjunction.:*: g)
instance forall l k (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (Type.Class.Higher.Ord1 f, Type.Class.Higher.Ord1 g) => Type.Class.Higher.Ord1 (f Data.Type.Conjunction.:*: g)
instance forall l k (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (Type.Class.Higher.Show1 f, Type.Class.Higher.Show1 g) => Type.Class.Higher.Show1 (f Data.Type.Conjunction.:*: g)
instance forall l k (p :: (k, l)) (a :: k) (b :: l) (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (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 k1 (f :: k1 -> GHC.Types.*). Type.Class.Higher.Functor1 ((Data.Type.Conjunction.:*:) f)
instance forall k k1 (f :: k1 -> GHC.Types.*). Type.Class.Higher.Foldable1 ((Data.Type.Conjunction.:*:) f)
instance forall k k1 (f :: k1 -> GHC.Types.*). Type.Class.Higher.Traversable1 ((Data.Type.Conjunction.:*:) f)
instance Type.Class.Higher.Bifunctor1 (Data.Type.Conjunction.:*:)
instance forall k m (f :: m -> GHC.Types.*). Type.Class.Higher.IxFunctor1 (Data.Type.Index.Trans.IxSecond (Data.Type.Equality.:~:)) ((Data.Type.Conjunction.:*:) f)
instance forall l k (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (Type.Class.Witness.DecEquality f, Type.Class.Witness.DecEquality g) => Type.Class.Witness.DecEquality (f Data.Type.Conjunction.:*: g)
instance forall l k (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: k -> GHC.Types.*) (a :: k) (s :: GHC.Types.Constraint) (t :: GHC.Types.Constraint) (g :: l -> GHC.Types.*) (b :: l) (x :: (k, l)). (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)


-- | 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
elimIndex :: (forall xs. p (a :< xs) a) -> (forall x xs. Index xs a -> p xs a -> p (x :< xs) a) -> Index as a -> p as a
ixNil :: Index Ø a -> b
onIxPred :: (Index as a -> Index bs a) -> Index (b :< as) a -> Index (b :< bs) a
type (∈) a as = Elem as a
class Elem (as :: [k]) (a :: k)
elemIndex :: Elem as a => Index as a
class EveryC c as => Every (c :: k -> Constraint) (as :: [k]) where type EveryC c as :: Constraint where {
    type family EveryC c as :: Constraint;
}
every :: Every c as => Index as a -> Wit (c a)
class ListC ((c <$> xs) <&> y) => Every2 (c :: k -> l -> Constraint) (xs :: [k]) (y :: l)
every2 :: Every2 c xs y => Index xs x -> Wit (c x y)
instance forall k (as :: [k]) (a :: k). GHC.Classes.Eq (Data.Type.Index.Index as a)
instance forall k (as :: [k]) (a :: k). GHC.Classes.Ord (Data.Type.Index.Index as a)
instance forall k (as :: [k]) (a :: k). GHC.Show.Show (Data.Type.Index.Index as a)
instance forall k (as :: [k]). Type.Class.Higher.Eq1 (Data.Type.Index.Index as)
instance forall k (as :: [k]). Type.Class.Higher.Ord1 (Data.Type.Index.Index as)
instance forall k (as :: [k]). Type.Class.Higher.Show1 (Data.Type.Index.Index as)
instance Type.Class.Higher.Read2 Data.Type.Index.Index
instance forall k (as :: [k]). Data.Type.Equality.TestEquality (Data.Type.Index.Index as)
instance forall k (a :: k) (as :: [k]). Data.Type.Index.Elem (a Type.Family.List.:< as) a
instance forall k (as :: [k]) (a :: k) (b :: k). Data.Type.Index.Elem as a => Data.Type.Index.Elem (b Type.Family.List.:< as) a
instance forall k (as :: [k]) (a :: k). Type.Class.Witness.Witness Type.Family.Constraint.ØC (Data.Type.Index.Elem as a) (Data.Type.Index.Index as a)
instance forall k (a :: k) (as :: [k]). (a Data.Type.Index.∈ as) => Type.Class.Known.Known (Data.Type.Index.Index as) a
instance forall k (c :: k -> GHC.Types.Constraint). Data.Type.Index.Every c Type.Family.List.Ø
instance forall a (c :: a -> GHC.Types.Constraint) (a1 :: a) (as :: [a]). (c a1, Data.Type.Index.Every c as) => Data.Type.Index.Every c (a1 Type.Family.List.:< as)
instance forall l k (c :: k -> l -> GHC.Types.Constraint) (y :: l). Data.Type.Index.Every2 c Type.Family.List.Ø y
instance forall l a (c :: a -> l -> GHC.Types.Constraint) (x :: a) (y :: l) (xs :: [a]). (c x y, Data.Type.Index.Every2 c xs y) => Data.Type.Index.Every2 c (x Type.Family.List.:< xs) y


-- | <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)
elimSum :: (forall x xs. f x -> p (x :< xs)) -> (forall x xs. Index as x -> p xs -> p (x :< xs)) -> Sum f as -> p as
instance forall k (f :: k -> *) (as :: [k]). Type.Family.List.ListC (GHC.Classes.Eq Type.Family.List.<$> (f Type.Family.List.<$> as)) => GHC.Classes.Eq (Data.Type.Sum.Sum f as)
instance forall k (f :: k -> *) (as :: [k]). (Type.Family.List.ListC (GHC.Classes.Eq Type.Family.List.<$> (f Type.Family.List.<$> as)), Type.Family.List.ListC (GHC.Classes.Ord Type.Family.List.<$> (f Type.Family.List.<$> as))) => GHC.Classes.Ord (Data.Type.Sum.Sum f as)
instance forall k (f :: k -> *) (as :: [k]). Type.Family.List.ListC (GHC.Show.Show Type.Family.List.<$> (f Type.Family.List.<$> as)) => GHC.Show.Show (Data.Type.Sum.Sum f as)
instance forall k (f :: k -> GHC.Types.*). Type.Class.Higher.Eq1 f => Type.Class.Higher.Eq1 (Data.Type.Sum.Sum f)
instance forall k (f :: k -> GHC.Types.*). Type.Class.Higher.Ord1 f => Type.Class.Higher.Ord1 (Data.Type.Sum.Sum f)
instance forall k (f :: k -> GHC.Types.*). Type.Class.Higher.Show1 f => Type.Class.Higher.Show1 (Data.Type.Sum.Sum f)
instance forall k (f :: k -> GHC.Types.*). Type.Class.Higher.Read1 f => Type.Class.Higher.Read1 (Data.Type.Sum.Sum f)
instance Type.Class.Higher.Functor1 Data.Type.Sum.Sum
instance Type.Class.Higher.IxFunctor1 Data.Type.Index.Index Data.Type.Sum.Sum
instance Type.Class.Higher.Foldable1 Data.Type.Sum.Sum
instance Type.Class.Higher.IxFoldable1 Data.Type.Index.Index Data.Type.Sum.Sum
instance Type.Class.Higher.Traversable1 Data.Type.Sum.Sum
instance Type.Class.Higher.IxTraversable1 Data.Type.Index.Index Data.Type.Sum.Sum
instance forall k (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: k -> GHC.Types.*) (a :: k). Type.Class.Witness.Witness p q (f a) => Type.Class.Witness.Witness p q (Data.Type.Sum.Sum f '[a])
instance forall a (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: a -> GHC.Types.*) (a1 :: a) (b :: a) (as :: [a]). (Type.Class.Witness.Witness p q (f a1), 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 (a1 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.Lifted
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>.
nilFSum :: FSum Ø a -> Void

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

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

-- | Project an implicit index out of an FSum.
fprj :: (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.
findex :: 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.
imapFSum :: (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!
ifoldMapFSum :: (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>.
itraverseFSum :: 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.Lifted.FSum fs)
instance Type.Family.List.ListC (Data.Foldable.Foldable Type.Family.List.<$> fs) => Data.Foldable.Foldable (Data.Type.Sum.Lifted.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.Lifted.FSum fs)


-- | 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
infixr 2 >|<
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
infixr 2 >+<
instance forall k (f :: k -> *) (a :: k) (g :: k -> *). (GHC.Classes.Eq (f a), GHC.Classes.Eq (g a)) => GHC.Classes.Eq ((Data.Type.Disjunction.:|:) f g a)
instance forall k (f :: k -> *) (a :: k) (g :: k -> *). (GHC.Classes.Ord (f a), GHC.Classes.Ord (g a)) => GHC.Classes.Ord ((Data.Type.Disjunction.:|:) f g a)
instance forall k (f :: k -> *) (a :: k) (g :: k -> *). (GHC.Show.Show (f a), GHC.Show.Show (g a)) => GHC.Show.Show ((Data.Type.Disjunction.:|:) f g a)
instance forall k (f :: k -> *) (a :: k) (g :: k -> *). (GHC.Read.Read (f a), GHC.Read.Read (g a)) => GHC.Read.Read ((Data.Type.Disjunction.:|:) f g a)
instance forall l k (f :: k -> *) (e :: Data.Either.Either k l) (g :: l -> *). (GHC.Classes.Eq (f (Type.Family.Either.FromLeft e)), GHC.Classes.Eq (g (Type.Family.Either.FromRight e))) => GHC.Classes.Eq ((Data.Type.Disjunction.:+:) f g e)
instance forall l k (f :: k -> *) (e :: Data.Either.Either k l) (g :: l -> *). (GHC.Classes.Ord (f (Type.Family.Either.FromLeft e)), GHC.Classes.Ord (g (Type.Family.Either.FromRight e))) => GHC.Classes.Ord ((Data.Type.Disjunction.:+:) f g e)
instance forall l k (f :: k -> *) (e :: Data.Either.Either k l) (g :: l -> *). (GHC.Show.Show (f (Type.Family.Either.FromLeft e)), GHC.Show.Show (g (Type.Family.Either.FromRight e))) => GHC.Show.Show ((Data.Type.Disjunction.:+:) f g e)
instance forall k (f :: k -> GHC.Types.*) (g :: k -> GHC.Types.*). (Type.Class.Higher.Eq1 f, Type.Class.Higher.Eq1 g) => Type.Class.Higher.Eq1 (f Data.Type.Disjunction.:|: g)
instance forall k (f :: k -> GHC.Types.*) (g :: k -> GHC.Types.*). (Type.Class.Higher.Ord1 f, Type.Class.Higher.Ord1 g) => Type.Class.Higher.Ord1 (f Data.Type.Disjunction.:|: g)
instance forall k (f :: k -> GHC.Types.*) (g :: k -> GHC.Types.*). (Type.Class.Higher.Show1 f, Type.Class.Higher.Show1 g) => Type.Class.Higher.Show1 (f Data.Type.Disjunction.:|: g)
instance forall k (f :: k -> GHC.Types.*) (g :: k -> GHC.Types.*). (Type.Class.Higher.Read1 f, Type.Class.Higher.Read1 g) => Type.Class.Higher.Read1 (f Data.Type.Disjunction.:|: g)
instance forall l (f :: l -> GHC.Types.*). Type.Class.Higher.Functor1 ((Data.Type.Disjunction.:|:) f)
instance forall l (f :: l -> GHC.Types.*). Type.Class.Higher.Foldable1 ((Data.Type.Disjunction.:|:) f)
instance forall l (f :: l -> GHC.Types.*). Type.Class.Higher.Traversable1 ((Data.Type.Disjunction.:|:) f)
instance Type.Class.Higher.Bifunctor1 (Data.Type.Disjunction.:|:)
instance forall k (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: k -> GHC.Types.*) (a :: k) (g :: k -> GHC.Types.*). (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 l k (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (Type.Class.Higher.Eq1 f, Type.Class.Higher.Eq1 g) => Type.Class.Higher.Eq1 (f Data.Type.Disjunction.:+: g)
instance forall l k (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (Type.Class.Higher.Ord1 f, Type.Class.Higher.Ord1 g) => Type.Class.Higher.Ord1 (f Data.Type.Disjunction.:+: g)
instance forall l k (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (Type.Class.Higher.Show1 f, Type.Class.Higher.Show1 g) => Type.Class.Higher.Show1 (f Data.Type.Disjunction.:+: g)
instance forall l k (f :: k -> GHC.Types.*) (g :: l -> GHC.Types.*). (Type.Class.Higher.Read1 f, Type.Class.Higher.Read1 g) => Type.Class.Higher.Read1 (f Data.Type.Disjunction.:+: g)
instance forall l a (f :: a -> GHC.Types.*) (a1 :: a) (g :: l -> GHC.Types.*). Type.Class.Known.Known f a1 => Type.Class.Known.Known (f Data.Type.Disjunction.:+: g) ('Data.Either.Left a1)
instance forall k b (g :: b -> GHC.Types.*) (b1 :: b) (f :: k -> GHC.Types.*). Type.Class.Known.Known g b1 => Type.Class.Known.Known (f Data.Type.Disjunction.:+: g) ('Data.Either.Right b1)
instance forall k k1 (f :: k1 -> GHC.Types.*). Type.Class.Higher.Functor1 ((Data.Type.Disjunction.:+:) f)
instance forall k k1 (f :: k1 -> GHC.Types.*). Type.Class.Higher.Foldable1 ((Data.Type.Disjunction.:+:) f)
instance forall k k1 (f :: k1 -> GHC.Types.*). Type.Class.Higher.Traversable1 ((Data.Type.Disjunction.:+:) f)
instance Type.Class.Higher.Bifunctor1 (Data.Type.Disjunction.:+:)
instance forall l a (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: a -> GHC.Types.*) (a1 :: a) (g :: l -> GHC.Types.*). Type.Class.Witness.Witness p q (f a1) => Type.Class.Witness.Witness p q ((Data.Type.Disjunction.:+:) f g ('Data.Either.Left a1))
instance forall k b (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (g :: b -> GHC.Types.*) (b1 :: b) (f :: k -> GHC.Types.*). Type.Class.Witness.Witness p q (g b1) => Type.Class.Witness.Witness p q ((Data.Type.Disjunction.:+:) f g ('Data.Either.Right b1))


-- | 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 forall k (f :: k -> *) (m :: GHC.Base.Maybe k). Type.Family.Maybe.MaybeC (GHC.Classes.Eq Type.Family.Maybe.<$> (f Type.Family.Maybe.<$> m)) => GHC.Classes.Eq (Data.Type.Option.Option f m)
instance forall k (f :: k -> *) (m :: GHC.Base.Maybe k). (Type.Family.Maybe.MaybeC (GHC.Classes.Eq Type.Family.Maybe.<$> (f Type.Family.Maybe.<$> m)), Type.Family.Maybe.MaybeC (GHC.Classes.Ord Type.Family.Maybe.<$> (f Type.Family.Maybe.<$> m))) => GHC.Classes.Ord (Data.Type.Option.Option f m)
instance forall k (f :: k -> *) (m :: GHC.Base.Maybe k). Type.Family.Maybe.MaybeC (GHC.Show.Show Type.Family.Maybe.<$> (f Type.Family.Maybe.<$> m)) => GHC.Show.Show (Data.Type.Option.Option f m)
instance Type.Class.Higher.Functor1 Data.Type.Option.Option
instance Type.Class.Higher.Foldable1 Data.Type.Option.Option
instance Type.Class.Higher.Traversable1 Data.Type.Option.Option
instance forall k (f :: k -> GHC.Types.*). Type.Class.Known.Known (Data.Type.Option.Option f) 'GHC.Base.Nothing
instance forall a (f :: a -> GHC.Types.*) (a1 :: a). Type.Class.Known.Known f a1 => Type.Class.Known.Known (Data.Type.Option.Option f) ('GHC.Base.Just a1)
instance forall k (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: k -> GHC.Types.*) (a :: k) (x :: GHC.Base.Maybe 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)


-- | Type combinators for type-level lists, where we have many functors
--   with a single index.
module Data.Type.Product.Lifted
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>
infix 6 :>>

-- | 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
infixl 6 >>:
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.Lifted.FProd fs)
instance Type.Family.List.ListC (Data.Foldable.Foldable Type.Family.List.<$> fs) => Data.Foldable.Foldable (Data.Type.Product.Lifted.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.Lifted.FProd fs)
instance forall k (a :: k). Type.Class.Known.Known (Data.Type.Product.Lifted.FProd Type.Family.List.Ø) a
instance forall k (f :: k -> GHC.Types.*) (a :: k) (fs :: [k -> GHC.Types.*]). (Type.Class.Known.Known f a, Type.Class.Known.Known (Data.Type.Product.Lifted.FProd fs) a) => Type.Class.Known.Known (Data.Type.Product.Lifted.FProd (f Type.Family.List.:< fs)) a
instance forall k (a :: k). Type.Class.Witness.Witness Type.Family.Constraint.ØC Type.Family.Constraint.ØC (Data.Type.Product.Lifted.FProd Type.Family.List.Ø a)
instance forall k (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: k -> GHC.Types.*) (a :: k) (s :: GHC.Types.Constraint) (t :: GHC.Types.Constraint) (fs :: [k -> GHC.Types.*]). (Type.Class.Witness.Witness p q (f a), Type.Class.Witness.Witness s t (Data.Type.Product.Lifted.FProd fs a)) => Type.Class.Witness.Witness (p, s) (q, t) (Data.Type.Product.Lifted.FProd (f Type.Family.List.:< fs) a)


-- | Convenient type families for working with type-level <tt>Bool</tt>s.
module Type.Family.Bool
type (==>) a b = Not a || b
type (<==>) a b = a == b
type (^^) a b = (a || b) && Not (a && b)


-- | Type-level natural numbers, along with frequently used type families
--   over them.
module Type.Family.Nat
data N
Z :: N
S :: N -> N
fromInt :: Int -> Maybe N
zeroCong :: (x ~ y) :- (IsZero x ~ IsZero y)
zNotS :: (Z ~ S x) :- Fail
iotaCong :: (x ~ y) :- (Iota x ~ Iota y)
type Pos n = n ~ S (Pred n)
predCong :: (x ~ y) :- (Pred x ~ Pred y)
data AddW (f :: N -> *) :: N -> *
[AddW] :: !(f x) -> !(f y) -> AddW f (x + y)
addCong :: (w ~ y, x ~ z) :- ((w + x) ~ (y + z))
data MulW (f :: N -> *) :: N -> *
[MulW] :: !(f x) -> !(f y) -> MulW f (x * y)
mulCong :: (w ~ y, x ~ z) :- ((w * x) ~ (y * z))
expCong :: (w ~ y, x ~ z) :- ((w ^ x) ~ (y ^ z))
lenCong :: (as ~ bs) :- (Len as ~ Len bs)
ixCong :: (x ~ y, as ~ bs) :- (Ix x as ~ Ix y bs)
type (<=) x y = (x == y) || (x < y)
type (>=) x y = (x == y) || (x > y)

-- | 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
instance GHC.Show.Show Type.Family.Nat.N
instance GHC.Classes.Ord Type.Family.Nat.N
instance GHC.Classes.Eq Type.Family.Nat.N


-- | A <tt>singleton</tt>-esque type for type-level Bool values.
module Data.Type.Boolean
data Boolean :: Bool -> *
[False_] :: Boolean False
[True_] :: Boolean True
if' :: Boolean b -> ((b ~ True) => a) -> ((b ~ False) => a) -> a
(.?) :: ((b ~ True) => a) -> ((b ~ False) => a) -> Boolean b -> a
infix 4 .?
not' :: Boolean a -> Boolean (Not a)
(.||) :: Boolean a -> Boolean b -> Boolean (a || b)
infixr 2 .||
(.&&) :: Boolean a -> Boolean b -> Boolean (a && b)
infixr 3 .&&
(.^^) :: Boolean a -> Boolean b -> Boolean (a ^^ b)
infixr 4 .^^
(==>) :: Boolean a -> Boolean b -> Boolean (a ==> b)
infixr 1 ==>
(<==>) :: Boolean a -> Boolean b -> Boolean (a <==> b)
infixr 1 <==>
class BoolEquality (f :: k -> *)
boolEquality :: BoolEquality f => f a -> f b -> Boolean (a == b)
(.==) :: BoolEquality f => f a -> f b -> Boolean (a == b)
infix 4 .==
toBool :: Boolean b -> Bool
instance GHC.Classes.Eq (Data.Type.Boolean.Boolean b)
instance GHC.Classes.Ord (Data.Type.Boolean.Boolean b)
instance GHC.Show.Show (Data.Type.Boolean.Boolean b)
instance Type.Class.Higher.Eq1 Data.Type.Boolean.Boolean
instance Type.Class.Higher.Ord1 Data.Type.Boolean.Boolean
instance Type.Class.Higher.Show1 Data.Type.Boolean.Boolean
instance Type.Class.Higher.Read1 Data.Type.Boolean.Boolean
instance Data.Type.Boolean.BoolEquality Data.Type.Boolean.Boolean
instance Data.Type.Equality.TestEquality Data.Type.Boolean.Boolean
instance Type.Class.Known.Known Data.Type.Boolean.Boolean 'GHC.Types.True
instance Type.Class.Known.Known Data.Type.Boolean.Boolean 'GHC.Types.False


-- | 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>.
pred' :: Nat (S x) -> Nat x
onNatPred :: (Nat x -> Nat y) -> Nat (S x) -> Nat (S y)
_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)
infixr 6 .+
(.*) :: Nat x -> Nat y -> Nat (x * y)
infixr 7 .*
(.^) :: Nat x -> Nat y -> Nat (x ^ y)
infixl 8 .^
elimNat :: p Z -> (forall x. Nat x -> p x -> p (S x)) -> Nat n -> p n
natVal :: Nat n -> Int
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.Higher.Eq1 Data.Type.Nat.Nat
instance Type.Class.Higher.Ord1 Data.Type.Nat.Nat
instance Type.Class.Higher.Show1 Data.Type.Nat.Nat
instance Type.Class.Higher.Read1 Data.Type.Nat.Nat
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 Data.Type.Boolean.BoolEquality Data.Type.Nat.Nat


-- | 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)
elimLength :: p Ø -> (forall x xs. Length xs -> p xs -> p (x :< xs)) -> Length as -> p as
lOdd :: Length as -> Bool
lEven :: Length as -> Bool
instance forall k (as :: [k]). GHC.Classes.Eq (Data.Type.Length.Length as)
instance forall k (as :: [k]). GHC.Classes.Ord (Data.Type.Length.Length as)
instance forall k (as :: [k]). GHC.Show.Show (Data.Type.Length.Length as)
instance Type.Class.Higher.Eq1 Data.Type.Length.Length
instance Type.Class.Higher.Ord1 Data.Type.Length.Length
instance Type.Class.Higher.Show1 Data.Type.Length.Length
instance Type.Class.Higher.Read1 Data.Type.Length.Length
instance Type.Class.Known.Known Data.Type.Length.Length Type.Family.List.Ø
instance forall k (as :: [k]) (a :: k). Type.Class.Known.Known Data.Type.Length.Length as => Type.Class.Known.Known Data.Type.Length.Length (a Type.Family.List.:< as)
instance forall k (n :: Type.Family.Nat.N) (as :: [k]). n ~ Type.Family.Nat.Len as => Type.Class.Witness.Witness Type.Family.Constraint.ØC (Type.Class.Known.Known Data.Type.Nat.Nat n, Type.Class.Known.Known Data.Type.Length.Length as) (Data.Type.Length.Length as)


-- | 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)
elimFin :: (forall x. p (S x)) -> (forall x. Fin x -> p x -> p (S x)) -> Fin n -> p 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))

-- | 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 Type.Class.Higher.Eq1 Data.Type.Fin.Fin
instance Type.Class.Higher.Ord1 Data.Type.Fin.Fin
instance Type.Class.Higher.Show1 Data.Type.Fin.Fin
instance Type.Class.Higher.Read1 Data.Type.Fin.Fin
instance (Type.Class.Known.Known Data.Type.Nat.Nat n, Type.Family.Nat.Pos n) => GHC.Enum.Enum (Data.Type.Fin.Fin n)
instance (Type.Class.Known.Known Data.Type.Nat.Nat n, Type.Family.Nat.Pos n) => GHC.Enum.Bounded (Data.Type.Fin.Fin n)
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 <tt>singleton</tt>-esque type for representing members of finite
--   sets, indexed by its Nat value.
module Data.Type.Fin.Indexed
data IFin :: N -> N -> *
[IFZ] :: IFin (S x) Z
[IFS] :: !(IFin x y) -> IFin (S x) (S y)
class LTC x y => LessEq (x :: N) (y :: N) where type LTC x y :: Constraint where {
    type family LTC x y :: Constraint;
}
liftIFin :: LessEq x y => IFin x z -> IFin y z
ifinZ :: IFin Z x -> Void
weaken :: IFin x y -> IFin (S x) y
ifinNat :: IFin x y -> Nat y
ifinVal :: IFin x y -> Int
onIFinPred :: (forall x. IFin m x -> IFin n x) -> IFin (S m) y -> IFin (S n) y

-- | An <tt>IFin x y</tt> is a <a>Witness</a> that <tt>x &gt;= 1</tt>.
--   
--   That is, <tt><a>Pred</a> x</tt> is well defined.
instance GHC.Classes.Eq (Data.Type.Fin.Indexed.IFin x y)
instance GHC.Classes.Ord (Data.Type.Fin.Indexed.IFin x y)
instance GHC.Show.Show (Data.Type.Fin.Indexed.IFin x y)
instance Type.Class.Higher.Eq1 (Data.Type.Fin.Indexed.IFin x)
instance Type.Class.Higher.Ord1 (Data.Type.Fin.Indexed.IFin x)
instance Type.Class.Higher.Show1 (Data.Type.Fin.Indexed.IFin x)
instance Type.Class.Higher.Eq2 Data.Type.Fin.Indexed.IFin
instance Type.Class.Higher.Ord2 Data.Type.Fin.Indexed.IFin
instance Type.Class.Higher.Show2 Data.Type.Fin.Indexed.IFin
instance Type.Class.Higher.Read2 Data.Type.Fin.Indexed.IFin
instance Data.Type.Fin.Indexed.LessEq 'Type.Family.Nat.Z y
instance (y ~ 'Type.Family.Nat.S (Type.Family.Nat.Pred y), Data.Type.Fin.Indexed.LessEq x (Type.Family.Nat.Pred y)) => Data.Type.Fin.Indexed.LessEq ('Type.Family.Nat.S x) y
instance x' ~ Type.Family.Nat.Pred x => Type.Class.Witness.Witness Type.Family.Constraint.ØC 'Type.Family.Nat.S x' ~ x (Data.Type.Fin.Indexed.IFin x y)

module Data.Type.Nat.Inequality
data NatLT :: N -> N -> *
[LTZ] :: NatLT Z (S y)
[LTS] :: !(NatLT x y) -> NatLT (S x) (S y)
data NatEQ :: N -> N -> *
[EQZ] :: NatEQ Z Z
[EQS] :: !(NatEQ x y) -> NatEQ (S x) (S y)
data NatGT :: N -> N -> *
[GTZ] :: NatGT (S x) Z
[GTS] :: !(NatGT x y) -> NatGT (S x) (S y)
natCompare :: Nat x -> Nat y -> Either (NatLT x y) (Either (NatEQ x y) (NatGT x y))
instance (lt ~ (x Type.Family.Nat.< y), eq ~ (x Data.Type.Equality.== y), gt ~ (x Type.Family.Nat.> y), y' ~ Type.Family.Nat.Pred y) => Type.Class.Witness.Witness Type.Family.Constraint.ØC (y ~ 'Type.Family.Nat.S y', Type.Class.Known.Known Data.Type.Nat.Nat x, lt ~ 'GHC.Types.True, eq ~ 'GHC.Types.False, gt ~ 'GHC.Types.False) (Data.Type.Nat.Inequality.NatLT x y)
instance (lt ~ (x Type.Family.Nat.< y), eq ~ (x Data.Type.Equality.== y), gt ~ (x Type.Family.Nat.> y)) => Type.Class.Witness.Witness Type.Family.Constraint.ØC (x ~ y, Type.Class.Known.Known Data.Type.Nat.Nat x, lt ~ 'GHC.Types.False, eq ~ 'GHC.Types.True, gt ~ 'GHC.Types.False) (Data.Type.Nat.Inequality.NatEQ x y)
instance (lt ~ (x Type.Family.Nat.< y), eq ~ (x Data.Type.Equality.== y), gt ~ (x Type.Family.Nat.> y), x' ~ Type.Family.Nat.Pred x) => Type.Class.Witness.Witness Type.Family.Constraint.ØC (x ~ 'Type.Family.Nat.S x', Type.Class.Known.Known Data.Type.Nat.Nat y, lt ~ 'GHC.Types.False, eq ~ 'GHC.Types.False, gt ~ 'GHC.Types.True) (Data.Type.Nat.Inequality.NatGT x y)


-- | 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 Kiselyov'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>
infix 6 :>

-- | 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)
infixl 6 >:
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)
lookupPar :: TestEquality f => f a -> Prod (f :*: g) as -> Maybe (Some g)
permute :: Known Length bs => (forall x. Index bs x -> Index as x) -> Prod f as -> Prod f bs
permute' :: (forall x. Index bs x -> Index as x) -> Prod f as -> Length bs -> Prod f bs

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

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

-- | Cons onto a Tuple.
infixr 5 ::<

-- | Snoc onto a Tuple.
(>::) :: Tuple as -> a -> Tuple (as >: a)
infixl 6 >::
elimProd :: p Ø -> (forall x xs. Index as x -> f x -> p xs -> p (x :< xs)) -> Prod f as -> p as
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
select :: Prod (Index as) bs -> Prod f as -> Prod f bs
toList :: (forall a. f a -> r) -> Prod f as -> [r]
instance forall k (f :: k -> *) (as :: [k]). Type.Family.List.ListC (GHC.Classes.Eq Type.Family.List.<$> (f Type.Family.List.<$> as)) => GHC.Classes.Eq (Data.Type.Product.Prod f as)
instance forall k (f :: k -> *) (as :: [k]). (Type.Family.List.ListC (GHC.Classes.Eq Type.Family.List.<$> (f Type.Family.List.<$> as)), Type.Family.List.ListC (GHC.Classes.Ord Type.Family.List.<$> (f Type.Family.List.<$> as))) => GHC.Classes.Ord (Data.Type.Product.Prod f as)
instance forall k (f :: k -> *) (as :: [k]). Type.Family.List.ListC (GHC.Show.Show Type.Family.List.<$> (f Type.Family.List.<$> as)) => GHC.Show.Show (Data.Type.Product.Prod f as)
instance forall k (f :: k -> GHC.Types.*). Type.Class.Higher.Eq1 f => Type.Class.Higher.Eq1 (Data.Type.Product.Prod f)
instance forall k (f :: k -> GHC.Types.*). Type.Class.Higher.Ord1 f => Type.Class.Higher.Ord1 (Data.Type.Product.Prod f)
instance forall k (f :: k -> GHC.Types.*). Type.Class.Higher.Show1 f => Type.Class.Higher.Show1 (Data.Type.Product.Prod f)
instance forall k (f :: k -> GHC.Types.*). Type.Class.Higher.Read1 f => Type.Class.Higher.Read1 (Data.Type.Product.Prod f)
instance forall k (f :: k -> GHC.Types.*). Data.Type.Boolean.BoolEquality f => Data.Type.Boolean.BoolEquality (Data.Type.Product.Prod f)
instance forall k (f :: k -> *). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (Data.Type.Product.Prod f)
instance Type.Class.Higher.Functor1 Data.Type.Product.Prod
instance Type.Class.Higher.IxFunctor1 Data.Type.Index.Index Data.Type.Product.Prod
instance Type.Class.Higher.Foldable1 Data.Type.Product.Prod
instance Type.Class.Higher.IxFoldable1 Data.Type.Index.Index Data.Type.Product.Prod
instance Type.Class.Higher.Traversable1 Data.Type.Product.Prod
instance Type.Class.Higher.IxTraversable1 Data.Type.Index.Index Data.Type.Product.Prod
instance forall k (as :: [k]) (f :: k -> GHC.Types.*). (Type.Class.Known.Known Data.Type.Length.Length as, Data.Type.Index.Every (Type.Class.Known.Known f) as) => Type.Class.Known.Known (Data.Type.Product.Prod f) as
instance forall k (f :: k -> GHC.Types.*). Type.Class.Witness.Witness Type.Family.Constraint.ØC Type.Family.Constraint.ØC (Data.Type.Product.Prod f Type.Family.List.Ø)
instance forall a (p :: GHC.Types.Constraint) (q :: GHC.Types.Constraint) (f :: a -> GHC.Types.*) (a1 :: a) (s :: GHC.Types.Constraint) (t :: GHC.Types.Constraint) (as :: [a]). (Type.Class.Witness.Witness p q (f a1), 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 (a1 Type.Family.List.:< as))


-- | A <tt>singleton</tt>-esque type for representing subsets of a type
--   level list.
module Data.Type.Subset
type Subset as = Prod (Index as)
subNil :: Subset Ø as -> (as :~: Ø)
type (⊆) as bs = Every (Elem bs) as
subRefl :: Known Length as => Subset as as
subTrans :: Subset as bs -> Subset bs cs -> Subset as cs
subProd :: Subset as bs -> Prod f as -> Prod f bs
subSum :: Subset as bs -> Sum f as -> Maybe (Sum f bs)
subIx :: Subset as bs -> Index bs x -> Index as x
subExt :: Known Length as => (forall x. Index as x -> Index bs x) -> Subset bs as
subExtBy :: (forall x. Index as x -> Index bs x) -> Length as -> Subset bs as


-- | A <tt>singleton</tt>-esque type for representing the removal of an
--   element from a type level list.
module Data.Type.Remove
data Remove :: [k] -> k -> [k] -> *
[RZ] :: Remove (a :< as) a as
[RS] :: !(Remove as a bs) -> Remove (b :< as) a (b :< bs)
remLen :: Remove as a bs -> S (Len bs) :~: Len as
elimRemove :: (forall xs. p (a :< xs) a xs) -> (forall x xs ys. Remove xs a ys -> p xs a ys -> p (x :< xs) a (x :< ys)) -> Remove as a bs -> p as a bs
remIx :: Remove as a bs -> Index as a
remSub :: Length bs -> Remove as a bs -> Subset as bs
ixRem :: Index as a -> Some (Remove as a)
remProd :: Remove as a bs -> Prod f as -> (f a, Prod f bs)
remSum :: Remove as a bs -> Sum f as -> Either (f a) (Sum f bs)
class Without (as :: [k]) (a :: k) (bs :: [k]) | as a -> bs
without :: Without as a bs => Remove as a bs
instance forall k (as :: [k]) (a :: k) (bs :: [k]). GHC.Classes.Eq (Data.Type.Remove.Remove as a bs)
instance forall k (as :: [k]) (a :: k) (bs :: [k]). GHC.Classes.Ord (Data.Type.Remove.Remove as a bs)
instance forall k (as :: [k]) (a :: k) (bs :: [k]). GHC.Show.Show (Data.Type.Remove.Remove as a bs)
instance forall k (as :: [k]) (a :: k). Type.Class.Higher.Eq1 (Data.Type.Remove.Remove as a)
instance forall k (as :: [k]) (a :: k). Type.Class.Higher.Ord1 (Data.Type.Remove.Remove as a)
instance forall k (as :: [k]) (a :: k). Type.Class.Higher.Show1 (Data.Type.Remove.Remove as a)
instance forall k (as :: [k]). Type.Class.Higher.Eq2 (Data.Type.Remove.Remove as)
instance forall k (as :: [k]). Type.Class.Higher.Ord2 (Data.Type.Remove.Remove as)
instance forall k (as :: [k]). Type.Class.Higher.Show2 (Data.Type.Remove.Remove as)
instance Type.Class.Higher.Eq3 Data.Type.Remove.Remove
instance Type.Class.Higher.Ord3 Data.Type.Remove.Remove
instance Type.Class.Higher.Show3 Data.Type.Remove.Remove
instance Type.Class.Higher.Read3 Data.Type.Remove.Remove
instance forall k (as :: [k]) (a :: k). Data.Type.Equality.TestEquality (Data.Type.Remove.Remove as a)
instance forall k (as :: [k]) (bs :: [k]) (a :: k). as ~ bs => Data.Type.Remove.Without (a Type.Family.List.:< as) a bs
instance forall k (cs :: [k]) (b :: k) (bs :: [k]) (as :: [k]) (a :: k). (cs ~ (b Type.Family.List.:< bs), Data.Type.Remove.Without as a bs) => Data.Type.Remove.Without (b Type.Family.List.:< as) a cs
instance forall k (as :: [k]) (a :: k) (bs :: [k]). Type.Class.Witness.Witness Type.Family.Constraint.ØC (Data.Type.Remove.Without as a bs) (Data.Type.Remove.Remove as a bs)
instance forall k (as :: [k]) (a :: k) (bs :: [k]). Data.Type.Remove.Without as a bs => Type.Class.Known.Known (Data.Type.Remove.Remove as a) bs


-- | A <tt>singleton</tt>-esque type for representing the removal of a
--   subset of a type level list.
module Data.Type.Difference
data Difference :: [k] -> [k] -> [k] -> *
[ØD] :: Difference as Ø as
[:-] :: !(Remove bs a cs) -> !(Difference cs as ds) -> Difference bs (a :< as) ds
diffLen :: Difference as bs cs -> Length bs
elimDifference :: (forall xs. p xs Ø xs) -> (forall x ws xs ys zs. Remove xs x ys -> Difference ys ws zs -> p ys ws zs -> p xs (x :< ws) zs) -> Difference as bs cs -> p as bs cs
diffProd :: Difference as bs cs -> Prod f as -> (Prod f bs, Prod f cs)
diffSum :: Difference as bs cs -> Sum f as -> Either (Sum f bs) (Sum f cs)
class WithoutAll (as :: [k]) (bs :: [k]) (cs :: [k]) | as bs -> cs
withoutAll :: WithoutAll as bs cs => Difference as bs cs
instance forall k (as :: [k]) (bs :: [k]). Data.Type.Equality.TestEquality (Data.Type.Difference.Difference as bs)
instance forall k (cs :: [k]) (as :: [k]). cs ~ as => Data.Type.Difference.WithoutAll as Type.Family.List.Ø cs
instance forall a (as :: [a]) (b :: a) (cs :: [a]) (bs :: [a]) (ds :: [a]). (Data.Type.Remove.Without as b cs, Data.Type.Difference.WithoutAll cs bs ds) => Data.Type.Difference.WithoutAll as (b Type.Family.List.:< bs) ds
instance forall k (as :: [k]) (bs :: [k]) (cs :: [k]). Type.Class.Witness.Witness Type.Family.Constraint.ØC (Data.Type.Difference.WithoutAll as bs cs) (Data.Type.Difference.Difference as bs cs)
instance forall k (as :: [k]) (bs :: [k]) (cs :: [k]). Data.Type.Difference.WithoutAll as bs cs => Type.Class.Known.Known (Data.Type.Difference.Difference as bs) cs


-- | <a>Vec</a> and its combinator analog <a>VecT</a> represent lists of
--   known length, characterized by the index <tt>(n :: N)</tt> in
--   <tt><a>Vec</a> n a</tt> or <tt><a>VecT</a> n f a</tt>.
--   
--   The classic example used ad nauseum for type-level programming.
--   
--   The operations on <a>Vec</a> and <a>VecT</a> correspond to the type
--   level arithmetic operations on the kind <a>N</a>.
module Data.Type.Vector
data VecT (n :: N) (f :: k -> *) :: k -> *
[ØV] :: VecT Z f a
[:*] :: !(f a) -> !(VecT n f a) -> VecT (S n) f a
elimVecT :: p Z -> (forall x. f a -> p x -> p (S x)) -> VecT n f a -> p n
elimV :: p Z -> (forall x. a -> p x -> p (S x)) -> Vec n a -> p n
type Vec n = VecT n I
infixr 4 :+
(.++) :: VecT x f a -> VecT y f a -> VecT (x + y) f a
infixr 5 .++
vrep :: forall n f a. Known Nat n => f a -> VecT n f a
head' :: VecT (S n) f a -> f a
tail' :: VecT (S n) f a -> VecT n f a
onTail :: (VecT m f a -> VecT n f a) -> VecT (S m) f a -> VecT (S n) f a
vDel :: Fin n -> VecT n f a -> VecT (Pred n) f a
imap :: (Fin n -> f a -> g b) -> VecT n f a -> VecT n g b
ifoldMap :: Monoid m => (Fin n -> f a -> m) -> VecT n f a -> m
itraverse :: Applicative h => (Fin n -> f a -> h (g b)) -> VecT n f a -> h (VecT n g b)
index :: Fin n -> VecT n f a -> f a
index' :: Fin n -> Vec n a -> a
vmap :: (f a -> g b) -> VecT n f a -> VecT n g b
vap :: (f a -> g b -> h c) -> VecT n f a -> VecT n g b -> VecT n h c
vfoldr :: (f a -> b -> b) -> b -> VecT n f a -> b
vfoldMap' :: (b -> b -> b) -> b -> (f a -> b) -> VecT n f a -> b
vfoldMap :: Monoid m => (f a -> m) -> VecT n f a -> m
withVecT :: [f a] -> (forall n. VecT n f a -> r) -> r
withV :: [a] -> (forall n. Vec n a -> r) -> r
findV :: Eq a => a -> Vec n a -> Maybe (Fin n)
findVecT :: Eq (f a) => f a -> VecT 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) -> VecT n f a
vgen :: Nat n -> (Fin n -> f a) -> VecT 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 :: VecT n (VecT n f) a -> VecT n f a
vtranspose :: Known Nat n => VecT m (VecT n f) a -> VecT n (VecT 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 :: (VecT n ((->) String) String -> ShowS) -> (f a -> ShowS) -> VecT n f a -> ShowS
ppMatrix :: forall ns a. (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 (f :: k -> *) (a :: k) (n :: Type.Family.Nat.N). GHC.Classes.Eq (f a) => GHC.Classes.Eq (Data.Type.Vector.VecT n f a)
instance forall k (f :: k -> *) (a :: k) (n :: Type.Family.Nat.N). GHC.Classes.Ord (f a) => GHC.Classes.Ord (Data.Type.Vector.VecT n f a)
instance forall k (f :: k -> *) (a :: k) (n :: Type.Family.Nat.N). GHC.Show.Show (f a) => GHC.Show.Show (Data.Type.Vector.VecT 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 Type.Class.Higher.Functor1 (Data.Type.Vector.VecT n)
instance Type.Class.Higher.Foldable1 (Data.Type.Vector.VecT n)
instance Type.Class.Higher.Traversable1 (Data.Type.Vector.VecT n)
instance GHC.Base.Functor f => GHC.Base.Functor (Data.Type.Vector.VecT n f)
instance (GHC.Base.Applicative f, Type.Class.Known.Known Data.Type.Nat.Nat n) => GHC.Base.Applicative (Data.Type.Vector.VecT n f)
instance (GHC.Base.Monad f, Type.Class.Known.Known Data.Type.Nat.Nat n) => GHC.Base.Monad (Data.Type.Vector.VecT n f)
instance Data.Foldable.Foldable f => Data.Foldable.Foldable (Data.Type.Vector.VecT n f)
instance Data.Traversable.Traversable f => Data.Traversable.Traversable (Data.Type.Vector.VecT n f)
instance forall k (n :: Type.Family.Nat.N) (f :: k -> GHC.Types.*) (a :: k). Type.Class.Witness.Witness Type.Family.Constraint.ØC (Type.Class.Known.Known Data.Type.Nat.Nat n) (Data.Type.Vector.VecT n f a)
instance forall k (f :: k -> *) (a :: k) (n :: Type.Family.Nat.N). (GHC.Num.Num (f a), Type.Class.Known.Known Data.Type.Nat.Nat n) => GHC.Num.Num (Data.Type.Vector.VecT n f a)
instance GHC.Num.Num (Data.Type.Vector.Matrix ns a) => GHC.Num.Num (Data.Type.Vector.M ns a)

module Data.Type.Product.Env
newtype Env k v ps
Env :: Prod (k :*: v) ps -> Env k v ps
[getEnv] :: Env k v ps -> Prod (k :*: v) ps
member' :: BoolEquality k => k x -> Env k v ps -> Boolean (Member x ps)
lookup' :: BoolEquality k => k x -> Env k v ps -> Option v (Lookup x ps)
insert' :: BoolEquality k => k x -> v a -> Env k v ps -> Env k v (Insert x a ps)
delete' :: BoolEquality k => k x -> Env k v ps -> Env k v (Delete x ps)
difference' :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Difference ps qs)
(.\\) :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Difference ps qs)
union' :: BoolEquality k => Env k v ps -> Env k v qs -> Env k v (Union ps qs)
intersection' :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Intersection ps qs)
ixList :: Index as a -> i a b -> IxList i as b
instance forall k k1 (k2 :: k1 -> GHC.Types.*). Type.Class.Higher.Functor1 (Data.Type.Product.Env.Env k2)
instance forall k m (k1 :: m -> GHC.Types.*). Type.Class.Higher.IxFunctor1 (Data.Type.Index.Trans.IxList (Data.Type.Index.Trans.IxSecond (Data.Type.Equality.:~:))) (Data.Type.Product.Env.Env k1)