{-# LANGUAGE QuantifiedConstraints #-}
module Util.Typeable
( gcastE
, eqP
, eqParam1
, eqParam2
, eqParam3
, eqExt
, compareExt
, castIgnoringPhantom
, (:~:) (..)
, eqT
) where
import Data.Typeable ((:~:)(..), Typeable, eqT, gcast, typeRep)
import qualified Type.Reflection as Refl
import Data.Coerce (coerce)
import Fmt ((+||), (||+))
gcastE :: forall a b t. (Typeable a, Typeable b) => t a -> Either Text (t b)
gcastE = maybeToRight errMsg . gcast
where
errMsg = "Type mismatch: expected " +|| typeRep (Proxy @b) ||+
", got " +|| typeRep (Proxy @a) ||+ ""
eqP :: (Typeable a, Typeable b) => Proxy a -> Proxy b -> Maybe (a :~: b)
eqP (_ :: Proxy a) (_ :: Proxy b) = eqT @a @b
eqParam1 ::
forall a1 a2 t.
( Typeable a1
, Typeable a2
, Eq (t a1)
)
=> t a1
-> t a2
-> Bool
eqParam1 t1 t2 = isJust @() $ do
Refl <- eqT @a1 @a2
guard (t1 == t2)
eqParam2 ::
forall a1 a2 b1 b2 t.
( Typeable a1
, Typeable a2
, Typeable b1
, Typeable b2
, Eq (t a1 b2)
)
=> t a1 b1
-> t a2 b2
-> Bool
eqParam2 t1 t2 = isJust @() $ do
Refl <- eqT @a1 @a2
Refl <- eqT @b1 @b2
guard (t1 == t2)
eqParam3 ::
forall a1 a2 b1 b2 c1 c2 t.
( Typeable a1
, Typeable a2
, Typeable b1
, Typeable b2
, Typeable c1
, Typeable c2
, Eq (t a1 b1 c1)
)
=> t a1 b1 c1
-> t a2 b2 c2
-> Bool
eqParam3 t1 t2 = isJust @() $ do
Refl <- eqT @a1 @a2
Refl <- eqT @b1 @b2
Refl <- eqT @c1 @c2
guard (t1 == t2)
eqExt ::
forall a1 a2.
( Typeable a1
, Typeable a2
, Eq a1
)
=> a1
-> a2
-> Bool
eqExt a1 a2 = isJust @() $ do
Refl <- eqT @a1 @a2
guard (a1 == a2)
compareExt ::
forall a1 a2.
( Typeable a1
, Typeable a2
, Ord a1
)
=> a1
-> a2
-> Ordering
compareExt t1 t2 =
case eqT @a1 @a2 of
Nothing -> typeRep (Proxy @a1) `compare` typeRep (Proxy @a2)
Just Refl -> t1 `compare` t2
castIgnoringPhantom
:: forall c x.
( Typeable x, Typeable c
, forall phantom1 phantom2. Coercible (c phantom1) (c phantom2)
)
=> x -> Maybe (c DummyPhantomType)
castIgnoringPhantom x = do
Refl.App x1Rep _ <- pure $ Refl.typeOf x
let cRep = Refl.typeRep @c
Refl.HRefl <- Refl.eqTypeRep x1Rep cRep
return (coerce x)
type family DummyPhantomType :: k where