ref: 96366c2426fc6ddc58f86d4c8b536ba219a62b4d
parent: d08ab630e62ea0a1e3c709a57ec5cca6a36fe096
author: Lennart Augustsson <lennart@augustsson.net>
date: Thu Dec 21 16:18:51 EST 2023
Implement eqT and gcast
--- a/lib/Data/Typeable.hs
+++ b/lib/Data/Typeable.hs
@@ -3,6 +3,8 @@
TypeRep,
typeOf,
cast,
+ eqT,
+ gcast,
TyCon,
tyConModule,
tyConName,
@@ -14,22 +16,9 @@
funResultTy,
typeRepTyCon,
typeRepArgs,
-
{-- -- * For backwards compatibility
- typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7,
- Typeable1, Typeable2, Typeable3, Typeable4, Typeable5, Typeable6,
- Typeable7,
- -- * Type-safe cast
- eqT,
- gcast, -- a generalisation of cast
-
- -- * Type representations
- showsTypeRep,
-
-
- -- * Construction of type representations
- -- mkTyCon, -- :: String -> TyCon
+ typeOf1, typeOf2, typeOf3, typeOf4, typeOf5, typeOf6, typeOf7,
+ Typeable1, Typeable2, Typeable3, Typeable4, Typeable5, Typeable6, Typeable7,
-}
) where
import Primitives
@@ -42,6 +31,7 @@
import Data.Proxy
import Data.Ratio
import Data.STRef
+import Data.Type.Equality
import Data.Void
import Data.Word8
import System.IO.MD5
@@ -128,15 +118,17 @@
then Just $ unsafeCoerce x
else Nothing
-{-eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT = if typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b)
- then Just $ unsafeCoerce Refl
+ then Just $ unsafeCoerce (Refl :: () :~: ())
else Nothing
-gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
-gcast x = fmap (\Refl -> x) (eqT :: Maybe (a :~: b))
--}
+gcast :: forall a b (c :: Type -> Type) .
+ (Typeable a, Typeable b) => c a -> Maybe (c b)
+gcast x =
+ case eqT :: Maybe (a :~: b) of
+ Just Refl -> Just x
+ Nothing -> Nothing
-----------------
--
⑨