How to use raiseUnder2 - Polysemy

  -- | Cut a `Methodology` into two pieces at a midpoint.
  cutMethodology :: forall b c d r a.
                    Members '[ Methodology b c
                             , Methodology c d] r
                 => Sem (Methodology b d ': r) a
                 -> Sem r a
  cutMethodology = interpret \case
    Process b -> process @b @c b >>= process @c @d

cutMethodology' :: forall b c d r a.
                         Sem (Methodology b d ': r) a
                    -> Sem (Methodology b c ': Methodology c d ': r) a
cutMethodology' = raiseUnder2 >>> cutMethodology @b @c @d

error:
    • Couldn't match ‘c’ with ‘b’
        arising from a use of ‘cutMethodology’
      ‘c’ is a rigid type variable bound by
        cutMethodology' :: forall b c d (r :: [(* -> *) -> * -> *]) a.
                             Sem (Methodology b d : r) a
                             -> Sem (Methodology b c : Methodology c d : r) a
        at /home/lc/Source/gitlab.com/homotopic-tech/flashblast/src/FlashBlast/Domain.hs:(51,1)-(53,72)
      ‘b’ is a rigid type variable bound by
        cutMethodology' :: forall b c d (r :: [(* -> *) -> * -> *]) a.
                             Sem (Methodology b d : r) a
                             -> Sem (Methodology b c : Methodology c d : r) a
        at /home/lc/Source/gitlab.com/homotopic-tech/flashblast/src/FlashBlast/Domain.hs:(51,1)-(53,72)
    • Known types:
        cutMethodology' :: Sem (Methodology b d : r) a
                           -> Sem (Methodology b c : Methodology c d : r) a
           -- /home/lc/Source/gitlab.com/homotopic-tech/flashblast/src/FlashBlast/Domain.hs:54:1
   |
54 | cutMethodology' = raiseUnder2 >>> cutMethodology @b @c @d

cutMethodology' :: forall r a.
                           Sem (Methodology Text Int ': r) a
                        -> Sem (Methodology Text String ': Methodology String Int ': r) a
 cutMethodology' = raiseUnder2 >>> cutMethodology

cutMethodology' :: forall b c d r a.
                           Sem (Methodology b d ': r) a
                      -> Sem (Methodology b c ': Methodology c d ': r) a
cutMethodology' f = f & raiseUnder2 @(Methodology b c) @(Methodology c d)
                        & cutMethodology @b @c @d

let
  sem' :: Sem (Methodology b d : Methodology b c : Methodology c d : r) a
  sem' = raiseUnder2 sem

  cutMethodology' :: forall b c d r a.
                           Sem (Methodology b d ': r) a
                      -> Sem (Methodology b c ': Methodology c d ': r) a
  cutMethodology' f =
    let
      sem' :: Sem (Methodology b d : Methodology b c : Methodology c d : r) a
      sem' = raiseUnder2 f
   in sem' & cutMethodology @b @c @d

  cutMethodology' :: forall b c d r a.
                           Sem (Methodology b d ': r) a
                      -> Sem (Methodology b c ': Methodology c d ': r) a
  cutMethodology' f =
    let
      sem' :: Sem (Methodology b d : Methodology b c : Methodology c d : r) a
      sem' = raiseUnder2 f
 in sem' & cutMethodology @b @c @d @(Methodology b c ': Methodology c d ': r)

bla :: forall b c d r a. Sem (Methodology b d : Methodology b c : Methodology c d : r) a -> Sem (Methodology b c : Methodology c d : r) a
bla = cutMethodology @b @c @d @(Methodology b c : Methodology c d : r)

  cutMethodology'' :: forall b c d r a.
                           Sem (Methodology b d ': r) a
                      -> Sem (Methodology b c ': Methodology c d ': r) a
  cutMethodology'' = reinterpret2 \case
   Process b -> process @b @c b >>= process @c @d t

    Ambiguous use of effect 'Methodology'
    ---
    Maybe-fix:
      add (Member (Methodology c d) (Methodology b c
                                       : Methodology c d : r)) to the context of
        the type signature
    If you already have the constraint you want, instead
      add a type application to specify
        'c', and 'd' directly, or activate polysemy-plugin which
          can usually infer the type correctly.
   |
64 |   Process b -> process @b @c b >>= process @c @d

f :: forall a b c r. Member (Methodology b c) r => Sem (Methodology a b ': r) a -> Sem r a
f = undefined

bla2 :: Sem (Methodology a b ': Methodology b c ': r) a -> Sem (Methodology b c ': r) a
bla2 = f

g :: (Member (Methodology a b) r, Member (Methodology b c) r) => Proxy (Methodology a c ': r) -> Proxy r
g = undefined

h :: forall a b c r. Proxy (Methodology a c : Methodology a b : Methodology b c : r) -> Proxy (Methodology a b : Methodology b c : r)
h = g

data Methodology' (sym :: Nat) a b

data Wrap1 a

data Wrap2 a

g :: (Member (Wrap1 (Methodology' n2 a b)) r, Member (Wrap2 (Methodology' n3 b c)) r) => Proxy ((Methodology' n1 a c) ': r) -> Proxy r
g = undefined

h :: Proxy ((Methodology' 0 a c) : Wrap1 (Methodology' 1 a b) : Wrap2 (Methodology' 2 b c) : r) -> Proxy (Wrap1 (Methodology' 1 a b) : Wrap2 (Methodology' 2 b c) : r)
h = g

data Methodology' a b

data Wrap0 a

data Wrap1 a

data Wrap2 a

g :: (Member (Wrap1 (Methodology' a b)) r, Member (Wrap2 (Methodology' b c)) r) => Proxy (W  rap0 (Methodology' a c) ': r) -> Proxy r typecheck: • Redundant constraints: (Member (Wrap1
g = undefined

h :: Proxy (Wrap0 (Methodology' a c) : Wrap1 (Methodology' a b) : Wrap2 (Methodology' b c)   : r) -> Proxy (Wrap1 (Methodology' a b) : Wrap2 (Methodology' b c) : r)
h = g

data Methodology' a b

data Wrap a

g :: (Member ((Methodology' a b)) r, Member (Wrap (Methodology' b c)) r) => Proxy ((Methodology' a c) ': r) -> Proxy r
g = undefined

h :: Proxy ((Methodology' a c) : (Methodology' a b) : Wrap (Methodology' b c) : r) -> Proxy ((Methodology' a b) : Wrap (Methodology' b c) : r)
h = g