module Data.Free.Union where
import Control.Effect.Class (Instruction, type (~>))
import Data.Kind (Constraint)
class Union (u :: [Instruction] -> Instruction) where
{-# MINIMAL inject, project, absurdUnion, (comp | (inject0, weaken), decomp | (|+|:)) #-}
type HasMembership u (f :: Instruction) (fs :: [Instruction]) :: Constraint
inject :: HasMembership u f fs => f ~> u fs
project :: HasMembership u f fs => u fs a -> Maybe (f a)
absurdUnion :: u '[] a -> x
comp :: Either (f a) (u fs a) -> u (f ': fs) a
comp = \case
Left f a
x -> forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 f a
x
Right u fs a
x -> forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken u fs a
x
{-# INLINE comp #-}
decomp :: u (f ': fs) a -> Either (f a) (u fs a)
decomp = forall a b. a -> Either a b
Left forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall a b. b -> Either a b
Right
{-# INLINE decomp #-}
infixr 5 |+|:
(|+|:) :: (f a -> r) -> (u fs a -> r) -> u (f ': fs) a -> r
(f a -> r
f |+|: u fs a -> r
g) u (f : fs) a
u = case forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]) a.
Union u =>
u (f : fs) a -> Either (f a) (u fs a)
decomp u (f : fs) a
u of
Left f a
x -> f a -> r
f f a
x
Right u fs a
x -> u fs a -> r
g u fs a
x
{-# INLINE (|+|:) #-}
inject0 :: f ~> u (f ': fs)
inject0 = forall (u :: [* -> *] -> * -> *) (f :: * -> *) a (fs :: [* -> *]).
Union u =>
Either (f a) (u fs a) -> u (f : fs) a
comp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left
{-# INLINE inject0 #-}
injectUnder :: f2 ~> u (f1 ': f2 ': fs)
injectUnder = forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0
{-# INLINE injectUnder #-}
injectUnder2 :: f3 ~> u (f1 ': f2 ': f3 ': fs)
injectUnder2 = forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : fs) a
weaken2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0
{-# INLINE injectUnder2 #-}
injectUnder3 :: f4 ~> u (f1 ': f2 ': f3 ': f4 ': fs)
injectUnder3 = forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0
{-# INLINE injectUnder3 #-}
weaken :: u fs a -> u (f ': fs) a
weaken = forall (u :: [* -> *] -> * -> *) (f :: * -> *) a (fs :: [* -> *]).
Union u =>
Either (f a) (u fs a) -> u (f : fs) a
comp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right
{-# INLINE weaken #-}
weaken2 :: u fs a -> u (f1 ': f2 ': fs) a
weaken2 = forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken
{-# INLINE weaken2 #-}
weaken3 :: u fs a -> u (f1 ': f2 ': f3 ': fs) a
weaken3 = forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : fs) a
weaken2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken
{-# INLINE weaken3 #-}
weaken4 :: u fs a -> u (f1 ': f2 ': f3 ': f4 ': fs) a
weaken4 = forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken
{-# INLINE weaken4 #-}
weakenUnder :: u (f1 ': fs) ~> u (f1 ': f2 ': fs)
weakenUnder = forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : fs) a
weaken2
weakenUnder2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': fs)
weakenUnder2 = forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3
weakenUnder3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
weakenUnder3 = forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *) (f4 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : f4 : fs) a
weaken4
weaken2Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': fs)
weaken2Under = forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3
weaken2Under2 :: u (f1 ': f2 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
weaken2Under2 = forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *) (f4 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : f4 : fs) a
weaken4
weaken3Under :: u (f1 ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
weaken3Under = forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *) (f4 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : f4 : fs) a
weaken4
flipUnion :: u (f1 ': f2 ': fs) ~> u (f2 ': f1 ': fs)
flipUnion = forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : fs) a
weaken2
flipUnion3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f2 ': f1 ': fs)
flipUnion3 = forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3
flipUnionUnder :: u (f1 ': f2 ': f3 ': fs) ~> u (f1 ': f3 ': f2 ': fs)
flipUnionUnder = forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3
rot3 :: u (f1 ': f2 ': f3 ': fs) ~> u (f2 ': f3 ': f1 ': fs)
rot3 = forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3
rot3' :: u (f1 ': f2 ': f3 ': fs) ~> u (f3 ': f1 ': f2 ': fs)
rot3' = forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3
bundleUnion2 :: Union u' => u (f1 ': f2 ': fs) ~> u (u' '[f1, f2] ': fs)
bundleUnion2 = forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken
bundleUnion3 :: Union u' => u (f1 ': f2 ': f3 ': fs) ~> u (u' '[f1, f2, f3] ': fs)
bundleUnion3 =
(forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0)
forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: (forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder)
forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: (forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2)
forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken
bundleUnion4 :: Union u' => u (f1 ': f2 ': f3 ': f4 ': fs) ~> u (u' '[f1, f2, f3, f4] ': fs)
bundleUnion4 =
(forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0)
forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: (forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder)
forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: (forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2)
forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: (forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [* -> *] -> * -> *) (f4 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *) (fs :: [* -> *]).
Union u =>
f4 ~> u (f1 : f2 : f3 : f4 : fs)
injectUnder3)
forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f :: * -> *).
Union u =>
u fs a -> u (f : fs) a
weaken
unbundleUnion2 :: Union u' => u (u' '[f1, f2] ': fs) ~> u (f1 ': f2 ': fs)
unbundleUnion2 = (forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) a x. Union u => u '[] a -> x
absurdUnion) forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : fs) a
weaken2
unbundleUnion3 :: Union u' => u (u' '[f1, f2, f3] ': fs) ~> u (f1 ': f2 ': f3 ': fs)
unbundleUnion3 = (forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) a x. Union u => u '[] a -> x
absurdUnion) forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : fs) a
weaken3
unbundleUnion4 :: Union u' => u (u' '[f1, f2, f3, f4] ': fs) ~> u (f1 ': f2 ': f3 ': f4 ': fs)
unbundleUnion4 =
(forall (u :: [* -> *] -> * -> *) (f :: * -> *) (fs :: [* -> *]).
Union u =>
f ~> u (f : fs)
inject0 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f2 :: * -> *) (f1 :: * -> *)
(fs :: [* -> *]).
Union u =>
f2 ~> u (f1 : f2 : fs)
injectUnder forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f3 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (fs :: [* -> *]).
Union u =>
f3 ~> u (f1 : f2 : f3 : fs)
injectUnder2 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (f4 :: * -> *) (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *) (fs :: [* -> *]).
Union u =>
f4 ~> u (f1 : f2 : f3 : f4 : fs)
injectUnder3 forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) a x. Union u => u '[] a -> x
absurdUnion)
forall (u :: [* -> *] -> * -> *) (f :: * -> *) a r
(fs :: [* -> *]).
Union u =>
(f a -> r) -> (u fs a -> r) -> u (f : fs) a -> r
|+|: forall (u :: [* -> *] -> * -> *) (fs :: [* -> *]) a (f1 :: * -> *)
(f2 :: * -> *) (f3 :: * -> *) (f4 :: * -> *).
Union u =>
u fs a -> u (f1 : f2 : f3 : f4 : fs) a
weaken4
type family IsMember (f :: Instruction) fs where
IsMember f (f ': fs) = 'True
IsMember f (_ ': fs) = IsMember f fs
IsMember _ '[] = 'False
type Member u f fs = (HasMembership u f fs, IsMember f fs ~ 'True)