-- 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.1.0.1

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

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

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.Show.GShow (Unsafe.Unique.Tag.Tag GHC.Prim.RealWorld)
instance Data.GADT.Compare.GEq (Unsafe.Unique.Tag.Tag s)
instance Data.GADT.Compare.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)

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

-- | Backwards compatibility alias; as of GHC 7.8, this is the same as
--   `(:~:)`.
type (:=) = ((:~:) :: k -> k -> Type)

-- | A class for type-contexts which contain enough information to (at
--   least in some cases) decide the equality of types occurring within
--   them.
class GEq (f :: k -> Type)

-- | Produce a witness of type-equality, if one exists.
--   
--   A handy idiom for using this would be to pattern-bind in the Maybe
--   monad, eg.:
--   
--   <pre>
--   extract :: GEq tag =&gt; tag a -&gt; DSum tag -&gt; Maybe a
--   extract t1 (t2 :=&gt; x) = do
--       Refl &lt;- geq t1 t2
--       return x
--   </pre>
--   
--   Or in a list comprehension:
--   
--   <pre>
--   extractMany :: GEq tag =&gt; tag a -&gt; [DSum tag] -&gt; [a]
--   extractMany t1 things = [ x | (t2 :=&gt; x) &lt;- things, Refl &lt;- maybeToList (geq t1 t2)]
--   </pre>
--   
--   (Making use of the <tt>DSum</tt> type from <a>Data.Dependent.Sum</a>
--   in both examples)
geq :: GEq f => f a -> f b -> Maybe (a := b)

-- | A type for the result of comparing GADT constructors; the type
--   parameters of the GADT values being compared are included so that in
--   the case where they are equal their parameter types can be unified.
data GOrdering (a :: k) (b :: k) :: forall k. () => k -> k -> Type
[GLT] :: forall k (a :: k) (b :: k). () => GOrdering a b
[GEQ] :: forall k (a :: k) (b :: k). () => GOrdering a a
[GGT] :: forall k (a :: k) (b :: k). () => GOrdering a b

-- | Type class for comparable GADT-like structures. When 2 things are
--   equal, must return a witness that their parameter types are equal as
--   well (<a>GEQ</a>).
class GEq f => GCompare (f :: k -> Type)
gcompare :: GCompare f => f a -> f b -> GOrdering a b
