-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2023 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable

A type class representing a general open union for first-order effects, independent of the internal
implementation.
-}
module Data.Free.Union where

import Control.Effect.Class (Instruction, type (~>))
import Data.Kind (Constraint)

{- |
A type class representing a general open union for first-order effects, independent of the internal
implementation.
-}
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)