-- 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 = maybeToRight errMsg . gcast
  where
    errMsg = "Type mismatch: expected " +|| typeRep (Proxy @b) ||+
                               ", got " +|| typeRep (Proxy @a) ||+ ""

-- | 'Proxy' version of 'eqT'.
eqP :: (Typeable a, Typeable b) => Proxy a -> Proxy b -> Maybe (a :~: b)
eqP (_ :: Proxy a) (_ :: Proxy 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 t1 t2 = isJust @() $ do
  Refl <- eqT @a1 @a2
  guard (t1 == 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 t1 t2 = isJust @() $ do
  Refl <- eqT @a1 @a2
  Refl <- eqT @b1 @b2
  guard (t1 == 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 t1 t2 = isJust @() $ do
  Refl <- eqT @a1 @a2
  Refl <- eqT @b1 @b2
  Refl <- eqT @c1 @c2
  guard (t1 == t2)

-- | Compare two entries of completely different types.
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)

-- | Extension of 'eqExt' to 'compare' function.
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

{- | 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 = 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

-- | 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 cont = do
  Refl.App x1Rep xArgRep <- pure $ Refl.typeRep @x
  let cRep = Refl.typeRep @c
  Refl.HRefl <- Refl.eqTypeRep x1Rep cRep
  return $ Refl.withTypeable xArgRep (cont Refl Proxy)