How to write gcast for type families?

Question

I'm trying to write a variant of Data.Typeable.gcast which works for type families of kind * -> *. What I'm looking for is:

{-# LANGUAGE TypeFamilies #-}
import Data.Typeable

type family T

gcastT :: (Typeable a,Typeable b) => T a -> Maybe (T b)
gcastT = undefined -- but that's not working too well!

going by analogy to gcast :: (Typeable a,Typeable b) => f a -> Maybe (f b).

Is this possible?

I could change the context to (Typeable (T a),Typeable (T b)) => but I'd prefer this signature for aesthetic reasons: gcast doesn't need Typeable1 f, after all.

---

Some background in case I'm solving the wrong problem for what I actually want to achieve: my goal is to write a function matchAndExtract:

matchAndExtract :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> T b -> Maybe (T a)
matchAndExtract x k v = if (cast x == Just k) then gcastT v else Nothing

which checks x and k for being of the same type and being equal, and then returning the supplied T b (which we by then know to be the same as T a - T might not be injective, but it is a function!) or Nothing, otherwise.

I've got a work-around by wrapping the offending T a in a newtype, using gcast, and unwrapping again:

matchAndExtractF :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> f b -> Maybe (f a)
matchAndExtractF x k v = if (cast x == Just k) then gcast v else Nothing

newtype WrapT a = WrapT { unWrapT :: T a }

matchAndExtractViaWrap :: (Eq a, Typeable a, Eq b, Typeable b) => a -> b -> T b -> Maybe (T a)
matchAndExtractViaWrap x k v = fmap unWrapT $ matchAndExtractF a k (WrapT v)

but that just rubs me the wrong way! This also works for instances for which T a is not an instance of Typeable; that again seems to me to indicate the Typeable (T a) contexts shouldn't be needed.

The work-around is perfectly acceptable, but I'd like to get rid of the spurious WrapT type.

Answer 1

What you are trying to do is not possible they way you have implemented it. Instead you can use

type family T x :: *
newtype NT x = NT {fromNT :: T x}
gcastT :: (Typeable a, Typeable b) => NT a -> Maybe (NT b)
gcastT = gcast

In this case you do not need to use the Eq constraint.

Another option is to reify the typeable dictionaries into GADTs

data Type x where
  Typeable :: Typeable x => Type x

asT :: NT x -> Type x -> NT x
asT = const

gcastTD :: Type a -> Type b -> Type a -> Maybe (T b)
gcastTD t@Typeable Typeable x = fmap fromNT $ gcastT $ (NT x) `asT` t

(code not tested, but should be almost correct)

once you have this you can use it by passing explicit type signatures

type instance T Int = ()

justUnit = gcastTD (Typeable :: Type Int) (Typeable :: Type Int) ()