Polymorphic function inside a type family

Question

I am trying to define a function inside a type family which is polymorphic over a phantom type of a GADT itself defined within the type family.

My type family definition is along the lines of:

class Channel t where
    data Elem t a :: * 
    foo :: t -> Elem t a
    bar :: Elem t a -> [a]

I have an instance as follows:

data MyChannelType = Ch

instance Channel MyChannelType where

    data Elem MyChannelType a where
        MyConstructor :: Char -> Elem MyChannelType Char

    foo _ = MyConstructor 'a'

    bar (MyConstructor c) = repeat c

The compiler complains that:

Couldn't match type ‘a’ with ‘Char’
      ‘a’ is a rigid type variable bound by
          the type signature for foo :: MyChannelType -> Elem MyChannelType a

Is it possible to write this function with Rank2Types or to reformulate my data types to enable it?

---

EDIT : In response to the clarification Ganesh requested

I would want foo (bar Ch) :: [Int] to be illegal.

I have been using exactly the solution Ganesh suggests but I am motivated by the following more complicated example, where it falls down; given:

data MyOtherType = IntCh | StringCh

I have an instance as follows:

instance Channel MyOtherType where

    data Elem MyOtherType a where
        ElemInt    :: Int ->    Elem MyOtherType Int
        ElemString :: String -> Elem MyOtherType String

    foo IntCh    = ElemInt 0
    foo StringCh = ElemString "a"

    bar (ElemInt i)    = repeat i
    bar (ElemString s) = repeat s

Many thanks,

Michael

Answer 1

With the signatures you've given, foo is unimplementable for MyChannelType because it claims to be able to produce Elem MyChannelType a for any a type.

If what you really want is that there should only be one a type for a given t, you can use a type function to express this:

class Channel t where
    data Elem t a :: *
    type Contents t :: *

    foo :: t -> Elem t (Contents t)
    bar :: Elem t a -> [a]

and then add

type Contents MyChannelType = Char

to the instance.

In response to your edit, I would break up Channel into two classes:

class Channel t where
    data Elem t a :: *
    bar :: Elem t a -> [a]

class Channel t => ChannelContents t a where
    foo :: t -> Elem t a

You can then define the MyOtherType instances with:

instance Channel MyOtherType where

    data Elem MyOtherType a where
        ElemInt :: Int -> Elem MyOtherType Int
        ElemString :: String -> Elem MyOtherType String

    bar (ElemInt i) = repeat i
    bar (ElemString s) = repeat s

instance ChannelContents MyOtherType Int where
    foo IntCh = ElemInt 0

instance ChannelContents MyOtherType String where
    foo StringCh = ElemString "a"

You'll need to enable a few extensions: MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances (the latter two only because of the String instance).