-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Utility for 'Typeable'.
module Morley.Util.Typeable
  ( eqParam1
  , eqParam2
  , eqParam3
  , eqExt
  , compareExt
  , castIgnoringPhantom
  , eqTypeIgnoringPhantom
    -- * Re-exports
  , (:~:) (..)
  , eqT
  ) where

import Data.Coerce (coerce)
import Data.Typeable (eqT, typeRep, (:~:)(..))
import qualified Type.Reflection as Refl

-- | Suppose you have a data type @X@ with parameter @a@ and you have
-- two values: @x1 :: X a1@ and @x2 :: X a2@. You can't compare them
-- using '==', because they have different types. However, you can
-- compare them using 'eqParam1' as long as both parameters are
-- 'Typeable'.
eqParam1 ::
     forall a1 a2 t.
     ( Typeable a1
     , Typeable a2
     , Eq (t a1)
     )
  => t a1
  -> t a2
  -> Bool
eqParam1 :: t a1 -> t a2 -> Bool
eqParam1 t a1
t1 t a2
t2 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  a1 :~: a2
Refl <- (Typeable a1, Typeable a2) => Maybe (a1 :~: a2)
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)

-- | Version of 'eqParam1' for types with 2 parameters.
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 :: t a1 b1 -> t a2 b2 -> Bool
eqParam2 t a1 b1
t1 t a2 b2
t2 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  a1 :~: a2
Refl <- (Typeable a1, Typeable a2) => Maybe (a1 :~: a2)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a1 @a2
  b1 :~: b2
Refl <- (Typeable b1, Typeable b2) => Maybe (b1 :~: b2)
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)

-- | Version of 'eqParam1' for types with 3 parameters.
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 :: t a1 b1 c1 -> t a2 b2 c2 -> Bool
eqParam3 t a1 b1 c1
t1 t a2 b2 c2
t2 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  a1 :~: a2
Refl <- (Typeable a1, Typeable a2) => Maybe (a1 :~: a2)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a1 @a2
  b1 :~: b2
Refl <- (Typeable b1, Typeable b2) => Maybe (b1 :~: b2)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @b1 @b2
  c1 :~: c2
Refl <- (Typeable c1, Typeable c2) => Maybe (c1 :~: c2)
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)

-- | Compare two entries of completely different types.
eqExt ::
     forall a1 a2.
     ( Typeable a1
     , Typeable a2
     , Eq a1
     )
  => a1
  -> a2
  -> Bool
eqExt :: a1 -> a2 -> Bool
eqExt a1
a1 a2
a2 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust @() (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
  a1 :~: a2
Refl <- (Typeable a1, Typeable a2) => Maybe (a1 :~: a2)
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 (a1
a1 a1 -> a1 -> Bool
forall a. Eq a => a -> a -> Bool
== a1
a2
a2)

-- | Extension of 'eqExt' to 'compare' function.
compareExt ::
     forall a1 a2.
     ( Typeable a1
     , Typeable a2
     , Ord a1
     )
  => a1
  -> a2
  -> Ordering
compareExt :: a1 -> a2 -> Ordering
compareExt a1
t1 a2
t2 =
  case (Typeable a1, Typeable a2) => Maybe (a1 :~: a2)
forall k (a :: k) (b :: k).
(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 (Proxy a1
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 (Proxy a2
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

{- | Cast to a type with phantom type argument without matching this argument.
The phantom type must be the last type argument of the type.

Example of use: imagine a type

@
data MyType a = MyType
@

Normally, if object of this type was hidden under existential quantification with
'Typeable' constraint, then in order to get it back with 'Data.Typeable.cast' you need to know
the exact type of the hidden object, including its phantom type parameter.
With 'castIgnoringPhantom' you get a way to extract this object no matter which
phantom argument it had.
-}
castIgnoringPhantom
  :: forall c x.
     ( Typeable x, Typeable c
     , forall phantom1 phantom2. Coercible (c phantom1) (c phantom2)
     )
  => x -> Maybe (c DummyPhantomType)
castIgnoringPhantom :: 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 = Typeable c => TypeRep c
forall k (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

-- | Match given type against another type of @* -> *@ kind without caring
-- about its type argument.
eqTypeIgnoringPhantom
  :: forall c x r.
     (Typeable x, Typeable c)
  => (forall a. Typeable a => (c a :~: x) -> Proxy a -> r) -> Maybe r
eqTypeIgnoringPhantom :: (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
$ Typeable x => TypeRep x
forall k (a :: k). Typeable a => TypeRep a
Refl.typeRep @x
  let cRep :: TypeRep c
cRep = Typeable c => TypeRep c
forall k (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
  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)