How do I use Data.Constraint to reify constraints?

Question

I have a function of type

(forall m. (MonadCo r m, MonadReader Int m) => m ())
    -> (forall m. (MonadCo r m, MonadReader Int m) => m ())

(MonadCo is my own typeclass representing a coroutine monad. If you like you could consider the case MonadError e m instead. The question will be identical.)

It seems like I should be able to reify the constraint and end up with a function with type signature like

(Equals k (MonadCo r, MonadReader Int))
    => (Constrain k ()) -> (Constrain k ())

but I have no idea how to go about implementing this in practice. I am completely baffled as to what :- and :=> actually are. I suppose I also need a Forall1 in there somewhere, because I'm universally quantifying over m, but I don't see where it should fit.

Really what I want to do is reify the forall m. (MonadCo r m, MonadReader Int m) constraint. I presume that when I do that, whatever ends up appearing on the left hand side will automatically be "the right thing".

Data.Constraint seems very powerful, but I can't work out where to start.

Answer 1

This should be a good start:

type ReaderAndCo r m = (MonadCo r m, MonadReader Int m)

g :: (forall m . Dict (ReaderAndCo r m) -> m ())
  -> (forall m . Dict (ReaderAndCo r m) -> m ())
g x Dict = f (x Dict)

You can further split the dictionary for ReaderAndCo into two components if you wish.

To make it more similar to the code in your question, you can introduce an additional synonym:

type Constrain k a = forall m . Dict (k m) -> m a

g :: Constrain (ReaderAndCo r) () -> Constrain (ReaderAndCo r) ()
g x Dict = f (x Dict)

Is this what you wanted to achieve?

Answer 2

Doesn't seem possible. Looks like your "Implies" would be contravariant in k, while the function you want won't be.

I mean, what if you have some bizarre class MonadFoo m, and you define

type k m = (MonadCo r m, MonadReader Int m, MonadFoo m)

Suppose that this class is specifically designed in such a way that there could be only one instance of this class (well, if you don't use GeneralizedNewtypeDeriving at least), some monad MMM, which is also an instance of MonadCo r and MonadReader Int . Then your type Constrain k () would likely be isomorphic to just MMM (). So, you want a function MMM () -> MMM () — but the input type, MMM () is so much weaker than what you need for your function to work. It's unlikely you'd be able to generalize your function in this way.

UPDATE:

Some happy Oleg'ing, and we have the following code:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Forall where
import Control.Monad.Reader
class Monad m => MonadCo r m where
scary ::
    (forall m. (MonadCo r m, MonadReader Int m) => m ()) ->
    (forall m. (MonadCo r m, MonadReader Int m) => m ())
scary = undefined -- here goes your original function
class Equals (d1 :: (* -> *) -> *) d2 where
    equals :: p d2 -> p d1
    default equals :: p d1 -> p d1
    equals = id
data Dict k (m :: * -> *) where Dict :: k m => Dict k m
type Constraint d a = forall m. d m -> m a
data (d1 :+: d2) (m :: * -> *) = Plus (d1 m) (d2 m)
newtype ConstraintTrans d = ConstraintTrans {runCT :: Constraint d () -> Constraint d ()}
warmAndFuzzy ::
    forall r d.
    Equals d (Dict (MonadCo r) :+: Dict (MonadReader Int)) =>
    Constraint d () -> Constraint d ()
warmAndFuzzy =
    let scary' ::
            (MonadCo r m, MonadReader Int m)
            => (forall m'. (MonadCo r m', MonadReader Int m') => m' ())
                -> m ()
        scary' = scary
        waf :: Constraint (Dict (MonadCo r) :+: Dict (MonadReader Int)) () ->
               Constraint (Dict (MonadCo r) :+: Dict (MonadReader Int)) ()
        waf c (Plus Dict Dict) =
            let arg :: forall m'. (MonadCo r m', MonadReader Int m') => m' ()
                arg = c $ Plus Dict Dict
            in scary' arg
    in runCT $ equals $ ConstraintTrans waf