cast
alone can't do this because it needs to know the types of all variables, but its implementation is quite simple so you can write your own. cast
checks a
and b
are the same type and unsafeCoerce
s it if they match.
You can do something using typeRepCon
. This deconstructs a TypeRep
into the type constructer and a list of types that make it's parameters. First match the type constructors to make sure it's a Value
, then check if y
is the same. If everything matches you can unsafeCoerce
.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}
import Unsafe.Coerce
import Data.Typeable
data Value x y = Value x y
deriving Typeable
data Box where
Box :: Typeable a => a -> Box
value :: Value Int Char
value = Value 3 'a'
box :: Box
box = Box value
box2 :: Box
box2 = Box 'Z'
getValueY :: forall a y. (Typeable a, Typeable y) => a -> Maybe (forall x. Value x y)
getValueY a
| con == typeRepTyCon (typeOf value) && y == typeRep (Proxy :: Proxy y)
= Just $ unsafeCoerce a
| otherwise = Nothing
where
(con, ~[_x, y]) = splitTyConApp (typeOf a)
valueChar :: Value x Char -> Char
valueChar (Value _ c) = c
boxChar :: Box -> Maybe Char
boxChar (Box b) =
case getValueY b of
Just v -> Just (valueChar v)
Nothing -> Nothing
which gives
>>> getY box
Just 'a'
>>> getY box2
Nothing
The impredicative type (forall x. Value x y
) is here to make sure you can't choose what x is, otherwise you could make it whatever you want as long as the y
matches. Another (possibly nicer) solution is make another wrapper like
data YValue y where
YValue :: Value x y -> YValue y
deriving Typeable
A lot of the trouble comes from not even knowing it's a Value
, otherwise you could use gcast
.
Edit: you can avoid ImpredicativeTypes
completely by giving it a forall x. Value x y -> b
function:
withValueY :: forall a y b. (Typeable a, Typeable y)
=> (forall x. Value x y -> b) -> a -> Maybe b
withValueY f a
| con == typeRepTyCon (typeOf value) && y == typeRep (Proxy :: Proxy y)
= Just $ f (unsafeCoerce a)
| otherwise = Nothing
where
(con, ~[_x, y]) = splitTyConApp (typeOf a)
boxChar :: Box -> Maybe Char
boxChar (Box b) = withValueY valueChar b
Value
.cast
to change types arbitrarily, it will fail. Ifv :: Value Int Char
, thencast v :: Maybe (Value Int Bool)
will returnNothing
. I think you need a real conversion function, which exploitsValue
's constructors.