-- 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 Uniq is a value that can only be constructed under controlled
--   conditions (in IO or ST, basically), and once constructed can only be
--   compared to Uniq values created under the same conditions (in
--   the same monad). Upon comparison, a Uniq 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, > is transitive and irreflexive, etc.)
data Uniq s

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

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

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

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

module Data.Unique.Prim

-- | A Uniq is a value that can only be constructed under controlled
--   conditions (in IO or ST, basically), and once constructed can only be
--   compared to Uniq values created under the same conditions (in
--   the same monad). Upon comparison, a Uniq 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, > is transitive and irreflexive, etc.)
data Uniq s

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

-- | RealWorld is deeply magical. It is primitive, but it is
--   not unlifted (hence ptrArg). We never manipulate
--   values of type RealWorld; it's only used in the type system, to
--   parameterise State#.
data RealWorld

module Unsafe.Unique.Tag

-- | 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 Tags 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.
data Tag s a

-- | 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)

-- | 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
instance GHC.Classes.Eq (Unsafe.Unique.Tag.Tag s a)
instance Data.GADT.Internal.GCompare (Unsafe.Unique.Tag.Tag s)
instance Data.GADT.Internal.GEq (Unsafe.Unique.Tag.Tag s)
instance Data.GADT.Internal.GShow (Unsafe.Unique.Tag.Tag GHC.Prim.RealWorld)
instance GHC.Classes.Ord (Unsafe.Unique.Tag.Tag s a)
instance GHC.Internal.Show.Show (Unsafe.Unique.Tag.Tag GHC.Prim.RealWorld a)

module Data.Unique.Tag

-- | 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 Tags 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.
data Tag s a

-- | 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)

-- | RealWorld is deeply magical. It is primitive, but it is
--   not unlifted (hence ptrArg). We never manipulate
--   values of type RealWorld; it's only used in the type system, to
--   parameterise State#.
data RealWorld

-- | Propositional equality. If a :~: b is inhabited by some
--   terminating value, then the type a is the same as the type
--   b. To use this equality in practice, pattern-match on the
--   a :~: b to get out the Refl constructor; in the body
--   of the pattern-match, the compiler knows that a ~ b.
data (a :: k) :~: (b :: k)
[Refl] :: forall {k} (a :: k). a :~: a
infix 4 :~:
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
