I kind of feel we should generalize this data family and add it to its own package. (or to reflection possibly), with the intent that we could generate these with Template Haskell, probably:

data family Reified (c :: Constraint)

(and we would transform Reified tag c m into Reified (c m).

The tag disappears, in this transformation. This is fishy, do we actually need the tag in the current presentation?

Reified was a convenient location to attach the tag for interpret_ and interpret to ship it into the action. The suggested transformation is possible, then we just need to find another way to transport the tag into the action of interpret.

What I mean is the following. Take this example:

example :: [()]
example =
  interpret_ @"sink"
    ReifiedSink { _yield = (:[]) }
    (do yield @"sink" (); yield @"sink" ())

And assume

data family Reified (c :: Constraint)
interpret_ :: forall tag c m a.
  (Monad m, forall s. Reifies s (Reified (c m)) => c (Reflected s c m)) =>
  Reified (c m) -> (forall m'. c m' => m' a) -> m a

Then we will get the following type error on example:

    • Could not deduce (HasSink "sink" () m')
        arising from a use of ‘yield’
      from the context: HasSink tag0 () m'
        bound by a type expected by the context:
                   forall (m' :: * -> *). HasSink tag0 () m' => m' ()

I.e. it hasn't inferred tag0 ~ "sink" because there is no such constraint between tag and c.

A user would have to provide a type annotation to the ReifiedSink constructor to set the tag, for example

  interpret_
    (ReifiedSink { _yield = (:[]) } :: Reified (HasSink "sink" () []))
    (do yield @"sink" (); yield @"sink" ())

That's pretty clumsy to write. Is there a way to use TypeApplications on record constructors? I tried the following, which don't work

ReifiedSink @_ @"sink" { _yield = ... }
ReifiedSink { _yield = ... } @_ @"sink"

I've found two other ways that allow the same API to interpret_.

1. Be explicit about the tag in the capability, i.e. use the following type for interpret_:

   interpret_ :: forall tag c m v a.
     (Monad m, forall s. Reifies s (Reified (c tag v m)) => c tag v (Reflected s (c tag v) m)) =>
     Reified (c tag v m) -> (forall m'. c tag v m' => m' a) -> m a
   

   I'm not too fond of this approach because it hard codes that capabilities should have the kind tag -> value -> (* -> *) -> Constraint. This happens to be the case so far, because all capabilities have some sort of value type parameter, e.g. the r in HasReader tag r or the w in HasWriter tag w. But, this seems coincidental. Why shouldn't there be a capability with none, or two, or more value type parameters?
   Maybe the shape of capabilities should have been value -> tag -> (* -> *) -> Constraint, e.g. HasReader r tag, then we could use c tag m in interpret_ without making assumptions about the number of value type parameters.
2. Define an additional constraint, say TagOf tag c, and use it as follows

   interpret_ :: forall tag c m a.
     (TagOf tag c, Monad m, forall s. Reifies s (Reified (c m)) => c (Reflected s c m)) =>
     Reified (c m) -> (forall m'. (TagOf tag c, c m') => m' a) -> m a
   

   This enforces that c has the tag without hard-coding the number of value type parameters.
   This requires some boilerplate when defining a new capability though, e.g. instances of the form

   instance tag ~ tag' => TagOf tag (HasReader tag' r)
   

   (The example takes a short cut with instance tag ~ tag' => TagOf tag (c tag' v), but that seems to conflict with instances for capabilities with different number of value type parameters.)

Out of all those, attaching tag to Reified seemed like the least bad option.

Ah, yes, this makes it a bit annoying to generate with template haskell (even eventually). Maybe template haskell lets us access super-classes and iterate on them.

Yes, I think it does, ClassD carries a Cxt which boils down to a [Type]. I'm guessing that's going to be a bunch of AppT for all super class constraints.