Transitivity of Members

[adamConnerSax]

I know a question like this has been asked before but I think I have a different version. Maybe.

The basic question is should a context of
Members es r
allow GHC to deduce
Members es (Eff0 ': r)

I would think it would. But I'm running into something where that seems to fail.
From reading through the last time this was asked, I imagine I may just be doing something silly.

I'm trying to pass around a thing, which is, more or less,

data RunnableThing es a where
  RunnableThing :: (forall r .Members es r => Sem r a) -> RunnableThing es a

that has, as a type parameter, a list of effects that need to be available for it to be "run". That's the es in the above. It works, as in, I can run it, with

f :: Members es r => RunnableThing es a -> Sem r b
f (RunnableThing t) runEffs = do
  --some other things
  t
  -- more things
 return ()

But if I try to hand t off to a different function, running in a larger stack:

runEff0 :: Sem (Eff0 ': r) a -> Sem r a
runEff0 = ..

g :: (Members es r, Member Eff0 r) => RunnableThing es a -> Sem r' a
g = ...

f :: Members es r => RunnableThing es a -> Sem r b
f (RunnableThing t) runEffs = do
  --some other things
  runEff0 $ g t
  -- more things
 return ()

I get an error like the above. In my case, I can get around it by making the stacks the same but I'm confused...

[TheMatten]

It won't - it would be potentially possible if Member was defined inductively as a class, but instead it is a type family that will be stuck until it gets supplied with concrete arguments. Maybe we want to consider changing it to class, but that touches optimization and possibly other things around interface and will need to be further discussed.

[adamConnerSax]

Ah. Thanks! That makes sense. Would it be possible to have both? To define a class and then warn that it's possibly less optimal? Just for use in cases like this. I'll think about it, I guess.

[TheMatten]

It should be possible, but I would rather not duplicate interface in this way. We need to solve this properly.

It is a relevant issue for sure though - let's keep it open for now.

[expipiplus1]

This would be a really handy thing to have for dealing with Sem values in negative positions!

On a similar topic it would be nice for Members to be reflexive too. It's not nice for GHC to tell me that it can't deduct Members r r :)

It should be possible to conjure up this witness if one had a singleton of the effect list or (equivalently) some KnownEffects es constraint. I guess this is just another description of the class @adamConnerSax was proposing.

[isovector]

I looked into doing this tonight, but it's unclear how exactly. The problem is today we assume Members is an alias for a bunch of Members. Fine, but if we wanted to do some induction stuff, we could instead write this:

class Members (es :: EffectRow) (r :: EffectRow)
instance (Members es r, Member e r) => Members (e : es) r
instance Members '[] r

which compiles, except that now we can't go from Members to Members since we don't have an appropriate superclass constraint.