Typeably casting GADTs

Question

Let's say I'm writing a DSL and want to have support for both phantom type support and badly typed expressions. My value types might be

{-# LANGUAGE GADTs, DataKinds #-}

data Ty = Num | Bool deriving (Typeable)

data Val a where
  VNum  :: Int  -> Val Num
  VBool :: Bool -> Val Bool

and I can work with an phantom erased version

{-# LANGUAGE ExistentialQuantification #-}

data Valunk = forall a . Valunk (V' a)

Now, I can operate on values of Valunk by caseing out both VNum and VBool and even reestablish my phantom types in this way

getNum :: Valunk -> Maybe (Val Num)
getNum (Valunk n@(VNum _)) = Just n
getNum _                   = Nothing

But this just feels like I'm reimplementing the Typeable machinery. Unfortunately, GHC won't let me derive a Typeable for Val

src/Types/Core.hs:97:13:
    Can't make a derived instance of `Typeable (Val a)':
      Val must only have arguments of kind `*'
    In the data declaration for Val

Is there a way to get around this restriction? I'd love to write

getIt :: Typeable a => Valunk -> Maybe (Val a)
getIt (Valunk v) = cast v

but right now I have to resort to machinery like this

class Typeably b x where kast :: x a -> Maybe (x b)
instance Typeably Num Val where 
  kast n@(VNum _) = Just n
  kast _          = Nothing

for all of my types.

Answer 1

First of all, you need to store a witness that the quantified type in Valunk is in Typeable:

data Valunk = forall a . Typeable a => Valunk (Val a)

Once you have this, you can just use gcast to achieve what you're asking for:

getIt :: Typeable a => Valunk -> Maybe (Val a)
getIt (Valunk v) = gcast v

This was tested with:

data Val a where
  VNum  :: Int  -> Val Int
  VBool :: Bool -> Val Bool

Answer 2

You can derive Data.Typeable on your own:

{-# LANGUAGE GADTs, DataKinds, DeriveDataTypeable, ExistentialQuantification #-}

import Data.Typeable

data Ty = TNum | TBool deriving Typeable 

data Valunk = forall a. Typeable a => Valunk a 

data Val a where 
    VInt :: Int -> Val TNum
    VBool :: Bool -> Val TBool 

instance Show (Val a) where 
    show (VInt a) = show a
    show (VBool a) = show a 

valtypenam = mkTyCon3 "package" "module" "Val"

instance Typeable (Val a) where 
    typeOf _ = mkTyConApp valtypenam []

getIt :: Valunk -> Maybe (Val a)
getIt (Valunk p) = cast p 

This will provide the get it function. Just be sure to name your type correctly (thus file the package, module and type truthfully) otherwise other packages can get into problems.

For some more examples of how to write these instances, look into: Data.Derive.Typeable source.

EDIT: I had a very strange copy and past error in the code, but now it works.