{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Eta reduce" #-}
module Data.HTree.Tree
(
TyTree (..)
, TyForest
, HTree (HLeaf, ..)
, HForest
, hmap
, hcmap
, TreeMap
, ForestMap
, htraverse
, hctraverse
, hFoldMap
, hcFoldMap
, hFlatten
, FlattenTree
, FlattenForest
, Path (..)
, replaceAt
, AllTree
, AllTreeC
, AllForest
, allTopHTree
, allTopHForest
)
where
import Data.Functor.Identity (Identity (Identity, runIdentity))
import Data.HTree.Constraint (Dict, withDict, pattern Dict)
import Data.HTree.Families (All, Top, type (++))
import Data.HTree.List (HList (HCons, HNil), hconcat)
import Data.HTree.List qualified as L
import Data.Kind (Constraint, Type)
type TyTree :: forall k. k -> Type
data TyTree k where
TyNode :: forall a. a -> TyForest a -> TyTree a
type TyForest :: forall k. k -> Type
type TyForest a = [TyTree a]
type HTree :: forall k. (k -> Type) -> TyTree k -> Type
data HTree f t where
HNode :: forall f a ts. f a -> HForest f ts -> HTree f ('TyNode a ts)
pattern HLeaf :: forall f a. forall. f a -> HTree f ('TyNode a '[])
pattern $mHLeaf :: forall {r} {a1} {f :: a1 -> Type} {a :: a1}.
HTree @a1 f ('TyNode @a1 a ('[] @(TyTree @Type a1)))
-> (f a -> r) -> ((# #) -> r) -> r
$bHLeaf :: forall {a1} (f :: a1 -> Type) (a :: a1).
f a -> HTree @a1 f ('TyNode @a1 a ('[] @(TyTree @Type a1)))
HLeaf a = HNode a HNil
type HForest :: forall k. (k -> Type) -> TyForest k -> Type
type HForest f ts = HList (HTree f) ts
hmap
:: forall {k} (f :: k -> Type) (g :: k -> Type) (t :: TyTree k)
. (forall a. f a -> g a)
-> HTree f t
-> HTree g t
hmap :: forall {k} (f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(forall (a :: k). f a -> g a) -> HTree @k f t -> HTree @k g t
hmap forall (a :: k). f a -> g a
f HTree @k f t
t = Dict (AllTree @k (Top @k) t)
-> (AllTree @k (Top @k) t => HTree @k g t) -> HTree @k g t
forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict (HTree @k f t -> Dict (AllTree @k (Top @k) t)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree HTree @k f t
t) ((AllTree @k (Top @k) t => HTree @k g t) -> HTree @k g t)
-> (AllTree @k (Top @k) t => HTree @k g t) -> HTree @k g t
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
(t :: TyTree @Type k).
AllTree @k c t =>
(forall (a :: k). c a => f a -> g a)
-> HTree @k f t -> HTree @k g t
forall (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
(t :: TyTree @Type k).
AllTree @k c t =>
(forall (a :: k). c a => f a -> g a)
-> HTree @k f t -> HTree @k g t
hcmap @Top @f @g f a -> g a
forall (a :: k). f a -> g a
forall (a :: k). Top @k a => f a -> g a
f HTree @k f t
t
hcmap
:: forall
{k}
(c :: k -> Constraint)
(f :: k -> Type)
(g :: k -> Type)
(t :: TyTree k)
. AllTree c t
=> (forall a. c a => f a -> g a)
-> HTree f t
-> HTree g t
hcmap :: forall {k} (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
(t :: TyTree @Type k).
AllTree @k c t =>
(forall (a :: k). c a => f a -> g a)
-> HTree @k f t -> HTree @k g t
hcmap forall (a :: k). c a => f a -> g a
f = Identity (HTree @k g t) -> HTree @k g t
forall a. Identity a -> a
runIdentity (Identity (HTree @k g t) -> HTree @k g t)
-> (HTree @k f t -> Identity (HTree @k g t))
-> HTree @k f t
-> HTree @k g t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: k -> Constraint) (h :: Type -> Type)
(f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
forall (c :: k -> Constraint) (h :: Type -> Type) (f :: k -> Type)
(g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
hctraverse @c @Identity @f @g (g a -> Identity (g a)
forall a. a -> Identity a
Identity (g a -> Identity (g a)) -> (f a -> g a) -> f a -> Identity (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
forall (a :: k). c a => f a -> g a
f)
htraverse
:: forall
{k}
(h :: Type -> Type)
(f :: k -> Type)
(g :: k -> Type)
(t :: TyTree k)
. Applicative h
=> (forall a. f a -> h (g a))
-> HTree f t
-> h (HTree g t)
htraverse :: forall {k} (h :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
(t :: TyTree @Type k).
Applicative h =>
(forall (a :: k). f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
htraverse forall (a :: k). f a -> h (g a)
f HTree @k f t
t = Dict (AllTree @k (Top @k) t)
-> (AllTree @k (Top @k) t => h (HTree @k g t)) -> h (HTree @k g t)
forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict (HTree @k f t -> Dict (AllTree @k (Top @k) t)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree HTree @k f t
t) ((AllTree @k (Top @k) t => h (HTree @k g t)) -> h (HTree @k g t))
-> (AllTree @k (Top @k) t => h (HTree @k g t)) -> h (HTree @k g t)
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (h :: Type -> Type)
(f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
forall (c :: k -> Constraint) (h :: Type -> Type) (f :: k -> Type)
(g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
hctraverse @Top f a -> h (g a)
forall (a :: k). f a -> h (g a)
forall (a :: k). Top @k a => f a -> h (g a)
f HTree @k f t
t
hctraverse
:: forall
{k}
(c :: k -> Constraint)
(h :: Type -> Type)
(f :: k -> Type)
(g :: k -> Type)
(t :: TyTree k)
. (AllTree c t, Applicative h)
=> (forall a. c a => f a -> h (g a))
-> HTree f t
-> h (HTree g t)
hctraverse :: forall {k} (c :: k -> Constraint) (h :: Type -> Type)
(f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
hctraverse forall (a :: k). c a => f a -> h (g a)
f (HNode f a
x HForest @k f ts
ts) = g a -> HForest @k g ts -> HTree @k g t
g a -> HForest @k g ts -> HTree @k g ('TyNode @k a ts)
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode (g a -> HForest @k g ts -> HTree @k g t)
-> h (g a) -> h (HForest @k g ts -> HTree @k g t)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> h (g a)
forall (a :: k). c a => f a -> h (g a)
f f a
x h (HForest @k g ts -> HTree @k g t)
-> h (HForest @k g ts) -> h (HTree @k g t)
forall a b. h (a -> b) -> h a -> h b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall {k} (c :: k -> Constraint) (t :: Type -> Type)
(f :: k -> Type) (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
forall (c :: TyTree @Type k -> Constraint) (t :: Type -> Type)
(f :: TyTree @Type k -> Type) (g :: TyTree @Type k -> Type)
(xs :: [TyTree @Type k]).
(All @(TyTree @Type k) c xs, Applicative t) =>
(forall (a :: TyTree @Type k). c a => f a -> t (g a))
-> HList @(TyTree @Type k) f xs -> t (HList @(TyTree @Type k) g xs)
L.hctraverse @(AllTreeC c) @h @(HTree f) @(HTree g) (forall {k} (c :: k -> Constraint) (h :: Type -> Type)
(f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
forall (c :: k -> Constraint) (h :: Type -> Type) (f :: k -> Type)
(g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
hctraverse @c f a -> h (g a)
forall (a :: k). c a => f a -> h (g a)
f) HForest @k f ts
ts
type TreeMap :: forall k l. (k -> l) -> TyTree k -> TyTree l
type family TreeMap f t where
forall f x. TreeMap f ('TyNode x '[]) = 'TyNode (f x) '[]
forall f x xs. TreeMap f ('TyNode x xs) = 'TyNode (f x) (ForestMap f xs)
type ForestMap :: forall k l. (k -> l) -> TyForest k -> TyForest l
type family ForestMap f t where
ForestMap _ '[] = '[]
forall f n ns. ForestMap f (n : ns) = TreeMap f n : ForestMap f ns
hcFoldMap
:: forall
{k}
(c :: k -> Constraint)
(f :: k -> Type)
(t :: TyTree k)
(b :: Type)
. (AllTree c t, Semigroup b)
=> (forall a. c a => f a -> b)
-> HTree f t
-> b
hcFoldMap :: forall {k} (c :: k -> Constraint) (f :: k -> Type)
(t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
hcFoldMap forall (a :: k). c a => f a -> b
f (HNode f a
x HList @(TyTree @Type k) (HTree @k f) ts
HNil) = f a -> b
forall (a :: k). c a => f a -> b
f f a
x
hcFoldMap forall (a :: k). c a => f a -> b
f (HNode f a
x (HTree @k f x
y `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ys)) = forall {k} (c :: k -> Constraint) (f :: k -> Type)
(t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
forall (c :: k -> Constraint) (f :: k -> Type)
(t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
hcFoldMap @c f a -> b
forall (a :: k). c a => f a -> b
f HTree @k f x
y b -> b -> b
forall a. Semigroup a => a -> a -> a
<> forall {k} (c :: k -> Constraint) (f :: k -> Type)
(t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
forall (c :: k -> Constraint) (f :: k -> Type)
(t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
hcFoldMap @c f a -> b
forall (a :: k). c a => f a -> b
f (f a
-> HList @(TyTree @Type k) (HTree @k f) xs
-> HTree @k f ('TyNode @k a xs)
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode f a
x HList @(TyTree @Type k) (HTree @k f) xs
ys)
hFoldMap
:: forall
{k}
(f :: k -> Type)
(t :: TyTree k)
(b :: Type)
. Semigroup b
=> (forall a. f a -> b)
-> HTree f t
-> b
hFoldMap :: forall {k} (f :: k -> Type) (t :: TyTree @Type k) b.
Semigroup b =>
(forall (a :: k). f a -> b) -> HTree @k f t -> b
hFoldMap forall (a :: k). f a -> b
f HTree @k f t
t = Dict (AllTree @k (Top @k) t) -> (AllTree @k (Top @k) t => b) -> b
forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict (HTree @k f t -> Dict (AllTree @k (Top @k) t)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree HTree @k f t
t) ((AllTree @k (Top @k) t => b) -> b)
-> (AllTree @k (Top @k) t => b) -> b
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (f :: k -> Type)
(t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
forall (c :: k -> Constraint) (f :: k -> Type)
(t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
hcFoldMap @Top f a -> b
forall (a :: k). f a -> b
forall (a :: k). Top @k a => f a -> b
f HTree @k f t
t
hFlatten
:: forall
{k}
(f :: k -> Type)
(t :: TyTree k)
. HTree f t
-> HList f (FlattenTree t)
hFlatten :: forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> HList @k f (FlattenTree @k t)
hFlatten (HNode f a
x HForest @k f ts
xs) = f a
x f a
-> HList @k f (FlattenForest @k ts)
-> HList @k f ((':) @k a (FlattenForest @k ts))
forall {k} (f :: k -> Type) (x :: k) (xs :: [k]).
f x -> HList @k f xs -> HList @k f ((':) @k x xs)
`HCons` HForest @k f ts -> HList @k f (FlattenForest @k ts)
forall (ts :: TyForest @Type k).
HForest @k f ts -> HList @k f (FlattenForest @k ts)
hflattenForest HForest @k f ts
xs
where
hflattenForest :: forall ts. HForest f ts -> HList f (FlattenForest ts)
hflattenForest :: forall (ts :: TyForest @Type k).
HForest @k f ts -> HList @k f (FlattenForest @k ts)
hflattenForest HList @(TyTree @Type k) (HTree @k f) ts
HNil = HList @k f ('[] @k)
HList @k f (FlattenForest @k ts)
forall {k} (f :: k -> Type). HList @k f ('[] @k)
HNil
hflattenForest (HTree @k f x
y `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ys) = HTree @k f x -> HList @k f (FlattenTree @k x)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> HList @k f (FlattenTree @k t)
hFlatten HTree @k f x
y HList @k f (FlattenTree @k x)
-> HList @k f (FlattenForest @k xs)
-> HList @k f ((++) @k (FlattenTree @k x) (FlattenForest @k xs))
forall {k} (f :: k -> Type) (xs :: [k]) (ys :: [k]).
HList @k f xs -> HList @k f ys -> HList @k f ((++) @k xs ys)
`hconcat` HList @(TyTree @Type k) (HTree @k f) xs
-> HList @k f (FlattenForest @k xs)
forall (ts :: TyForest @Type k).
HForest @k f ts -> HList @k f (FlattenForest @k ts)
hflattenForest HList @(TyTree @Type k) (HTree @k f) xs
ys
type FlattenTree :: forall k. TyTree k -> [k]
type family FlattenTree t where
forall x xs. FlattenTree ('TyNode x xs) = x : FlattenForest xs
type FlattenForest :: forall k. TyForest k -> [k]
type family FlattenForest f where
FlattenForest '[] = '[]
FlattenForest (x : xs) = FlattenTree x ++ FlattenForest xs
type AllTree :: forall k. (k -> Constraint) -> TyTree k -> Constraint
type family AllTree c ts where
forall c x ts. AllTree c ('TyNode x ts) = (c x, AllForest c ts)
type AllTreeC :: forall k. (k -> Constraint) -> TyTree k -> Constraint
class AllTree c ts => AllTreeC c ts
instance forall c ts. AllTree c ts => AllTreeC c ts
type AllForest :: forall k. (k -> Constraint) -> TyForest k -> Constraint
type family AllForest c t where
AllForest c xs = All (AllTreeC c) xs
allTopHTree :: forall f t. HTree f t -> Dict (AllTree Top t)
allTopHTree :: forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree (HNode f a
_ (HForest @k f ts -> Dict (AllForest @k (Top @k) ts)
forall {k} (f :: k -> Type) (t :: TyForest @Type k).
HForest @k f t -> Dict (AllForest @k (Top @k) t)
allTopHForest -> Dict (All @(TyTree @Type k) (AllTreeC @k (Top @k)) ts)
Dict (AllForest @k (Top @k) ts)
Dict)) = Dict (Top @k a, All @(TyTree @Type k) (AllTreeC @k (Top @k)) ts)
Has @Type (Charge @Type (AllTree @k (Top @k) t)) (Proxy @Type) ()
forall (c :: Constraint). c => Dict c
Dict
allTopHForest :: forall f t. HForest f t -> Dict (AllForest Top t)
allTopHForest :: forall {k} (f :: k -> Type) (t :: TyForest @Type k).
HForest @k f t -> Dict (AllForest @k (Top @k) t)
allTopHForest HList @(TyTree @Type k) (HTree @k f) t
HNil = Dict (() :: Constraint)
Has @Type (Charge @Type (AllForest @k (Top @k) t)) (Proxy @Type) ()
forall (c :: Constraint). c => Dict c
Dict
allTopHForest (HCons (HTree @k f x -> Dict (AllTree @k (Top @k) x)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree -> Dict (AllTree @k (Top @k) x)
Dict) (HList @(TyTree @Type k) (HTree @k f) xs
-> Dict (AllForest @k (Top @k) xs)
forall {k} (f :: k -> Type) (t :: TyForest @Type k).
HForest @k f t -> Dict (AllForest @k (Top @k) t)
allTopHForest -> Dict (All @(TyTree @Type k) (AllTreeC @k (Top @k)) xs)
Dict (AllForest @k (Top @k) xs)
Dict)) = Dict
(AllTreeC @k (Top @k) x,
All @(TyTree @Type k) (AllTreeC @k (Top @k)) xs)
Has @Type (Charge @Type (AllForest @k (Top @k) t)) (Proxy @Type) ()
forall (c :: Constraint). c => Dict c
Dict
replaceAt :: Path typ t -> f typ -> HTree f t -> HTree f t
replaceAt :: forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> f typ -> HTree @k f t -> HTree @k f t
replaceAt Path @k typ t
Here f typ
x (HNode f a
_ HForest @k f ts
xs) = f typ -> HForest @k f ts -> HTree @k f ('TyNode @k typ ts)
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode f typ
x HForest @k f ts
xs
replaceAt (Deeper Path @k typ t
pt) f typ
x (HNode f a
y (HTree @k f x
t `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ts)) = f a
-> HForest @k f ((':) @(TyTree @Type k) t xs)
-> HTree @k f ('TyNode @k a ((':) @(TyTree @Type k) t xs))
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode f a
y (Path @k typ t -> f typ -> HTree @k f t -> HTree @k f t
forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> f typ -> HTree @k f t -> HTree @k f t
replaceAt Path @k typ t
pt f typ
x HTree @k f t
HTree @k f x
t HTree @k f t
-> HList @(TyTree @Type k) (HTree @k f) xs
-> HForest @k f ((':) @(TyTree @Type k) t xs)
forall {k} (f :: k -> Type) (x :: k) (xs :: [k]).
f x -> HList @k f xs -> HList @k f ((':) @k x xs)
`HCons` HList @(TyTree @Type k) (HTree @k f) xs
ts)
replaceAt (Farther Path @k typ ('TyNode @k b ts)
pt) f typ
x (HNode f a
y (HTree @k f x
t `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ts)) = let HNode f b
f a
y' HList @(TyTree @Type k) (HTree @k f) ts
HForest @k f ts
ts' = Path @k typ ('TyNode @k b ts)
-> f typ
-> HTree @k f ('TyNode @k b ts)
-> HTree @k f ('TyNode @k b ts)
forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> f typ -> HTree @k f t -> HTree @k f t
replaceAt Path @k typ ('TyNode @k b ts)
pt f typ
x (f b
-> HList @(TyTree @Type k) (HTree @k f) ts
-> HTree @k f ('TyNode @k b ts)
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode f b
f a
y HList @(TyTree @Type k) (HTree @k f) ts
HList @(TyTree @Type k) (HTree @k f) xs
ts) in f b
-> HForest @k f ((':) @(TyTree @Type k) x ts)
-> HTree @k f ('TyNode @k b ((':) @(TyTree @Type k) x ts))
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode f b
y' (HTree @k f x
t HTree @k f x
-> HList @(TyTree @Type k) (HTree @k f) ts
-> HForest @k f ((':) @(TyTree @Type k) x ts)
forall {k} (f :: k -> Type) (x :: k) (xs :: [k]).
f x -> HList @k f xs -> HList @k f ((':) @k x xs)
`HCons` HList @(TyTree @Type k) (HTree @k f) ts
ts')
type Path :: forall k. k -> TyTree k -> Type
data Path k t where
Here :: forall a ts. Path a ('TyNode a ts)
Deeper :: forall a b t ts. Path a t -> Path a ('TyNode b (t : ts))
Farther :: forall a b t ts. Path a ('TyNode b ts) -> Path a ('TyNode b (t : ts))
infixr 4 `HNode`
infixr 4 `TyNode`
deriving stock instance (Show (f a), Show (HForest f t)) => Show (HTree f ('TyNode a t))
deriving stock instance (Eq (f a), Eq (HForest f t)) => Eq (HTree f ('TyNode a t))
deriving stock instance Show (Path typ t)
deriving stock instance Eq (Path typ t)