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


-- | Dependent sum type
--   
--   A dependent sum is a generalization of a particular way of thinking
--   about the <tt>Either</tt> type. <tt>Either a b</tt> can be thought of
--   as a 2-tuple <tt>(tag, value)</tt>, where the value of the tag
--   determines the type of the value. In particular, either <tt>tag =
--   Left</tt> and <tt>value :: a</tt> or <tt>tag = Right</tt> and
--   <tt>value :: b</tt>.
--   
--   This package allows you to define your own dependent sum types by
--   using your own "tag" types.
@package dependent-sum
@version 0.6.1

module Data.GADT.Show

-- | <a>Show</a>-like class for 1-type-parameter GADTs. <tt>GShow t =&gt;
--   ...</tt> is equivalent to something like <tt>(forall a. Show (t a))
--   =&gt; ...</tt>. The easiest way to create instances would probably be
--   to write (or derive) an <tt>instance Show (T a)</tt>, and then simply
--   say:
--   
--   <pre>
--   instance GShow t where gshowsPrec = showsPrec
--   </pre>
class GShow t
gshowsPrec :: GShow t => Int -> t a -> ShowS
gshows :: GShow t => t a -> ShowS
gshow :: GShow t => t a -> String
newtype GReadResult t
GReadResult :: (forall b. (forall a. t a -> b) -> b) -> GReadResult t
[getGReadResult] :: GReadResult t -> forall b. (forall a. t a -> b) -> b

-- | <tt>GReadS t</tt> is equivalent to <tt>ReadS (forall b. (forall a. t a
--   -&gt; b) -&gt; b)</tt>, which is in turn equivalent to <tt>ReadS
--   (Exists t)</tt> (with <tt>data Exists t where Exists :: t a -&gt;
--   Exists t</tt>)
type GReadS t = String -> [(GReadResult t, String)]

-- | <a>Read</a>-like class for 1-type-parameter GADTs. Unlike
--   <a>GShow</a>, this one cannot be mechanically derived from a
--   <a>Read</a> instance because <a>greadsPrec</a> must choose the phantom
--   type based on the <a>String</a> being parsed.
class GRead t
greadsPrec :: GRead t => Int -> GReadS t
greads :: GRead t => GReadS t
gread :: GRead t => String -> (forall a. t a -> b) -> b

-- | <pre>
--   &gt;&gt;&gt; greadMaybe "InL Refl" mkSome :: Maybe (Some (Sum ((:~:) Int) ((:~:) Bool)))
--   Just (Some (InL Refl))
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; greadMaybe "garbage" mkSome :: Maybe (Some ((:~:) Int))
--   Nothing
--   </pre>
greadMaybe :: GRead t => String -> (forall a. t a -> b) -> Maybe b
instance forall k (a :: k). Data.GADT.Show.GRead ((Data.Type.Equality.:~:) a)
instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.Show.GRead a, Data.GADT.Show.GRead b) => Data.GADT.Show.GRead (Data.Functor.Sum.Sum a b)
instance forall k (a :: k). Data.GADT.Show.GShow ((Data.Type.Equality.:~:) a)
instance Data.GADT.Show.GShow Data.Typeable.Internal.TypeRep
instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.Show.GShow a, Data.GADT.Show.GShow b) => Data.GADT.Show.GShow (Data.Functor.Sum.Sum a b)
instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.Show.GShow a, Data.GADT.Show.GShow b) => Data.GADT.Show.GShow (Data.Functor.Product.Product a b)

module Data.GADT.Compare

-- | 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
gcompare :: GCompare f => f a -> f b -> GOrdering 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 b
[GLT] :: GOrdering a b
[GEQ] :: GOrdering t t
[GGT] :: GOrdering a b

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

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

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

-- | <i>Deprecated: use '(:~:)' from 'Data.Type,Equality'.</i>
type (:=) = (:~:)

-- | If <tt>f</tt> has a <a>GEq</a> instance, this function makes a
--   suitable default implementation of '(==)'.
defaultEq :: GEq f => f a -> f b -> Bool

-- | If <tt>f</tt> has a <a>GEq</a> instance, this function makes a
--   suitable default implementation of '(/=)'.
defaultNeq :: GEq f => f a -> f b -> Bool

-- | TODO: Think of a better name
--   
--   This operation forgets the phantom types of a <a>GOrdering</a> value.
weakenOrdering :: GOrdering a b -> Ordering
defaultCompare :: GCompare f => f a -> f b -> Ordering

-- | Propositional equality. If <tt>a :~: b</tt> is inhabited by some
--   terminating value, then the type <tt>a</tt> is the same as the type
--   <tt>b</tt>. To use this equality in practice, pattern-match on the
--   <tt>a :~: b</tt> to get out the <tt>Refl</tt> constructor; in the body
--   of the pattern-match, the compiler knows that <tt>a ~ b</tt>.
data (:~:) (a :: k) (b :: k) :: forall k. () => k -> k -> Type
[Refl] :: forall k (a :: k) (b :: k). () => a :~: a
infix 4 :~:
instance forall k (a :: k). Data.GADT.Compare.GCompare ((Data.Type.Equality.:~:) a)
instance Data.GADT.Compare.GCompare Data.Typeable.Internal.TypeRep
instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.Compare.GCompare a, Data.GADT.Compare.GCompare b) => Data.GADT.Compare.GCompare (Data.Functor.Sum.Sum a b)
instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.Compare.GCompare a, Data.GADT.Compare.GCompare b) => Data.GADT.Compare.GCompare (Data.Functor.Product.Product a b)
instance forall k (a :: k) (b :: k). GHC.Classes.Eq (Data.GADT.Compare.GOrdering a b)
instance forall k (a :: k) (b :: k). GHC.Classes.Ord (Data.GADT.Compare.GOrdering a b)
instance forall k (a :: k) (b :: k). GHC.Show.Show (Data.GADT.Compare.GOrdering a b)
instance forall k (a :: k). Data.GADT.Show.GShow (Data.GADT.Compare.GOrdering a)
instance forall k (a :: k). Data.GADT.Show.GRead (Data.GADT.Compare.GOrdering a)
instance forall k (a :: k). Data.GADT.Compare.GEq ((Data.Type.Equality.:~:) a)
instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.Compare.GEq a, Data.GADT.Compare.GEq b) => Data.GADT.Compare.GEq (Data.Functor.Sum.Sum a b)
instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.Compare.GEq a, Data.GADT.Compare.GEq b) => Data.GADT.Compare.GEq (Data.Functor.Product.Product a b)
instance Data.GADT.Compare.GEq Data.Typeable.Internal.TypeRep

module Data.Dependent.Sum

-- | A basic dependent sum type; the first component is a tag that
--   specifies the type of the second; for example, think of a GADT such
--   as:
--   
--   <pre>
--   data Tag a where
--      AString :: Tag String
--      AnInt   :: Tag Int
--   </pre>
--   
--   Then, we have the following valid expressions of type <tt>Applicative
--   f =&gt; DSum Tag f</tt>:
--   
--   <pre>
--   AString ==&gt; "hello!"
--   AnInt   ==&gt; 42
--   </pre>
--   
--   And we can write functions that consume <tt>DSum Tag f</tt> values by
--   matching, such as:
--   
--   <pre>
--   toString :: DSum Tag Identity -&gt; String
--   toString (AString :=&gt; Identity str) = str
--   toString (AnInt   :=&gt; Identity int) = show int
--   </pre>
--   
--   By analogy to the (key =&gt; value) construction for dictionary
--   entries in many dynamic languages, we use (key :=&gt; value) as the
--   constructor for dependent sums. The :=&gt; and ==&gt; operators have
--   very low precedence and bind to the right, so if the <tt>Tag</tt> GADT
--   is extended with an additional constructor <tt>Rec :: Tag (DSum Tag
--   Identity)</tt>, then <tt>Rec ==&gt; AnInt ==&gt; 3 + 4</tt> is parsed
--   as would be expected (<tt>Rec ==&gt; (AnInt ==&gt; (3 + 4))</tt>) and
--   has type <tt>DSum Identity Tag</tt>. Its precedence is just above that
--   of <a>$</a>, so <tt>foo bar $ AString ==&gt; "eep"</tt> is equivalent
--   to <tt>foo bar (AString ==&gt; "eep")</tt>.
data DSum tag f
(:=>) :: !tag a -> f a -> DSum tag f
infixr 1 :=>
(==>) :: Applicative f => tag a -> a -> DSum tag f
infixr 1 ==>

-- | <i>Deprecated: Instead of 'ShowTag tag f', use '(GShow tag, Has' Show
--   tag f)'</i>
type ShowTag tag f = (GShow tag, Has' Show tag f)
showTaggedPrec :: forall tag f a. (GShow tag, Has' Show tag f) => tag a -> Int -> f a -> ShowS

-- | <i>Deprecated: Instead of 'ReadTag tag f', use '(GRead tag, Has' Read
--   tag f)'</i>
type ReadTag tag f = (GRead tag, Has' Read tag f)
readTaggedPrec :: forall tag f a. (GRead tag, Has' Read tag f) => tag a -> Int -> ReadS (f a)

-- | <i>Deprecated: Instead of 'EqTag tag f', use '(GEq tag, Has' Eq tag
--   f)'</i>
type EqTag tag f = (GEq tag, Has' Eq tag f)
eqTaggedPrec :: forall tag f a. (GEq tag, Has' Eq tag f) => tag a -> tag a -> f a -> f a -> Bool
eqTagged :: forall tag f a. EqTag tag f => tag a -> tag a -> f a -> f a -> Bool

-- | <i>Deprecated: Instead of 'OrdTag tag f', use '(GCompare tag, Has' Eq
--   tag f, Has' Ord tag f)'</i>
type OrdTag tag f = (GCompare tag, Has' Eq tag f, Has' Ord tag f)
compareTaggedPrec :: forall tag f a. (GCompare tag, Has' Eq tag f, Has' Ord tag f) => tag a -> tag a -> f a -> f a -> Ordering
compareTagged :: forall tag f a. OrdTag tag f => tag a -> tag a -> f a -> f a -> Ordering
instance forall k (tag :: k -> *) (f :: k -> *). (Data.GADT.Show.GShow tag, Data.Constraint.Extras.Has' GHC.Show.Show tag f) => GHC.Show.Show (Data.Dependent.Sum.DSum tag f)
instance forall k (tag :: k -> *) (f :: k -> *). (Data.GADT.Show.GRead tag, Data.Constraint.Extras.Has' GHC.Read.Read tag f) => GHC.Read.Read (Data.Dependent.Sum.DSum tag f)
instance forall k (tag :: k -> *) (f :: k -> *). (Data.GADT.Compare.GEq tag, Data.Constraint.Extras.Has' GHC.Classes.Eq tag f) => GHC.Classes.Eq (Data.Dependent.Sum.DSum tag f)
instance forall k (tag :: k -> *) (f :: k -> *). (Data.GADT.Compare.GCompare tag, Data.Constraint.Extras.Has' GHC.Classes.Eq tag f, Data.Constraint.Extras.Has' GHC.Classes.Ord tag f) => GHC.Classes.Ord (Data.Dependent.Sum.DSum tag f)

module Data.Some

-- | Existential. This is type is useful to hide GADTs' parameters.
--   
--   <pre>
--   &gt;&gt;&gt; data Tag :: * -&gt; * where TagInt :: Tag Int; TagBool :: Tag Bool
--   
--   &gt;&gt;&gt; instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"
--   </pre>
--   
--   You can either use <tt>PatternSynonyms</tt>
--   
--   <pre>
--   &gt;&gt;&gt; let x = Some TagInt
--   
--   &gt;&gt;&gt; x
--   Some TagInt
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; case x of { Some TagInt -&gt; "I"; Some TagBool -&gt; "B" } :: String
--   "I"
--   </pre>
--   
--   or you can use functions
--   
--   <pre>
--   &gt;&gt;&gt; let y = mkSome TagBool
--   
--   &gt;&gt;&gt; y
--   Some TagBool
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; withSome y $ \y' -&gt; case y' of { TagInt -&gt; "I"; TagBool -&gt; "B" } :: String
--   "B"
--   </pre>
--   
--   The implementation of <a>mapSome</a> is <i>safe</i>.
--   
--   <pre>
--   &gt;&gt;&gt; let f :: Tag a -&gt; Tag a; f TagInt = TagInt; f TagBool = TagBool
--   
--   &gt;&gt;&gt; mapSome f y
--   Some TagBool
--   </pre>
--   
--   but you can also use:
--   
--   <pre>
--   &gt;&gt;&gt; withSome y (mkSome . f)
--   Some TagBool
--   </pre>
data Some tag
pattern Some :: tag a -> Some tag

-- | <i>Deprecated: Use <a>Some</a> instead</i>
pattern This :: tag a -> Some tag

-- | Constructor.
mkSome :: tag a -> Some tag

-- | Eliminator.
withSome :: Some tag -> (forall a. tag a -> b) -> b
mapSome :: (forall t. f t -> g t) -> Some f -> Some g
instance forall k (tag :: k -> *). Data.GADT.Show.GShow tag => GHC.Show.Show (Data.Some.Some tag)
instance forall k (f :: k -> *). Data.GADT.Show.GRead f => GHC.Read.Read (Data.Some.Some f)
instance forall k (tag :: k -> *). Data.GADT.Compare.GEq tag => GHC.Classes.Eq (Data.Some.Some tag)
instance forall k (tag :: k -> *). Data.GADT.Compare.GCompare tag => GHC.Classes.Ord (Data.Some.Some tag)