{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- Copyright 2018, Ideas project team. This file is distributed under the
-- terms of the Apache License 2.0. For more information, see the files
-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- Typeable type class, with the IsTypeable data type for witnessing instances
--
-----------------------------------------------------------------------------

module Ideas.Utils.Typeable
   ( IsTypeable, typeable
   , HasTypeable(..)
   , castFrom, castTo, castBetween
   , gcastFrom, gcastTo, gcastBetween
   , module Data.Typeable
   ) where

import Control.Monad
import Data.Typeable
import Unsafe.Coerce

newtype IsTypeable a = IT TypeRep

class HasTypeable f where
   getTypeable :: f a -> Maybe (IsTypeable a)

instance HasTypeable IsTypeable where
   getTypeable = Just

typeable :: forall a . Typeable a => IsTypeable a
typeable = IT (typeRep (Proxy :: Proxy a))

castFrom :: (HasTypeable f, Typeable b) => f a -> a -> Maybe b
castFrom = flip castBetween typeable

castTo :: (HasTypeable f, Typeable a) => f b -> a -> Maybe b
castTo = castBetween typeable

castBetween :: (HasTypeable f, HasTypeable g) => f a -> g b -> a -> Maybe b
castBetween x y a = do
   guardEq x y
   return $ unsafeCoerce a

gcastFrom :: (HasTypeable f, Typeable b) => f a -> c a -> Maybe (c b)
gcastFrom = flip gcastBetween typeable

gcastTo :: (HasTypeable f, Typeable a) => f b -> c a -> Maybe (c b)
gcastTo = gcastBetween typeable

gcastBetween :: (HasTypeable f, HasTypeable g) => f a -> g b -> c a -> Maybe (c b)
gcastBetween ta tb x = fmap (\Refl -> x) (eqIT ta tb)

eqIT :: (HasTypeable f, HasTypeable g) => f a -> g b -> Maybe (a :~: b)
eqIT x y = do
   guardEq x y
   return $ unsafeCoerce Refl

guardEq :: (HasTypeable f, HasTypeable g) => f a -> g b -> Maybe ()
guardEq x y = do
   IT ta <- getTypeable x
   IT tb <- getTypeable y
   guard (ta == tb)