module Morley.Util.Typeable
( eqParam1
, eqParam2
, eqParam3
, eqExt
, compareExt
, castIgnoringPhantom
, eqTypeIgnoringPhantom
, (:~:) (..)
, eqT
) where
import Data.Coerce (coerce)
import Data.Typeable (eqT, typeRep, (:~:)(..))
import Type.Reflection qualified as Refl
eqParam1 ::
forall a1 a2 t.
( Typeable a1
, Typeable a2
, Eq (t a1)
)
=> t a1
-> t a2
-> Bool
eqParam1 :: forall {k} (a1 :: k) (a2 :: k) (t :: k -> *).
(Typeable a1, Typeable a2, Eq (t a1)) =>
t a1 -> t a2 -> Bool
eqParam1 t a1
t1 t a2
t2 = forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
a1 :~: a2
Refl <- forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a1 @a2
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t a1
t1 t a1 -> t a1 -> Bool
forall a. Eq a => a -> a -> Bool
== t a1
t a2
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 :: forall {k} {k} (a1 :: k) (a2 :: k) (b1 :: k) (b2 :: k)
(t :: k -> k -> *).
(Typeable a1, Typeable a2, Typeable b1, Typeable b2,
Eq (t a1 b2)) =>
t a1 b1 -> t a2 b2 -> Bool
eqParam2 t a1 b1
t1 t a2 b2
t2 = forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
a1 :~: a2
Refl <- forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a1 @a2
b1 :~: b2
Refl <- forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @b1 @b2
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t a1 b1
t1 t a1 b1 -> t a1 b1 -> Bool
forall a. Eq a => a -> a -> Bool
== t a1 b1
t a2 b2
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 :: forall {k} {k} {k} (a1 :: k) (a2 :: k) (b1 :: k) (b2 :: k)
(c1 :: k) (c2 :: k) (t :: k -> k -> k -> *).
(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 t a1 b1 c1
t1 t a2 b2 c2
t2 = forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
a1 :~: a2
Refl <- forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a1 @a2
b1 :~: b2
Refl <- forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @b1 @b2
c1 :~: c2
Refl <- forall (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @c1 @c2
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t a1 b1 c1
t1 t a1 b1 c1 -> t a1 b1 c1 -> Bool
forall a. Eq a => a -> a -> Bool
== t a1 b1 c1
t a2 b2 c2
t2)
eqExt ::
forall a1 a2.
( Typeable a1
, Typeable a2
, Eq a1
)
=> a1
-> a2
-> Bool
eqExt :: forall a1 a2. (Typeable a1, Typeable a2, Eq a1) => a1 -> a2 -> Bool
eqExt a1
a1 a2
a2 = forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
a1 :~: a2
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a1 @a2
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a1
a1 a1 -> a1 -> Bool
forall a. Eq a => a -> a -> Bool
== a1
a2
a2)
compareExt ::
forall a1 a2.
( Typeable a1
, Typeable a2
, Ord a1
)
=> a1
-> a2
-> Ordering
compareExt :: forall a1 a2.
(Typeable a1, Typeable a2, Ord a1) =>
a1 -> a2 -> Ordering
compareExt a1
t1 a2
t2 =
case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a1 @a2 of
Maybe (a1 :~: a2)
Nothing -> Proxy a1 -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a1) TypeRep -> TypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Proxy a2 -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a2)
Just a1 :~: a2
Refl -> a1
t1 a1 -> a1 -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a1
a2
t2
castIgnoringPhantom
:: forall c x.
( Typeable x, Typeable c
, forall phantom1 phantom2. Coercible (c phantom1) (c phantom2)
)
=> x -> Maybe (c DummyPhantomType)
castIgnoringPhantom :: forall {k} (c :: k -> *) x.
(Typeable x, Typeable c,
forall (phantom1 :: k) (phantom2 :: k).
Coercible (c phantom1) (c phantom2)) =>
x -> Maybe (c DummyPhantomType)
castIgnoringPhantom x
x = do
Refl.App TypeRep a
x1Rep TypeRep b
_ <- TypeRep x -> Maybe (TypeRep x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeRep x -> Maybe (TypeRep x)) -> TypeRep x -> Maybe (TypeRep x)
forall a b. (a -> b) -> a -> b
$ x -> TypeRep x
forall a. Typeable a => a -> TypeRep a
Refl.typeOf x
x
let cRep :: TypeRep c
cRep = forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: k -> *). Typeable a => TypeRep a
Refl.typeRep @c
a :~~: c
Refl.HRefl <- TypeRep a -> TypeRep c -> Maybe (a :~~: c)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
Refl.eqTypeRep TypeRep a
x1Rep TypeRep c
cRep
c DummyPhantomType -> Maybe (c DummyPhantomType)
forall (m :: * -> *) a. Monad m => a -> m a
return (x -> c DummyPhantomType
coerce x
x)
type family DummyPhantomType :: k where
eqTypeIgnoringPhantom
:: forall c x r.
(Typeable x, Typeable c)
=> (forall a. Typeable a => (c a :~: x) -> Proxy a -> r) -> Maybe r
eqTypeIgnoringPhantom :: forall {k} {k} (c :: k -> k) (x :: k) r.
(Typeable x, Typeable c) =>
(forall (a :: k). Typeable a => (c a :~: x) -> Proxy a -> r)
-> Maybe r
eqTypeIgnoringPhantom forall (a :: k). Typeable a => (c a :~: x) -> Proxy a -> r
cont = do
Refl.App TypeRep a
x1Rep TypeRep b
xArgRep <- TypeRep x -> Maybe (TypeRep x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeRep x -> Maybe (TypeRep x)) -> TypeRep x -> Maybe (TypeRep x)
forall a b. (a -> b) -> a -> b
$ forall (a :: k). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
Refl.typeRep @x
let cRep :: TypeRep c
cRep = forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: k -> k). Typeable a => TypeRep a
Refl.typeRep @c
a :~~: c
Refl.HRefl <- TypeRep a -> TypeRep c -> Maybe (a :~~: c)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
Refl.eqTypeRep TypeRep a
x1Rep TypeRep c
cRep
r -> Maybe r
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> Maybe r) -> r -> Maybe r
forall a b. (a -> b) -> a -> b
$ TypeRep b -> (Typeable b => r) -> r
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
Refl.withTypeable TypeRep b
xArgRep ((c b :~: x) -> Proxy b -> r
forall (a :: k). Typeable a => (c a :~: x) -> Proxy a -> r
cont c b :~: x
forall {k} (a :: k). a :~: a
Refl Proxy b
forall {k} (t :: k). Proxy t
Proxy)