Cannot Lift through Stream

[aherrmann]

Attempting to apply the Lift strategy on Stream (Of a) to access an underlying MonadState produces a type error in a coercion. In the example to derive HasSource, the same error occurs for HasSink and HasState.

newtype MyStates a = MyStates (Stream (Of String) (State Bool) a)
  deriving (Functor, Applicative, Monad)
  deriving (HasSource () Bool) via
    Lift (Stream (Of String) (MonadState (State Bool)))

    • Couldn't match type ‘StateT Bool Data.Functor.Identity.Identity’
                     with ‘MonadState (State Bool)’
        arising from the coercion of the method ‘await_’
          from type ‘ghc-prim-0.5.3:GHC.Prim.Proxy# ()
                     -> Lift (Stream (Of String) (MonadState (State Bool))) Bool’
            to type ‘ghc-prim-0.5.3:GHC.Prim.Proxy# () -> MyStates Bool’
    • When deriving the instance for (HasSource () Bool MyStates)
   |
70 |   deriving (HasSource () Bool) via
   |             ^^^^^^^^^^^^^^^^^

This has been observed on master with GHC 8.6.5 and GHC 8.8.1.

The same issue is also present in version 0.2.0.0 of capability with an adjusted reproduction

newtype MyStates a = MyStates (Stream (Of String) (State Bool) a)
  deriving (Functor, Applicative, Monad)
    deriving (HasState () Bool) via
        Lift (Stream (Of String) (MonadState (State Bool)))

[aspiwack]

> :info Stream
type role Stream nominal nominal nominal
data Stream (f :: * -> *) (m :: * -> *) r

Indeed…

It's the inferred role too, because m appears (because of recursion) under m (and f), and f may be nominal (there is not, at this point, a way to give a more precise value to these roles (see the higher-order role proposal).

Basically, we would want some instance of the form

instance
   ((forall a b. Coercible a b => Coercible (f a) (g b))
  , (forall a b. Coercible a b => Coercible (m a) (n b))
  , Coercible a b)
   => Coercible (Stream f m a) (Stream g n b)

But I don't think there is a way to write such an instance in GHC today. So I'm not sure there will be a solution for a while.

[mboes]

Worth a ticket on the GHC issue tracker. Which could become a GHC proposal eventually. Is what your are looking for a slight generalization of -XQuantifiedConstraints?

[goldfirere]

This looks like the the higher-order role proposal. I thought it would be easy and lightweight, but it needs a proof of correctness before proceeding. That said, I don't think it would take me more than a day to belt out.

[mboes]

It sounds like that proposal is fairly straightforward to implement. If convincing ourselves of soundness is matter of just a day or two, then I guess there's not much on the critical path to getting this proposal accepted, implemented, and shipping in GHC. @aherrmann @aspiwack are we sure that @goldfirere's proposal would unblock this particular ticket?

[aspiwack]

Well, I'm not sure. The problem that we would face, then, is to add a bunch of weird-looking constraints to the declaration of the Stream datatype. Which is in a public library, and it may not be acceptable to make such a change there.

That is, we will want

data
   ((forall a b. Coercible a b => Coercible (f a) (f b)),
    (forall a b. Coercible a b => Coercible (m a) (m b)) =>
   Stream f m a = …

These are not unreasonable constraints, as far as I can tell (though experience would tell). But it would make the streaming package a tad more tricky (we also would have to add such constraint on every function which is polymorphic on either f or m, wouldn't we?).

[mboes]

Sounds like constraints nearly all datatypes would want to have. Could we make them implicit?

[goldfirere]

Despite my interest in datatype contexts, I don't think we should use them here. Instead, we can put the contexts on e.g. instances and functions. To make them simpler, we could always have

type Representational :: forall k1 k2. (k1 -> k2) -> Constraint
type Representational (f :: k1 -> k2) = (forall (a :: k1) (b :: k1). Coercible a b => Coercible (f a) (f b))

and then use Representational constraints, which is less scary-looking.

[aspiwack]

In this case, we need to make the roles of Stream representational in each argument. Within the scope of your proposal, as I understand it, either we put the constraint on the datatype context, or in the data constructor contexts. Maybe the latter is better (though may add in performance costs without optimisation), especially since it doesn't require copying the constraint everywhere.

But you are suggesting “we can put the contexts on e.g. instances and functions”, and I don't see how that works.

PS: I don't think that you can currently put universally quantified constraints in type synonyms. Last time I tried, anyway, it failed some impredicativity check.

[goldfirere]

Oof -- you're right. I forgot about the details of the proposal when I wrote my last comment. But I do think the Representational synonym should work... we just can't make a tuple of such things.

[aspiwack]

But I do think the Representational synonym should work... we just can't make a tuple of such things.

Oh, maybe that's what I was thinking about, indeed.

[mboes]

So can we foresee a solution to this ticket? Or will it need new research?

[goldfirere]

I guess the question is: with the higher-order roles proposal fix the problem. https://github.com/tweag/capability/issues/81#issuecomment-584513572 does not unambiguously say "yes".