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


-- | open witnesses
--   
--   Open witnesses are witnesses that can witness to any type. However,
--   they cannot be constructed, they can only be generated in the IO
--   monad. See the paper <i>Witnesses and Open Witnesses</i>
--   (<a>http://semantic.org/stuff/Open-Witnesses.pdf</a>).
@package open-witness
@version 0.4.0.1

module Data.Type.Heterogeneous
data HetEq (a :: ka) (b :: kb)
[ReflH] :: forall (k :: *) (t :: k). HetEq t t

-- | somewhat awkwardly named
homoHetEq :: forall (k :: *) (a :: k) (b :: k). HetEq a b -> a :~: b
class TestHetEquality (w :: forall k. k -> *)
testHetEquality :: forall (ka :: *) (a :: ka) (kb :: *) (b :: kb). TestHetEquality w => w a -> w b -> Maybe (HetEq a b)

module Data.OpenWitness

-- | A witness type that can witness to any type. But values cannot be
--   constructed; they can only be generated in <a>IO</a> and certain other
--   monads.
data OpenWitness :: * -> forall (k :: *). k -> *

-- | The <tt>s</tt> type for running <a>OW</a> in <a>IO</a>.
data RealWorld

-- | An <a>OpenWitness</a> for <a>IO</a>.
type IOWitness = OpenWitness RealWorld

-- | Generate a new <a>IOWitness</a> in <a>IO</a>.
newIOWitness :: forall a. IO (IOWitness a)

-- | A runnable monad in which <a>OpenWitness</a> values can be generated.
--   The <tt>s</tt> parameter plays the same role as it does in
--   <tt>ST</tt>, preventing <a>OpenWitness</a> values from one run being
--   used in another.
data OW s a

-- | Generate a new <a>OpenWitness</a> in <a>OW</a>.
newOpenWitnessOW :: forall s a. OW s (OpenWitness s a)

-- | Run an <a>OW</a> computation.
runOW :: forall a. (forall s. OW s a) -> a

-- | Run an <a>OW</a> computation in <a>IO</a>.
owToIO :: OW RealWorld a -> IO a

-- | Template Haskell function to declare <a>IOWitness</a> values.
iowitness :: TypeQ -> Q Exp
instance forall k (s :: k). Control.Monad.Fix.MonadFix (Data.OpenWitness.OW s)
instance forall k (s :: k). GHC.Base.Monad (Data.OpenWitness.OW s)
instance forall k (s :: k). GHC.Base.Applicative (Data.OpenWitness.OW s)
instance forall k (s :: k). GHC.Base.Functor (Data.OpenWitness.OW s)
instance forall k s (a :: k). GHC.Classes.Eq (Data.OpenWitness.OpenWitness s k a)
instance Data.Type.Heterogeneous.TestHetEquality (Data.OpenWitness.OpenWitness s)
instance Data.Type.Equality.TestEquality (Data.OpenWitness.OpenWitness s k)

module Data.OpenWitness.TypeRep
data TypeRep :: forall (k :: *). k -> *
[SimpleTypeRep] :: forall (k :: *) (a :: k). IOWitness a -> TypeRep a
[ApplyTypeRep] :: forall (k1 :: *) (k2 :: *) (p :: k1 -> k2) (a :: k1). TypeRep p -> TypeRep a -> TypeRep (p a)
instance Data.Type.Heterogeneous.TestHetEquality Data.OpenWitness.TypeRep.TypeRep
instance Data.Type.Equality.TestEquality Data.OpenWitness.TypeRep.TypeRep
instance Data.Witness.Representative.Eq1 Data.OpenWitness.TypeRep.TypeRep


-- | This is an approximate re-implementation of <a>Data.Typeable</a> using
--   open witnesses.
module Data.OpenWitness.Typeable

-- | types of kind <tt>*</tt> with a representation
class Typeable (a :: k)
typeRep :: Typeable a => TypeRep a
type Fun = (->)
cast :: forall (a :: *) (b :: *). (Typeable a, Typeable b) => a -> Maybe b
gcast :: forall (k :: *) (a :: k) (b :: k) (c :: k -> *). (Typeable a, Typeable b) => c a -> Maybe (c b)

-- | given representations of <tt>a</tt> and <tt>b</tt>, make a
--   representation of <tt>a -&gt; b</tt>
mkFunTy :: TypeRep a -> TypeRep b -> TypeRep (a -> b)

-- | given representations of <tt>a -&gt; b</tt> and <tt>a</tt>, make a
--   representation of <tt>b</tt> (otherwise not)
funResultTy :: TypeRep (a -> b) -> TypeRep a -> Maybe (TypeRep b)
mkAppTy :: forall (k1 :: *) (k2 :: *) (f :: k1 -> k2) (a :: k1). TypeRep f -> TypeRep a -> TypeRep (f a)
instance Data.OpenWitness.Typeable.Typeable (->)
instance forall k1 k2 (f :: k1 -> k2) (a :: k1). (Data.OpenWitness.Typeable.Typeable f, Data.OpenWitness.Typeable.Typeable a) => Data.OpenWitness.Typeable.Typeable (f a)
instance Data.OpenWitness.Typeable.Typeable *
instance Data.OpenWitness.Typeable.Typeable GHC.Types.Constraint
instance Data.OpenWitness.Typeable.Typeable Data.OpenWitness.TypeRep.TypeRep
instance Data.OpenWitness.Typeable.Typeable Data.OpenWitness.Typeable.Typeable
instance Data.OpenWitness.Typeable.Typeable ()
instance Data.OpenWitness.Typeable.Typeable (,)
instance Data.OpenWitness.Typeable.Typeable Data.Either.Either
instance Data.OpenWitness.Typeable.Typeable GHC.Base.Maybe
instance Data.OpenWitness.Typeable.Typeable []
instance Data.OpenWitness.Typeable.Typeable GHC.Types.Bool
instance Data.OpenWitness.Typeable.Typeable GHC.Types.Char
instance Data.OpenWitness.Typeable.Typeable GHC.Types.Int

module Data.OpenWitness.Instance
data Instance
MkInstance :: (TypeRep t) -> Instance
findInstance :: [Instance] -> TypeRep t -> Maybe (Dict t)


-- | This is an approximate re-implementation of <a>Data.Dynamic</a> using
--   open witnesses.
module Data.OpenWitness.Dynamic
type Dynamic = Any TypeRep
toDyn :: forall (a :: *). Typeable a => a -> Dynamic
fromDyn :: Typeable a => Dynamic -> a -> a
fromDynamic :: forall (a :: *). Typeable a => Dynamic -> Maybe a
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
dynApp :: Dynamic -> Dynamic -> Dynamic
dynTypeRep :: Dynamic -> AnyWitness (TypeRep :: * -> *)


-- | This is an approximate re-implementation of <a>Control.Monad.ST</a>
--   and <a>Data.STRef</a> using open witnesses.
module Data.OpenWitness.ST
type ST s = StateT (WitnessDict (OpenWitness s)) (OW s)
runST :: (forall s. ST s a) -> a
fixST :: (a -> ST s a) -> ST s a
stToOW :: ST s a -> OW s a

-- | The <tt>s</tt> type for running <a>OW</a> in <a>IO</a>.
data RealWorld
stToIO :: ST RealWorld a -> IO a
type STRef s = OpenWitness s
newSTRef :: a -> ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
writeSTRef :: forall s a. STRef s a -> a -> ST s ()
modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ()

module Data.OpenWitness.Exception

-- | A key to match exceptions. The type variable is the data the exception
--   carries.
data Exn (e :: *)

-- | Template Haskell function to declare <a>Exn</a> exception keys.
declexn :: TypeQ -> Q Exp
throw :: Exn e -> e -> a
catch :: IO a -> Exn e -> (e -> IO a) -> IO a
instance GHC.Show.Show Data.OpenWitness.Exception.ExnException
instance GHC.Exception.Exception Data.OpenWitness.Exception.ExnException
instance Data.Type.Equality.TestEquality Data.OpenWitness.Exception.Exn
