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


-- | a library to build and work with heterogeneous, type level indexed rose trees
--   
--   This library implements a heterogeneous rose-tree (HTree) that is
--   indexed by a type-level rosetree (TyTree).
@package htree
@version 0.2.0.0


-- | A couple of types to work with Constraints
module Data.HTree.Constraint

-- | a functor useful for proving a constraint for some type
--   
--   <pre>
--   &gt;&gt;&gt; import Data.Functor.Identity
--   
--   &gt;&gt;&gt; Proves @Eq (Identity (5 :: Int))
--   Proves (Identity 5)
--   </pre>
data Has (c :: k -> Constraint) (f :: k -> Type) (k1 :: k)
[Proves] :: forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type). c k1 => f k1 -> Has c f k1

-- | <a>Has</a> but specialised to <a>Typeable</a>
type HasTypeable = Has Typeable :: k -> Constraint

-- | <a>Has</a> but specialised to a constant type, <tt>Some (HasIs k
--   f)</tt> is isomorphic to <tt>f k</tt>
type HasIs (k1 :: k) = Has k ~ k1

-- | destruct a <a>Has</a>
proves :: forall {k} c f (a :: k) r. Has c f a -> (c a => f a -> r) -> r

-- | transform a <a>Constraint</a> in something of kind <tt>k -&gt;
--   <a>Constraint</a></tt> to be able to use it in <a>Has</a>
class c => Charge c (a :: k)

-- | a Dict witnesses some constraint
type Dict c = Has Charge c :: Type -> Constraint Proxy :: Type -> Type ()

-- | match on a <a>Dict</a>
pattern Dict :: () => c => Dict c

-- | destructing a <a>Dict</a>
withDict :: Dict c -> (c => r) -> r
instance forall k (c :: GHC.Types.Constraint) (a :: k). c => Data.HTree.Constraint.Charge @k c a
instance forall k1 (f :: k1 -> GHC.Types.Type) (k2 :: k1) (c :: k1 -> GHC.Types.Constraint). GHC.Internal.Show.Show (f k2) => GHC.Internal.Show.Show (Data.HTree.Constraint.Has @k1 c f k2)


-- | generic types and type families used in some of the modules
module Data.HTree.Families

-- | for all elements of a list, a contraint holds
type family All (c :: k -> Constraint) (xs :: [k])

-- | like All but can be partially applied
class All c xs => AllC (c :: k -> Constraint) (xs :: [k])

-- | <a>All</a> but inversed: holds if all constraints in the list hold
class AllInv (l :: [k -> Constraint]) (k1 :: k)

-- | product of two classes
class (c1 a, c2 a) => Both (c1 :: k -> Constraint) (c2 :: k -> Constraint) (a :: k)

-- | like <a>not</a> but on the type level
type family Not (a :: Bool) :: Bool

-- | the class that every type has an instance for
class Top (k1 :: k)

-- | like 'Prelude.(++)' on the value level but on the type level
type family (xs :: [k]) ++ (ys :: [k]) :: [k]
infixr 5 ++

-- | typelevel Or
type family (a :: Bool) || (b :: Bool) :: Bool
instance forall k (c :: k -> GHC.Types.Constraint) (xs :: [k]). Data.HTree.Families.All @k c xs => Data.HTree.Families.AllC @k c xs
instance forall k1 (c :: k1 -> GHC.Types.Constraint) (k2 :: k1) (cs :: [k1 -> GHC.Types.Constraint]). (c k2, Data.HTree.Families.AllInv @k1 cs k2) => Data.HTree.Families.AllInv @k1 ((':) @(k1 -> GHC.Types.Constraint) c cs) k2
instance forall k1 (k2 :: k1). Data.HTree.Families.AllInv @k1 ('[] @(k1 -> GHC.Types.Constraint)) k2
instance forall k (c1 :: k -> GHC.Types.Constraint) (a :: k) (c2 :: k -> GHC.Types.Constraint). (c1 a, c2 a) => Data.HTree.Families.Both @k c1 c2 a
instance forall k1 (k2 :: k1). Data.HTree.Families.Top @k1 k2


-- | implements a heterogeneous list to use for forests of heterogeneous
--   trees
module Data.HTree.List

-- | A heterogeneous list
--   
--   <pre>
--   &gt;&gt;&gt; "bla" `HCons` 23 `HCons` HNil :: HList Identity '[ String, Int ]
--   HCons (Identity "bla") (HCons (Identity 23) HNil)
--   </pre>
data HList (f :: k -> Type) (ts :: [k])
[HCons] :: forall {k} (f :: k -> Type) (x :: k) (xs :: [k]). f x -> HList f xs -> HList f (x ': xs)
[HNil] :: forall {k} (f :: k -> Type). HList f ('[] :: [k])

-- | pattern synonym for <a>HCons</a>
--   
--   <pre>
--   &gt;&gt;&gt; t = "bla" ::: 23 ::: HNil :: HList Identity '[ String, Int ]
--   
--   &gt;&gt;&gt; t
--   HCons (Identity "bla") (HCons (Identity 23) HNil)
--   
--   &gt;&gt;&gt; case t of (x ::: _) -&gt; runIdentity x
--   "bla"
--   </pre>
pattern (:::) :: forall {a} f (x :: a) xs. f x -> HList f xs -> HList f (x ': xs)

-- | pattern that allows to construct a singleton HList
--   
--   <pre>
--   &gt;&gt;&gt; HSing 42 :: HList Identity '[ Int ]
--   HCons (Identity 42) HNil
--   </pre>
pattern HSing :: forall {k} f (a :: k). f a -> HList f '[a]
infixr 5 `HCons`
infixr 5 :::

-- | map with a constraint that holds for all elements of the list
--   
--   <pre>
--   &gt;&gt;&gt; import Data.Functor.Const
--   
--   &gt;&gt;&gt; hcmap @Show (Const . show . runIdentity) (42 `HCons` HSing "bla" :: HList Identity '[ Int, String ])
--   HCons (Const "42") (HCons (Const "\"bla\"") HNil)
--   </pre>
hcmap :: forall {k} f g (xs :: [k]). forall (c :: k -> Constraint) -> All c xs => (forall (a :: k). c a => f a -> g a) -> HList f xs -> HList g xs

-- | map with a function that maps forall f a
hmap :: forall {k} f g (xs :: [k]). (forall (a :: k). () => f a -> g a) -> HList f xs -> HList g xs

-- | traverse a structure with a function
htraverse :: forall {k} t f g (xs :: [k]). Applicative t => (forall (a :: k). () => f a -> t (g a)) -> HList f xs -> t (HList g xs)

-- | traverse a structure such that a constraint holds; this is the
--   workhorse of mapping and traversing
--   
--   <pre>
--   &gt;&gt;&gt; import Data.Functor.Const
--   
--   &gt;&gt;&gt; hctraverse @Show (Just . Const . show . runIdentity) (42 `HCons` HSing "bla" :: HList Identity '[ Int, String ])
--   Just (HCons (Const "42") (HCons (Const "\"bla\"") HNil))
--   </pre>
hctraverse :: forall {k} t f g (xs :: [k]). forall (c :: k -> Constraint) -> (All c xs, Applicative t) => (forall (a :: k). c a => f a -> t (g a)) -> HList f xs -> t (HList g xs)

-- | foldr for HLists.
hcFold :: forall {k} f b (xs :: [k]). forall (c :: k -> Constraint) -> All c xs => (forall (a :: k). c a => f a -> b -> b) -> b -> HList f xs -> b

-- | witnesses that for all HLists, we can always derive the All Top
--   constraint
allTopHList :: forall {k} (f :: k -> Type) (xs :: [k]). HList f xs -> Dict (All (Top :: k -> Constraint) xs)

-- | concats two heterogeneous lists
hconcat :: forall {k} (f :: k -> Type) (xs :: [k]) (ys :: [k]). HList f xs -> HList f ys -> HList f (xs ++ ys)
infixr 5 `hconcat`
instance forall k (f :: k -> GHC.Types.Type). GHC.Classes.Eq (Data.HTree.List.HList @k f ('[] @k))
instance forall a (f :: a -> GHC.Types.Type) (x :: a) (xs :: [a]). (GHC.Classes.Eq (f x), GHC.Classes.Eq (Data.HTree.List.HList @a f xs)) => GHC.Classes.Eq (Data.HTree.List.HList @a f ((':) @a x xs))
instance forall k (f :: k -> GHC.Types.Type). GHC.Internal.Show.Show (Data.HTree.List.HList @k f ('[] @k))
instance forall a (f :: a -> GHC.Types.Type) (x :: a) (xs :: [a]). (GHC.Internal.Show.Show (f x), GHC.Internal.Show.Show (Data.HTree.List.HList @a f xs)) => GHC.Internal.Show.Show (Data.HTree.List.HList @a f ((':) @a x xs))


-- | implements a heterogeneous tree (<a>HTree</a>) indexed by a
--   homogeneous type level tree (<a>TyTree</a>)
module Data.HTree.Tree

-- | a type level rose-tree that is only intended to store something of a
--   certain kind, e.g. Type
data TyTree (k1 :: k)
[TyNode] :: forall a. a -> TyForest a -> TyTree a
infixr 4 `TyNode`

-- | a forest of TyTrees
type TyForest (a :: k) = [TyTree a]

-- | a heterogeneous rose tree indexed by a TyTree
data HTree (f :: k -> Type) (t :: TyTree k)
[HNode] :: forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest k). f a -> HForest f ts -> HTree f ('TyNode a ts)

-- | a pattern synonym for the leaf of an HTree
pattern HLeaf :: forall {a1} f (a2 :: a1). f a2 -> HTree f ('TyNode a2 ('[] :: [TyTree a1]))
infixr 4 `HNode`

-- | A forest of heterogeneous rose trees
type HForest (f :: k -> Type) (ts :: TyForest k) = HList HTree f ts

-- | map a function over an HTree
hmap :: forall {k} f g (t :: TyTree k). (forall (a :: k). () => f a -> g a) -> HTree f t -> HTree g t

-- | map a function with a constraint over an HTree
hcmap :: forall {k} f g (t :: TyTree k). forall (c :: k -> Constraint) -> AllTree c t => (forall (a :: k). c a => f a -> g a) -> HTree f t -> HTree g t

-- | map a functor over a TyTree
type family TreeMap (f :: k -> l) (t :: TyTree k) :: TyTree l

-- | map a functor over a TyForest
type family ForestMap (f :: k -> l) (t :: TyForest k) :: TyForest l

-- | traverse a structure with a function
htraverse :: forall {k} h f g (t :: TyTree k). Applicative h => (forall (a :: k). () => f a -> h (g a)) -> HTree f t -> h (HTree g t)

-- | traverse a structure such that a constraint holds; this is the
--   workhorse of mapping and traversing
hctraverse :: forall {k} h f g (t :: TyTree k). forall (c :: k -> Constraint) -> (AllTree c t, Applicative h) => (forall (a :: k). c a => f a -> h (g a)) -> HTree f t -> h (HTree g t)

-- | monoidally folds down a tree to a single value, this is similar to
--   <a>foldMap</a>
hFoldMap :: forall {k} f (t :: TyTree k) b. Semigroup b => (forall (a :: k). () => f a -> b) -> HTree f t -> b

-- | monoidally folds down a tree to a single value using a constraint on
--   the element in the wrapping functor, this is similar to <a>foldMap</a>
hcFoldMap :: forall {k} f (t :: TyTree k) b. forall (c :: k -> Constraint) -> (AllTree c t, Semigroup b) => (forall (a :: k). c a => f a -> b) -> HTree f t -> b

-- | flatten a heterogeneous tree down to a heterogeneous list
hFlatten :: forall {k} (f :: k -> Type) (t :: TyTree k). HTree f t -> HList f (FlattenTree t)

-- | a type family that flattens a tree down to a list
type family FlattenTree (t :: TyTree k) :: [k]

-- | a type family that flattens a forest down to a list
type family FlattenForest (f :: TyForest k) :: [k]

-- | provides evidence that an element is in the tree by providing a path
--   to the element
data Path (k1 :: k) (t :: TyTree k)
[Here] :: forall {k} (k1 :: k) (ts :: TyForest k). Path k1 ('TyNode k1 ts)
[Deeper] :: forall {k} (k1 :: k) (b :: k) (t1 :: TyTree k) (ts :: [TyTree k]). Path k1 t1 -> Path k1 ('TyNode b (t1 ': ts))
[Farther] :: forall {k} (k1 :: k) (b :: k) (t1 :: TyTree k) (ts :: [TyTree k]). Path k1 ('TyNode b ts) -> Path k1 ('TyNode b (t1 ': ts))

-- | replace an element at a certain path.
replaceAt :: forall {k} (typ :: k) (t :: TyTree k) f. Path typ t -> f typ -> HTree f t -> HTree f t

-- | a constraint holds for all elements in the tree
type family AllTree (c :: k -> Constraint) (ts :: TyTree k)

-- | constraint synonym for AllTree
class AllTree c ts => AllTreeC (c :: k -> Constraint) (ts :: TyTree k)

-- | a constraint holds for all elements in the forest
type family AllForest (c :: k -> Constraint) (t :: TyForest k)

-- | witnesses that for any HTree the constraint AllTree Top always holds
allTopHTree :: forall {k} (f :: k -> Type) (t :: TyTree k). HTree f t -> Dict (AllTree (Top :: k -> Constraint) t)

-- | witnesses that for any HForest the constraint AllForest Top always
--   holds
allTopHForest :: forall {k} (f :: k -> Type) (t :: TyForest k). HForest f t -> Dict (AllForest (Top :: k -> Constraint) t)
instance forall k (c :: k -> GHC.Types.Constraint) (ts :: Data.HTree.Tree.TyTree @GHC.Types.Type k). Data.HTree.Tree.AllTree @k c ts => Data.HTree.Tree.AllTreeC @k c ts
instance forall a1 (f :: a1 -> GHC.Types.Type) (a2 :: a1) (t :: Data.HTree.Tree.TyForest @GHC.Types.Type a1). (GHC.Classes.Eq (f a2), GHC.Classes.Eq (Data.HTree.Tree.HForest @a1 f t)) => GHC.Classes.Eq (Data.HTree.Tree.HTree @a1 f ('Data.HTree.Tree.TyNode @a1 a2 t))
instance forall k (typ :: k) (t :: Data.HTree.Tree.TyTree @GHC.Types.Type k). GHC.Classes.Eq (Data.HTree.Tree.Path @k typ t)
instance forall a1 (f :: a1 -> GHC.Types.Type) (a2 :: a1) (t :: Data.HTree.Tree.TyForest @GHC.Types.Type a1). (GHC.Internal.Show.Show (f a2), GHC.Internal.Show.Show (Data.HTree.Tree.HForest @a1 f t)) => GHC.Internal.Show.Show (Data.HTree.Tree.HTree @a1 f ('Data.HTree.Tree.TyNode @a1 a2 t))
instance forall k (typ :: k) (t :: Data.HTree.Tree.TyTree @GHC.Types.Type k). GHC.Internal.Show.Show (Data.HTree.Tree.Path @k typ t)


-- | This module implements a search in a typelevel tree and offers a handy
--   interface via <tt>-XOverloaedRecordDot</tt> and <a>HasField</a>. We
--   can search in the tree via BFS or DFS. Performance wise this doesn't
--   make a difference, as the search is performed at compile time anyway
--   however, it can change the semantics if the tree contains an element
--   more than once, see the example in <a>getElem</a>.
module Data.HTree.Labeled

-- | a newtype that is labeled with some typelevel tag
newtype Labeled (l1 :: l) a
MkLabeled :: a -> Labeled (l1 :: l) a
[unLabel] :: Labeled (l1 :: l) a -> a

-- | a pattern that allows for direct construction and destruction of nodes
--   with labels
pattern HNodeL :: forall {l1} (l2 :: l1) a f (ts :: TyForest Type). Functor f => f a -> HForest f ts -> HTree f ('TyNode (Labeled l2 a) ts)
infixr 4 `HNodeL`

-- | a labeled HNode Leaf
pattern HLeafL :: forall {l1} (l2 :: l1) a f. Functor f => f a -> HTree f ('TyNode (Labeled l2 a) ('[] :: [TyTree Type]))

-- | a type syonym that allows for easy construction of TyTrees that have
--   labeled nodes
type TyNodeL (l1 :: l) a = 'TyNode Labeled l1 a
infixr 4 `TyNodeL`

-- | searches a tree for an element and returns that element, specialised
--   to <a>Labeled</a> and unwraps
--   
--   <pre>
--   &gt;&gt;&gt; import Data.Functor.Identity
--   
--   &gt;&gt;&gt; type T = TyNodeL "top" Int [ TyNodeL "inter" Int '[ TyNodeL "foo" Int '[]], TyNodeL "foo" Int '[]]
--   
--   &gt;&gt;&gt; t :: HTree Identity T = 42 `HNodeL` HNodeL 4 (HNodeL 69 HNil `HCons` HNil) `HCons` HNodeL 67 HNil `HCons` HNil
--   
--   &gt;&gt;&gt; getElem DFS "foo" Int t
--   Identity 69
--   
--   &gt;&gt;&gt; getElem BFS "foo" Int t
--   Identity 67
--   </pre>
getElem :: forall {k} (t :: TyTree Type) f. forall (strat :: SearchStrategy) (l :: k) typ -> (HasField' strat (Labeled l typ) t, Functor f) => HTree f t -> f typ

-- | searches a tree for an element and returns that element
getElem' :: forall (t :: TyTree Type) f. forall (strat :: SearchStrategy) typ -> HasField' strat typ t => HTree f t -> f typ

-- | the search strategy used in <a>HasField'</a>, this is intended to be
--   used only as a DataKind
data SearchStrategy
DFS :: SearchStrategy
BFS :: SearchStrategy

-- | Constraint representing the fact that the field <tt>x</tt> belongs to
--   the record type <tt>r</tt> and has field type <tt>a</tt>. This will be
--   solved automatically, but manual instances may be provided as well.
class HasField (x :: k) r a | x r -> a

-- | Selector function to extract the field from the record.
getField :: HasField x r a => r -> a

-- | This is the helper class that creates evidence, it implements a DFS
--   together with Decide
class HasField' (strat :: SearchStrategy) typ (t :: TyTree Type) | strat t -> typ
evidence :: HasField' strat typ t => proxy strat -> Path typ t

-- | Together with HasField' implements a DFS in the tree
class Decide (strat :: SearchStrategy) (elem :: Bool) typ (t :: TyTree Type) | strat t -> typ
evidence' :: forall {proxy :: forall k. () => k -> Type}. Decide strat elem typ t => proxy strat -> proxy elem -> Path typ t

-- | simple typelevel predicate that tests whether some element is in a
--   tree
type family Elem (typ :: k) (t :: TyTree k) :: Bool

-- | typelevel predicate that tests whether the element is in any of the
--   subtrees
type family AnyElem (typ :: k) (ts :: TyForest k) :: Bool

-- | gets an element given a path into the tree
getElemWithPath :: forall {k} (typ :: k) (t :: TyTree k) f. Path typ t -> HTree f t -> f typ
instance forall (strat :: Data.HTree.Labeled.SearchStrategy) typ (t :: Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) typ' (ts' :: [Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type]). Data.HTree.Labeled.HasField' strat typ t => Data.HTree.Labeled.Decide strat 'GHC.Types.False typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ' ((':) @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) t ts'))
instance forall (strat :: Data.HTree.Labeled.SearchStrategy) typ typ' (ts :: Data.HTree.Tree.TyForest @GHC.Types.Type GHC.Types.Type) (t' :: Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type). Data.HTree.Labeled.HasField' strat typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ' ts) => Data.HTree.Labeled.Decide strat 'GHC.Types.True typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ' ((':) @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) t' ts))
instance forall l1 (l2 :: l1) a. GHC.Classes.Eq a => GHC.Classes.Eq (Data.HTree.Labeled.Labeled @l1 l2 a)
instance forall l1 (l2 :: l1). GHC.Internal.Data.Foldable.Foldable (Data.HTree.Labeled.Labeled @l1 l2)
instance forall l1 (l2 :: l1). GHC.Internal.Base.Functor (Data.HTree.Labeled.Labeled @l1 l2)
instance forall l1 (l2 :: l1) a. GHC.Internal.Generics.Generic (Data.HTree.Labeled.Labeled @l1 l2 a)
instance forall typ (ts :: Data.HTree.Tree.TyForest @GHC.Types.Type GHC.Types.Type) typ' (t :: Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type). Data.HTree.Labeled.Decide 'Data.HTree.Labeled.BFS (Data.HTree.Labeled.AnyElem @GHC.Types.Type typ ts) typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ' ((':) @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) t ts)) => Data.HTree.Labeled.HasField' 'Data.HTree.Labeled.BFS typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ' ((':) @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) t ts))
instance forall typ (t :: Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) (ts :: [Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type]). Data.HTree.Labeled.HasField' 'Data.HTree.Labeled.BFS typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ ((':) @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) t ts))
instance forall typ. Data.HTree.Labeled.HasField' 'Data.HTree.Labeled.BFS typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ ('[] @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type)))
instance forall typ (t :: Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) typ' (ts :: [Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type]). Data.HTree.Labeled.Decide 'Data.HTree.Labeled.DFS (Data.HTree.Families.Not (Data.HTree.Labeled.Elem @GHC.Types.Type typ t)) typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ' ((':) @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) t ts)) => Data.HTree.Labeled.HasField' 'Data.HTree.Labeled.DFS typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ' ((':) @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) t ts))
instance forall typ (t :: Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) (ts :: [Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type]). Data.HTree.Labeled.HasField' 'Data.HTree.Labeled.DFS typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ ((':) @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) t ts))
instance forall typ. Data.HTree.Labeled.HasField' 'Data.HTree.Labeled.DFS typ ('Data.HTree.Tree.TyNode @GHC.Types.Type typ ('[] @(Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type)))
instance forall k (l :: k) typ (t :: Data.HTree.Tree.TyTree @GHC.Types.Type GHC.Types.Type) (f :: GHC.Types.Type -> GHC.Types.Type). (Data.HTree.Labeled.HasField' 'Data.HTree.Labeled.BFS (Data.HTree.Labeled.Labeled @k l typ) t, GHC.Internal.Base.Functor f) => GHC.Internal.Records.HasField @{k} l (Data.HTree.Tree.HTree @GHC.Types.Type f t) (f typ)
instance forall l1 (l2 :: l1) a. GHC.Classes.Ord a => GHC.Classes.Ord (Data.HTree.Labeled.Labeled @l1 l2 a)
instance forall l1 (l2 :: l1) a. GHC.Internal.Show.Show a => GHC.Internal.Show.Show (Data.HTree.Labeled.Labeled @l1 l2 a)
instance forall l1 (l2 :: l1). GHC.Internal.Data.Traversable.Traversable (Data.HTree.Labeled.Labeled @l1 l2)


-- | Existential types and helpers to work with existentials <a>HList</a>s
--   and <a>HTree</a>s
module Data.HTree.Existential

-- | a Some type that takes an arity one type constructor, this is for
--   completeness
data Some (g :: l -> Type)
[MkSome] :: forall {l} (g :: l -> Type) (k :: l). g k -> Some g

-- | a Some type that take an arity two type constructor, this is necessary
--   so that we avoid using composition on the type level or having visible
--   parameters to the type synonyms
data Some2 (g :: k -> l -> Type) (f :: k)
[MkSome2] :: forall {k} {l} (g :: k -> l -> Type) (f :: k) (k1 :: l). g f k1 -> Some2 g f

-- | HTree but the type level tree is existential
type ETree = Some2 HTree :: k -> Type -> TyTree k -> Type

-- | HList but the type level list is existential
type EList = Some2 HList :: k -> Type -> [k] -> Type

-- | take some existentai arity one type constructor and a function that
--   takes the non-existential one and returns some <tt>r</tt> and return
--   an <tt>r</tt>
with :: Some g -> (forall (m :: l). () => g m -> r) -> r

-- | take some existential arity two type constructor and a function that
--   takes the non-existential one and returns some <tt>r</tt> and return
--   an <tt>r</tt>
with2 :: forall {k} {l} g (f :: k) r. Some2 g f -> (forall (m :: l). () => g f m -> r) -> r

-- | <a>with2</a> specialized to <a>HTree</a>s
withSomeHTree :: forall {k} (f :: k -> Type) r. ETree f -> (forall (t :: TyTree k). () => HTree f t -> r) -> r

-- | <a>with2</a> specialized to <a>HList</a>s
withSomeHList :: forall {k} (f :: k -> Type) r. EList f -> (forall (xs :: [k]). () => HList f xs -> r) -> r

-- | fold over existential hlists
hcFoldEHList :: (forall (x :: k). c x => f x -> y -> y) -> y -> EList (Has c f) -> y

-- | fold over existential htrees
hcFoldMapEHTree :: forall {k} c f y. Semigroup y => (forall (a :: k). c a => f a -> y) -> ETree (Has c f) -> y

-- | a functor useful for proving a constraint for some type
--   
--   <pre>
--   &gt;&gt;&gt; import Data.Functor.Identity
--   
--   &gt;&gt;&gt; Proves @Eq (Identity (5 :: Int))
--   Proves (Identity 5)
--   </pre>
data Has (c :: k -> Constraint) (f :: k -> Type) (k1 :: k)
[Proves] :: forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type). c k1 => f k1 -> Has c f k1

-- | <a>Has</a> but specialised to <a>Typeable</a>
type HasTypeable = Has Typeable :: k -> Constraint

-- | <a>Has</a> but specialised to a constant type, <tt>Some (HasIs k
--   f)</tt> is isomorphic to <tt>f k</tt>
type HasIs (k1 :: k) = Has k ~ k1

-- | destruct <a>Some</a>, destruct <a>Has</a>
withProves :: Some (Has c f) -> (forall (a :: l). c a => f a -> r) -> r

-- | condens the <a>Has</a> constraints in an existential
prodHas :: forall {l} (c1 :: l -> Constraint) (c2 :: l -> Constraint) (f :: l -> Type). Some (Has c1 (Has c2 f)) -> Some (Has (Both c1 c2) f)

-- | flip the constraints in an existential
flipHas :: forall {l} (c1 :: l -> Constraint) (c2 :: l -> Constraint) (f :: l -> Type). Some (Has c1 (Has c2 f)) -> Some (Has c2 (Has c1 f))
instance forall (f :: GHC.Types.Type -> GHC.Types.Type). (forall x. GHC.Classes.Eq x => GHC.Classes.Eq (f x), GHC.Internal.Data.Typeable.Internal.Typeable @(GHC.Types.Type -> GHC.Types.Type) f) => GHC.Classes.Eq (Data.HTree.Existential.Some @GHC.Types.Type (Data.HTree.Constraint.Has @GHC.Types.Type (GHC.Internal.Data.Typeable.Internal.Typeable @GHC.Types.Type) (Data.HTree.Constraint.Has @GHC.Types.Type GHC.Classes.Eq f)))
instance forall (f :: GHC.Types.Type -> GHC.Types.Type). (forall x. GHC.Classes.Eq x => GHC.Classes.Eq (f x), GHC.Internal.Data.Typeable.Internal.Typeable @(GHC.Types.Type -> GHC.Types.Type) f) => GHC.Classes.Eq (Data.HTree.Existential.EList @GHC.Types.Type (Data.HTree.Constraint.Has @GHC.Types.Type (Data.HTree.Families.Both @GHC.Types.Type (GHC.Internal.Data.Typeable.Internal.Typeable @GHC.Types.Type) GHC.Classes.Eq) f))
instance forall k1 (f :: k1 -> GHC.Types.Type) (k2 :: k1). GHC.Classes.Eq (f k2) => GHC.Classes.Eq (Data.HTree.Existential.EList @k1 (Data.HTree.Constraint.HasIs @k1 k2 f))
instance forall (f :: GHC.Types.Type -> GHC.Types.Type). (forall x. GHC.Classes.Eq x => GHC.Classes.Eq (f x), GHC.Internal.Data.Typeable.Internal.Typeable @(GHC.Types.Type -> GHC.Types.Type) f) => GHC.Classes.Eq (Data.HTree.Existential.ETree @GHC.Types.Type (Data.HTree.Constraint.Has @GHC.Types.Type (Data.HTree.Families.Both @GHC.Types.Type (GHC.Internal.Data.Typeable.Internal.Typeable @GHC.Types.Type) GHC.Classes.Eq) f))
instance forall (f :: GHC.Types.Type -> GHC.Types.Type). (forall x. GHC.Classes.Ord x => GHC.Classes.Ord (f x), GHC.Internal.Data.Typeable.Internal.Typeable @(GHC.Types.Type -> GHC.Types.Type) f, GHC.Classes.Eq (Data.HTree.Existential.Some @GHC.Types.Type (Data.HTree.Constraint.Has @GHC.Types.Type (GHC.Internal.Data.Typeable.Internal.Typeable @GHC.Types.Type) (Data.HTree.Constraint.Has @GHC.Types.Type GHC.Classes.Ord f)))) => GHC.Classes.Ord (Data.HTree.Existential.Some @GHC.Types.Type (Data.HTree.Constraint.Has @GHC.Types.Type (GHC.Internal.Data.Typeable.Internal.Typeable @GHC.Types.Type) (Data.HTree.Constraint.Has @GHC.Types.Type GHC.Classes.Ord f)))
instance forall l (g :: l -> GHC.Types.Type). (forall (k :: l). GHC.Internal.Show.Show (g k)) => GHC.Internal.Show.Show (Data.HTree.Existential.Some @l g)
instance forall l (f :: l -> GHC.Types.Type). GHC.Internal.Data.Typeable.Internal.Typeable @(l -> GHC.Types.Type) f => GHC.Internal.Show.Show (Data.HTree.Existential.Some @l (Data.HTree.Constraint.Has @l (GHC.Internal.Data.Typeable.Internal.Typeable @l) f))
instance forall k l (g :: k -> l -> GHC.Types.Type) (f :: k). (forall (k1 :: l). GHC.Internal.Show.Show (g f k1)) => GHC.Internal.Show.Show (Data.HTree.Existential.Some2 @k @l g f)


-- | a module for useful reexports from the modules
module Data.HTree

-- | A heterogeneous list
--   
--   <pre>
--   &gt;&gt;&gt; "bla" `HCons` 23 `HCons` HNil :: HList Identity '[ String, Int ]
--   HCons (Identity "bla") (HCons (Identity 23) HNil)
--   </pre>
data HList (f :: k -> Type) (ts :: [k])
[HCons] :: forall {k} (f :: k -> Type) (x :: k) (xs :: [k]). f x -> HList f xs -> HList f (x ': xs)
[HNil] :: forall {k} (f :: k -> Type). HList f ('[] :: [k])

-- | pattern synonym for <a>HCons</a>
--   
--   <pre>
--   &gt;&gt;&gt; t = "bla" ::: 23 ::: HNil :: HList Identity '[ String, Int ]
--   
--   &gt;&gt;&gt; t
--   HCons (Identity "bla") (HCons (Identity 23) HNil)
--   
--   &gt;&gt;&gt; case t of (x ::: _) -&gt; runIdentity x
--   "bla"
--   </pre>
pattern (:::) :: forall {a} f (x :: a) xs. f x -> HList f xs -> HList f (x ': xs)

-- | pattern that allows to construct a singleton HList
--   
--   <pre>
--   &gt;&gt;&gt; HSing 42 :: HList Identity '[ Int ]
--   HCons (Identity 42) HNil
--   </pre>
pattern HSing :: forall {k} f (a :: k). f a -> HList f '[a]
infixr 5 `HCons`
infixr 5 :::

-- | a heterogeneous rose tree indexed by a TyTree
data HTree (f :: k -> Type) (t :: TyTree k)
[HNode] :: forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest k). f a -> HForest f ts -> HTree f ('TyNode a ts)

-- | a pattern synonym for the leaf of an HTree
pattern HLeaf :: forall {a1} f (a2 :: a1). f a2 -> HTree f ('TyNode a2 ('[] :: [TyTree a1]))
infixr 4 `HNode`

-- | a pattern that allows for direct construction and destruction of nodes
--   with labels
pattern HNodeL :: forall {l1} (l2 :: l1) a f (ts :: TyForest Type). Functor f => f a -> HForest f ts -> HTree f ('TyNode (Labeled l2 a) ts)
infixr 4 `HNodeL`

-- | a type level rose-tree that is only intended to store something of a
--   certain kind, e.g. Type
data TyTree (k1 :: k)
[TyNode] :: forall a. a -> TyForest a -> TyTree a
infixr 4 `TyNode`

-- | a type syonym that allows for easy construction of TyTrees that have
--   labeled nodes
type TyNodeL (l1 :: l) a = 'TyNode Labeled l1 a
infixr 4 `TyNodeL`

-- | map a function over an HTree
hmap :: forall {k} f g (t :: TyTree k). (forall (a :: k). () => f a -> g a) -> HTree f t -> HTree g t

-- | map a function with a constraint over an HTree
hcmap :: forall {k} f g (t :: TyTree k). forall (c :: k -> Constraint) -> AllTree c t => (forall (a :: k). c a => f a -> g a) -> HTree f t -> HTree g t

-- | traverse a structure with a function
htraverse :: forall {k} h f g (t :: TyTree k). Applicative h => (forall (a :: k). () => f a -> h (g a)) -> HTree f t -> h (HTree g t)

-- | traverse a structure such that a constraint holds; this is the
--   workhorse of mapping and traversing
hctraverse :: forall {k} h f g (t :: TyTree k). forall (c :: k -> Constraint) -> (AllTree c t, Applicative h) => (forall (a :: k). c a => f a -> h (g a)) -> HTree f t -> h (HTree g t)

-- | monoidally folds down a tree to a single value, this is similar to
--   <a>foldMap</a>
hFoldMap :: forall {k} f (t :: TyTree k) b. Semigroup b => (forall (a :: k). () => f a -> b) -> HTree f t -> b

-- | monoidally folds down a tree to a single value using a constraint on
--   the element in the wrapping functor, this is similar to <a>foldMap</a>
hcFoldMap :: forall {k} f (t :: TyTree k) b. forall (c :: k -> Constraint) -> (AllTree c t, Semigroup b) => (forall (a :: k). c a => f a -> b) -> HTree f t -> b

-- | flatten a heterogeneous tree down to a heterogeneous list
hFlatten :: forall {k} (f :: k -> Type) (t :: TyTree k). HTree f t -> HList f (FlattenTree t)

-- | a type family that flattens a tree down to a list
type family FlattenTree (t :: TyTree k) :: [k]

-- | a type family that flattens a forest down to a list
type family FlattenForest (f :: TyForest k) :: [k]

-- | a newtype that is labeled with some typelevel tag
newtype Labeled (l1 :: l) a
MkLabeled :: a -> Labeled (l1 :: l) a
[unLabel] :: Labeled (l1 :: l) a -> a

-- | Constraint representing the fact that the field <tt>x</tt> belongs to
--   the record type <tt>r</tt> and has field type <tt>a</tt>. This will be
--   solved automatically, but manual instances may be provided as well.
class HasField (x :: k) r a | x r -> a

-- | Selector function to extract the field from the record.
getField :: HasField x r a => r -> a

-- | searches a tree for an element and returns that element, specialised
--   to <a>Labeled</a> and unwraps
--   
--   <pre>
--   &gt;&gt;&gt; import Data.Functor.Identity
--   
--   &gt;&gt;&gt; type T = TyNodeL "top" Int [ TyNodeL "inter" Int '[ TyNodeL "foo" Int '[]], TyNodeL "foo" Int '[]]
--   
--   &gt;&gt;&gt; t :: HTree Identity T = 42 `HNodeL` HNodeL 4 (HNodeL 69 HNil `HCons` HNil) `HCons` HNodeL 67 HNil `HCons` HNil
--   
--   &gt;&gt;&gt; getElem DFS "foo" Int t
--   Identity 69
--   
--   &gt;&gt;&gt; getElem BFS "foo" Int t
--   Identity 67
--   </pre>
getElem :: forall {k} (t :: TyTree Type) f. forall (strat :: SearchStrategy) (l :: k) typ -> (HasField' strat (Labeled l typ) t, Functor f) => HTree f t -> f typ

-- | <a>Proxy</a> is a type that holds no data, but has a phantom parameter
--   of arbitrary type (or even kind). Its use is to provide type
--   information, even though there is no value available of that type (or
--   it may be too costly to create one).
--   
--   Historically, <tt><a>Proxy</a> :: <a>Proxy</a> a</tt> is a safer
--   alternative to the <tt><a>undefined</a> :: a</tt> idiom.
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy (Void, Int -&gt; Int)
--   Proxy
--   </pre>
--   
--   Proxy can even hold types of higher kinds,
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy Either
--   Proxy
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy Functor
--   Proxy
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy complicatedStructure
--   Proxy
--   </pre>
data Proxy (t :: k)
Proxy :: Proxy (t :: k)

-- | The kind of types with lifted values. For example <tt>Int ::
--   Type</tt>.
type Type = TYPE LiftedRep

-- | The kind of lifted constraints
type Constraint = CONSTRAINT LiftedRep

-- | a Dict witnesses some constraint
type Dict c = Has Charge c :: Type -> Constraint Proxy :: Type -> Type ()

-- | match on a <a>Dict</a>
pattern Dict :: () => c => Dict c

-- | destructing a <a>Dict</a>
withDict :: Dict c -> (c => r) -> r