-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Opaque unique identifiers in primitive state monads
--   
--   Opaque unique identifiers in primitive state monads and a GADT-like
--   type using them as witnesses of type equality.
@package prim-uniq
@version 0.2

module Unsafe.Unique.Prim

-- | A <a>Uniq</a> is a value that can only be constructed under controlled
--   conditions (in IO or ST, basically), and once constructed can only be
--   compared to <a>Uniq</a> values created under the same conditions (in
--   the same monad). Upon comparison, a <a>Uniq</a> is ONLY ever equal to
--   itself. Beyond that, no promises regarding ordering are made except
--   that once constructed the order is deterministic and a proper ordering
--   relation (eg, &gt; is transitive and irreflexive, etc.)
data Uniq s

-- | Construct a new <a>Uniq</a> that is equal to itself, unequal to every
--   other <a>Uniq</a> constructed in the same monad, and incomparable to
--   every <a>Uniq</a> constructed in any other monad.
getUniq :: PrimMonad m => m (Uniq (PrimState m))

-- | For the implementation of <a>Uniq</a> construction in new monads, this
--   operation is exposed. Users must accept responsibility for ensuring
--   true uniqueness across the lifetime of the resulting <a>Uniq</a>
--   value. Failure to do so could lead to type unsoundness in code
--   depending on uniqueness as a type witness (eg,
--   <a>Data.Unique.Tag</a>).
unsafeMkUniq :: Integer -> Uniq s

-- | A <a>Show</a> instance for <tt><a>Uniq</a> s</tt> would not be sound,
--   but for debugging purposes we occasionally will want to do it anyway.
--   Its unsoundness is nicely demonstrated by:
--   
--   <pre>
--   runST (fmap show getUniq) :: String
--   </pre>
--   
--   Which, despite having type <a>String</a>, is not referentially
--   transparent.
unsafeShowsPrecUniq :: Int -> Uniq s -> ShowS

-- | See <a>unsafeShowsPrecUniq</a>.
unsafeShowUniq :: Uniq s -> String
instance GHC.Classes.Ord (Unsafe.Unique.Prim.Uniq s)
instance GHC.Classes.Eq (Unsafe.Unique.Prim.Uniq s)
instance GHC.Show.Show (Unsafe.Unique.Prim.Uniq GHC.Prim.RealWorld)

module Data.Unique.Prim

-- | A <a>Uniq</a> is a value that can only be constructed under controlled
--   conditions (in IO or ST, basically), and once constructed can only be
--   compared to <a>Uniq</a> values created under the same conditions (in
--   the same monad). Upon comparison, a <a>Uniq</a> is ONLY ever equal to
--   itself. Beyond that, no promises regarding ordering are made except
--   that once constructed the order is deterministic and a proper ordering
--   relation (eg, &gt; is transitive and irreflexive, etc.)
data Uniq s

-- | Construct a new <a>Uniq</a> that is equal to itself, unequal to every
--   other <a>Uniq</a> constructed in the same monad, and incomparable to
--   every <a>Uniq</a> constructed in any other monad.
getUniq :: PrimMonad m => m (Uniq (PrimState m))
data RealWorld

module Unsafe.Unique.Tag

-- | The <a>Tag</a> 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 <a>Tag</a> 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 <a>GOrdering</a> class allows rediscovery
--   of a tag's phantom type, so that <a>Tag</a>s and values of type
--   <tt><tt>DSum</tt> (<a>Tag</a> s)</tt> can be tested for equality even
--   when their types are not known to be equal.
--   
--   <a>Tag</a> uses a <a>Uniq</a> as a witness of type equality, which is
--   sound as long as the <a>Uniq</a> is truly unique and only one
--   <a>Tag</a> is ever constructed from any given <a>Uniq</a>. The type of
--   <a>newTag</a> enforces these conditions. <a>veryUnsafeMkTag</a>
--   provides a way for adventurous (or malicious!) users to assert that
--   they know better than the type system.
data Tag s a

-- | Create a new tag witnessing a type <tt>a</tt>. The <a>GEq</a> or
--   <a>GOrdering</a> 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 <tt>a</tt> 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)

-- | Very dangerous! This is essentially a deferred <a>unsafeCoerce</a>: by
--   creating a tag with this function, the user accepts responsibility for
--   ensuring uniqueness of the <a>Integer</a> across the lifetime of the
--   <a>Tag</a> (including properly controlling the lifetime of the
--   <a>Tag</a> if necessary by universal quantification when discharging
--   the <tt>s</tt> phantom type)
veryUnsafeMkTag :: Integer -> Tag s a
instance GHC.Classes.Ord (Unsafe.Unique.Tag.Tag s a)
instance GHC.Classes.Eq (Unsafe.Unique.Tag.Tag s a)
instance GHC.Show.Show (Unsafe.Unique.Tag.Tag GHC.Prim.RealWorld a)
instance Data.GADT.Internal.GShow (Unsafe.Unique.Tag.Tag GHC.Prim.RealWorld)
instance Data.GADT.Internal.GEq (Unsafe.Unique.Tag.Tag s)
instance Data.GADT.Internal.GCompare (Unsafe.Unique.Tag.Tag s)

module Data.Unique.Tag

-- | The <a>Tag</a> 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 <a>Tag</a> 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 <a>GOrdering</a> class allows rediscovery
--   of a tag's phantom type, so that <a>Tag</a>s and values of type
--   <tt><tt>DSum</tt> (<a>Tag</a> s)</tt> can be tested for equality even
--   when their types are not known to be equal.
--   
--   <a>Tag</a> uses a <a>Uniq</a> as a witness of type equality, which is
--   sound as long as the <a>Uniq</a> is truly unique and only one
--   <a>Tag</a> is ever constructed from any given <a>Uniq</a>. The type of
--   <a>newTag</a> enforces these conditions. <a>veryUnsafeMkTag</a>
--   provides a way for adventurous (or malicious!) users to assert that
--   they know better than the type system.
data Tag s a

-- | Create a new tag witnessing a type <tt>a</tt>. The <a>GEq</a> or
--   <a>GOrdering</a> 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 <tt>a</tt> 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)
data RealWorld
data (a :: k) :~: (b :: k)
[Refl] :: forall k (a :: k). a :~: a
class GEq (f :: k -> Type)
geq :: forall (a :: k) (b :: k). GEq f => f a -> f b -> Maybe (a :~: b)
data GOrdering (a :: k) (b :: k)
[GLT] :: forall k (a :: k) (b :: k). GOrdering a b
[GEQ] :: forall k (a :: k). GOrdering a a
[GGT] :: forall k (a :: k) (b :: k). GOrdering a b
class GEq f => GCompare (f :: k -> Type)
gcompare :: forall (a :: k) (b :: k). GCompare f => f a -> f b -> GOrdering a b
