What is the role of localEs when it can be bypassed without localUnlift?

[torgeirsh]

Consider this contrived effect:

data SomeEffect :: Effect where
    Something :: Eff localEs a -> SomeEffect (Eff localEs) a

runSomeEffect :: Eff (SomeEffect : es) a -> Eff es a

Usually in order to interpret it, one would have to use localUnlift to convert localEs to es, which involves specifying an unlift strategy. However, we can change the definition a bit:

data SomeEffect localEs :: Effect where
    Something :: Eff localEs a -> SomeEffect localEs (Eff localEs) a

runSomeEffect :: Eff (SomeEffect es : es) a -> Eff es a

Now the interpreter knows that localEs and es are the same, so localUnlift isn't needed, which bypasses the unlift strategy. That seems bad, because one would think the unlift strategy is there for a reason, but on the other hand, the effects "below" SomeEffect are known by runSomeEffect to be es either way, so the distinction between es and localEs seems artificial. Am I missing something? Is the hack that bypasses localUnlift safe or bad?

[arybczak]

It's absolutely fine. Why do you call it a hack? 🙂 You're simply restricting the actions taken by Something to work in the effect stack at the point of running the effect.

Such effect has awkward usability though. Try running it, then putting one or more additional effect on the effect stack and invoke Something 2-3 functions deeper down the call stack.

[torgeirsh]

@arybczak I've tried to reduce the problem further, and found that this compiles:

test1 :: forall e es a. Eff es a -> Eff ('[e] ++ es) a
test1 = inject @es @('[e] ++ es)

But this doesn't (Couldn't match type ‘es’ with ‘e ++ es’):

test2 :: forall e es a. Eff es a -> Eff (e ++ es) a
test2 = inject @es @(e ++ es)

Perhaps this is the core issue that prevents the inject in the last line of runExample in the previous post from being compiled? I can make test2 compile by adding a "Subset es (e ++ es)" constraint, but that's just moves the compile error to the call site. In runExample, the tail of the effect stack is the universally quantified localEs introduced by interpret, so I can't add a similar Subset constraint, unless I redefine interpret:

interpret2 ::
    forall otherEs lendEs e es a. (HasCallStack, DispatchOf e ~ Dynamic) =>
    (forall a localEs. (Subset (otherEs ++ localEs) (otherEs ++ lendEs ++ localEs), HasCallStack, e :> localEs) => LocalEnv localEs es -> e (Eff localEs) a -> Eff es a) ->
    Eff (e : es) a ->
    Eff es a
interpret2 = undefined

That actually does make the code in the previous post compile, but is obviously not practical. :)

[arybczak]

Does this work when you write a working implementation of this modified interpret? You can copy paste it from effectful (you'll most likely have to inline interpretImpl though). Perhaps this is an acceptable compromise for this particular case 🤔

[torgeirsh]

I just realised that the type errors have distracted me from the fact that the scoping of the example problem isn't exactly what I need. I don't actually want to call f inside interpret in runExample, instead I want to use it with reinterpret. That means the effect stack in f no longer has to be universally quantified, and all the problems go away. Sorry for that, I feel a bit silly now. :D

With that problem out of the way, I found myself with effect stacks containing ++, and quickly ran into errors along the lines of "Could not deduce ‘SomeEffect :> (es1 ++ es2)’". It works if es1 is an actual list instead of a variable, so I guess :> only works with ++ if es1 is known? Is that a fundamental limitation, or something that could be worked around with a mechanism similar to KnownPrefix or other such type constraints?

[arybczak]

It works if es1 is an actual list instead of a variable, so I guess :> only works with ++ if es1 is known?

I guess you have e :> es1 and it can't deduce e :> (es1 ++ es2) from this? If so, it's a common problem with unreduced type families. GHC doesn't see any relation between es1 and es1 ++ es2 if es1 is not a fully known list.

[torgeirsh]

Yes, that's exactly the situation. Is there also no way to make it work with a typeclass constraint acting as a proof?