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.

not possible. Type families are not injective, and as such you can't solve the constraint from which them come in this way. — Philip JF
@DanielWagner: True, but my limited tests included a case where T a was explicitly not a member of Typeable. Now I don't understand why matchAndExtractViaWrap works! Could that be a bug in GHC (I'm using 7.6.1)? I'll try to implement unsafeCoerce tomorrow... — yatima2975
@yatima2975 Type families + newtypes are known to be unsound, yep. See also Trac #1496. — Daniel Wagner
@DanielWagner: Well, it also works when I use data WrapT = ... but I fortunately haven't been able to write anything 'bad'. — yatima2975

Philip JF Philip JF · Accepted Answer · 2013-02-28T21:45:30

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) ()

How to write gcast for type families?

1 Answers