[Haskell-cafe] Specific to General to Specific

[Edward Z. Yang]

Imagine that I have the following type-class:

    class (Monad (m n)) => NetworkMonad m n

    data NT n a
    instance NetworkMonad NT n

    data NQ n a
    instance NetworkMonad NQ n

    monadicValue :: NetworkMonad m n => m n ()

It defines some family of phantom monads, in this case NT n and NQ n, and
permits some values to inhabit either monad (resolved by the surrounding code).
Suppose, however, that there are multiple possible implementations for the pair
(NT, NQ).  Then we might like to generalize this typeclass with an associated
type.  (Suppose that our old implementation was g = Int.)

    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE FlexibleContexts #-}

    class Network g where 
        data GNT g :: * -> * -> *
        data GNQ g :: * -> * -> *
    class (Monad (m g n)) => GenericNetworkMonad g m n 

    type NT n a = GNT Int n a
    type NQ n a = GNQ Int n a

    genericMonadicValue :: GenericNetworkMonad g m n => m g n ()
    genericMonadicValue = undefined

    monadicValue :: GenericNetworkMonad Int m n => m Int n ()
    monadicValue = undefined

My question is, how can I write a specialized typeclass NetworkMonad
that recaptures the original simple interface?

    monadicValue' :: NetworkMonad m n => m n ()
    monadicValue' = undefined

I've tried something like this:

    type family GetM (x :: * -> * -> *) :: (* -> * -> * -> *)
    type instance GetM (m g) = m

    type family GetG (x :: * -> * -> *) :: *
    type instance GetG (m g) = g

    class (GenericNetworkMonad (GetG mg) (GetM mg) n) => NetworkMonad mg n where

But this doesn't seem to be enough information to do inference with:

    monadicValue'' :: NetworkMonad m n => m n ()
    monadicValue'' = genericMonadicValue

gives the type error:

    Test.hs:28:17:
        Could not deduce (GenericNetworkMonad g m n)
          from the context (NetworkMonad m1 n)
          arising from a use of `genericMonadicValue' at Test.hs:28:17-35
        Possible fix:
          add (GenericNetworkMonad g m n) to the context of
            the type signature for `monadicValue'''
        In the expression: genericMonadicValue
        In the definition of `monadicValue''':
            monadicValue'' = genericMonadicValue

    Test.hs:28:17:
        Couldn't match expected type `m1' against inferred type `m g'
          `m1' is a rigid type variable bound by
               the type signature for `monadicValue''' at Test.hs:27:31
        In the expression: genericMonadicValue
        In the definition of `monadicValue''':
            monadicValue'' = genericMonadicValu

Am I out of luck without superclass equality constraints?

Cheers,
Edward