-- 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 <a>Eval</a> 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 <a>Fcf.Data.Function</a> 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 <tt>($) f</tt> can
--   usually be replaced with <tt>f</tt>.
data ( (c :: a -> Exp b) $ (d :: a) ) (e :: b)
infixr 0 $


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

-- | Type-level semigroup composition <tt>(<a>&lt;&gt;</a>)</tt>.
type family (x :: a) <> (y :: a) :: a

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

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

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


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

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

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

module Fcf.Class.Functor

-- | Type-level <a>fmap</a> for type-level functors.
--   
--   Note: this name clashes with <a>Map</a> from <i>containers</i>.
--   <a>FMap</a> is provided as a synonym to avoid this.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; data Example where Ex :: a -&gt; Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   &gt;&gt;&gt; data AddMul :: Nat -&gt; Nat -&gt; Exp Nat
--   
--   &gt;&gt;&gt; type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Map (c :: a -> Exp b) (d :: f a) (e :: f b)

-- | Synonym of <a>Map</a> 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 <a>Data.Bifunctor</a>.
module Fcf.Class.Bifunctor

-- | Type-level <a>bimap</a>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; data Example where Ex :: a -&gt; Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   &gt;&gt;&gt; :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)
--   </pre>
data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')

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

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


-- | Overloaded functions.

-- | <i>Deprecated: Use Fcf.Class.Functor or Fcf.Class.Bifunctor
--   instead.</i>
module Fcf.Classes

-- | Type-level <a>fmap</a> for type-level functors.
--   
--   Note: this name clashes with <a>Map</a> from <i>containers</i>.
--   <a>FMap</a> is provided as a synonym to avoid this.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; data Example where Ex :: a -&gt; Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   &gt;&gt;&gt; data AddMul :: Nat -&gt; Nat -&gt; Exp Nat
--   
--   &gt;&gt;&gt; type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Map (c :: a -> Exp b) (d :: f a) (e :: f b)

-- | Type-level <a>bimap</a>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; data Example where Ex :: a -&gt; Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   &gt;&gt;&gt; :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)
--   </pre>
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
--   <a>Data.Type.Bool</a>.
module Fcf.Data.Bool

-- | N.B.: The order of the two branches is the opposite of "if":
--   <tt>UnBool ifFalse ifTrue bool</tt>.
--   
--   This mirrors the default order of constructors:
--   
--   <pre>
--   data Bool = False | True
--   ----------- False &lt; True
--   </pre>
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, <a>Either</a>, <a>Maybe</a>.
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 <a>Bimap</a> 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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ('(True, Nothing) &amp; Fst)
--   Eval ('(True, Nothing) &amp; Fst) :: Bool
--   = True
--   </pre>
data ( (c :: a) & (d :: a -> Exp b) ) (e :: b)
infixl 1 &

-- | Lift a binary function to the domain of a projection.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (((&amp;&amp;) `On` Fst) '(True, Nothing) '(False, Just '()))
--   Eval (((&amp;&amp;) `On` Fst) '(True, Nothing) '(False, Just '())) :: Bool
--   = False
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Bicomap Fst Pure (||) '(False, Nothing) True)
--   Eval (Bicomap Fst Pure (||) '(False, Nothing) True) :: Bool
--   = True
--   </pre>
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
--   <a>GHC.TypeLits</a> and <a>GHC.TypeNats</a>.
module Fcf.Data.Nat

-- | A type synonym for <a>Natural</a>.
--   
--   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
--   <a>FoldMap</a> or <a>Foldr</a>, but a default still needs to be given
--   explicitly for the other.
--   
--   <pre>
--   data MyType a = ... {- Some custom Foldable type -}
--   
--   -- Method 1: Implement Foldr, default FoldMap.
--   type instance <a>Eval</a> (<a>Foldr</a> f y xs) = ... {- Explicit implementation -}
--   type instance <a>Eval</a> (<a>FoldMap</a> f xs) = <a>FoldMapDefault_</a> f xs {- Default -}
--   
--   -- Method 2: Implement FoldMap, default Foldr.
--   type instance <a>Eval</a> (<a>FoldMap</a> f xs) = ... {- Explicit implementation -}
--   type instance <a>Eval</a> (<a>Foldr</a> f y xs) = <a>FoldrDefault_</a> f y xs {- Default -}
--   </pre>
module Fcf.Class.Foldable

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

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

-- | Default implementation of <a>FoldMap</a>.
--   
--   <h3><b>Usage</b></h3>
--   
--   To define an instance of <a>FoldMap</a> for a custom <tt>MyType</tt>
--   for which you already have an instance of <a>Foldr</a>:
--   
--   <pre>
--   type instance <a>Eval</a> (<a>FoldMap</a> f (xs :: MyType a)) = <a>FoldMapDefault_</a> f xs
--   </pre>
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! FoldMapDefault_ Pure [EQ, LT, GT]
--   FoldMapDefault_ Pure [EQ, LT, GT] :: Ordering
--   = LT
--   </pre>
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 <a>Foldr</a>.
--   
--   <h3><b>Usage</b></h3>
--   
--   To define an instance of <a>Foldr</a> for a custom <tt>MyType</tt> for
--   which you already have an instance of <a>FoldMap</a>:
--   
--   <pre>
--   type instance <a>Eval</a> (<a>Foldr</a> f y (xs :: MyType a)) = <a>FoldrDefault_</a> f y xs
--   </pre>
--   
--   <h4><b>Example</b></h4>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! FoldrDefault_ (.&lt;&gt;) EQ [EQ, LT, GT]
--   FoldrDefault_ (.&lt;&gt;) EQ [EQ, LT, GT] :: Ordering
--   = LT
--   </pre>
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 <tt>True</tt> if all of the booleans in the list are
--   <tt>True</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (And [True, True])
--   Eval (And [True, True]) :: Bool
--   = True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (And [True, True, False])
--   Eval (And [True, True, False]) :: Bool
--   = False
--   </pre>
data And (a :: t Bool) (b :: Bool)

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

-- | Whether all elements of the list satisfy a predicate.
--   
--   Note: this identifier conflicts with <a>All</a> (from
--   <a>Data.Monoid</a>).
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (All (Flip (&lt;) 6) [0,1,2,3,4,5])
--   Eval (All (Flip (&lt;) 6) [0,1,2,3,4,5]) :: Bool
--   = True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (All (Flip (&lt;) 5) [0,1,2,3,4,5])
--   Eval (All (Flip (&lt;) 5) [0,1,2,3,4,5]) :: Bool
--   = False
--   </pre>
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 <a>Any</a> (from
--   <a>Fcf.Utils</a>), <a>Any</a> (from <a>Data.Monoid</a>), and
--   <a>Any</a> (from <a>GHC.Exts</a>).
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Any (Flip (&lt;) 5) [0,1,2,3,4,5])
--   Eval (Any (Flip (&lt;) 5) [0,1,2,3,4,5]) :: Bool
--   = True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Any (Flip (&lt;) 0) [0,1,2,3,4,5])
--   Eval (Any (Flip (&lt;) 0) [0,1,2,3,4,5]) :: Bool
--   = False
--   </pre>
data Any (b :: a -> Exp Bool) (c :: t a) (d :: Bool)

-- | Sum a <tt>Nat</tt>-list.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Sum '[1,2,3])
--   Eval (Sum '[1,2,3]) :: Natural
--   = 6
--   </pre>
data Sum (a :: t Nat) (b :: Nat)

-- | Concatenate a collection of elements from a monoid.
--   
--   <h3><b>Example</b></h3>
--   
--   For example, fold a list of lists.
--   
--   <pre>
--   Concat :: [[a]] -&gt; Exp [a]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Concat ([[1,2], [3,4], [5,6]]))
--   Eval (Concat ([[1,2], [3,4], [5,6]])) :: [Natural]
--   = [1, 2, 3, 4, 5, 6]
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Concat (a :: t m) (b :: m)

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


-- | <h1>Symbols</h1>
--   
--   Type-level strings.
--   
--   Note that the operators from this module conflict with
--   <a>GHC.TypeLits</a>.
--   
--   <a>Symbol</a> also has instances of <tt>(<a>&lt;&gt;</a>)</tt> and
--   <a>MEmpty</a>.
module Fcf.Data.Symbol

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


-- | Miscellaneous families.
module Fcf.Utils

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

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

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

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

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

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

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

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

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

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

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

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

-- | Compile-time assert, with condition negated.
--   
--   Raises the provided <a>TypeError</a>, whenever the condition evaluates
--   to <a>True</a>.
--   
--   Also see <a>Assert</a>.
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. <tt>ShowType :: k -&gt; ErrorMessage</tt>
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 <a>error</a>.
--   
--   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,
--   
--   <pre>
--   -- in a context
--   instance TypeError (Text "Cannot <tt>Show</tt> functions." :$$:
--                       Text "Perhaps there is a missing argument?")
--         =&gt; Show (a -&gt; b) where
--       showsPrec = error "unreachable"
--   </pre>
--   
--   It can also be placed on the right-hand side of a type-level function
--   to provide an error for an invalid case,
--   
--   <pre>
--   type family ByteSize x where
--      ByteSize Word16   = 2
--      ByteSize Word8    = 1
--      ByteSize a        = TypeError (Text "The type " :&lt;&gt;: ShowType a :&lt;&gt;:
--                                     Text " is not exportable.")
--   </pre>
type family TypeError (a :: ErrorMessage) :: b
instance Fcf.Utils.IsBool 'GHC.Types.False
instance Fcf.Utils.IsBool 'GHC.Types.True


-- | Lists.
--   
--   See also <a>Fcf.Class.Foldable</a> for additional functions.
module Fcf.Data.List

-- | List catenation.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; data Example where Ex :: a -&gt; Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   &gt;&gt;&gt; :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
--   Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
--   = Ex [1, 2, 3, 4]
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Cons 1 [2, 3])
--   Eval (Cons 1 [2, 3]) :: [Natural]
--   = [1, 2, 3]
--   
--   &gt;&gt;&gt; :kind! Eval (Cons Int [Char, Maybe Double])
--   Eval (Cons Int [Char, Maybe Double]) :: [*]
--   = [Int, Char, Maybe Double]
--   </pre>
data Cons (b :: a) (c :: [a]) (d :: [a])

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

-- | Append elements to two lists. Used in the definition of <a>Unzip</a>.
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 <a>init</a> and <a>last</a>
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Unsnoc '[])
--   Eval (Unsnoc '[]) :: Maybe ([a], a)
--   = Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Unsnoc '[1])
--   Eval (Unsnoc '[1]) :: Maybe ([Natural], Natural)
--   = Just '( '[], 1)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Unsnoc '[1,2,3])
--   Eval (Unsnoc '[1,2,3]) :: Maybe ([Natural], Natural)
--   = Just '([1, 2], 3)
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Reverse [1,2,3,4,5])
--   Eval (Reverse [1,2,3,4,5]) :: [Natural]
--   = [5, 4, 3, 2, 1]
--   </pre>
data Reverse (b :: [a]) (c :: [a])

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

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

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

-- | This is <a>Foldr</a> 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.
--   
--   <h3><b>Example</b></h3>
--   
--   For example, fold a list of lists.
--   
--   <pre>
--   Concat :: [[a]] -&gt; Exp [a]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Concat ([[1,2], [3,4], [5,6]]))
--   Eval (Concat ([[1,2], [3,4], [5,6]])) :: [Natural]
--   = [1, 2, 3, 4, 5, 6]
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Concat (a :: t m) (b :: m)

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

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

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

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

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

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

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

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

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

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

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

-- | Return <tt>True</tt> when the first list is a prefix of the second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ('[] `IsPrefixOf` [0,1,3,2,4,5])
--   Eval ('[] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
--   = True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ([0,1,3,2,4,5] `IsPrefixOf` '[])
--   Eval ([0,1,3,2,4,5] `IsPrefixOf` '[]) :: Bool
--   = False
--   </pre>
data IsPrefixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return <tt>True</tt> when the first list is a suffix of the second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (IsSuffixOf '[] [0,1,3,2,4,5])
--   Eval (IsSuffixOf '[] [0,1,3,2,4,5]) :: Bool
--   = True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (IsSuffixOf [0,1,3,2,4,5] '[])
--   Eval (IsSuffixOf [0,1,3,2,4,5] '[]) :: Bool
--   = False
--   </pre>
data IsSuffixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return <tt>True</tt> when the first list is contained within the
--   second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
data IsInfixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return <tt>True</tt> if an element is in a list.
--   
--   See also <a>FindIndex</a>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Elem 1 [1,2,3])
--   Eval (Elem 1 [1,2,3]) :: Bool
--   = True
--   
--   &gt;&gt;&gt; :kind! Eval (Elem 1 [2,3])
--   Eval (Elem 1 [2,3]) :: Bool
--   = False
--   </pre>
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 <tt>Just</tt> the first element satisfying a predicate, or
--   evaluate to <tt>Nothing</tt> if no element satisfies the predicate.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Find (TyEq 0) [1,2,3])
--   Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural
--   = Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Find (TyEq 0) [1,2,3,0])
--   Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural
--   = Just 0
--   </pre>
data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a)

-- | Keep all elements that satisfy a predicate, remove all that don't.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Filter ((&gt;) 3) [1,2,3,0])
--   Eval (Filter ((&gt;) 3) [1,2,3,0]) :: [Natural]
--   = [1, 2, 0]
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Partition ((&gt;=) 35) [20, 30, 40, 50])
--   Eval (Partition ((&gt;=) 35) [20, 30, 40, 50]) :: ([Natural],
--                                                   [Natural])
--   = '([20, 30], [40, 50])
--   </pre>
data Partition (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))

-- | Find the index of an element satisfying the predicate.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (FindIndex ((&lt;=) 3) [1,2,3,1,2,3])
--   Eval (FindIndex ((&lt;=) 3) [1,2,3,1,2,3]) :: Maybe Natural
--   = Just 2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (FindIndex ((&gt;) 0) [1,2,3,1,2,3])
--   Eval (FindIndex ((&gt;) 0) [1,2,3,1,2,3]) :: Maybe Natural
--   = Nothing
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (SetIndex 2 7 [1,2,3])
--   Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
--   = [1, 2, 7]
--   </pre>
data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])

-- | Combine elements of two lists pairwise.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (ZipWith (+) [1,2,3] [1,1,1])
--   Eval (ZipWith (+) [1,2,3] [1,1,1]) :: [Natural]
--   = [2, 3, 4]
--   </pre>
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 <a>TyEq</a>.
module Fcf.Class.Ord

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

-- | "Smaller than or equal to". Type-level version of
--   <tt>(<a>&lt;=</a>)</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ("b" &lt;= "a")
--   Eval ("b" &lt;= "a") :: Bool
--   = False
--   </pre>
data ( (b :: a) <= (c :: a) ) (d :: Bool)

-- | "Greater than or equal to". Type-level version of
--   <tt>(<a>&gt;=</a>)</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ("b" &gt;= "a")
--   Eval ("b" &gt;= "a") :: Bool
--   = True
--   </pre>
data ( (b :: a) >= (c :: a) ) (d :: Bool)

-- | "Smaller than". Type-level version of <tt>(<a>&lt;</a>)</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ("a" &lt; "b")
--   Eval ("a" &lt; "b") :: Bool
--   = True
--   </pre>
data ( (b :: a) < (c :: a) ) (d :: Bool)

-- | "Greater than". Type-level version of <tt>(<a>&gt;</a>)</tt>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ("b" &gt; "a")
--   Eval ("b" &gt; "a") :: Bool
--   = True
--   </pre>
data ( (b :: a) > (c :: a) ) (d :: Bool)

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


-- | First-class type families
--   
--   For example, here is a regular type family:
--   
--   <pre>
--   type family   FromMaybe (a :: k) (m :: Maybe k) :: k
--   type instance FromMaybe a 'Nothing  = a
--   type instance FromMaybe a ('Just b) = b
--   </pre>
--   
--   With <tt>Fcf</tt>, it translates to a <tt>data</tt> declaration:
--   
--   <pre>
--   data FromMaybe :: k -&gt; Maybe k -&gt; <a>Exp</a> k
--   type instance <a>Eval</a> (FromMaybe a 'Nothing)  = a
--   type instance <a>Eval</a> (FromMaybe a ('Just b)) = b
--   </pre>
--   
--   <ul>
--   <li>Fcfs can be higher-order.</li>
--   <li>The kind constructor <a>Exp</a> is a monad: there's
--   <tt>(<a>=&lt;&lt;</a>)</tt> and <a>Pure</a>.</li>
--   </ul>
--   
--   Essential language extensions for <a>Fcf</a>:
--   
--   <pre>
--   {-# LANGUAGE
--       DataKinds,
--       PolyKinds,
--       TypeFamilies,
--       TypeOperators,
--       UndecidableInstances #-}
--   </pre>
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 <tt>($) f</tt> can
--   usually be replaced with <tt>f</tt>.
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 <a>Bimap</a> 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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; data Example where Ex :: a -&gt; Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   &gt;&gt;&gt; :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
--   Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
--   = Ex [1, 2, 3, 4]
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Cons 1 [2, 3])
--   Eval (Cons 1 [2, 3]) :: [Natural]
--   = [1, 2, 3]
--   
--   &gt;&gt;&gt; :kind! Eval (Cons Int [Char, Maybe Double])
--   Eval (Cons Int [Char, Maybe Double]) :: [*]
--   = [Int, Char, Maybe Double]
--   </pre>
data Cons (b :: a) (c :: [a]) (d :: [a])

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

-- | Append elements to two lists. Used in the definition of <a>Unzip</a>.
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 <a>init</a> and <a>last</a>
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Unsnoc '[])
--   Eval (Unsnoc '[]) :: Maybe ([a], a)
--   = Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Unsnoc '[1])
--   Eval (Unsnoc '[1]) :: Maybe ([Natural], Natural)
--   = Just '( '[], 1)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Unsnoc '[1,2,3])
--   Eval (Unsnoc '[1,2,3]) :: Maybe ([Natural], Natural)
--   = Just '([1, 2], 3)
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Reverse [1,2,3,4,5])
--   Eval (Reverse [1,2,3,4,5]) :: [Natural]
--   = [5, 4, 3, 2, 1]
--   </pre>
data Reverse (b :: [a]) (c :: [a])

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

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

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

-- | This is <a>Foldr</a> 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.
--   
--   <h3><b>Example</b></h3>
--   
--   For example, fold a list of lists.
--   
--   <pre>
--   Concat :: [[a]] -&gt; Exp [a]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Concat ([[1,2], [3,4], [5,6]]))
--   Eval (Concat ([[1,2], [3,4], [5,6]])) :: [Natural]
--   = [1, 2, 3, 4, 5, 6]
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Concat (a :: t m) (b :: m)

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

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

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

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

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

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

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

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

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

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

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

-- | Return <tt>True</tt> when the first list is a prefix of the second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ('[] `IsPrefixOf` [0,1,3,2,4,5])
--   Eval ('[] `IsPrefixOf` [0,1,3,2,4,5]) :: Bool
--   = True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval ([0,1,3,2,4,5] `IsPrefixOf` '[])
--   Eval ([0,1,3,2,4,5] `IsPrefixOf` '[]) :: Bool
--   = False
--   </pre>
data IsPrefixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return <tt>True</tt> when the first list is a suffix of the second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (IsSuffixOf '[] [0,1,3,2,4,5])
--   Eval (IsSuffixOf '[] [0,1,3,2,4,5]) :: Bool
--   = True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (IsSuffixOf [0,1,3,2,4,5] '[])
--   Eval (IsSuffixOf [0,1,3,2,4,5] '[]) :: Bool
--   = False
--   </pre>
data IsSuffixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return <tt>True</tt> when the first list is contained within the
--   second.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :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
--   </pre>
data IsInfixOf (b :: [a]) (c :: [a]) (d :: Bool)

-- | Return <tt>True</tt> if an element is in a list.
--   
--   See also <a>FindIndex</a>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Elem 1 [1,2,3])
--   Eval (Elem 1 [1,2,3]) :: Bool
--   = True
--   
--   &gt;&gt;&gt; :kind! Eval (Elem 1 [2,3])
--   Eval (Elem 1 [2,3]) :: Bool
--   = False
--   </pre>
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 <tt>Just</tt> the first element satisfying a predicate, or
--   evaluate to <tt>Nothing</tt> if no element satisfies the predicate.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Find (TyEq 0) [1,2,3])
--   Eval (Find (TyEq 0) [1,2,3]) :: Maybe Natural
--   = Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Find (TyEq 0) [1,2,3,0])
--   Eval (Find (TyEq 0) [1,2,3,0]) :: Maybe Natural
--   = Just 0
--   </pre>
data Find (b :: a -> Exp Bool) (c :: [a]) (d :: Maybe a)

-- | Keep all elements that satisfy a predicate, remove all that don't.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Filter ((&gt;) 3) [1,2,3,0])
--   Eval (Filter ((&gt;) 3) [1,2,3,0]) :: [Natural]
--   = [1, 2, 0]
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (Partition ((&gt;=) 35) [20, 30, 40, 50])
--   Eval (Partition ((&gt;=) 35) [20, 30, 40, 50]) :: ([Natural],
--                                                   [Natural])
--   = '([20, 30], [40, 50])
--   </pre>
data Partition (b :: a -> Exp Bool) (c :: [a]) (d :: ([a], [a]))

-- | Find the index of an element satisfying the predicate.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (FindIndex ((&lt;=) 3) [1,2,3,1,2,3])
--   Eval (FindIndex ((&lt;=) 3) [1,2,3,1,2,3]) :: Maybe Natural
--   = Just 2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (FindIndex ((&gt;) 0) [1,2,3,1,2,3])
--   Eval (FindIndex ((&gt;) 0) [1,2,3,1,2,3]) :: Maybe Natural
--   = Nothing
--   </pre>
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.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (SetIndex 2 7 [1,2,3])
--   Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
--   = [1, 2, 7]
--   </pre>
data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])

-- | Combine elements of two lists pairwise.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Eval (ZipWith (+) [1,2,3] [1,1,1])
--   Eval (ZipWith (+) [1,2,3] [1,1,1]) :: [Natural]
--   = [2, 3, 4]
--   </pre>
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":
--   <tt>UnBool ifFalse ifTrue bool</tt>.
--   
--   This mirrors the default order of constructors:
--   
--   <pre>
--   data Bool = False | True
--   ----------- False &lt; True
--   </pre>
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 <tt>\case { .. }</tt> syntax. Supports
--   matching of exact values (<a>--&gt;</a>) and final matches for any
--   value (<a>Any</a>) or for passing value to subcomputation
--   (<a>Else</a>). Examples:
--   
--   <pre>
--   type BoolToNat = <a>Case</a>
--     [ 'True  <a>--&gt;</a> 0
--     , 'False <a>--&gt;</a> 1
--     ]
--   
--   type NatToBool = <a>Case</a>
--     [ 0 <a>--&gt;</a> 'False
--     , <a>Any</a>   'True
--     ]
--   
--   type ZeroOneOrSucc = <a>Case</a>
--     [ 0  <a>--&gt;</a> 0
--     , 1  <a>--&gt;</a> 1
--     , <a>Else</a>   ((<a>+</a>) 1)
--     ]
--   </pre>
data Case (a :: [Match j k]) (b :: j) (c :: k)
data Match j k

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

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

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

-- | Pass type being matched in <a>Case</a> 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 <a>fmap</a> for type-level functors.
--   
--   Note: this name clashes with <a>Map</a> from <i>containers</i>.
--   <a>FMap</a> is provided as a synonym to avoid this.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; data Example where Ex :: a -&gt; Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   &gt;&gt;&gt; data AddMul :: Nat -&gt; Nat -&gt; Exp Nat
--   
--   &gt;&gt;&gt; type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--   
--   &gt;&gt;&gt; :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]
--   </pre>
data Map (c :: a -> Exp b) (d :: f a) (e :: f b)

-- | Type-level <a>bimap</a>.
--   
--   <h3><b>Example</b></h3>
--   
--   <pre>
--   &gt;&gt;&gt; data Example where Ex :: a -&gt; Example  -- Hide the type of examples to avoid brittleness in different GHC versions
--   
--   &gt;&gt;&gt; :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)
--   </pre>
data Bimap (c :: a -> Exp a') (d :: b -> Exp b') (e :: f a b) (g :: f a' b')

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

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

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

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

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

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

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