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


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

module Type.Family.Symbol


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


-- | 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
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 family WitnessC p q t :: Constraint WitnessC p q t = ØC
(\\) :: (Witness p q t, p) => (q => r) -> t -> r
(//) :: (Witness p q t, p) => t -> (q => r) -> r

-- | 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 :: 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
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
(//?+) :: (Witness p q t, p) => Either e t -> (q => Either e r) -> Either e r
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)
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)
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 :: BOX) (c :: GHC.Prim.Constraint) (d :: k). c => Type.Class.Witness.Const c d
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> GHC.Prim.Constraint) (g :: k1 -> k) (a :: k1). f (g a) => (Type.Class.Witness.∘) f g a
instance forall (k :: BOX) (f :: k -> GHC.Prim.Constraint) (g :: k -> GHC.Prim.Constraint) (a :: k). (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 :: BOX) (c :: k -> GHC.Prim.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 :: 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) (c :: k -> GHC.Prim.Constraint) (a :: k). c a => Type.Class.Known.Known (Type.Class.Witness.Wit1 c) a


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


-- | 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)


-- | 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)
predCong :: (x ~ y) :- (Pred x ~ Pred y)
addCong :: (w ~ y, x ~ z) :- ((w + x) ~ (y + z))
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


-- | 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
(>>-) :: Some f -> (forall a. f a -> r) -> r
(>->) :: (forall x. f x -> Some g) -> (forall x. g x -> Some h) -> f a -> Some h
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
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
(>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h
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
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
(>--->) :: (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
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
data SomeC (c :: k -> Constraint) (f :: k -> *)
SomeC :: 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
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
data Every (f :: k -> *) :: *
Every :: (forall a. f a) -> Every f
[instEvery] :: Every f -> forall a. f a
data Every2 (f :: k -> l -> *) :: *
Every2 :: (forall a b. f a b) -> Every2 f
[instEvery2] :: Every2 f -> forall a b. f a b
data Every3 (f :: k -> l -> m -> *) :: *
Every3 :: (forall a b c. f a b c) -> Every3 f
[instEvery3] :: Every3 f -> forall a b c. f a b c
data EveryC (c :: k -> Constraint) (f :: k -> *) :: *
EveryC :: (forall a. c a => f a) -> EveryC c f
[instEveryC] :: EveryC c f -> forall a. c a => f a


-- | Higher order analogs of type classes from the Prelude.
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
neq1 :: Eq1 f => f a -> f a -> Bool
(=#=) :: Eq1 f => f a -> f a -> Bool
class Eq2 (f :: k -> l -> *) where eq2 = (==) neq2 a b = not $ eq2 a b
eq2 :: Eq2 f => 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
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
neq3 :: Eq3 f => f a b c -> f a b c -> Bool
(=###=) :: Eq3 f => f a b c -> f a b c -> Bool
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
(<#) :: 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
(<##) :: 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
(<###) :: 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
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
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
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


-- | 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.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 :: 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 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
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 :: p a b -> Uncur p (a # b)
[getUncur] :: Uncur p (a # b) -> 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 :: p a b c -> Uncur3 p '(a, b, c)
[getUncur3] :: Uncur3 p '(a, b, c) -> 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
instance forall (k :: BOX) (k1 :: BOX) (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 :: 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 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 (k :: BOX) r (a :: k). GHC.Read.Read r => GHC.Read.Read (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) r (a :: k). GHC.Classes.Ord r => GHC.Classes.Ord (Data.Type.Combinator.C r a)
instance forall (k :: BOX) r (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 :: BOX) (k :: BOX) (f :: l -> *) (g :: k -> l) (a :: k). GHC.Read.Read (f (g a)) => GHC.Read.Read ((Data.Type.Combinator.:.:) f g a)
instance forall (l :: BOX) (k :: BOX) (f :: l -> *) (g :: k -> l) (a :: k). GHC.Show.Show (f (g a)) => GHC.Show.Show ((Data.Type.Combinator.:.:) f g a)
instance forall (l :: BOX) (k :: BOX) (f :: l -> *) (g :: k -> l) (a :: k). GHC.Classes.Ord (f (g a)) => GHC.Classes.Ord ((Data.Type.Combinator.:.:) f g a)
instance forall (l :: BOX) (k :: BOX) (f :: l -> *) (g :: k -> l) (a :: k). GHC.Classes.Eq (f (g a)) => GHC.Classes.Eq ((Data.Type.Combinator.:.:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (p :: (,) k k1 -> *) (a :: k) (b :: k1). GHC.Classes.Eq (p (a Type.Family.Tuple.# b)) => GHC.Classes.Eq (Data.Type.Combinator.Cur p a b)
instance forall (k :: BOX) (k1 :: BOX) (p :: (,) k k1 -> *) (a :: k) (b :: k1). GHC.Classes.Ord (p (a Type.Family.Tuple.# b)) => GHC.Classes.Ord (Data.Type.Combinator.Cur p a b)
instance forall (k :: BOX) (k1 :: BOX) (p :: (,) k k1 -> *) (a :: k) (b :: k1). GHC.Show.Show (p (a Type.Family.Tuple.# b)) => GHC.Show.Show (Data.Type.Combinator.Cur p a b)
instance forall (k :: BOX) (k1 :: BOX) (p :: (,) k k1 -> *) (a :: k) (b :: k1). GHC.Read.Read (p (a Type.Family.Tuple.# b)) => GHC.Read.Read (Data.Type.Combinator.Cur p a b)
instance forall (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (x :: (,) k k1). 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 (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (x :: (,) k k1). 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 (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (x :: (,) k k1). 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 (k :: BOX) (k1 :: BOX) (p :: k -> k1 -> *) (x :: (,) k k1) (a :: k) (b :: k1). (x ~ (a Type.Family.Tuple.# b), GHC.Read.Read (p a b)) => GHC.Read.Read (Data.Type.Combinator.Uncur p x)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: (,,) k k1 k2 -> *) (a :: k) (b :: k1) (c :: k2). GHC.Classes.Eq (p '(a, b, c)) => GHC.Classes.Eq (Data.Type.Combinator.Cur3 p a b c)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: (,,) k k1 k2 -> *) (a :: k) (b :: k1) (c :: k2). GHC.Classes.Ord (p '(a, b, c)) => GHC.Classes.Ord (Data.Type.Combinator.Cur3 p a b c)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: (,,) k k1 k2 -> *) (a :: k) (b :: k1) (c :: k2). GHC.Show.Show (p '(a, b, c)) => GHC.Show.Show (Data.Type.Combinator.Cur3 p a b c)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: (,,) k k1 k2 -> *) (a :: k) (b :: k1) (c :: k2). GHC.Read.Read (p '(a, b, c)) => GHC.Read.Read (Data.Type.Combinator.Cur3 p a b c)
instance forall (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: k -> k1 -> k2 -> *) (x :: (,,) k k1 k2). 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 (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: k -> k1 -> k2 -> *) (x :: (,,) k k1 k2). 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 (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: k -> k1 -> k2 -> *) (x :: (,,) k k1 k2). 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 (k :: BOX) (k1 :: BOX) (k2 :: BOX) (p :: k -> k1 -> k2 -> *) (x :: (,,) k k1 k2) (a :: k) (b :: k1) (c :: k2). (x ~ '(a, b, c), GHC.Read.Read (p a b c)) => GHC.Read.Read (Data.Type.Combinator.Uncur3 p x)
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) (f :: k -> k -> *) (a :: k). GHC.Read.Read (f a a) => GHC.Read.Read (Data.Type.Combinator.Join f a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *) (g :: k -> k1). Type.Class.Higher.Eq1 f => Type.Class.Higher.Eq1 (f Data.Type.Combinator.:.: g)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *) (g :: k -> k1). Type.Class.Higher.Ord1 f => Type.Class.Higher.Ord1 (f Data.Type.Combinator.:.: g)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *) (g :: k -> k1). Type.Class.Higher.Show1 f => Type.Class.Higher.Show1 (f Data.Type.Combinator.:.: g)
instance forall (k :: BOX) (k1 :: BOX) (p :: GHC.Prim.Constraint) (q :: GHC.Prim.Constraint) (f :: k -> *) (g :: k1 -> k) (a :: k1). 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) (f :: k1 -> *) (g :: k -> k1). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (f Data.Type.Combinator.:.: g)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). 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 :: 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) (k1 :: BOX) (p :: k -> k1 -> *) (b :: k1). Type.Class.Witness.TestEquality1 p => Data.Type.Equality.TestEquality (Data.Type.Combinator.Flip p b)
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 :: 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 :: (,) 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 -> *). Type.Class.Higher.Read2 p => Type.Class.Higher.Read1 (Data.Type.Combinator.Uncur p)
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 -> *). Type.Class.Higher.Read3 p => Type.Class.Higher.Read1 (Data.Type.Combinator.Uncur3 p)
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)
instance forall (k :: BOX) (f :: k -> k -> *). Type.Class.Higher.Eq2 f => Type.Class.Higher.Eq1 (Data.Type.Combinator.Join f)
instance forall (k :: BOX) (f :: k -> k -> *). Type.Class.Higher.Ord2 f => Type.Class.Higher.Ord1 (Data.Type.Combinator.Join f)
instance forall (k :: BOX) (f :: k -> k -> *). Type.Class.Higher.Show2 f => Type.Class.Higher.Show1 (Data.Type.Combinator.Join f)
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)


-- | 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 -> *) (g :: k -> *) (a :: k). (GHC.Classes.Eq (f a), GHC.Classes.Eq (g a)) => GHC.Classes.Eq ((Data.Type.Disjunction.:|:) 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.Disjunction.:|:) 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.Disjunction.:|:) f g a)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *) (a :: k). (GHC.Read.Read (f a), GHC.Read.Read (g a)) => GHC.Read.Read ((Data.Type.Disjunction.:|:) f g a)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (e :: Data.Either.Either k k1). (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 (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (e :: Data.Either.Either k k1). (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 (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (e :: Data.Either.Either k k1). (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 :: BOX) (f :: k -> *) (g :: k -> *). (Type.Class.Higher.Eq1 f, Type.Class.Higher.Eq1 g) => Type.Class.Higher.Eq1 (f Data.Type.Disjunction.:|: g)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *). (Type.Class.Higher.Ord1 f, Type.Class.Higher.Ord1 g) => Type.Class.Higher.Ord1 (f Data.Type.Disjunction.:|: g)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *). (Type.Class.Higher.Show1 f, Type.Class.Higher.Show1 g) => Type.Class.Higher.Show1 (f Data.Type.Disjunction.:|: g)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *). (Type.Class.Higher.Read1 f, Type.Class.Higher.Read1 g) => Type.Class.Higher.Read1 (f Data.Type.Disjunction.:|: g)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Functor1 ((Data.Type.Disjunction.:|:) f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Foldable1 ((Data.Type.Disjunction.:|:) f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Traversable1 ((Data.Type.Disjunction.:|:) f)
instance Type.Class.Higher.Bifunctor1 (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 :: k -> *) (g :: k1 -> *). (Type.Class.Higher.Eq1 f, Type.Class.Higher.Eq1 g) => Type.Class.Higher.Eq1 (f Data.Type.Disjunction.:+: g)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *). (Type.Class.Higher.Ord1 f, Type.Class.Higher.Ord1 g) => Type.Class.Higher.Ord1 (f Data.Type.Disjunction.:+: g)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *). (Type.Class.Higher.Show1 f, Type.Class.Higher.Show1 g) => Type.Class.Higher.Show1 (f Data.Type.Disjunction.:+: g)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *). (Type.Class.Higher.Read1 f, Type.Class.Higher.Read1 g) => Type.Class.Higher.Read1 (f Data.Type.Disjunction.:+: g)
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.Higher.Functor1 ((Data.Type.Disjunction.:+:) f)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.Higher.Foldable1 ((Data.Type.Disjunction.:+:) f)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.Higher.Traversable1 ((Data.Type.Disjunction.:+:) f)
instance Type.Class.Higher.Bifunctor1 (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
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 -> Void
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
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) (as :: [k]). Type.Class.Higher.Eq1 (Data.Type.Index.Index as)
instance forall (k :: BOX) (as :: [k]). Type.Class.Higher.Ord1 (Data.Type.Index.Index as)
instance forall (k :: BOX) (as :: [k]). Type.Class.Higher.Show1 (Data.Type.Index.Index as)
instance Type.Class.Higher.Read2 Data.Type.Index.Index
instance forall (k :: BOX) (as :: [k]). Data.Type.Equality.TestEquality (Data.Type.Index.Index as)
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


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

-- | 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.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 :: BOX) (a :: k). Type.Class.Known.Known (Data.Type.Product.Lifted.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.Lifted.FProd fs) a) => Type.Class.Known.Known (Data.Type.Product.Lifted.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.Lifted.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.Lifted.FProd fs a)) => Type.Class.Witness.Witness (p, s) (q, t) (Data.Type.Product.Lifted.FProd (f Type.Family.List.:< fs) a)


-- | <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)


-- | 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 :: 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.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 :: 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)


-- | <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 :: BOX) (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 :: BOX) (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 :: BOX) (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 :: BOX) (f :: k -> *). Type.Class.Higher.Eq1 f => Type.Class.Higher.Eq1 (Data.Type.Sum.Sum f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Ord1 f => Type.Class.Higher.Ord1 (Data.Type.Sum.Sum f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Show1 f => Type.Class.Higher.Show1 (Data.Type.Sum.Sum f)
instance forall (k :: BOX) (f :: k -> *). 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 :: 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 <tt>singleton</tt>-esque type for type-level Bool values.
module Data.Type.Boolean
data Boolean :: Bool -> *
False_ :: Boolean False
True_ :: Boolean True
not' :: Boolean a -> Boolean (Not a)
(.||) :: Boolean a -> Boolean b -> Boolean (a || b)
(.&&) :: Boolean a -> Boolean b -> Boolean (a && b)
(.^^) :: Boolean a -> Boolean b -> Boolean (a ^^ b)
(==>) :: Boolean a -> Boolean b -> Boolean (a ==> b)
(<==>) :: Boolean a -> Boolean b -> Boolean (a <==> b)
class BoolEquality (f :: k -> *) where type family BoolEqC f (a :: k) (b :: k) :: Constraint BoolEqC f a b = ØC
(.==) :: (BoolEquality f, BoolEqC f a b) => f a -> f b -> Boolean (a == b)
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 Type.Class.Known.Known Data.Type.Boolean.Boolean 'GHC.Types.True
instance Type.Class.Known.Known Data.Type.Boolean.Boolean 'GHC.Types.False


-- | 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
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 :: 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) (f :: k -> *) (g :: k -> *) (a :: k). (GHC.Read.Read (f a), GHC.Read.Read (g a)) => GHC.Read.Read ((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) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *) (p :: (,) k k1) (a :: k) (b :: k1). (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 :: BOX) (f :: k -> *) (g :: k -> *). (Type.Class.Higher.Eq1 f, Type.Class.Higher.Eq1 g) => Type.Class.Higher.Eq1 (f Data.Type.Conjunction.:&: g)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *). (Type.Class.Higher.Ord1 f, Type.Class.Higher.Ord1 g) => Type.Class.Higher.Ord1 (f Data.Type.Conjunction.:&: g)
instance forall (k :: BOX) (f :: k -> *) (g :: k -> *). (Type.Class.Higher.Show1 f, Type.Class.Higher.Show1 g) => Type.Class.Higher.Show1 (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.Higher.Functor1 ((Data.Type.Conjunction.:&:) f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Foldable1 ((Data.Type.Conjunction.:&:) f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Traversable1 ((Data.Type.Conjunction.:&:) f)
instance Type.Class.Higher.Bifunctor1 (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 -> *). (Type.Class.Higher.Eq1 f, Type.Class.Higher.Eq1 g) => Type.Class.Higher.Eq1 (f Data.Type.Conjunction.:*: g)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *). (Type.Class.Higher.Ord1 f, Type.Class.Higher.Ord1 g) => Type.Class.Higher.Ord1 (f Data.Type.Conjunction.:*: g)
instance forall (k :: BOX) (k1 :: BOX) (f :: k -> *) (g :: k1 -> *). (Type.Class.Higher.Show1 f, Type.Class.Higher.Show1 g) => Type.Class.Higher.Show1 (f Data.Type.Conjunction.:*: g)
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.Higher.Functor1 ((Data.Type.Conjunction.:*:) f)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.Higher.Foldable1 ((Data.Type.Conjunction.:*:) f)
instance forall (k :: BOX) (k1 :: BOX) (f :: k1 -> *). Type.Class.Higher.Traversable1 ((Data.Type.Conjunction.:*:) f)
instance Type.Class.Higher.Bifunctor1 (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)


-- | 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)
lookup' :: TestEquality f => f a -> Prod (f :&: g) as -> Maybe (g a)
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.

-- | Snoc onto a Tuple.
(>::) :: Tuple as -> a -> Tuple (as >: a)
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
instance forall (k :: BOX) (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 :: BOX) (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 :: BOX) (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 :: BOX) (f :: k -> *). Type.Class.Higher.Eq1 f => Type.Class.Higher.Eq1 (Data.Type.Product.Prod f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Ord1 f => Type.Class.Higher.Ord1 (Data.Type.Product.Prod f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Show1 f => Type.Class.Higher.Show1 (Data.Type.Product.Prod f)
instance forall (k :: BOX) (f :: k -> *). Type.Class.Higher.Read1 f => Type.Class.Higher.Read1 (Data.Type.Product.Prod f)
instance forall (k :: BOX) (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 :: 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>.
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)
(.*) :: Nat x -> Nat y -> Nat (x * y)
(.^) :: Nat x -> Nat y -> Nat (x ^ y)
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 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 (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 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)


-- | <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
elimVT :: p Z -> (forall x. f a -> p x -> p (S x)) -> VT n f a -> p n
elimV :: p Z -> (forall x. a -> p x -> p (S x)) -> V n a -> p n
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)


-- | A <tt>singleton</tt>-esque type for representing type-level Symbols.
module Data.Type.Sym
data Sym :: Symbol -> *
Sym :: Sym x
symbol :: Sym x -> String
instance GHC.Classes.Eq (Data.Type.Sym.Sym x)
instance GHC.Classes.Ord (Data.Type.Sym.Sym x)
instance GHC.Show.Show (Data.Type.Sym.Sym x)
instance Type.Class.Higher.Eq1 Data.Type.Sym.Sym
instance Type.Class.Higher.Ord1 Data.Type.Sym.Sym
instance Type.Class.Higher.Show1 Data.Type.Sym.Sym
instance Data.Type.Equality.TestEquality Data.Type.Sym.Sym
instance Data.Type.Boolean.BoolEquality Data.Type.Sym.Sym
instance GHC.TypeLits.KnownSymbol x => Type.Class.Known.Known Data.Type.Sym.Sym x
instance Type.Class.Witness.Witness Type.Family.Constraint.ØC (GHC.TypeLits.KnownSymbol x) (Data.Type.Sym.Sym x)