-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Existential type: Some -- -- This library defines an existential type Some. -- -- 
--   data Some f where
--       Some :: f a -> Some f
--
-- -- in few variants, and utilities to work with it. -- -- If you are unsure which variant to use, use the one in -- Data.Some module. @package some @version 1.0.5 module Data.EqP -- | Heterogenous lifted equality. -- -- This class is stronger version of Eq1 from base -- -- 
--   class (forall a. Eq a => Eq (f a)) => Eq1 f where
--       liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
--
-- -- as we don't require a a -> b -> Bool function. -- -- Morally Eq1 should be a superclass of EqP, but it -- cannot be, as GHC wouldn't allow EqP to be polykinded. -- https://gitlab.haskell.org/ghc/ghc/-/issues/22682 -- --

Laws

-- -- -- -- Note: P stands for phantom. class (forall a. Eq (f a)) => EqP (f :: k -> Type) eqp :: EqP f => f a -> f b -> Bool instance forall k (a :: k). Data.EqP.EqP ((Data.Type.Equality.:~:) a) instance forall k1 k (a :: k1). Data.EqP.EqP ((Data.Type.Equality.:~~:) a) instance forall k (f :: k -> *) (g :: k -> *). (Data.EqP.EqP f, Data.EqP.EqP g) => Data.EqP.EqP (f GHC.Generics.:+: g) instance forall k (a :: k -> *) (b :: k -> *). (Data.EqP.EqP a, Data.EqP.EqP b) => Data.EqP.EqP (a GHC.Generics.:*: b) instance Data.EqP.EqP Data.Typeable.Internal.TypeRep instance Data.EqP.EqP Data.Proxy.Proxy instance GHC.Classes.Eq a => Data.EqP.EqP (Data.Functor.Const.Const a) instance Data.EqP.EqP GHC.StableName.StableName module Data.GADT.DeepSeq class GNFData f grnf :: GNFData f => f a -> () instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.DeepSeq.GNFData a, Data.GADT.DeepSeq.GNFData b) => Data.GADT.DeepSeq.GNFData (Data.Functor.Product.Product a b) instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.DeepSeq.GNFData a, Data.GADT.DeepSeq.GNFData b) => Data.GADT.DeepSeq.GNFData (Data.Functor.Sum.Sum a b) instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.DeepSeq.GNFData a, Data.GADT.DeepSeq.GNFData b) => Data.GADT.DeepSeq.GNFData (a GHC.Generics.:*: b) instance forall k (a :: k -> *) (b :: k -> *). (Data.GADT.DeepSeq.GNFData a, Data.GADT.DeepSeq.GNFData b) => Data.GADT.DeepSeq.GNFData (a GHC.Generics.:+: b) instance forall k (a :: k). Data.GADT.DeepSeq.GNFData ((Data.Type.Equality.:~:) a) instance forall k1 k (a :: k1). Data.GADT.DeepSeq.GNFData ((Data.Type.Equality.:~~:) a) instance Data.GADT.DeepSeq.GNFData Data.Typeable.Internal.TypeRep module Data.GADT.Compare -- | A class for type-contexts which contain enough information to (at -- least in some cases) decide the equality of types occurring within -- them. -- -- This class is sometimes confused with TestEquality from base. -- TestEquality only checks type equality. -- -- Consider -- -- 
--   >>> data Tag a where TagInt1 :: Tag Int; TagInt2 :: Tag Int
--
-- -- The correct TestEquality Tag instance is -- -- 
--   >>> :{
--   instance TestEquality Tag where
--       testEquality TagInt1 TagInt1 = Just Refl
--       testEquality TagInt1 TagInt2 = Just Refl
--       testEquality TagInt2 TagInt1 = Just Refl
--       testEquality TagInt2 TagInt2 = Just Refl
--   :}
--
-- -- While we can define -- -- 
--   instance GEq Tag where
--      geq = testEquality
--
-- -- this will mean we probably want to have -- -- 
--   instance Eq Tag where
--      _ == _ = True
--
-- -- Note: In the future version of some package (to be -- released around GHC-9.6 / 9.8) the forall a. Eq (f a) -- constraint will be added as a constraint to GEq, with a law -- relating GEq and Eq: -- -- 
--   geq x y = Just Refl   ⇒  x == y = True        ∀ (x :: f a) (y :: f b)
--   x == y                ≡  isJust (geq x y)     ∀ (x, y :: f a)
--
-- -- So, the more useful GEq Tag instance would -- differentiate between different constructors: -- -- 
--   >>> :{
--   instance GEq Tag where
--       geq TagInt1 TagInt1 = Just Refl
--       geq TagInt1 TagInt2 = Nothing
--       geq TagInt2 TagInt1 = Nothing
--       geq TagInt2 TagInt2 = Just Refl
--   :}
--
-- -- which is consistent with a derived Eq instance for Tag -- -- 
--   >>> deriving instance Eq (Tag a)
--
-- -- Note that even if a ~ b, the geq (x :: f a) (y :: -- f b) may be Nothing (when value terms are inequal). -- -- The consistency of GEq and Eq is easy to check by -- exhaustion: -- -- 
--   >>> let checkFwdGEq :: (forall a. Eq (f a), GEq f) => f a -> f b -> Bool; checkFwdGEq x y = case geq x y of Just Refl -> x == y; Nothing -> True
--   
--   >>> (checkFwdGEq TagInt1 TagInt1, checkFwdGEq TagInt1 TagInt2, checkFwdGEq TagInt2 TagInt1, checkFwdGEq TagInt2 TagInt2)
--   (True,True,True,True)
--
-- -- 
--   >>> let checkBwdGEq :: (Eq (f a), GEq f) => f a -> f a -> Bool; checkBwdGEq x y = if x == y then isJust (geq x y) else isNothing (geq x y)
--   
--   >>> (checkBwdGEq TagInt1 TagInt1, checkBwdGEq TagInt1 TagInt2, checkBwdGEq TagInt2 TagInt1, checkBwdGEq TagInt2 TagInt2)
--   (True,True,True,True)
--
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.: -- -- 
--   extract :: GEq tag => tag a -> DSum tag -> Maybe a
--   extract t1 (t2 :=> x) = do
--       Refl <- geq t1 t2
--       return x
--
-- -- Or in a list comprehension: -- -- 
--   extractMany :: GEq tag => tag a -> [DSum tag] -> [a]
--   extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]
--
-- -- (Making use of the DSum type from Data.Dependent.Sum -- in both examples) geq :: GEq f => f a -> f b -> Maybe (a :~: b) -- | If f has a GCompare instance, this function makes a -- suitable default implementation of geq. defaultGeq :: GCompare f => f a -> f b -> Maybe (a :~: b) -- | If f has a GEq instance, this function makes a -- suitable default implementation of (==). defaultEq :: GEq f => f a -> f b -> Bool -- | If f has a GEq instance, this function makes a -- suitable default implementation of (/=). defaultNeq :: GEq f => f a -> f b -> Bool -- | Type class for comparable GADT-like structures. When 2 things are -- equal, must return a witness that their parameter types are equal as -- well (GEQ). class GEq f => GCompare f gcompare :: GCompare f => f a -> f b -> GOrdering a b defaultCompare :: GCompare f => f a -> f b -> Ordering -- | 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 module Data.GADT.Show -- | Show-like class for 1-type-parameter GADTs. GShow t => -- ... is equivalent to something like (forall a. Show (t a)) -- => .... The easiest way to create instances would probably be -- to write (or derive) an instance Show (T a), and then simply -- say: -- -- 
--   instance GShow t where gshowsPrec = defaultGshowsPrec
--
class GShow t gshowsPrec :: GShow t => Int -> t a -> ShowS -- | If f has a 'Show (f a)' instance, this function makes a -- suitable default implementation of gshowsPrec. defaultGshowsPrec :: Show (t a) => Int -> t a -> ShowS gshows :: GShow t => t a -> ShowS gshow :: GShow t => t a -> String -- | Read-like class for 1-type-parameter GADTs. Unlike -- GShow, this one cannot be mechanically derived from a -- Read instance because greadsPrec must choose the phantom -- type based on the String being parsed. class GRead t greadsPrec :: GRead t => Int -> GReadS t -- | GReadS t is equivalent to ReadS (forall b. (forall a. t a -- -> b) -> b), which is in turn equivalent to ReadS -- (Exists t) (with data Exists t where Exists :: t a -> -- Exists t) type GReadS t = String -> [(Some t, String)] greads :: GRead t => GReadS t gread :: GRead t => String -> (forall a. t a -> b) -> b -- | 
--   >>> greadMaybe "InL Refl" mkSome :: Maybe (Some (Sum ((:~:) Int) ((:~:) Bool)))
--   Just (mkSome (InL Refl))
--
-- -- 
--   >>> greadMaybe "L1 Refl" mkSome :: Maybe (Some ((:~:) Int :+: (:~:) Bool))
--   Just (mkSome (L1 Refl))
--
-- -- 
--   >>> greadMaybe "garbage" mkSome :: Maybe (Some ((:~:) Int))
--   Nothing
--
greadMaybe :: GRead t => String -> (forall a. t a -> b) -> Maybe b getGReadResult :: Some tag -> (forall a. tag a -> b) -> b mkGReadResult :: tag a -> Some tag module Data.OrdP -- | Heterogenous lifted total order. -- -- This class is stronger version of Ord1 from base -- -- 
--   class (forall a. Ord a => Ord (f a)) => Ord1 f where
--       liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering
--
class (EqP f, forall a. Ord (f a)) => OrdP (f :: k -> Type) comparep :: OrdP f => f a -> f b -> Ordering instance forall k (a :: k). Data.OrdP.OrdP ((Data.Type.Equality.:~:) a) instance forall k1 k (a :: k1). Data.OrdP.OrdP ((Data.Type.Equality.:~~:) a) instance forall k (f :: k -> *) (g :: k -> *). (Data.OrdP.OrdP f, Data.OrdP.OrdP g) => Data.OrdP.OrdP (f GHC.Generics.:+: g) instance forall k (a :: k -> *) (b :: k -> *). (Data.OrdP.OrdP a, Data.OrdP.OrdP b) => Data.OrdP.OrdP (a GHC.Generics.:*: b) instance Data.OrdP.OrdP Data.Typeable.Internal.TypeRep instance Data.OrdP.OrdP Data.Proxy.Proxy instance GHC.Classes.Ord a => Data.OrdP.OrdP (Data.Functor.Const.Const a) module Data.Some.Church -- | Existential. This is type is useful to hide GADTs' parameters. -- -- 
--   >>> data Tag :: * -> * where TagInt :: Tag Int; TagBool :: Tag Bool
--   
--   >>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"
--   
--   >>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []
--   
--   >>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]
--
-- -- With Church-encoding youcan only use a functions: -- -- 
--   >>> let y = mkSome TagBool
--   
--   >>> y
--   mkSome TagBool
--
-- -- 
--   >>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String
--   "B"
--
-- -- or explicitly work with S -- -- 
--   >>> let x = S $ \f -> f TagInt
--   
--   >>> x
--   mkSome TagInt
--
-- -- 
--   >>> case x of S f -> f $ \x' -> case x' of { TagInt -> "I"; TagBool -> "B" } :: String
--   "I"
--
-- -- The implementation of mapSome is safe. -- -- 
--   >>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool
--   
--   >>> mapSome f y
--   mkSome TagBool
--
-- -- but you can also use: -- -- 
--   >>> withSome y (mkSome . f)
--   mkSome TagBool
--
-- -- 
--   >>> read "Some TagBool" :: Some Tag
--   mkSome TagBool
--
-- -- 
--   >>> read "mkSome TagInt" :: Some Tag
--   mkSome TagInt
--
newtype Some tag S :: (forall r. (forall a. tag a -> r) -> r) -> Some tag -- | Eliminator. [withSome] :: Some tag -> forall r. (forall a. tag a -> r) -> r -- | Constructor. mkSome :: tag a -> Some tag -- | Map over argument. mapSome :: (forall x. f x -> g x) -> Some f -> Some g -- | Monadic withSome. withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r -- | 
--   flip withSome
--
foldSome :: (forall a. tag a -> b) -> Some tag -> b -- | Traverse over argument. traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g) module Data.Some.GADT -- | Existential. This is type is useful to hide GADTs' parameters. -- -- 
--   >>> data Tag :: Type -> Type where TagInt :: Tag Int; TagBool :: Tag Bool
--   
--   >>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"
--   
--   >>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []
--   
--   >>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]
--
-- -- You can either use constructor: -- -- 
--   >>> let x = Some TagInt
--   
--   >>> x
--   Some TagInt
--
-- -- 
--   >>> case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String
--   "I"
--
-- -- or you can use functions -- -- 
--   >>> let y = mkSome TagBool
--   
--   >>> y
--   Some TagBool
--
-- -- 
--   >>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String
--   "B"
--
-- -- The implementation of mapSome is safe. -- -- 
--   >>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool
--   
--   >>> mapSome f y
--   Some TagBool
--
-- -- but you can also use: -- -- 
--   >>> withSome y (mkSome . f)
--   Some TagBool
--
-- -- 
--   >>> read "Some TagBool" :: Some Tag
--   Some TagBool
--
-- -- 
--   >>> read "mkSome TagInt" :: Some Tag
--   Some TagInt
--
data Some tag [Some] :: tag a -> Some tag -- | Constructor. mkSome :: tag a -> Some tag -- | Eliminator. withSome :: Some tag -> (forall a. tag a -> b) -> b -- | Monadic withSome. withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r -- | Map over argument. mapSome :: (forall x. f x -> g x) -> Some f -> Some g -- | 
--   flip withSome
--
foldSome :: (forall a. tag a -> b) -> Some tag -> b -- | Traverse over argument. traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g) instance forall k (tag :: k -> *). Data.GADT.Internal.GShow tag => GHC.Show.Show (Data.Some.GADT.Some tag) instance forall k (f :: k -> *). Data.GADT.Internal.GRead f => GHC.Read.Read (Data.Some.GADT.Some f) instance forall k (tag :: k -> *). Data.GADT.Internal.GEq tag => GHC.Classes.Eq (Data.Some.GADT.Some tag) instance forall k (tag :: k -> *). Data.GADT.Internal.GCompare tag => GHC.Classes.Ord (Data.Some.GADT.Some tag) instance forall k (tag :: k -> *). Data.GADT.DeepSeq.GNFData tag => Control.DeepSeq.NFData (Data.Some.GADT.Some tag) instance GHC.Base.Applicative m => GHC.Base.Semigroup (Data.Some.GADT.Some m) instance GHC.Base.Applicative m => GHC.Base.Monoid (Data.Some.GADT.Some m) module Data.Some.Newtype -- | Existential. This is type is useful to hide GADTs' parameters. -- -- 
--   >>> data Tag :: Type -> Type where TagInt :: Tag Int; TagBool :: Tag Bool
--   
--   >>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"
--   
--   >>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []
--   
--   >>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]
--
-- -- You can either use PatternSynonyms (available with GHC >= -- 8.0) -- -- 
--   >>> let x = Some TagInt
--   
--   >>> x
--   Some TagInt
--
-- -- 
--   >>> case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String
--   "I"
--
-- -- or you can use functions -- -- 
--   >>> let y = mkSome TagBool
--   
--   >>> y
--   Some TagBool
--
-- -- 
--   >>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String
--   "B"
--
-- -- The implementation of mapSome is safe. -- -- 
--   >>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool
--   
--   >>> mapSome f y
--   Some TagBool
--
-- -- but you can also use: -- -- 
--   >>> withSome y (mkSome . f)
--   Some TagBool
--
-- -- 
--   >>> read "Some TagBool" :: Some Tag
--   Some TagBool
--
-- -- 
--   >>> read "mkSome TagInt" :: Some Tag
--   Some TagInt
--
data Some tag pattern Some :: tag a -> Some tag -- | Constructor. mkSome :: tag a -> Some tag -- | Eliminator. withSome :: Some tag -> (forall a. tag a -> b) -> b -- | Monadic withSome. withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r -- | Map over argument. mapSome :: (forall t. f t -> g t) -> Some f -> Some g -- | 
--   flip withSome
--
foldSome :: (forall a. tag a -> b) -> Some tag -> b -- | Traverse over argument. traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g) instance forall k (tag :: k -> *). Data.GADT.Internal.GShow tag => GHC.Show.Show (Data.Some.Newtype.Some tag) instance forall k (f :: k -> *). Data.GADT.Internal.GRead f => GHC.Read.Read (Data.Some.Newtype.Some f) instance forall k (tag :: k -> *). Data.GADT.Internal.GEq tag => GHC.Classes.Eq (Data.Some.Newtype.Some tag) instance forall k (tag :: k -> *). Data.GADT.Internal.GCompare tag => GHC.Classes.Ord (Data.Some.Newtype.Some tag) instance forall k (tag :: k -> *). Data.GADT.DeepSeq.GNFData tag => Control.DeepSeq.NFData (Data.Some.Newtype.Some tag) instance GHC.Base.Applicative m => GHC.Base.Semigroup (Data.Some.Newtype.Some m) instance GHC.Base.Applicative m => GHC.Base.Monoid (Data.Some.Newtype.Some m) -- | An existential type. -- -- The constructor is exported only on GHC-8 and later. module Data.Some -- | Existential. This is type is useful to hide GADTs' parameters. -- -- 
--   >>> data Tag :: Type -> Type where TagInt :: Tag Int; TagBool :: Tag Bool
--   
--   >>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"
--   
--   >>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []
--   
--   >>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]
--
-- -- You can either use PatternSynonyms (available with GHC >= -- 8.0) -- -- 
--   >>> let x = Some TagInt
--   
--   >>> x
--   Some TagInt
--
-- -- 
--   >>> case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String
--   "I"
--
-- -- or you can use functions -- -- 
--   >>> let y = mkSome TagBool
--   
--   >>> y
--   Some TagBool
--
-- -- 
--   >>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String
--   "B"
--
-- -- The implementation of mapSome is safe. -- -- 
--   >>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool
--   
--   >>> mapSome f y
--   Some TagBool
--
-- -- but you can also use: -- -- 
--   >>> withSome y (mkSome . f)
--   Some TagBool
--
-- -- 
--   >>> read "Some TagBool" :: Some Tag
--   Some TagBool
--
-- -- 
--   >>> read "mkSome TagInt" :: Some Tag
--   Some TagInt
--
data Some tag pattern Some :: tag a -> Some tag -- | Constructor. mkSome :: tag a -> Some tag -- | Eliminator. withSome :: Some tag -> (forall a. tag a -> b) -> b -- | Monadic withSome. withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r -- | Map over argument. mapSome :: (forall t. f t -> g t) -> Some f -> Some g -- | 
--   flip withSome
--
foldSome :: (forall a. tag a -> b) -> Some tag -> b -- | Traverse over argument. traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g)