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

{-# LANGUAGE QuantifiedConstraints #-}

-- | Utility for 'Typeable'.
module Util.Typeable
  ( gcastE
  , eqP
  , eqParam1
  , eqParam2
  , eqParam3
  , eqExt
  , compareExt
  , castIgnoringPhantom
  , eqTypeIgnoringPhantom

    -- * Re-exports
  , (:~:) (..)
  , eqT
  ) where

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

-- | Like 'gcast', casts some container's elements,
-- producing informative error on mismatch.
gcastE :: forall a b t. (Typeable a, Typeable b) => t a -> Either Text (t b)
gcastE :: t a -> Either Text (t b)
gcastE = Text -> Maybe (t b) -> Either Text (t b)
forall l r. l -> Maybe r -> Either l r
maybeToRight Text
errMsg (Maybe (t b) -> Either Text (t b))
-> (t a -> Maybe (t b)) -> t a -> Either Text (t b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Maybe (t b)
forall k (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast
  where
    errMsg :: Text
errMsg = "Type mismatch: expected " Builder -> Builder -> Text
forall b. FromBuilder b => Builder -> Builder -> b
+|| Proxy b -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy b
forall k (t :: k). Proxy t
Proxy @b) TypeRep -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+
                               ", got " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+|| Proxy a -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a
forall k (t :: k). Proxy t
Proxy @a) TypeRep -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ ""

-- | 'Proxy' version of 'eqT'.
eqP :: (Typeable a, Typeable b) => Proxy a -> Proxy b -> Maybe (a :~: b)
eqP :: Proxy a -> Proxy b -> Maybe (a :~: b)
eqP (Proxy a
_ :: Proxy a) (Proxy b
_ :: Proxy b) = (Typeable a, Typeable b) => Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b

-- | 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 t1 :: t a1
t1 t2 :: 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 t1 :: t a1 b1
t1 t2 :: 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 t1 :: t a1 b1 c1
t1 t2 :: 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
a1 a2 :: 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 t1 :: a1
t1 t2 :: 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
    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 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 '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
x = do
  Refl.App x1Rep :: TypeRep a
x1Rep _ <- 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
forall a b. Coercible a b => a -> b
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 cont :: forall (a :: k). Typeable a => (c a :~: x) -> Proxy a -> r
cont = do
  Refl.App x1Rep :: TypeRep a
x1Rep xArgRep :: 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)