{-# LANGUAGE GADTs, FlexibleInstances #-}
module Unsafe.Unique.Tag
    ( Tag
    , newTag
    , veryUnsafeMkTag
    ) where

import Data.GADT.Compare
import Data.GADT.Show
import Unsafe.Unique.Prim
import Unsafe.Coerce
import Control.Monad.Primitive
import Control.Monad
import Data.Type.Equality ((:~:)(..))

-- |The 'Tag' type is like an ad-hoc GADT allowing runtime creation of new 
-- constructors.  Specifically, it is like a GADT \"enumeration\" with one
-- phantom type.
-- 
-- A 'Tag' constructor can be generated in any primitive monad (but only tags
-- from the same one can be compared).  Every tag is equal to itself and to 
-- no other.  The 'GOrdering' class allows rediscovery of a tag's phantom type,
-- so that 'Tag's and values of type @'DSum' ('Tag' s)@ can be tested for
-- equality even when their types are not known to be equal.
--
-- 'Tag' uses a 'Uniq' as a witness of type equality, which is sound as long
-- as the 'Uniq' is truly unique and only one 'Tag' is ever constructed from
-- any given 'Uniq'.  The type of 'newTag' enforces these conditions.
-- 'veryUnsafeMkTag' provides a way for adventurous (or malicious!) users to 
-- assert that they know better than the type system.
newtype Tag s a = Tag (Uniq s) deriving (Tag s a -> Tag s a -> Bool
(Tag s a -> Tag s a -> Bool)
-> (Tag s a -> Tag s a -> Bool) -> Eq (Tag s a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s a. Tag s a -> Tag s a -> Bool
/= :: Tag s a -> Tag s a -> Bool
$c/= :: forall s a. Tag s a -> Tag s a -> Bool
== :: Tag s a -> Tag s a -> Bool
$c== :: forall s a. Tag s a -> Tag s a -> Bool
Eq, Eq (Tag s a)
Eq (Tag s a) =>
(Tag s a -> Tag s a -> Ordering)
-> (Tag s a -> Tag s a -> Bool)
-> (Tag s a -> Tag s a -> Bool)
-> (Tag s a -> Tag s a -> Bool)
-> (Tag s a -> Tag s a -> Bool)
-> (Tag s a -> Tag s a -> Tag s a)
-> (Tag s a -> Tag s a -> Tag s a)
-> Ord (Tag s a)
Tag s a -> Tag s a -> Bool
Tag s a -> Tag s a -> Ordering
Tag s a -> Tag s a -> Tag s a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s a. Eq (Tag s a)
forall s a. Tag s a -> Tag s a -> Bool
forall s a. Tag s a -> Tag s a -> Ordering
forall s a. Tag s a -> Tag s a -> Tag s a
min :: Tag s a -> Tag s a -> Tag s a
$cmin :: forall s a. Tag s a -> Tag s a -> Tag s a
max :: Tag s a -> Tag s a -> Tag s a
$cmax :: forall s a. Tag s a -> Tag s a -> Tag s a
>= :: Tag s a -> Tag s a -> Bool
$c>= :: forall s a. Tag s a -> Tag s a -> Bool
> :: Tag s a -> Tag s a -> Bool
$c> :: forall s a. Tag s a -> Tag s a -> Bool
<= :: Tag s a -> Tag s a -> Bool
$c<= :: forall s a. Tag s a -> Tag s a -> Bool
< :: Tag s a -> Tag s a -> Bool
$c< :: forall s a. Tag s a -> Tag s a -> Bool
compare :: Tag s a -> Tag s a -> Ordering
$ccompare :: forall s a. Tag s a -> Tag s a -> Ordering
$cp1Ord :: forall s a. Eq (Tag s a)
Ord)
instance Show (Tag RealWorld a) where showsPrec :: Int -> Tag RealWorld a -> ShowS
showsPrec p :: Int
p (Tag u :: Uniq RealWorld
u) = Int -> Uniq RealWorld -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Uniq RealWorld
u
instance GShow (Tag RealWorld)  where gshowsPrec :: Int -> Tag RealWorld a -> ShowS
gshowsPrec = Int -> Tag RealWorld a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance GEq (Tag s) where
    geq :: Tag s a -> Tag s b -> Maybe (a :~: b)
geq (Tag a :: Uniq s
a) (Tag b :: Uniq s
b)
        | Uniq s
a Uniq s -> Uniq s -> Bool
forall a. Eq a => a -> a -> Bool
== Uniq s
b    = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
        | Bool
otherwise = Maybe (a :~: b)
forall a. Maybe a
Nothing
instance GCompare (Tag s) where
    gcompare :: Tag s a -> Tag s b -> GOrdering a b
gcompare (Tag a :: Uniq s
a) (Tag b :: Uniq s
b) = case Uniq s -> Uniq s -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Uniq s
a Uniq s
b of
        LT -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GLT
        EQ -> GOrdering () () -> GOrdering a b
forall a b. a -> b
unsafeCoerce (GOrdering () ()
forall k (a :: k). GOrdering a a
GEQ :: GOrdering () ())
        GT -> GOrdering a b
forall k (a :: k) (b :: k). GOrdering a b
GGT

-- |Create a new tag witnessing a type @a@.  The 'GEq' or 'GOrdering' instance 
-- can be used to discover type equality of two occurrences of the same tag.
-- 
-- (I'm not sure whether the recovery is sound if @a@ is instantiated as a
-- polymorphic type, so I'd advise caution if you intend to try it.  I suspect 
-- it is, but I have not thought through it very deeply and certainly have not
-- proved it.)
newTag :: PrimMonad m => m (Tag (PrimState m) a)
newTag :: m (Tag (PrimState m) a)
newTag = (Uniq (PrimState m) -> Tag (PrimState m) a)
-> m (Uniq (PrimState m)) -> m (Tag (PrimState m) a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Uniq (PrimState m) -> Tag (PrimState m) a
forall s a. Uniq s -> Tag s a
Tag m (Uniq (PrimState m))
forall (m :: * -> *). PrimMonad m => m (Uniq (PrimState m))
getUniq

-- |Very dangerous! This is essentially a deferred 'unsafeCoerce': by creating
-- a tag with this function, the user accepts responsibility for ensuring 
-- uniqueness of the 'Integer' across the lifetime of the 'Tag' (including
-- properly controlling the lifetime of the 'Tag' if necessary 
-- by universal quantification when discharging the @s@ phantom type)
veryUnsafeMkTag :: Integer -> Tag s a
veryUnsafeMkTag :: Integer -> Tag s a
veryUnsafeMkTag = Uniq s -> Tag s a
forall s a. Uniq s -> Tag s a
Tag (Uniq s -> Tag s a) -> (Integer -> Uniq s) -> Integer -> Tag s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Uniq s
forall s. Integer -> Uniq s
unsafeMkUniq