    {-# 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
    $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
    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
    $ccompare :: forall s a. Tag s a -> Tag s a -> Ordering
    compare :: Tag s a -> Tag s a -> Ordering
    $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
    >= :: Tag s a -> Tag s a -> Bool
    $cmax :: forall s a. Tag s a -> Tag s a -> Tag s a
    max :: Tag s a -> Tag s a -> Tag s a
    $cmin :: forall s a. Tag s a -> Tag s a -> Tag s a
    min :: Tag s a -> Tag s a -> Tag s a
    Ord)
    instance Show (Tag RealWorld a) where showsPrec :: Int -> Tag RealWorld a -> ShowS
    showsPrec Int
    p (Tag 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 :: forall a. 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 :: forall a b. Tag s a -> Tag s b -> Maybe (a :~: b)
    geq (Tag Uniq s
    a) (Tag 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 ((ZonkAny 1 :~: ZonkAny 1) -> a :~: b
    forall a b. a -> b
    unsafeCoerce ZonkAny 1 :~: ZonkAny 1
    forall {k} (a :: k). a :~: a
    Refl)
            | Bool
    otherwise = Maybe (a :~: b)
    forall a. Maybe a
    Nothing
    instance GCompare (Tag s) where
        gcompare :: forall a b. Tag s a -> Tag s b -> GOrdering a b
    gcompare (Tag Uniq s
    a) (Tag Uniq s
    b) = case Uniq s -> Uniq s -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Uniq s
    a Uniq s
    b of
            Ordering
    LT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
            Ordering
    EQ -> GOrdering () () -> GOrdering a b
    forall a b. a -> b
    unsafeCoerce (GOrdering () ()
    forall {k} (a :: k). GOrdering a a
    GEQ :: GOrdering () ())
            Ordering
    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 :: forall (m :: * -> *) a. PrimMonad m => 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 :: forall s a. 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