Polymorphic function within type family

Question

I am trying to define a function within a type family that is polymorphic in the phantom type of the GADT itself defined in the type family.

Determining my family type is done by line:

class Channel t where data Elem ta :: * foo :: t -> Elem ta bar :: Elem ta -> [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 using Rank2Types or reformulate my data types to include it?

---

EDIT : in response to clarification, Ganesha requested

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

I use exactly the solution that Ganesh offers, but I am motivated by the following more complex example, where it falls; 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 specified, foo not implemented for MyChannelType because it claims to be able to create Elem MyChannelType a for any type a .

If you really want only one type a for a given t , you can use a type function to express this:

 class Channel t where data Elem ta :: * type Contents t :: * foo :: t -> Elem t (Contents t) bar :: Elem ta -> [a] 

and then add

 type Contents MyChannelType = Char 

to the instance.

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

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

Then you can define instances of MyOtherType 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 need to enable several extensions: MultiParamTypeClasses , TypeSynonymInstances , FlexibleInstances (the last two are only due to the String instance).

Answer 2

As a more general alternative to the Ganesh solution, you can also restrict the variable a an entire class of types (possibly just one):

 {-# LANGUAGE ConstraintKinds #-} import GHC.Exts (Constraint) class Channel t where data Elem ta :: * type ElemConstraint ta :: Constraint foo :: ElemConstraint ta => t -> Elem ta bar :: ElemConstraint ta => Elem ta -> [a] instance Channel MyChannelType where data Elem MyChannelType a where MyConstructor :: Char -> Elem MyChannelType Char type ElemConstraint ta = a ~ Char foo _ = MyConstructor 'a' bar (MyConstructor c) = repeat c class OtherType_Class c where mkOtherTypeElem :: c -> Elem MyOtherType c evOtherTypeElem :: Elem MyOtherType c -> c instance OtherType_Class Int where mkOtherTypeElem = ElemInt evOtherTypeElem (ElemInt i) = i instance OtherType_Class String where ... instance Channel MyOtherType where data Elem MyOtherType a where ElemInt :: Int -> Elem MyOtherType Int ElemString :: String -> Elem MyOtherType String type ElemConstraint MyOtherType a = OtherType_Class a 

However, I must say that this is rather inconvenient for a simply fixed type collection.