# Raising a singleton effect row? - Polysemy

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

I want to implement `lift :: Member e r => Sem '[e] a -> Sem r a`. `Raise` doesn't work for my purposes because everything is necessarily polymorphic and the instances don't terminate

Hmm, maybe you could just go through `Sem`, unpacking that `Union` with single effect and sending it further?

yeah, was trying that, but the types make my head spin

who wrote this library even??

Wait, couldn't you just raise it over `Embed (Sem r)`, interpret into it and call `runEmbedded`?

now that's an interesting idea

this seems to do it:

``````inject :: forall eff r a. Member eff r => Sem '[eff] a -> Sem r a
inject (Sem a) = Sem \$ \k -> a \$ \case
Union Here (Weaving e s f n v) ->
k \$ Union (membership @eff) \$ Weaving e s (inject . f) n v
``````

amazing what a nap can do

full solution:

``````inject :: Inject effs r => Sem effs a -> Sem r a
inject (Sem a) = a \$ liftSem . deject . hoist inject

class Inject effs r where
deject :: Union effs (Sem r) a -> Union r (Sem r) a

instance Inject '[] r where
deject = absurdU

instance (Member eff r, Inject effs r) => Inject (eff ': effs) r where
deject u =
case decomp u of
Left  u' -> deject u'
Right w  -> Union membership w
``````

starting to get my sea legs back

``````    • Could not deduce: Members effs effs arising from a use of ‘gen’
``````
``````type family Members2 es r :: Constraint where
Members2 r         r = ()
Members2 '[]       r = ()
Members2 (e ': es) r = (Member e r, Members2 es r)

works great
``````

no, doesnt seem to work great actually

adding `Members effs effs` to the context works /shrug

put this all together to make some stuff that can prove equivalence of interpreters https://gist.github.com/isovector/681d15e9ca398692278df3612dcfc3cd