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

-- | First-class type families
--   
--   A library for type-level programming.
--   
--   See README.
@package first-class-families
@version 0.8.2.0

-- | The Eval family.
module Fcf.Core

-- | Kind of type-level expressions indexed by their result type.
type Exp a = a -> Type

-- | Expression evaluator.
type family Eval (e :: Exp a) :: a

-- | Apply and evaluate a unary type function.
type (f :: k1 -> Exp k) @@ (x :: k1) = Eval f x

-- | General fcf combinators.
--   
--   See also Fcf.Data.Function for more.
module Fcf.Combinators
data Pure (b :: a) (c :: a)
data Pure1 (c :: a -> b) (d :: a) (e :: b)
data Pure2 (d :: a -> b -> c) (e :: a) (f :: b) (g :: c)
data Pure3 (e :: a -> b -> c -> d) (f :: a) (g :: b) (h :: c) (i :: d)
data Pure4 (f :: a -> b -> c -> d -> e) (g :: a) (h :: b) (i :: c) (j :: d) (k :: e)
data Pure5 (g :: a -> b -> c -> d -> e -> f) (h :: a) (i :: b) (j :: c) (k :: d) (l :: e) (m :: f)
data Pure6 (h :: a -> b -> c -> d -> e -> f -> g) (i :: a) (j :: b) (k :: c) (l :: d) (m :: e) (n :: f) (o :: g)
data Pure7 (i :: a -> b -> c -> d -> e -> f -> g -> h) (j :: a) (k :: b) (l :: c) (m :: d) (n :: e) (o :: f) (p :: g) (q :: h)
data Pure8 (j :: a -> b -> c -> d -> e -> f -> g -> h -> i) (k :: a) (l :: b) (m :: c) (n :: d) (o :: e) (p :: f) (q :: g) (r :: h) (s :: i)
data Pure9 (k :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j) (l :: a) (m :: b) (n :: c) (o :: d) (p :: e) (q :: f) (r :: g) (s :: h) (t :: i) (u :: j)
data ( (c :: a -> Exp b) =<< (d :: Exp a) ) (e :: b)
infixr 1 =<<
data ( (c :: Exp a) >>= (d :: a -> Exp b) ) (e :: b)
infixl 1 >>=
data ( (d :: b -> Exp c) <=< (e :: a -> Exp b) ) (f :: a) (g :: c)
infixr 1 <=<
type LiftM = (=<<) :: a -> Exp b -> Exp a -> b -> Type
data LiftM2 (d :: a -> b -> Exp c) (e :: Exp a) (f :: Exp b) (g :: c)
data LiftM3 (e :: a -> b -> c -> Exp d) (f :: Exp a) (g :: Exp b) (h :: Exp c) (i :: d)
data Join (b :: Exp Exp a) (c :: a)
data ( (c :: a -> b) <$> (d :: Exp a) ) (e :: b)
infixl 4 <$>
data ( (c :: Exp a -> b) <*> (d :: Exp a) ) (e :: b)
infixl 4 <*>
data Flip (d :: a -> b -> Exp c) (e :: b) (f :: a) (g :: c)
data ConstFn (c :: a) (d :: b) (e :: a)

-- | Note that this denotes the identity function, so ($) f can
--   usually be replaced with f.
data ( (c :: a -> Exp b) $ (d :: a) ) (e :: b)
infixr 0 $

-- | Semigroups and monoids.
module Fcf.Class.Monoid

-- | Type-level semigroup composition (<>).
type family (x :: a) <> (y :: a) :: a

-- | Type-level monoid identity mempty.
--   
--   
Examples
--   
--   
--   >>> :kind! LT <> MEmpty
--   LT <> MEmpty :: Ordering
--   = LT
--   
--   
--   
--   >>> :kind! MEmpty <> '(EQ, [1, 2])
--   MEmpty <> '(EQ, [1, 2]) :: (Ordering, [Natural])
--   = '(EQ, [1, 2])
--   
--   
--   
--   >>> :kind! '(GT, Just '()) <> MEmpty
--   '(GT, Just '()) <> MEmpty :: (Ordering, Maybe ())
--   = '(GT, Just '())
--   
type family MEmpty :: a

-- | Type-level semigroup composition (<>).
--   
--   This is the fcf-encoding of (<>). To define a
--   new semigroup, add type instances to (<>).
data ( (b :: a) .<> (c :: a) ) (d :: a)

-- | Type-level monoid identity mempty.
--   
--   This is the fcf-encoding of MEmpty.
data MEmpty_ (b :: a)

-- | Carriers of useful monoid instances.
module Fcf.Class.Monoid.Types

-- | Endofunctions.
--   
--   
Details
--   
--   This is is used in the default implementation of Foldr in terms
--   of FoldMap.
newtype Endo a
Endo :: (a -> Exp a) -> Endo a

-- | Inverse of the Endo constructor.
type family UnEndo (e :: Endo a) :: a -> Exp a

module Fcf.Class.Functor

-- | Type-level fmap for type-level functors.
--   
--   Note: this name clashes with Map from containers.
--   FMap is provided as a synonym to avoid this.
--   
--   
Example
--   
--   
--   >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   >>> data AddMul :: Nat -> Nat -> Exp Nat
--   
--   >>> type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   >>> :kind! Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat])
--   Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]) :: Example
--   = Ex [4, 9, 16, 25, 36]
--   
data Map (c :: a -> Exp b) (d :: f a) (e :: f b)

-- | Synonym of Map to avoid name clashes.
type FMap = Map :: a -> Exp b -> f a -> f b -> Type

-- | Bifunctors.
--   
--   Bifunctors are "two-argument functors".
--   
--   This module is the type-level equivalent of Data.Bifunctor.
module Fcf.Class.Bifunctor

-- | Type-level bimap.
--   
--   
Example
--   
--   
--   >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   >>> :kind! Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural))
--   Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural)) :: Example
--   = Ex '(3, 3)
--   
data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')

-- | Type-level first. Apply a function along the first parameter of
--   a bifunctor.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (First ((+) 1) '(3,"a"))
--   Eval (First ((+) 1) '(3,"a")) :: (Natural, Symbol)
--   = '(4, "a")
--   
data First (d :: a -> Exp b) (e :: f a c) (g :: f b c)

-- | Type-level second. Apply a function along the second parameter
--   of a bifunctor.
--   
--   This is generally equivalent to Map.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Second ((+) 1) '("a",3))
--   Eval (Second ((+) 1) '("a",3)) :: (Symbol, Natural)
--   = '("a", 4)
--   
data Second (b :: c -> Exp d) (e :: f a c) (g :: f a d)

-- | Overloaded functions.

-- | Deprecated: Use Fcf.Class.Functor or Fcf.Class.Bifunctor
--   instead.
module Fcf.Classes

-- | Type-level fmap for type-level functors.
--   
--   Note: this name clashes with Map from containers.
--   FMap is provided as a synonym to avoid this.
--   
--   
Example
--   
--   
--   >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   >>> data AddMul :: Nat -> Nat -> Exp Nat
--   
--   >>> type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   >>> :kind! Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat])
--   Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]) :: Example
--   = Ex [4, 9, 16, 25, 36]
--   
data Map (c :: a -> Exp b) (d :: f a) (e :: f b)

-- | Type-level bimap.
--   
--   
Example
--   
--   
--   >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   >>> :kind! Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural))
--   Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural)) :: Example
--   = Ex '(3, 3)
--   
data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')

-- | Booleans.
--   
--   Note that the operations from this module conflict with
--   Data.Type.Bool.
module Fcf.Data.Bool

-- | N.B.: The order of the two branches is the opposite of "if":
--   UnBool ifFalse ifTrue bool.
--   
--   This mirrors the default order of constructors:
--   
--   
--   data Bool = False | True
--   ----------- False < True
--   
data UnBool (b :: Exp a) (c :: Exp a) (d :: Bool) (e :: a)
data ( (a :: Bool) || (b :: Bool) ) (c :: Bool)
infixr 2 ||
data ( (a :: Bool) && (b :: Bool) ) (c :: Bool)
infixr 3 &&
data Not (a :: Bool) (b :: Bool)

-- | Common data types: tuples, Either, Maybe.
module Fcf.Data.Common
data Uncurry (d :: a -> b -> Exp c) (e :: (a, b)) (f :: c)
data Fst (c :: (a, b)) (d :: a)
data Snd (c :: (a, b)) (d :: b)

-- | Specialization of Bimap for pairs.
data ( (a :: b -> Exp c) *** (d :: b' -> Exp c') ) (e :: (b, b')) (f :: (c, c'))
infixr 3 ***
data UnEither (d :: a -> Exp c) (e :: b -> Exp c) (f :: Either a b) (g :: c)
data IsLeft (c :: Either a b) (d :: Bool)
data IsRight (c :: Either a b) (d :: Bool)
data UnMaybe (c :: Exp b) (d :: a -> Exp b) (e :: Maybe a) (f :: b)
data FromMaybe (a :: k) (b :: Maybe k) (c :: k)
data IsNothing (b :: Maybe a) (c :: Bool)
data IsJust (b :: Maybe a) (c :: Bool)

-- | Simple combinators for functions.
module Fcf.Data.Function

-- | Reverse function application, argument first.
--   
--   
Example
--   
--   
--   >>> :kind! Eval ('(True, Nothing) & Fst)
--   Eval ('(True, Nothing) & Fst) :: Bool
--   = True
--   
data ( (c :: a) & (d :: a -> Exp b) ) (e :: b)
infixl 1 &

-- | Lift a binary function to the domain of a projection.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (((&&) `On` Fst) '(True, Nothing) '(False, Just '()))
--   Eval (((&&) `On` Fst) '(True, Nothing) '(False, Just '())) :: Bool
--   = False
--   
data On (d :: b -> b -> Exp c) (e :: a -> Exp b) (f :: a) (g :: a) (h :: c)

-- | Pre-compose a binary function with a function for each argument.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Bicomap Fst Pure (||) '(False, Nothing) True)
--   Eval (Bicomap Fst Pure (||) '(False, Nothing) True) :: Bool
--   = True
--   
data Bicomap (f :: a -> Exp c) (g :: b -> Exp d) (h :: c -> d -> Exp e) (i :: a) (j :: b) (k :: e)

-- | Natural numbers.
--   
--   Note that the operators from this module conflict with
--   GHC.TypeLits and GHC.TypeNats.
module Fcf.Data.Nat

-- | A type synonym for Natural.
--   
--   Previously, this was an opaque data type, but it was changed to a type
--   synonym.
type Nat = Natural
data ( (a :: Nat) + (b :: Nat) ) (c :: Nat)
data ( (a :: Nat) - (b :: Nat) ) (c :: Nat)
data ( (a :: Nat) * (b :: Nat) ) (c :: Nat)
data ( (a :: Nat) ^ (b :: Nat) ) (c :: Nat)
data ( (a :: Nat) <= (b :: Nat) ) (c :: Bool)
data ( (a :: Nat) >= (b :: Nat) ) (c :: Bool)
data ( (a :: Nat) < (b :: Nat) ) (c :: Bool)
data ( (a :: Nat) > (b :: Nat) ) (c :: Bool)

-- | Foldable types.
--   
--   A minimal implementation of this interface is given by either
--   FoldMap or Foldr, but a default still needs to be given
--   explicitly for the other.
--   
--   
--   data MyType a = ... {- Some custom Foldable type -}
--   
--   -- Method 1: Implement Foldr, default FoldMap.
--   type instance Eval (Foldr f y xs) = ... {- Explicit implementation -}
--   type instance Eval (FoldMap f xs) = FoldMapDefault_ f xs {- Default -}
--   
--   -- Method 2: Implement FoldMap, default Foldr.
--   type instance Eval (FoldMap f xs) = ... {- Explicit implementation -}
--   type instance Eval (Foldr f y xs) = FoldrDefault_ f y xs {- Default -}
--   
module Fcf.Class.Foldable

-- | Right fold.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Foldr (+) 0 [1, 2, 3, 4])
--   Eval (Foldr (+) 0 [1, 2, 3, 4]) :: Natural
--   = 10
--   
data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b)

-- | Type-level foldMap.
data FoldMap (b :: a -> Exp m) (c :: t a) (d :: m)

-- | Default implementation of FoldMap.
--   
--   
Usage
--   
--   To define an instance of FoldMap for a custom MyType
--   for which you already have an instance of Foldr:
--   
--   
--   type instance Eval (FoldMap f (xs :: MyType a)) = FoldMapDefault_ f xs
--   
--   
--   
Example
--   
--   
--   >>> :kind! FoldMapDefault_ Pure [EQ, LT, GT]
--   FoldMapDefault_ Pure [EQ, LT, GT] :: Ordering
--   = LT
--   
type FoldMapDefault_ (f :: a -> Exp k) (xs :: t a) = Eval Foldr Bicomap f Pure :: k -> k -> Type (.<>) :: k -> k -> k -> Type MEmpty :: k xs

-- | Default implementation of Foldr.
--   
--   
Usage
--   
--   To define an instance of Foldr for a custom MyType for
--   which you already have an instance of FoldMap:
--   
--   
--   type instance Eval (Foldr f y (xs :: MyType a)) = FoldrDefault_ f y xs
--   
--   
--   
Example
--   
--   
--   >>> :kind! FoldrDefault_ (.<>) EQ [EQ, LT, GT]
--   FoldrDefault_ (.<>) EQ [EQ, LT, GT] :: Ordering
--   = LT
--   
type FoldrDefault_ (f :: a -> k -> Exp k) (y :: k) (xs :: t a) = Eval UnEndo Eval FoldMap Pure1 'Endo :: k -> Exp k -> Endo k <=< Pure1 f xs y

-- | Give True if all of the booleans in the list are
--   True.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (And [True, True])
--   Eval (And [True, True]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (And [True, True, False])
--   Eval (And [True, True, False]) :: Bool
--   = False
--   
data And (a :: t Bool) (b :: Bool)

-- | Give True if any of the booleans in the list are
--   True.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Or [True, True])
--   Eval (Or [True, True]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (Or [False, False])
--   Eval (Or [False, False]) :: Bool
--   = False
--   
data Or (a :: t Bool) (b :: Bool)

-- | Whether all elements of the list satisfy a predicate.
--   
--   Note: this identifier conflicts with All (from
--   Data.Monoid).
--   
--   
Example
--   
--   
--   >>> :kind! Eval (All (Flip (<) 6) [0,1,2,3,4,5])
--   Eval (All (Flip (<) 6) [0,1,2,3,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (All (Flip (<) 5) [0,1,2,3,4,5])
--   Eval (All (Flip (<) 5) [0,1,2,3,4,5]) :: Bool
--   = False
--   
data All (b :: a -> Exp Bool) (c :: t a) (d :: Bool)

-- | Whether any element of the list satisfies a predicate.
--   
--   Note: this identifier conflicts with Any (from
--   Fcf.Utils), Any (from Data.Monoid), and
--   Any (from GHC.Exts).
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Any (Flip (<) 5) [0,1,2,3,4,5])
--   Eval (Any (Flip (<) 5) [0,1,2,3,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (Any (Flip (<) 0) [0,1,2,3,4,5])
--   Eval (Any (Flip (<) 0) [0,1,2,3,4,5]) :: Bool
--   = False
--   
data Any (b :: a -> Exp Bool) (c :: t a) (d :: Bool)

-- | Sum a Nat-list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Sum '[1,2,3])
--   Eval (Sum '[1,2,3]) :: Natural
--   = 6
--   
data Sum (a :: t Nat) (b :: Nat)

-- | Concatenate a collection of elements from a monoid.
--   
--   
Example
--   
--   For example, fold a list of lists.
--   
--   
--   Concat :: [[a]] -> Exp [a]
--   
--   
--   
--   >>> :kind! Eval (Concat ([[1,2], [3,4], [5,6]]))
--   Eval (Concat ([[1,2], [3,4], [5,6]])) :: [Natural]
--   = [1, 2, 3, 4, 5, 6]
--   
--   >>> :kind! Eval (Concat ([[Int, Maybe Int], [Maybe String, Either Double Int]]))
--   Eval (Concat ([[Int, Maybe Int], [Maybe String, Either Double Int]])) :: [*]
--   = [Int, Maybe Int, Maybe [Char], Either Double Int]
--   
data Concat (a :: t m) (b :: m)

-- | Map a function and concatenate the results.
--   
--   This is FoldMap specialized to the list monoid.
data ConcatMap (c :: a -> Exp [b]) (d :: t a) (e :: [b])

-- | 
Symbols
--   
--   Type-level strings.
--   
--   Note that the operators from this module conflict with
--   GHC.TypeLits.
--   
--   Symbol also has instances of (<>) and
--   MEmpty.
module Fcf.Data.Symbol

-- | (Kind) This is the kind of type-level symbols.
data Symbol

-- | Miscellaneous families.
module Fcf.Utils

-- | Type-level error.
data Error (b :: Symbol) (c :: a)

-- | TypeError as a fcf.
data TError (b :: ErrorMessage) (c :: a)

-- | Conjunction of a list of constraints.
data Constraints (a :: [Constraint]) b

-- | Type equality.
--   
--   
Details
--   
--   The base library also defines a similar (==); it
--   differs from TyEq in the following ways:
--   
--   
--   
- TyEq is heterogeneous: its arguments may have different
--   kinds;
--   
- TyEq is reflexive: TyEq a a always reduces to
--   True even if a is a variable.
--   
data TyEq (c :: a) (d :: b) (e :: Bool)

-- | A stuck type that can be used like a type-level undefined.
type family Stuck :: a
class IsBool (b :: Bool)
_If :: IsBool b => (b ~ 'True => r) -> (b ~ 'False => r) -> r

-- | (Limited) equivalent of \case { .. } syntax. Supports
--   matching of exact values (-->) and final matches for any
--   value (Any) or for passing value to subcomputation
--   (Else). Examples:
--   
--   
--   type BoolToNat = Case
--     [ 'True  --> 0
--     , 'False --> 1
--     ]
--   
--   type NatToBool = Case
--     [ 0 --> 'False
--     , Any   'True
--     ]
--   
--   type ZeroOneOrSucc = Case
--     [ 0  --> 0
--     , 1  --> 1
--     , Else   ((+) 1)
--     ]
--   
data Case (a :: [Match j k]) (b :: j) (c :: k)
data Match j k

-- | Match concrete type in Case.
type (-->) = 'Match_ :: j -> k -> Match j k
infix 0 -->

-- | Match on predicate being successful with type in Case.
type Is = 'Is_ :: j -> Exp Bool -> k -> Match j k

-- | Match any type in Case. Should be used as a final branch.
--   
--   Note: this identifier conflicts with Any (from
--   Fcf.Class.Foldable) Any (from Data.Monoid), and
--   Any (from GHC.Exts).
--   
--   We recommend importing this one qualified.
type Any = 'Any_ :: k -> Match j k

-- | Pass type being matched in Case to subcomputation. Should be
--   used as a final branch.
type Else = 'Else_ :: j -> Exp k -> Match j k

-- | Type-level If. If True a b ==> a; If
--   False a b ==> b
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k

-- | A compile-time assert.
--   
--   Raises the provided TypeError, whenever the condition evaluates
--   to False.
--   
--   Usage example:  type ExampleAssertionFailure = Eval ( Pure
--   '["foo", "bar"] >>= Length >>= Assert ('Text
--   Assertion) (TyEq Int Void) ) 
data Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)

-- | Compile-time assert, with condition negated.
--   
--   Raises the provided TypeError, whenever the condition evaluates
--   to True.
--   
--   Also see Assert.
data AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)

-- | A description of a custom type error.
data ErrorMessage

-- | Show the text as is.
Text :: Symbol -> ErrorMessage

-- | Pretty print the type. ShowType :: k -> ErrorMessage
ShowType :: t -> ErrorMessage

-- | Put two pieces of error message next to each other.
(:<>:) :: ErrorMessage -> ErrorMessage -> ErrorMessage

-- | Stack two pieces of error message on top of each other.
(:$$:) :: ErrorMessage -> ErrorMessage -> ErrorMessage
infixl 6 :<>:
infixl 5 :$$:

-- | The type-level equivalent of error.
--   
--   The polymorphic kind of this type allows it to be used in several
--   settings. For instance, it can be used as a constraint, e.g. to
--   provide a better error message for a non-existent instance,
--   
--   
--   -- in a context
--   instance TypeError (Text "Cannot Show functions." :$$:
--                       Text "Perhaps there is a missing argument?")
--         => Show (a -> b) where
--       showsPrec = error "unreachable"
--   
--   
--   It can also be placed on the right-hand side of a type-level function
--   to provide an error for an invalid case,
--   
--   
--   type family ByteSize x where
--      ByteSize Word16   = 2
--      ByteSize Word8    = 1
--      ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
--                                     Text " is not exportable.")
--   
type family TypeError (a :: ErrorMessage) :: b
instance Fcf.Utils.IsBool 'GHC.Types.False
instance Fcf.Utils.IsBool 'GHC.Types.True

-- | Lists.
--   
--   See also Fcf.Class.Foldable for additional functions.
module Fcf.Data.List

-- | List catenation.
--   
--   
Example
--   
--   
--   >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   >>> :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
--   Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
--   = Ex [1, 2, 3, 4]
--   
data ( (b :: [a]) ++ (c :: [a]) ) (d :: [a])
data Head (b :: [a]) (c :: Maybe a)
data Last (b :: [a]) (c :: Maybe a)
data Tail (b :: [a]) (c :: Maybe [a])

-- | Append an element to a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Cons 1 [2, 3])
--   Eval (Cons 1 [2, 3]) :: [Natural]
--   = [1, 2, 3]
--   
--   >>> :kind! Eval (Cons Int [Char, Maybe Double])
--   Eval (Cons Int [Char, Maybe Double]) :: [*]
--   = [Int, Char, Maybe Double]
--   
data Cons (b :: a) (c :: [a]) (d :: [a])

-- | Append an element to the end of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Snoc [1,2,3] 4)
--   Eval (Snoc [1,2,3] 4) :: [Natural]
--   = [1, 2, 3, 4]
--   
data Snoc (b :: [a]) (c :: a) (d :: [a])

-- | Append elements to two lists. Used in the definition of Unzip.
data Cons2 (c :: (a, b)) (d :: ([a], [b])) (e :: ([a], [b]))
data Init (b :: [a]) (c :: Maybe [a])
data Uncons (b :: [a]) (c :: Maybe (a, [a]))

-- | Decompose a list into init and last
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Unsnoc '[])
--   Eval (Unsnoc '[]) :: Maybe ([a], a)
--   = Nothing
--   
--   
--   
--   >>> :kind! Eval (Unsnoc '[1])
--   Eval (Unsnoc '[1]) :: Maybe ([Natural], Natural)
--   = Just '( '[], 1)
--   
--   
--   
--   >>> :kind! Eval (Unsnoc '[1,2,3])
--   Eval (Unsnoc '[1,2,3]) :: Maybe ([Natural], Natural)
--   = Just '([1, 2], 3)
--   
data Unsnoc (b :: [a]) (c :: Maybe ([a], a))
data Singleton (b :: a) (c :: [a])
data Null (b :: [a]) (c :: Bool)
data Length (b :: [a]) (c :: Nat)

-- | Reverse a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Reverse [1,2,3,4,5])
--   Eval (Reverse [1,2,3,4,5]) :: [Natural]
--   = [5, 4, 3, 2, 1]
--   
data Reverse (b :: [a]) (c :: [a])

-- | Intersperse a separator between elements of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Intersperse 0 [1,2,3,4])
--   Eval (Intersperse 0 [1,2,3,4]) :: [Natural]
--   = [1, 0, 2, 0, 3, 0, 4]
--   
data Intersperse (b :: a) (c :: [a]) (d :: [a])

-- | Join a list of words separated by some word.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ])
--   Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
--   = ["Lorem", ", ", "ipsum", ", ", "dolor"]
--   
data Intercalate (b :: [a]) (c :: [[a]]) (d :: [a])

-- | Right fold.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Foldr (+) 0 [1, 2, 3, 4])
--   Eval (Foldr (+) 0 [1, 2, 3, 4]) :: Natural
--   = 10
--   
data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b)

-- | This is Foldr with its argument flipped.
data UnList (c :: b) (d :: a -> b -> Exp b) (e :: [a]) (f :: b)

-- | Concatenate a collection of elements from a monoid.
--   
--   
Example
--   
--   For example, fold a list of lists.
--   
--   
--   Concat :: [[a]] -> Exp [a]
--   
--   
--   
--   >>> :kind! Eval (Concat ([[1,2], [3,4], [5,6]]))
--   Eval (Concat ([[1,2], [3,4], [5,6]])) :: [Natural]
--   = [1, 2, 3, 4, 5, 6]
--   
--   >>> :kind! Eval (Concat ([[Int, Maybe Int], [Maybe String, Either Double Int]]))
--   Eval (Concat ([[Int, Maybe Int], [Maybe String, Either Double Int]])) :: [*]
--   = [Int, Maybe Int, Maybe [Char], Either Double Int]
--   
data Concat (a :: t m) (b :: m)

-- | Map a function and concatenate the results.
--   
--   This is FoldMap specialized to the list monoid.
data ConcatMap (c :: a -> Exp [b]) (d :: t a) (e :: [b])

-- | Unfold a generator into a list.
--   
--   
Example
--   
--   
--   >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))
--   
--   >>> :{
--   type instance Eval (ToThree b) =
--     If (4 TL.<=? b)
--       Nothing
--       (Just '(b, b TL.+ 1))
--   :}
--   
--   
--   
--   >>> :kind! Eval (Unfoldr ToThree 0)
--   Eval (Unfoldr ToThree 0) :: [Natural]
--   = [0, 1, 2, 3]
--   
--   
--   See also the definition of Replicate.
data Unfoldr (c :: b -> Exp Maybe (a, b)) (d :: b) (e :: [a])

-- | Repeat the same element in a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Replicate 4 '("ok", 2))
--   Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Natural)]
--   = ['("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]
--   
data Replicate (b :: Nat) (c :: a) (d :: [a])

-- | Take a prefix of fixed length.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Take 2 [1,2,3,4,5])
--   Eval (Take 2 [1,2,3,4,5]) :: [Natural]
--   = [1, 2]
--   
data Take (b :: Nat) (c :: [a]) (d :: [a])

-- | Drop a prefix of fixed length, evaluate to the remaining suffix.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Drop 2 [1,2,3,4,5])
--   Eval (Drop 2 [1,2,3,4,5]) :: [Natural]
--   = [3, 4, 5]
--   
data Drop (b :: Nat) (c :: [a]) (d :: [a])

-- | Return a tuple where first element is xs prefix of length
--   n and second element is the remainder of the list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (SplitAt 3 '[1,2,3,4,5])
--   Eval (SplitAt 3 '[1,2,3,4,5]) :: ([Natural], [Natural])
--   = '([1, 2, 3], [4, 5])
--   
data SplitAt (b :: Nat) (c :: [a]) (d :: ([a], [a]))

-- | Take the longest prefix of elements satisfying a predicate.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5])
--   Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
--   = [1, 2, 3]
--   
data TakeWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])

-- | Drop the longest prefix of elements satisfying a predicate, evaluate
--   to the remaining suffix.
--   
--   
Example
--   
--   :kind! Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5]) Eval (DropWhile
--   ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural] = [4, 5]
data DropWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])

-- | Span, applied to a predicate p and a list xs,
--   returns a tuple: the first component is the longest prefix (possibly
--   empty) of xs whose elements satisfy p; the second
--   component is the remainder of the list.
--   
--   See also TakeWhile, DropWhile, and Break.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 3) [1,2,3,4,1,2])
--   Eval (Span (Flip (<) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
--   = '([1, 2], [3, 4, 1, 2])
--   
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 9) [1,2,3])
--   Eval (Span (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
--   = '([1, 2, 3], '[])
--   
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 0) [1,2,3])
--   Eval (Span (Flip (<) 0) [1,2,3]) :: ([Natural], [Natural])
--   = '( '[], [1, 2, 3])
--   
data Span (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))

-- | Break, applied to a predicate p and a list
--   xs, returns a tuple: the first component is the longest
--   prefix (possibly empty) of xs whose elements do not
--   satisfy p; the second component is the remainder of the
--   list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Break (Flip (>) 3) [1,2,3,4,1,2])
--   Eval (Break (Flip (>) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
--   = '([1, 2, 3], [4, 1, 2])
--   
--   
--   
--   >>> :kind! Eval (Break (Flip (<) 9) [1,2,3])
--   Eval (Break (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
--   = '( '[], [1, 2, 3])
--   
--   
--   
--   >>> :kind! Eval (Break (Flip (>) 9) [1,2,3])
--   Eval (Break (Flip (>) 9) [1,2,3]) :: ([Natural], [Natural])
--   = '([1, 2, 3], '[])
--   
data Break (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))

-- | List of suffixes of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Tails [0,1,2,3])
--   Eval (Tails [0,1,2,3]) :: [[Natural]]
--   = [[0, 1, 2, 3], [1, 2, 3], [2, 3], '[3]]
--   
data Tails (b :: [a]) (c :: [[a]])

-- | Return True when the first list is a prefix of the second.
--   
--   
Example
--   
--   
--   >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5])
--   Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5])
--   Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
--   = False
--   
--   
--   
--   >>> :kind! Eval ('[] `IsPrefixOf` [0,1,3,2,4,5])
--   Eval ('[] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval ([0,1,3,2,4,5] `IsPrefixOf` '[])
--   Eval ([0,1,3,2,4,5] `IsPrefixOf` '[]) :: Bool
--   = False
--   
data IsPrefixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return True when the first list is a suffix of the second.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5])
--   Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5])
--   Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5]) :: Bool
--   = False
--   
--   
--   
--   >>> :kind! Eval (IsSuffixOf '[] [0,1,3,2,4,5])
--   Eval (IsSuffixOf '[] [0,1,3,2,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (IsSuffixOf [0,1,3,2,4,5] '[])
--   Eval (IsSuffixOf [0,1,3,2,4,5] '[]) :: Bool
--   = False
--   
data IsSuffixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return True when the first list is contained within the
--   second.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6])
--   Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6])
--   Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6]) :: Bool
--   = False
--   
data IsInfixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return True if an element is in a list.
--   
--   See also FindIndex.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Elem 1 [1,2,3])
--   Eval (Elem 1 [1,2,3]) :: Bool
--   = True
--   
--   >>> :kind! Eval (Elem 1 [2,3])
--   Eval (Elem 1 [2,3]) :: Bool
--   = False
--   
data Elem (b :: a) (c :: [a]) (d :: Bool)

-- | Find an element associated with a key in an association list.
data Lookup (a :: k) (c :: [(k, b)]) (d :: Maybe b)

-- | Find Just the first element satisfying a predicate, or
--   evaluate to Nothing if no element satisfies the predicate.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Find (TyEq 0) [1,2,3])
--   Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural
--   = Nothing
--   
--   
--   
--   >>> :kind! Eval (Find (TyEq 0) [1,2,3,0])
--   Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural
--   = Just 0
--   
data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a)

-- | Keep all elements that satisfy a predicate, remove all that don't.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Filter ((>) 3) [1,2,3,0])
--   Eval (Filter ((>) 3) [1,2,3,0]) :: [Natural]
--   = [1, 2, 0]
--   
data Filter (b :: a -> Exp Bool) (c :: [a]) (d :: [a])

-- | Split a list into one where all elements satisfy a predicate, and a
--   second where no elements satisfy it.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Partition ((>=) 35) [20, 30, 40, 50])
--   Eval (Partition ((>=) 35) [20, 30, 40, 50]) :: ([Natural],
--                                                   [Natural])
--   = '([20, 30], [40, 50])
--   
data Partition (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))

-- | Find the index of an element satisfying the predicate.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (FindIndex ((<=) 3) [1,2,3,1,2,3])
--   Eval (FindIndex ((<=) 3) [1,2,3,1,2,3]) :: Maybe Natural
--   = Just 2
--   
--   
--   
--   >>> :kind! Eval (FindIndex ((>) 0) [1,2,3,1,2,3])
--   Eval (FindIndex ((>) 0) [1,2,3,1,2,3]) :: Maybe Natural
--   = Nothing
--   
data FindIndex (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe Nat)

-- | Modify an element at a given index.
--   
--   The list is unchanged if the index is out of bounds.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (SetIndex 2 7 [1,2,3])
--   Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
--   = [1, 2, 7]
--   
data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])

-- | Combine elements of two lists pairwise.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (ZipWith (+) [1,2,3] [1,1,1])
--   Eval (ZipWith (+) [1,2,3] [1,1,1]) :: [Natural]
--   = [2, 3, 4]
--   
data ZipWith (d :: a -> b -> Exp c) (e :: [a]) (f :: [b]) (g :: [c])
data Zip (c :: [a]) (d :: [b]) (e :: [(a, b)])
data Unzip (c :: Exp [(a, b)]) (d :: ([a], [b]))

-- | Equality and ordering.
--   
--   Note that equality doesn't really require a class, it can be defined
--   uniformly as TyEq.
module Fcf.Class.Ord

-- | Type-level compare for totally ordered data types.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Compare "a" "b")
--   Eval (Compare "a" "b") :: Ordering
--   = LT
--   
--   
--   
--   >>> :kind! Eval (Compare '[1, 2, 3] '[1, 2, 3])
--   Eval (Compare '[1, 2, 3] '[1, 2, 3]) :: Ordering
--   = EQ
--   
--   
--   
--   >>> :kind! Eval (Compare '[1, 3] '[1, 2])
--   Eval (Compare '[1, 3] '[1, 2]) :: Ordering
--   = GT
--   
data Compare (b :: a) (c :: a) (d :: Ordering)

-- | "Smaller than or equal to". Type-level version of
--   (<=).
--   
--   
Example
--   
--   
--   >>> :kind! Eval ("b" <= "a")
--   Eval ("b" <= "a") :: Bool
--   = False
--   
data ( (b :: a) <= (c :: a) ) (d :: Bool)

-- | "Greater than or equal to". Type-level version of
--   (>=).
--   
--   
Example
--   
--   
--   >>> :kind! Eval ("b" >= "a")
--   Eval ("b" >= "a") :: Bool
--   = True
--   
data ( (b :: a) >= (c :: a) ) (d :: Bool)

-- | "Smaller than". Type-level version of (<).
--   
--   
Example
--   
--   
--   >>> :kind! Eval ("a" < "b")
--   Eval ("a" < "b") :: Bool
--   = True
--   
data ( (b :: a) < (c :: a) ) (d :: Bool)

-- | "Greater than". Type-level version of (>).
--   
--   
Example
--   
--   
--   >>> :kind! Eval ("b" > "a")
--   Eval ("b" > "a") :: Bool
--   = True
--   
data ( (b :: a) > (c :: a) ) (d :: Bool)

-- | Type equality.
--   
--   
Details
--   
--   The base library also defines a similar (==); it
--   differs from TyEq in the following ways:
--   
--   
--   
- TyEq is heterogeneous: its arguments may have different
--   kinds;
--   
- TyEq is reflexive: TyEq a a always reduces to
--   True even if a is a variable.
--   
data TyEq (c :: a) (d :: b) (e :: Bool)

-- | First-class type families
--   
--   For example, here is a regular type family:
--   
--   
--   type family   FromMaybe (a :: k) (m :: Maybe k) :: k
--   type instance FromMaybe a 'Nothing  = a
--   type instance FromMaybe a ('Just b) = b
--   
--   
--   With Fcf, it translates to a data declaration:
--   
--   
--   data FromMaybe :: k -> Maybe k -> Exp k
--   type instance Eval (FromMaybe a 'Nothing)  = a
--   type instance Eval (FromMaybe a ('Just b)) = b
--   
--   
--   
--   
- Fcfs can be higher-order.
--   
- The kind constructor Exp is a monad: there's
--   (=<<) and Pure.
--   
--   
--   Essential language extensions for Fcf:
--   
--   
--   {-# LANGUAGE
--       DataKinds,
--       PolyKinds,
--       TypeFamilies,
--       TypeOperators,
--       UndecidableInstances #-}
--   
module Fcf

-- | Kind of type-level expressions indexed by their result type.
type Exp a = a -> Type

-- | Expression evaluator.
type family Eval (e :: Exp a) :: a

-- | Apply and evaluate a unary type function.
type (f :: k1 -> Exp k) @@ (x :: k1) = Eval f x
data Pure (b :: a) (c :: a)
data Pure1 (c :: a -> b) (d :: a) (e :: b)
data Pure2 (d :: a -> b -> c) (e :: a) (f :: b) (g :: c)
data Pure3 (e :: a -> b -> c -> d) (f :: a) (g :: b) (h :: c) (i :: d)
data Pure4 (f :: a -> b -> c -> d -> e) (g :: a) (h :: b) (i :: c) (j :: d) (k :: e)
data Pure5 (g :: a -> b -> c -> d -> e -> f) (h :: a) (i :: b) (j :: c) (k :: d) (l :: e) (m :: f)
data Pure6 (h :: a -> b -> c -> d -> e -> f -> g) (i :: a) (j :: b) (k :: c) (l :: d) (m :: e) (n :: f) (o :: g)
data Pure7 (i :: a -> b -> c -> d -> e -> f -> g -> h) (j :: a) (k :: b) (l :: c) (m :: d) (n :: e) (o :: f) (p :: g) (q :: h)
data Pure8 (j :: a -> b -> c -> d -> e -> f -> g -> h -> i) (k :: a) (l :: b) (m :: c) (n :: d) (o :: e) (p :: f) (q :: g) (r :: h) (s :: i)
data Pure9 (k :: a -> b -> c -> d -> e -> f -> g -> h -> i -> j) (l :: a) (m :: b) (n :: c) (o :: d) (p :: e) (q :: f) (r :: g) (s :: h) (t :: i) (u :: j)
data ( (c :: a -> Exp b) =<< (d :: Exp a) ) (e :: b)
infixr 1 =<<
data ( (c :: Exp a) >>= (d :: a -> Exp b) ) (e :: b)
infixl 1 >>=
data ( (d :: b -> Exp c) <=< (e :: a -> Exp b) ) (f :: a) (g :: c)
infixr 1 <=<
type LiftM = (=<<) :: a -> Exp b -> Exp a -> b -> Type
data LiftM2 (d :: a -> b -> Exp c) (e :: Exp a) (f :: Exp b) (g :: c)
data LiftM3 (e :: a -> b -> c -> Exp d) (f :: Exp a) (g :: Exp b) (h :: Exp c) (i :: d)
data Join (b :: Exp Exp a) (c :: a)
data ( (c :: a -> b) <$> (d :: Exp a) ) (e :: b)
infixl 4 <$>
data ( (c :: Exp a -> b) <*> (d :: Exp a) ) (e :: b)
infixl 4 <*>
data Flip (d :: a -> b -> Exp c) (e :: b) (f :: a) (g :: c)
data ConstFn (c :: a) (d :: b) (e :: a)

-- | Note that this denotes the identity function, so ($) f can
--   usually be replaced with f.
data ( (c :: a -> Exp b) $ (d :: a) ) (e :: b)
infixr 0 $
data Uncurry (d :: a -> b -> Exp c) (e :: (a, b)) (f :: c)
data Fst (c :: (a, b)) (d :: a)
data Snd (c :: (a, b)) (d :: b)

-- | Specialization of Bimap for pairs.
data ( (a :: b -> Exp c) *** (d :: b' -> Exp c') ) (e :: (b, b')) (f :: (c, c'))
infixr 3 ***
data UnEither (d :: a -> Exp c) (e :: b -> Exp c) (f :: Either a b) (g :: c)
data IsLeft (c :: Either a b) (d :: Bool)
data IsRight (c :: Either a b) (d :: Bool)
data UnMaybe (c :: Exp b) (d :: a -> Exp b) (e :: Maybe a) (f :: b)
data FromMaybe (a :: k) (b :: Maybe k) (c :: k)
data IsNothing (b :: Maybe a) (c :: Bool)
data IsJust (b :: Maybe a) (c :: Bool)

-- | List catenation.
--   
--   
Example
--   
--   
--   >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   >>> :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
--   Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
--   = Ex [1, 2, 3, 4]
--   
data ( (b :: [a]) ++ (c :: [a]) ) (d :: [a])
data Head (b :: [a]) (c :: Maybe a)
data Last (b :: [a]) (c :: Maybe a)
data Tail (b :: [a]) (c :: Maybe [a])

-- | Append an element to a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Cons 1 [2, 3])
--   Eval (Cons 1 [2, 3]) :: [Natural]
--   = [1, 2, 3]
--   
--   >>> :kind! Eval (Cons Int [Char, Maybe Double])
--   Eval (Cons Int [Char, Maybe Double]) :: [*]
--   = [Int, Char, Maybe Double]
--   
data Cons (b :: a) (c :: [a]) (d :: [a])

-- | Append an element to the end of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Snoc [1,2,3] 4)
--   Eval (Snoc [1,2,3] 4) :: [Natural]
--   = [1, 2, 3, 4]
--   
data Snoc (b :: [a]) (c :: a) (d :: [a])

-- | Append elements to two lists. Used in the definition of Unzip.
data Cons2 (c :: (a, b)) (d :: ([a], [b])) (e :: ([a], [b]))
data Init (b :: [a]) (c :: Maybe [a])
data Uncons (b :: [a]) (c :: Maybe (a, [a]))

-- | Decompose a list into init and last
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Unsnoc '[])
--   Eval (Unsnoc '[]) :: Maybe ([a], a)
--   = Nothing
--   
--   
--   
--   >>> :kind! Eval (Unsnoc '[1])
--   Eval (Unsnoc '[1]) :: Maybe ([Natural], Natural)
--   = Just '( '[], 1)
--   
--   
--   
--   >>> :kind! Eval (Unsnoc '[1,2,3])
--   Eval (Unsnoc '[1,2,3]) :: Maybe ([Natural], Natural)
--   = Just '([1, 2], 3)
--   
data Unsnoc (b :: [a]) (c :: Maybe ([a], a))
data Singleton (b :: a) (c :: [a])
data Null (b :: [a]) (c :: Bool)
data Length (b :: [a]) (c :: Nat)

-- | Reverse a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Reverse [1,2,3,4,5])
--   Eval (Reverse [1,2,3,4,5]) :: [Natural]
--   = [5, 4, 3, 2, 1]
--   
data Reverse (b :: [a]) (c :: [a])

-- | Intersperse a separator between elements of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Intersperse 0 [1,2,3,4])
--   Eval (Intersperse 0 [1,2,3,4]) :: [Natural]
--   = [1, 0, 2, 0, 3, 0, 4]
--   
data Intersperse (b :: a) (c :: [a]) (d :: [a])

-- | Join a list of words separated by some word.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ])
--   Eval (Intercalate '[", "] [ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
--   = ["Lorem", ", ", "ipsum", ", ", "dolor"]
--   
data Intercalate (b :: [a]) (c :: [[a]]) (d :: [a])

-- | Right fold.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Foldr (+) 0 [1, 2, 3, 4])
--   Eval (Foldr (+) 0 [1, 2, 3, 4]) :: Natural
--   = 10
--   
data Foldr (c :: a -> b -> Exp b) (d :: b) (e :: t a) (f :: b)

-- | This is Foldr with its argument flipped.
data UnList (c :: b) (d :: a -> b -> Exp b) (e :: [a]) (f :: b)

-- | Concatenate a collection of elements from a monoid.
--   
--   
Example
--   
--   For example, fold a list of lists.
--   
--   
--   Concat :: [[a]] -> Exp [a]
--   
--   
--   
--   >>> :kind! Eval (Concat ([[1,2], [3,4], [5,6]]))
--   Eval (Concat ([[1,2], [3,4], [5,6]])) :: [Natural]
--   = [1, 2, 3, 4, 5, 6]
--   
--   >>> :kind! Eval (Concat ([[Int, Maybe Int], [Maybe String, Either Double Int]]))
--   Eval (Concat ([[Int, Maybe Int], [Maybe String, Either Double Int]])) :: [*]
--   = [Int, Maybe Int, Maybe [Char], Either Double Int]
--   
data Concat (a :: t m) (b :: m)

-- | Map a function and concatenate the results.
--   
--   This is FoldMap specialized to the list monoid.
data ConcatMap (c :: a -> Exp [b]) (d :: t a) (e :: [b])

-- | Unfold a generator into a list.
--   
--   
Example
--   
--   
--   >>> data ToThree :: Nat -> Exp (Maybe (Nat, Nat))
--   
--   >>> :{
--   type instance Eval (ToThree b) =
--     If (4 TL.<=? b)
--       Nothing
--       (Just '(b, b TL.+ 1))
--   :}
--   
--   
--   
--   >>> :kind! Eval (Unfoldr ToThree 0)
--   Eval (Unfoldr ToThree 0) :: [Natural]
--   = [0, 1, 2, 3]
--   
--   
--   See also the definition of Replicate.
data Unfoldr (c :: b -> Exp Maybe (a, b)) (d :: b) (e :: [a])

-- | Repeat the same element in a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Replicate 4 '("ok", 2))
--   Eval (Replicate 4 '("ok", 2)) :: [(TL.Symbol, Natural)]
--   = ['("ok", 2), '("ok", 2), '("ok", 2), '("ok", 2)]
--   
data Replicate (b :: Nat) (c :: a) (d :: [a])

-- | Take a prefix of fixed length.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Take 2 [1,2,3,4,5])
--   Eval (Take 2 [1,2,3,4,5]) :: [Natural]
--   = [1, 2]
--   
data Take (b :: Nat) (c :: [a]) (d :: [a])

-- | Drop a prefix of fixed length, evaluate to the remaining suffix.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Drop 2 [1,2,3,4,5])
--   Eval (Drop 2 [1,2,3,4,5]) :: [Natural]
--   = [3, 4, 5]
--   
data Drop (b :: Nat) (c :: [a]) (d :: [a])

-- | Return a tuple where first element is xs prefix of length
--   n and second element is the remainder of the list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (SplitAt 3 '[1,2,3,4,5])
--   Eval (SplitAt 3 '[1,2,3,4,5]) :: ([Natural], [Natural])
--   = '([1, 2, 3], [4, 5])
--   
data SplitAt (b :: Nat) (c :: [a]) (d :: ([a], [a]))

-- | Take the longest prefix of elements satisfying a predicate.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5])
--   Eval (TakeWhile ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural]
--   = [1, 2, 3]
--   
data TakeWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])

-- | Drop the longest prefix of elements satisfying a predicate, evaluate
--   to the remaining suffix.
--   
--   
Example
--   
--   :kind! Eval (DropWhile ((>=) 3) [1, 2, 3, 4, 5]) Eval (DropWhile
--   ((>=) 3) [1, 2, 3, 4, 5]) :: [Natural] = [4, 5]
data DropWhile (b :: a -> Exp Bool) (c :: [a]) (d :: [a])

-- | Span, applied to a predicate p and a list xs,
--   returns a tuple: the first component is the longest prefix (possibly
--   empty) of xs whose elements satisfy p; the second
--   component is the remainder of the list.
--   
--   See also TakeWhile, DropWhile, and Break.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 3) [1,2,3,4,1,2])
--   Eval (Span (Flip (<) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
--   = '([1, 2], [3, 4, 1, 2])
--   
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 9) [1,2,3])
--   Eval (Span (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
--   = '([1, 2, 3], '[])
--   
--   
--   
--   >>> :kind! Eval (Span (Flip (<) 0) [1,2,3])
--   Eval (Span (Flip (<) 0) [1,2,3]) :: ([Natural], [Natural])
--   = '( '[], [1, 2, 3])
--   
data Span (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))

-- | Break, applied to a predicate p and a list
--   xs, returns a tuple: the first component is the longest
--   prefix (possibly empty) of xs whose elements do not
--   satisfy p; the second component is the remainder of the
--   list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Break (Flip (>) 3) [1,2,3,4,1,2])
--   Eval (Break (Flip (>) 3) [1,2,3,4,1,2]) :: ([Natural], [Natural])
--   = '([1, 2, 3], [4, 1, 2])
--   
--   
--   
--   >>> :kind! Eval (Break (Flip (<) 9) [1,2,3])
--   Eval (Break (Flip (<) 9) [1,2,3]) :: ([Natural], [Natural])
--   = '( '[], [1, 2, 3])
--   
--   
--   
--   >>> :kind! Eval (Break (Flip (>) 9) [1,2,3])
--   Eval (Break (Flip (>) 9) [1,2,3]) :: ([Natural], [Natural])
--   = '([1, 2, 3], '[])
--   
data Break (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))

-- | List of suffixes of a list.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Tails [0,1,2,3])
--   Eval (Tails [0,1,2,3]) :: [[Natural]]
--   = [[0, 1, 2, 3], [1, 2, 3], [2, 3], '[3]]
--   
data Tails (b :: [a]) (c :: [[a]])

-- | Return True when the first list is a prefix of the second.
--   
--   
Example
--   
--   
--   >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5])
--   Eval ([0,1,2] `IsPrefixOf` [0,1,2,3,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5])
--   Eval ([0,1,2] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
--   = False
--   
--   
--   
--   >>> :kind! Eval ('[] `IsPrefixOf` [0,1,3,2,4,5])
--   Eval ('[] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval ([0,1,3,2,4,5] `IsPrefixOf` '[])
--   Eval ([0,1,3,2,4,5] `IsPrefixOf` '[]) :: Bool
--   = False
--   
data IsPrefixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return True when the first list is a suffix of the second.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5])
--   Eval (IsSuffixOf [3,4,5] [0,1,2,3,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5])
--   Eval (IsSuffixOf [3,4,5] [0,1,3,2,4,5]) :: Bool
--   = False
--   
--   
--   
--   >>> :kind! Eval (IsSuffixOf '[] [0,1,3,2,4,5])
--   Eval (IsSuffixOf '[] [0,1,3,2,4,5]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (IsSuffixOf [0,1,3,2,4,5] '[])
--   Eval (IsSuffixOf [0,1,3,2,4,5] '[]) :: Bool
--   = False
--   
data IsSuffixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return True when the first list is contained within the
--   second.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6])
--   Eval (IsInfixOf [2,3,4] [0,1,2,3,4,5,6]) :: Bool
--   = True
--   
--   
--   
--   >>> :kind! Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6])
--   Eval (IsInfixOf [2,4,4] [0,1,2,3,4,5,6]) :: Bool
--   = False
--   
data IsInfixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return True if an element is in a list.
--   
--   See also FindIndex.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Elem 1 [1,2,3])
--   Eval (Elem 1 [1,2,3]) :: Bool
--   = True
--   
--   >>> :kind! Eval (Elem 1 [2,3])
--   Eval (Elem 1 [2,3]) :: Bool
--   = False
--   
data Elem (b :: a) (c :: [a]) (d :: Bool)

-- | Find an element associated with a key in an association list.
data Lookup (a :: k) (c :: [(k, b)]) (d :: Maybe b)

-- | Find Just the first element satisfying a predicate, or
--   evaluate to Nothing if no element satisfies the predicate.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Find (TyEq 0) [1,2,3])
--   Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural
--   = Nothing
--   
--   
--   
--   >>> :kind! Eval (Find (TyEq 0) [1,2,3,0])
--   Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural
--   = Just 0
--   
data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a)

-- | Keep all elements that satisfy a predicate, remove all that don't.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Filter ((>) 3) [1,2,3,0])
--   Eval (Filter ((>) 3) [1,2,3,0]) :: [Natural]
--   = [1, 2, 0]
--   
data Filter (b :: a -> Exp Bool) (c :: [a]) (d :: [a])

-- | Split a list into one where all elements satisfy a predicate, and a
--   second where no elements satisfy it.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (Partition ((>=) 35) [20, 30, 40, 50])
--   Eval (Partition ((>=) 35) [20, 30, 40, 50]) :: ([Natural],
--                                                   [Natural])
--   = '([20, 30], [40, 50])
--   
data Partition (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))

-- | Find the index of an element satisfying the predicate.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (FindIndex ((<=) 3) [1,2,3,1,2,3])
--   Eval (FindIndex ((<=) 3) [1,2,3,1,2,3]) :: Maybe Natural
--   = Just 2
--   
--   
--   
--   >>> :kind! Eval (FindIndex ((>) 0) [1,2,3,1,2,3])
--   Eval (FindIndex ((>) 0) [1,2,3,1,2,3]) :: Maybe Natural
--   = Nothing
--   
data FindIndex (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe Nat)

-- | Modify an element at a given index.
--   
--   The list is unchanged if the index is out of bounds.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (SetIndex 2 7 [1,2,3])
--   Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
--   = [1, 2, 7]
--   
data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])

-- | Combine elements of two lists pairwise.
--   
--   
Example
--   
--   
--   >>> :kind! Eval (ZipWith (+) [1,2,3] [1,1,1])
--   Eval (ZipWith (+) [1,2,3] [1,1,1]) :: [Natural]
--   = [2, 3, 4]
--   
data ZipWith (d :: a -> b -> Exp c) (e :: [a]) (f :: [b]) (g :: [c])
data Zip (c :: [a]) (d :: [b]) (e :: [(a, b)])
data Unzip (c :: Exp [(a, b)]) (d :: ([a], [b]))

-- | N.B.: The order of the two branches is the opposite of "if":
--   UnBool ifFalse ifTrue bool.
--   
--   This mirrors the default order of constructors:
--   
--   
--   data Bool = False | True
--   ----------- False < True
--   
data UnBool (b :: Exp a) (c :: Exp a) (d :: Bool) (e :: a)
data ( (a :: Bool) || (b :: Bool) ) (c :: Bool)
infixr 2 ||
data ( (a :: Bool) && (b :: Bool) ) (c :: Bool)
infixr 3 &&
data Not (a :: Bool) (b :: Bool)

-- | (Limited) equivalent of \case { .. } syntax. Supports
--   matching of exact values (-->) and final matches for any
--   value (Any) or for passing value to subcomputation
--   (Else). Examples:
--   
--   
--   type BoolToNat = Case
--     [ 'True  --> 0
--     , 'False --> 1
--     ]
--   
--   type NatToBool = Case
--     [ 0 --> 'False
--     , Any   'True
--     ]
--   
--   type ZeroOneOrSucc = Case
--     [ 0  --> 0
--     , 1  --> 1
--     , Else   ((+) 1)
--     ]
--   
data Case (a :: [Match j k]) (b :: j) (c :: k)
data Match j k

-- | Match concrete type in Case.
type (-->) = 'Match_ :: j -> k -> Match j k
infix 0 -->

-- | Match on predicate being successful with type in Case.
type Is = 'Is_ :: j -> Exp Bool -> k -> Match j k

-- | Match any type in Case. Should be used as a final branch.
--   
--   Note: this identifier conflicts with Any (from
--   Fcf.Class.Foldable) Any (from Data.Monoid), and
--   Any (from GHC.Exts).
--   
--   We recommend importing this one qualified.
type Any = 'Any_ :: k -> Match j k

-- | Pass type being matched in Case to subcomputation. Should be
--   used as a final branch.
type Else = 'Else_ :: j -> Exp k -> Match j k
data ( (a :: Nat) + (b :: Nat) ) (c :: Nat)
data ( (a :: Nat) - (b :: Nat) ) (c :: Nat)
data ( (a :: Nat) * (b :: Nat) ) (c :: Nat)
data ( (a :: Nat) ^ (b :: Nat) ) (c :: Nat)
data ( (a :: Nat) <= (b :: Nat) ) (c :: Bool)
data ( (a :: Nat) >= (b :: Nat) ) (c :: Bool)
data ( (a :: Nat) < (b :: Nat) ) (c :: Bool)
data ( (a :: Nat) > (b :: Nat) ) (c :: Bool)

-- | Type-level fmap for type-level functors.
--   
--   Note: this name clashes with Map from containers.
--   FMap is provided as a synonym to avoid this.
--   
--   
Example
--   
--   
--   >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   >>> data AddMul :: Nat -> Nat -> Exp Nat
--   
--   >>> type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   >>> :kind! Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat])
--   Ex (Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]) :: Example
--   = Ex [4, 9, 16, 25, 36]
--   
data Map (c :: a -> Exp b) (d :: f a) (e :: f b)

-- | Type-level bimap.
--   
--   
Example
--   
--   
--   >>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   >>> :kind! Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural))
--   Ex (Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Natural, Natural)) :: Example
--   = Ex '(3, 3)
--   
data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')

-- | Type-level error.
data Error (b :: Symbol) (c :: a)

-- | Conjunction of a list of constraints.
data Constraints (a :: [Constraint]) b

-- | Type equality.
--   
--   
Details
--   
--   The base library also defines a similar (==); it
--   differs from TyEq in the following ways:
--   
--   
--   
- TyEq is heterogeneous: its arguments may have different
--   kinds;
--   
- TyEq is reflexive: TyEq a a always reduces to
--   True even if a is a variable.
--   
data TyEq (c :: a) (d :: b) (e :: Bool)

-- | A stuck type that can be used like a type-level undefined.
type family Stuck :: a
class IsBool (b :: Bool)
_If :: IsBool b => (b ~ 'True => r) -> (b ~ 'False => r) -> r

-- | Type-level If. If True a b ==> a; If
--   False a b ==> b
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k

-- | A compile-time assert.
--   
--   Raises the provided TypeError, whenever the condition evaluates
--   to False.
--   
--   Usage example:  type ExampleAssertionFailure = Eval ( Pure
--   '["foo", "bar"] >>= Length >>= Assert ('Text
--   Assertion) (TyEq Int Void) ) 
data Assert (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)

-- | Compile-time assert, with condition negated.
--   
--   Raises the provided TypeError, whenever the condition evaluates
--   to True.
--   
--   Also see Assert.
data AssertNot (a :: ErrorMessage) (b :: Exp Bool) (c :: r) (d :: r)
