{-# LANGUAGE UndecidableInstances #-}
module Data.Hefty.Union where
import Control.Effect.Class (Signature, type (~>))
import Data.Kind (Constraint)
class UnionH (u :: [Signature] -> Signature) where
{-# MINIMAL injectH, projectH, absurdUnionH, (compH | (inject0H, weakenH), decompH | (|+:)) #-}
type HasMembershipH u (h :: Signature) (hs :: [Signature]) :: Constraint
injectH :: HasMembershipH u h hs => h f ~> u hs f
projectH :: HasMembershipH u h hs => u hs f a -> Maybe (h f a)
absurdUnionH :: u '[] f a -> x
compH :: Either (h f a) (u hs f a) -> u (h ': hs) f a
compH = \case
Left h f a
x -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H h f a
x
Right u hs f a
x -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH u hs f a
x
{-# INLINE compH #-}
decompH :: u (h ': hs) f a -> Either (h f a) (u hs f a)
decompH = forall a b. a -> Either a b
Left forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall a b. b -> Either a b
Right
{-# INLINE decompH #-}
infixr 5 |+:
(|+:) :: (h f a -> r) -> (u hs f a -> r) -> u (h ': hs) f a -> r
(h f a -> r
f |+: u hs f a -> r
g) u (h : hs) f a
u = case forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *])
(f :: * -> *) a.
UnionH u =>
u (h : hs) f a -> Either (h f a) (u hs f a)
decompH u (h : hs) f a
u of
Left h f a
x -> h f a -> r
f h f a
x
Right u hs f a
x -> u hs f a -> r
g u hs f a
x
{-# INLINE (|+:) #-}
inject0H :: h f ~> u (h ': hs) f
inject0H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
Either (h f a) (u hs f a) -> u (h : hs) f a
compH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left
{-# INLINE inject0H #-}
injectUnderH :: h2 f ~> u (h1 ': h2 ': hs) f
injectUnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H
{-# INLINE injectUnderH #-}
injectUnder2H :: h3 f ~> u (h1 ': h2 ': h3 ': hs) f
injectUnder2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H
{-# INLINE injectUnder2H #-}
injectUnder3H :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
injectUnder3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H
{-# INLINE injectUnder3H #-}
weakenH :: u hs f ~> u (h ': hs) f
weakenH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
Either (h f a) (u hs f a) -> u (h : hs) f a
compH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right
{-# INLINE weakenH #-}
weaken2H :: u hs f ~> u (h1 ': h2 ': hs) f
weaken2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
{-# INLINE weaken2H #-}
weaken3H :: u hs f ~> u (h1 ': h2 ': h3 ': hs) f
weaken3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
{-# INLINE weaken3H #-}
weaken4H :: u hs f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
weaken4H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
{-# INLINE weaken4H #-}
weakenUnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': hs) f
weakenUnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H
weakenUnder2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
weakenUnder2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H
weakenUnder3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
weakenUnder3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (h4 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : h4 : hs) f
weaken4H
weaken2UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
weaken2UnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H
weaken2Under2H :: u (h1 ': h2 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
weaken2Under2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (h4 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : h4 : hs) f
weaken4H
weaken3UnderH :: u (h1 ': hs) f ~> u (h1 ': h2 ': h3 ': h4 ': hs) f
weaken3UnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (h4 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : h4 : hs) f
weaken4H
flipUnionH :: u (h1 ': h2 ': hs) f ~> u (h2 ': h1 ': hs) f
flipUnionH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H
flipUnion3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h2 ': h1 ': hs) f
flipUnion3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H
flipUnionUnderH :: u (h1 ': h2 ': h3 ': hs) f ~> u (h1 ': h3 ': h2 ': hs) f
flipUnionUnderH = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H
rot3H :: u (h1 ': h2 ': h3 ': hs) f ~> u (h2 ': h3 ': h1 ': hs) f
rot3H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H
rot3H' :: u (h1 ': h2 ': h3 ': hs) f ~> u (h3 ': h1 ': h2 ': hs) f
rot3H' = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H
bundleUnion2H :: UnionH u' => u (h1 ': h2 ': hs) f ~> u (u' '[h1, h2] ': hs) f
bundleUnion2H = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
bundleUnion3H :: UnionH u' => u (h1 ': h2 ': h3 ': hs) f ~> u (u' '[h1, h2, h3] ': hs) f
bundleUnion3H =
(forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H)
forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH)
forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H)
forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
bundleUnion4H ::
UnionH u' =>
u (h1 ': h2 ': h3 ': h4 ': hs) f ~> u (u' '[h1, h2, h3, h4] ': hs) f
bundleUnion4H =
(forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H)
forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH)
forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H)
forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h4 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (h3 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h4 f ~> u (h1 : h2 : h3 : h4 : hs) f
injectUnder3H)
forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h : hs) f
weakenH
unbundleUnion2H :: UnionH u' => u (u' '[h1, h2] ': hs) f ~> u (h1 ': h2 ': hs) f
unbundleUnion2H = (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(f :: * -> *) a x.
UnionH u =>
u '[] f a -> x
absurdUnionH) forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : hs) f
weaken2H
unbundleUnion3H :: UnionH u' => u (u' '[h1, h2, h3] ': hs) f ~> u (h1 ': h2 ': h3 ': hs) f
unbundleUnion3H = (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(f :: * -> *) a x.
UnionH u =>
u '[] f a -> x
absurdUnionH) forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : hs) f
weaken3H
unbundleUnion4H ::
UnionH u' =>
u (u' '[h1, h2, h3, h4] ': hs) f
~> u (h1 ': h2 ': h3 ': h4 ': hs) f
unbundleUnion4H =
(forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h f ~> u (h : hs) f
inject0H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h2 f ~> u (h1 : h2 : hs) f
injectUnderH forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (hs :: [(* -> *) -> * -> *]).
UnionH u =>
h3 f ~> u (h1 : h2 : h3 : hs) f
injectUnder2H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h4 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
(h2 :: (* -> *) -> * -> *) (h3 :: (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
h4 f ~> u (h1 : h2 : h3 : h4 : hs) f
injectUnder3H forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(f :: * -> *) a x.
UnionH u =>
u '[] f a -> x
absurdUnionH)
forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(h :: (* -> *) -> * -> *) (f :: * -> *) a r
(hs :: [(* -> *) -> * -> *]).
UnionH u =>
(h f a -> r) -> (u hs f a -> r) -> u (h : hs) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
(hs :: [(* -> *) -> * -> *]) (f :: * -> *)
(h1 :: (* -> *) -> * -> *) (h2 :: (* -> *) -> * -> *)
(h3 :: (* -> *) -> * -> *) (h4 :: (* -> *) -> * -> *).
UnionH u =>
u hs f ~> u (h1 : h2 : h3 : h4 : hs) f
weaken4H
type family IsMemberH (h :: Signature) hs where
IsMemberH h (h ': hs) = 'True
IsMemberH h (_ ': hs) = IsMemberH h hs
IsMemberH _ '[] = 'False
type MemberH u h hs = (HasMembershipH u h hs, IsMemberH h hs ~ 'True)