{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- 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-2024 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 higher-order effects, independent of the internal
implementation.
-}
module Data.Hefty.Union where

import Control.Effect (type (~>))
import Control.Monad ((<=<))
import Data.Effect (LNop, LiftIns (LiftIns), Nop, SigClass, unliftIns)
import Data.Effect.HFunctor (HFunctor, caseH, (:+:) (Inl, Inr))
import Data.Effect.Key (type (##>), type (#>))
import Data.Free.Sum (type (+))
import Data.Kind (Constraint)
import Data.Singletons (SingI, sing)
import Data.Singletons.TH (singletons)
import Data.Type.Bool (If)
import Data.Type.Equality ((:~:) (Refl))
import GHC.TypeLits (ErrorMessage (ShowType, Text, (:$$:), (:<>:)), Nat, TypeError)
import GHC.TypeNats qualified as N

{- |
A type class representing a general open union for higher-order effects, independent of the internal
implementation.
-}
class Union (u :: [SigClass] -> SigClass) where
    {-# MINIMAL inject, project, exhaust, (comp | (inject0, weaken), decomp | (|+:)) #-}

    type HasMembership u (e :: SigClass) (es :: [SigClass]) :: Constraint

    inject :: HasMembership u e es => e f ~> u es f
    project :: HasMembership u e es => u es f a -> Maybe (e f a)

    exhaust :: u '[] f a -> x

    comp :: Either (e f a) (u es f a) -> u (e ': es) f a
    comp = \case
        Left e f a
x -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 e f a
x
        Right u es f a
x -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken u es f a
x
    {-# INLINE comp #-}

    decomp :: u (e ': es) f a -> (e :+: u es) f a
    decomp = forall {k} (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
f h e -> (:+:) f g h e
Inl forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall {k} (f :: (* -> *) -> k -> *) (g :: (* -> *) -> k -> *)
       (h :: * -> *) (e :: k).
g h e -> (:+:) f g h e
Inr
    {-# INLINE decomp #-}

    infixr 5 |+:
    (|+:) :: (e f a -> r) -> (u es f a -> r) -> u (e ': es) f a -> r
    e f a -> r
f |+: u es f a -> r
g = forall {k} (f :: (* -> *) -> k -> *) (a :: * -> *) (b :: k) c
       (g :: (* -> *) -> k -> *).
(f a b -> c) -> (g a b -> c) -> (:+:) f g a b -> c
caseH e f a -> r
f u es f a -> r
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (f :: * -> *) a.
Union u =>
u (e : es) f a -> (:+:) e (u es) f a
decomp
    {-# INLINE (|+:) #-}

    inject0 :: e f ~> u (e ': es) f
    inject0 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a
       (es :: [(* -> *) -> * -> *]).
Union u =>
Either (e f a) (u es f a) -> u (e : es) f a
comp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left
    {-# INLINE inject0 #-}

    injectUnder :: h2 f ~> u (h1 ': h2 ': es) f
    injectUnder = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0
    {-# INLINE injectUnder #-}

    injectUnder2 :: h3 f ~> u (h1 ': h2 ': h3 ': es) f
    injectUnder2 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0
    {-# INLINE injectUnder2 #-}

    injectUnder3 :: h4 f ~> u (h1 ': h2 ': h3 ': h4 ': es) f
    injectUnder3 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0
    {-# INLINE injectUnder3 #-}

    weaken :: u es f ~> u (e ': es) f
    weaken = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a
       (es :: [(* -> *) -> * -> *]).
Union u =>
Either (e f a) (u es f a) -> u (e : es) f a
comp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right
    {-# INLINE weaken #-}

    weaken2 :: u es f ~> u (e1 ': e2 ': es) f
    weaken2 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken
    {-# INLINE weaken2 #-}

    weaken3 :: u es f ~> u (e1 ': e2 ': e3 ': es) f
    weaken3 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken
    {-# INLINE weaken3 #-}

    weaken4 :: u es f ~> u (e1 ': e2 ': e3 ': e4 ': es) f
    weaken4 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken
    {-# INLINE weaken4 #-}

    weakenUnder :: u (e1 ': es) f ~> u (e1 ': e2 ': es) f
    weakenUnder = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2

    weakenUnder2 :: u (e1 ': e2 ': es) f ~> u (e1 ': e2 ': e3 ': es) f
    weakenUnder2 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3

    weakenUnder3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f
    weakenUnder3 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : e4 : es) f
weaken4

    weaken2Under :: u (e1 ': es) f ~> u (e1 ': e2 ': e3 ': es) f
    weaken2Under = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3

    weaken2Under2 :: u (e1 ': e2 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f
    weaken2Under2 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : e4 : es) f
weaken4

    weaken3Under :: u (e1 ': es) f ~> u (e1 ': e2 ': e3 ': e4 ': es) f
    weaken3Under = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : e4 : es) f
weaken4

    flipUnion :: u (e1 ': e2 ': es) f ~> u (e2 ': e1 ': es) f
    flipUnion = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2

    flipUnion3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e3 ': e2 ': e1 ': es) f
    flipUnion3 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3

    flipUnionUnder :: u (e1 ': e2 ': e3 ': es) f ~> u (e1 ': e3 ': e2 ': es) f
    flipUnionUnder = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3

    rot3 :: u (e1 ': e2 ': e3 ': es) f ~> u (e2 ': e3 ': e1 ': es) f
    rot3 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3

    rot3' :: u (e1 ': e2 ': e3 ': es) f ~> u (e3 ': e1 ': e2 ': es) f
    rot3' = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3

    bundleUnion2 :: u (e1 ': e2 ': es) f ~> u (u '[e1, e2] ': es) f
    bundleUnion2 = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken

    bundleUnion3 :: u (e1 ': e2 ': e3 ': es) f ~> u (u '[e1, e2, e3] ': es) f
    bundleUnion3 =
        (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken

    bundleUnion4 ::
        u (e1 ': e2 ': e3 ': e4 ': es) f ~> u (u '[e1, e2, e3, e4] ': es) f
    bundleUnion4 =
        (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h4 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (h3 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h4 f ~> u (h1 : h2 : h3 : h4 : es) f
injectUnder3)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken

    unbundleUnion2 :: u (u '[e1, e2] ': es) f ~> u (e1 ': e2 ': es) f
    unbundleUnion2 = (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust) forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : es) f
weaken2

    unbundleUnion3 :: u (u '[e1, e2, e3] ': es) f ~> u (e1 ': e2 ': e3 ': es) f
    unbundleUnion3 = (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust) forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : es) f
weaken3

    unbundleUnion4 ::
        u (u '[e1, e2, e3, e4] ': es) f
            ~> u (e1 ': e2 ': e3 ': e4 ': es) f
    unbundleUnion4 =
        (forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h2 f ~> u (h1 : h2 : es) f
injectUnder forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h3 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *]).
Union u =>
h3 f ~> u (h1 : h2 : h3 : es) f
injectUnder2 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (h4 :: (* -> *) -> * -> *) (f :: * -> *) (h1 :: (* -> *) -> * -> *)
       (h2 :: (* -> *) -> * -> *) (h3 :: (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]).
Union u =>
h4 f ~> u (h1 : h2 : h3 : h4 : es) f
injectUnder3 forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (f :: * -> *) a x.
Union u =>
u '[] f a -> x
exhaust)
            forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
       (e3 :: (* -> *) -> * -> *) (e4 :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e1 : e2 : e3 : e4 : es) f
weaken4

type HFunctorUnion u = HFunctorUnion_ (ForallHFunctor u) u

-- A hack to avoid the "Quantified predicate must have a class or type variable head" error.
class
    ( Union u
    , forall e es. (HFunctor e, forallHFunctor es) => forallHFunctor (e ': es)
    , forall es. forallHFunctor es => HFunctor (u es)
    , forallHFunctor ~ ForallHFunctor u
    , forallHFunctor '[]
    ) =>
    HFunctorUnion_ forallHFunctor u
        | u -> forallHFunctor
    where
    type ForallHFunctor u :: [SigClass] -> Constraint

$( singletons
    [d|
        data SearchResult = FoundIn FoundLevel | NotFound

        data FoundLevel = CurrentLevel | LowerLevel
        |]
 )

type family FoundLevelOf found :: FoundLevel where
    FoundLevelOf ( 'FoundIn l) = l

type MemberH u e ehs = HasMembershipRec u e ehs
type Member u e efs = MemberH u (LiftIns e) efs

class MemberRec (u :: [SigClass] -> SigClass) e es where
    injectRec :: e f ~> u es f
    projectRec :: u es f a -> Maybe (e f a)

type HasMembershipRec u e es =
    ( SearchMemberRec es u e es
    , HasMembershipRec1_ u e es (Search u es e)
    )

type HasMembershipRec1_ u e es searchResult =
    ( HasMembershipRec2_ u e es (CurrentLevelSearchResult searchResult)
    , SingI (HeadLowerSearchResult searchResult)
    )
type HasMembershipRec2_ u e es found = HasMembershipRec3_ u e es found (FoundLevelOf found)
type HasMembershipRec3_ u e es found lvl =
    ( found ~ 'FoundIn lvl
    , SingI lvl
    , HasMembershipWhenCurrentLevel lvl u e es
    , SearchMemberRecWhenLowerLevel lvl es u e
    )

instance
    ( SearchMemberRec es u e es
    , MemberFound e es (CurrentLevelSearchResult searchResult)
    , searchResult ~ Search u es e
    , SingI (HeadLowerSearchResult searchResult)
    , found ~ CurrentLevelSearchResult searchResult
    ) =>
    MemberRec u e es
    where
    injectRec :: forall (f :: * -> *). e f ~> u es f
injectRec = forall {k} {k} (e :: k) (es :: k) (found :: SearchResult) a.
MemberFound e es found =>
(forall (lvl :: FoundLevel).
 (found ~ 'FoundIn lvl, SingI lvl) =>
 a)
-> a
withFound @e @es @found forall a b. (a -> b) -> a -> b
$ forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *).
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR @es forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). SingI a => Sing a
sing forall {k} (a :: k). SingI a => Sing a
sing
    projectRec :: forall (f :: * -> *) a. u es f a -> Maybe (e f a)
projectRec = forall {k} {k} (e :: k) (es :: k) (found :: SearchResult) a.
MemberFound e es found =>
(forall (lvl :: FoundLevel).
 (found ~ 'FoundIn lvl, SingI lvl) =>
 a)
-> a
withFound @e @es @found forall a b. (a -> b) -> a -> b
$ forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *)
       a.
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR @es forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). SingI a => Sing a
sing forall {k} (a :: k). SingI a => Sing a
sing
    {-# INLINE injectRec #-}
    {-# INLINE projectRec #-}

class MemberFound e es found where
    withFound :: (forall lvl. (found ~ 'FoundIn lvl, SingI lvl) => a) -> a

instance SingI lvl => MemberFound e es ( 'FoundIn lvl) where
    withFound :: forall a.
(forall (lvl :: FoundLevel).
 ('FoundIn lvl ~ 'FoundIn lvl, SingI lvl) =>
 a)
-> a
withFound forall (lvl :: FoundLevel).
('FoundIn lvl ~ 'FoundIn lvl, SingI lvl) =>
a
a = forall (lvl :: FoundLevel).
('FoundIn lvl ~ 'FoundIn lvl, SingI lvl) =>
a
a
    {-# INLINE withFound #-}

-- A stopgap until upgrading to base-4.19.
-- https://hackage.haskell.org/package/base-4.19.0.0/docs/GHC-TypeError.html#t:Unsatisfiable
instance
    TypeError
        ( 'Text "The effect class: " ':<>: 'ShowType e
            ':$$: 'Text " was not found in the union:"
            ':$$: 'Text "    " ':<>: 'ShowType es
        ) =>
    MemberFound e es 'NotFound
    where
    withFound :: forall a.
(forall (lvl :: FoundLevel).
 ('NotFound ~ 'FoundIn lvl, SingI lvl) =>
 a)
-> a
withFound forall (lvl :: FoundLevel).
('NotFound ~ 'FoundIn lvl, SingI lvl) =>
a
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable"

type SearchMemberRec rest u e = SearchMemberRec_ (NextSearchMemberRecAction rest u e) rest u e

class
    SearchMemberRec_
        (act :: SearchMemberRecAction)
        (rest :: [SigClass])
        (u :: [SigClass] -> SigClass)
        (e :: SigClass)
        (es :: [SigClass])
    where
    type Search_ act u rest e :: SearchResults

    injectSMR_ ::
        searchResult ~ Search_ act u rest e =>
        CurrentLevelSearchResult searchResult :~: 'FoundIn lvl ->
        SSearchResult ( 'FoundIn lvl) ->
        SSearchResult (HeadLowerSearchResult searchResult) ->
        e f ~> u es f

    projectSMR_ ::
        searchResult ~ Search_ act u rest e =>
        CurrentLevelSearchResult searchResult :~: 'FoundIn lvl ->
        SSearchResult ( 'FoundIn lvl) ->
        SSearchResult (HeadLowerSearchResult searchResult) ->
        u es f a ->
        Maybe (e f a)

type Search u rest e = Search_ (NextSearchMemberRecAction rest u e) u rest e

injectSMR ::
    forall rest u e es searchResult lvl f.
    (SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
    CurrentLevelSearchResult searchResult :~: 'FoundIn lvl ->
    SSearchResult ( 'FoundIn lvl) ->
    SSearchResult (HeadLowerSearchResult searchResult) ->
    e f ~> u es f
injectSMR :: forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *).
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR = forall (act :: SearchMemberRecAction)
       (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *).
(SearchMemberRec_ act rest u e es,
 searchResult ~ Search_ act u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR_ @(NextSearchMemberRecAction rest u e) @rest
{-# INLINE injectSMR #-}

projectSMR ::
    forall rest u e es searchResult lvl f a.
    (SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
    CurrentLevelSearchResult searchResult :~: 'FoundIn lvl ->
    SSearchResult ( 'FoundIn lvl) ->
    SSearchResult (HeadLowerSearchResult searchResult) ->
    u es f a ->
    Maybe (e f a)
projectSMR :: forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *)
       a.
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR = forall (act :: SearchMemberRecAction)
       (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *)
       a.
(SearchMemberRec_ act rest u e es,
 searchResult ~ Search_ act u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR_ @(NextSearchMemberRecAction rest u e) @rest
{-# INLINE projectSMR #-}

data SearchResults = SearchResults SearchResult SearchResult
type family CurrentLevelSearchResult a where
    CurrentLevelSearchResult ( 'SearchResults a _) = a

type family HeadLowerSearchResult a where
    HeadLowerSearchResult ( 'SearchResults _ a) = a

data SearchMemberRecAction = SmrStop | SmrRight | SmrDown

type family NextSearchMemberRecAction rest (u :: [SigClass] -> SigClass) e where
    NextSearchMemberRecAction (e ': _) u e = 'SmrStop
    NextSearchMemberRecAction (u _ ': _) u e = 'SmrDown
    NextSearchMemberRecAction _ _ _ = 'SmrRight

instance
    (HasMembership u e es, Union u) =>
    SearchMemberRec_ 'SmrStop (e ': _tail) u e es
    where
    type Search_ _ _ (e ': _tail) e = 'SearchResults ( 'FoundIn 'CurrentLevel) 'NotFound

    injectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel)
       (f :: * -> *).
(searchResult ~ Search_ 'SmrStop u (e : _tail) e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR_ CurrentLevelSearchResult searchResult :~: 'FoundIn lvl
_ SSearchResult ('FoundIn lvl)
_ SSearchResult (HeadLowerSearchResult searchResult)
_ = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (f :: * -> *).
(Union u, HasMembership u e es) =>
e f ~> u es f
inject
    projectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel)
       (f :: * -> *) a.
(searchResult ~ Search_ 'SmrStop u (e : _tail) e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR_ CurrentLevelSearchResult searchResult :~: 'FoundIn lvl
_ SSearchResult ('FoundIn lvl)
_ SSearchResult (HeadLowerSearchResult searchResult)
_ = forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (f :: * -> *) a.
(Union u, HasMembership u e es) =>
u es f a -> Maybe (e f a)
project
    {-# INLINE injectSMR_ #-}
    {-# INLINE projectSMR_ #-}

type family IsFound found where
    IsFound ( 'FoundIn _) = 'True
    IsFound 'NotFound = 'False

instance
    ( SearchMemberRec es' u e es'
    , headSearchResults ~ Search u es' e
    , tailSearchResults ~ Search u tail e
    , isFoundInHead ~ IsFound (CurrentLevelSearchResult headSearchResults)
    , If isFoundInHead (HasMembership u (u es') es) (() :: Constraint)
    , SearchMemberRec (If isFoundInHead '[] tail) u e es
    , Union u
    , SingI (HeadLowerSearchResult headSearchResults)
    , SingI (HeadLowerSearchResult tailSearchResults)
    ) =>
    SearchMemberRec_ 'SmrDown (u es' ': tail) u e es
    where
    type
        Search_ _ _ (u es' ': tail) e =
            SearchResultsOnSmrDown
                u
                es'
                tail
                e
                (CurrentLevelSearchResult (Search u es' e))
                (CurrentLevelSearchResult (Search u tail e))

    injectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel)
       (f :: * -> *).
(searchResult ~ Search_ 'SmrDown u (u es' : tail) e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR_ CurrentLevelSearchResult searchResult :~: 'FoundIn lvl
Refl SSearchResult ('FoundIn lvl)
found = \case
        SFoundIn Sing n
lvl -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (f :: * -> *).
(Union u, HasMembership u e es) =>
e f ~> u es f
inject forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *).
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR @es' @u @_ @es' forall {k} (a :: k). a :~: a
Refl (forall (arg :: FoundLevel).
Sing arg -> SSearchResult ('FoundIn arg)
SFoundIn Sing n
lvl) forall {k} (a :: k). SingI a => Sing a
sing
        SSearchResult (HeadLowerSearchResult searchResult)
SNotFound -> forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *).
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR @tail forall {k} (a :: k). a :~: a
Refl SSearchResult ('FoundIn lvl)
found forall {k} (a :: k). SingI a => Sing a
sing

    projectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel)
       (f :: * -> *) a.
(searchResult ~ Search_ 'SmrDown u (u es' : tail) e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR_ CurrentLevelSearchResult searchResult :~: 'FoundIn lvl
Refl SSearchResult ('FoundIn lvl)
found = \case
        SFoundIn Sing n
lvl -> forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *)
       a.
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR @es' @u @_ @es' forall {k} (a :: k). a :~: a
Refl (forall (arg :: FoundLevel).
Sing arg -> SSearchResult ('FoundIn arg)
SFoundIn Sing n
lvl) forall {k} (a :: k). SingI a => Sing a
sing forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (f :: * -> *) a.
(Union u, HasMembership u e es) =>
u es f a -> Maybe (e f a)
project
        SSearchResult (HeadLowerSearchResult searchResult)
SNotFound -> forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *)
       a.
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR @tail forall {k} (a :: k). a :~: a
Refl SSearchResult ('FoundIn lvl)
found forall {k} (a :: k). SingI a => Sing a
sing

    {-# INLINE injectSMR_ #-}
    {-# INLINE projectSMR_ #-}

type SearchResultsOnSmrDown u es' tail e foundInHead foundInTail =
    'SearchResults
        (If (IsFound foundInHead) ( 'FoundIn 'LowerLevel) foundInTail)
        foundInHead

instance
    ( HasMembershipWhenCurrentLevel lvl u e (_e ': rest)
    , SearchMemberRecWhenLowerLevel lvl rest u e
    , SingI (HeadLowerSearchResult searchResult)
    , Union u
    , searchResult ~ Search u rest e
    , lvl ~ FoundLevelOf (CurrentLevelSearchResult searchResult)
    ) =>
    SearchMemberRec_ 'SmrRight (_e ': rest) u e (_e ': rest)
    where
    type Search_ _ u (_ ': rest) e = 'SearchResults (CurrentLevelSearchResult (Search u rest e)) 'NotFound

    injectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel)
       (f :: * -> *).
(searchResult ~ Search_ 'SmrRight u (_e : rest) e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u (_e : rest) f
injectSMR_ CurrentLevelSearchResult searchResult :~: 'FoundIn lvl
Refl (SFoundIn Sing n
lvl) SSearchResult (HeadLowerSearchResult searchResult)
_ = case Sing n
lvl of
        Sing n
SFoundLevel lvl
SCurrentLevel -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (f :: * -> *).
(Union u, HasMembership u e es) =>
e f ~> u es f
inject
        Sing n
SFoundLevel lvl
SLowerLevel -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (es :: [(* -> *) -> * -> *]) (f :: * -> *)
       (e :: (* -> *) -> * -> *).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *).
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR @rest forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). SingI a => Sing a
sing forall {k} (a :: k). SingI a => Sing a
sing

    projectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel)
       (f :: * -> *) a.
(searchResult ~ Search_ 'SmrRight u (_e : rest) e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u (_e : rest) f a
-> Maybe (e f a)
projectSMR_ CurrentLevelSearchResult searchResult :~: 'FoundIn lvl
Refl (SFoundIn Sing n
lvl) SSearchResult (HeadLowerSearchResult searchResult)
_ = case Sing n
lvl of
        Sing n
SFoundLevel lvl
SCurrentLevel -> forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (f :: * -> *) a.
(Union u, HasMembership u e es) =>
u es f a -> Maybe (e f a)
project
        Sing n
SFoundLevel lvl
SLowerLevel -> forall a b. a -> b -> a
const forall a. Maybe a
Nothing forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (rest :: [(* -> *) -> * -> *])
       (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (es :: [(* -> *) -> * -> *])
       (searchResult :: SearchResults) (lvl :: FoundLevel) (f :: * -> *)
       a.
(SearchMemberRec rest u e es, searchResult ~ Search u rest e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR @rest forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). SingI a => Sing a
sing forall {k} (a :: k). SingI a => Sing a
sing

    {-# INLINE injectSMR_ #-}
    {-# INLINE projectSMR_ #-}

instance SearchMemberRec_ act '[] u e es where
    type Search_ _ _ _ _ = 'SearchResults 'NotFound 'NotFound
    injectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel)
       (f :: * -> *).
(searchResult ~ Search_ act u '[] e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> e f ~> u es f
injectSMR_ = \case {}
    projectSMR_ :: forall (searchResult :: SearchResults) (lvl :: FoundLevel)
       (f :: * -> *) a.
(searchResult ~ Search_ act u '[] e) =>
(CurrentLevelSearchResult searchResult :~: 'FoundIn lvl)
-> SSearchResult ('FoundIn lvl)
-> SSearchResult (HeadLowerSearchResult searchResult)
-> u es f a
-> Maybe (e f a)
projectSMR_ = \case {}
    {-# INLINE injectSMR_ #-}
    {-# INLINE projectSMR_ #-}

-- A hack to avoid the "Quantified predicate must have a class or type variable head" error.

type HasMembershipWhenCurrentLevel lvl u e es =
    HasMembershipWhenCurrentLevel_ (HasMembership u e es) lvl u e es
class
    (lvl ~ 'CurrentLevel => c, c ~ HasMembership u e es) =>
    HasMembershipWhenCurrentLevel_ c lvl u e es
        | u e es -> c
instance
    (lvl ~ 'CurrentLevel => c, c ~ HasMembership u e es) =>
    HasMembershipWhenCurrentLevel_ c lvl u e es

type SearchMemberRecWhenLowerLevel lvl rest u e =
    SearchMemberRecWhenLowerLevel_ (SearchMemberRec rest u e rest) lvl rest u e
class
    (lvl ~ 'LowerLevel => c, c ~ SearchMemberRec rest u e rest) =>
    SearchMemberRecWhenLowerLevel_ c lvl rest u e
        | rest u e -> c
instance
    (lvl ~ 'LowerLevel => c, c ~ SearchMemberRec rest u e rest) =>
    SearchMemberRecWhenLowerLevel_ c lvl rest u e

infixr 5 |+
(|+) :: Union u => (e a -> r) -> (u es f a -> r) -> u (LiftIns e ': es) f a -> r
e a -> r
f |+ :: forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: * -> *) a r (es :: [(* -> *) -> * -> *]) (f :: * -> *).
Union u =>
(e a -> r) -> (u es f a -> r) -> u (LiftIns e : es) f a -> r
|+ u es f a -> r
g = e a -> r
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (ins :: * -> *) (f :: * -> *) a. LiftIns ins f a -> ins a
unliftIns forall (u :: [(* -> *) -> * -> *] -> (* -> *) -> * -> *)
       (e :: (* -> *) -> * -> *) (f :: * -> *) a r
       (es :: [(* -> *) -> * -> *]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: u es f a -> r
g
{-# INLINE (|+) #-}

{- |
Recursively decompose the sum of first-order effects into a list, following the direction of right
association, with normalization.
-}
type U u ef = UH u (LiftIns ef)

{- |
Recursively decompose the sum of higher-order effects into a list, following the direction of right
association, with normalization.
-}
type UH u eh = SumToUnionList u (NormalizeSig eh)

{- |
Recursively decompose the sum of higher-order effects into a list, following the direction of right
association.
-}
type family SumToUnionList (u :: [SigClass] -> SigClass) (e :: SigClass) :: [SigClass] where
    SumToUnionList u (e1 :+: e2) = MultiListToUnion u (SumToUnionList u e1) ': SumToUnionList u e2
    SumToUnionList u LNop = '[]
    SumToUnionList u (SingleSig e) = '[e]

{- |
Convert a given list of higher-order effect classes into a suitable representation type for each
case of being empty, single, or multiple.
-}
type family MultiListToUnion (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where
    MultiListToUnion u '[] = LNop
    MultiListToUnion u '[e] = e
    MultiListToUnion u es = u es

{- |
Normalization in preparation for decomposing the sum of effect classes into a list.

In particular, mark an indivisible, single effect class by applying the t'SingleSig' wrapper to it.
-}
type family NormalizeSig e where
    NormalizeSig LNop = LNop
    NormalizeSig (LiftIns (e1 + e2)) = NormalizeSig (LiftIns e1) :+: NormalizeSig (LiftIns e2)
    NormalizeSig (e1 :+: e2) = NormalizeSig e1 :+: NormalizeSig e2
    NormalizeSig e = SingleSig e

{- |
A wrapper to mark a single, i.e., a higher-order effect class that cannot be further decomposed as
a sum.
-}
newtype SingleSig (e :: SigClass) f a = SingleSig {forall (e :: (* -> *) -> * -> *) (f :: * -> *) a.
SingleSig e f a -> e f a
unSingleSig :: e f a}
    deriving newtype (forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> SingleSig e f :-> SingleSig e g
forall (e :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor e =>
(f :-> g) -> SingleSig e f :-> SingleSig e g
forall (h :: (* -> *) -> * -> *).
(forall (f :: * -> *) (g :: * -> *). (f :-> g) -> h f :-> h g)
-> HFunctor h
hfmap :: forall (f :: * -> *) (g :: * -> *).
(f :-> g) -> SingleSig e f :-> SingleSig e g
$chfmap :: forall (e :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor e =>
(f :-> g) -> SingleSig e f :-> SingleSig e g
HFunctor)

type family UnionListToSum (u :: [SigClass] -> SigClass) (es :: [SigClass]) :: SigClass where
    UnionListToSum u '[e] = UnionToSum u e
    UnionListToSum u '[] = LNop
    UnionListToSum u (e ': r) = UnionToSum u e :+: UnionListToSum u r

type family UnionToSum (u :: [SigClass] -> SigClass) (e :: SigClass) :: SigClass where
    UnionToSum u (u es) = UnionListToSum u es
    UnionToSum u e = e

type S u es = UnionListToSum u es Nop
type SH u es = UnionListToSum u es

type NormalFormUnionList u es = U u (S u es) ~ es
type NormalFormUnionListH u es = UH u (SH u es) ~ es

type NFU u es = NormalFormUnionList u es
type NFUH u es = NormalFormUnionListH u es

type HeadIns le = LiftInsIfSingle (UnliftIfSingle le) le

type family UnliftIfSingle e where
    UnliftIfSingle (LiftIns e) = e
    UnliftIfSingle e = e Nop

class LiftInsIfSingle e le where
    liftInsIfSingle :: e ~> le Nop
    unliftInsIfSingle :: le Nop ~> e

instance LiftInsIfSingle (e Nop) e where
    liftInsIfSingle :: e Nop ~> e Nop
liftInsIfSingle = forall a. a -> a
id
    unliftInsIfSingle :: e Nop ~> e Nop
unliftInsIfSingle = forall a. a -> a
id
    {-# INLINE liftInsIfSingle #-}
    {-# INLINE unliftInsIfSingle #-}

instance LiftInsIfSingle e (LiftIns e) where
    liftInsIfSingle :: e ~> LiftIns e Nop
liftInsIfSingle = forall (ins :: * -> *) (f :: * -> *) a. ins a -> LiftIns ins f a
LiftIns
    unliftInsIfSingle :: LiftIns e Nop ~> e
unliftInsIfSingle = forall (ins :: * -> *) (f :: * -> *) a. LiftIns ins f a -> ins a
unliftIns
    {-# INLINE liftInsIfSingle #-}
    {-# INLINE unliftInsIfSingle #-}

type family ClassIndex (es :: [SigClass]) (e :: SigClass) :: Nat where
    ClassIndex (e ': es) e = 0
    ClassIndex (_ ': es) e = 1 N.+ ClassIndex es e
    ClassIndex '[] e =
        TypeError
            ( 'Text "The effect class ‘" ':<>: 'ShowType e ':<>: 'Text "’ was not found in the list.")

-- keyed effects

type MemberBy u key e efs = (Member u (key #> e) efs, Lookup key efs ~ 'Just (LiftIns (key #> e)))
type MemberHBy u key e ehs = (MemberH u (key ##> e) ehs, Lookup key ehs ~ 'Just (key ##> e))

type family Lookup (key :: k) es :: Maybe SigClass where
    Lookup key (key ##> e ': _) = 'Just (key ##> e)
    Lookup key (LiftIns (key #> e) ': _) = 'Just (LiftIns (key #> e))
    Lookup key (u es ': es') = Lookup key es `OrElse` Lookup key es'
    Lookup key (_ ': es) = Lookup key es
    Lookup key '[] = 'Nothing

type family OrElse (a :: Maybe k) (b :: Maybe k) :: Maybe k where
    OrElse ( 'Just a) _ = 'Just a
    OrElse 'Nothing a = a