    {-# LANGUAGE CPP                      #-}
    {-# LANGUAGE GADTs                    #-}
    {-# LANGUAGE PolyKinds                #-}
    {-# LANGUAGE RankNTypes               #-}
    {-# LANGUAGE RoleAnnotations          #-}
    {-# LANGUAGE Safe                     #-}
    {-# LANGUAGE ScopedTypeVariables      #-}
    {-# LANGUAGE TypeOperators            #-}
    #if __GLASGOW_HASKELL__ >= 810
    {-# LANGUAGE StandaloneKindSignatures #-}
    #endif
    module Data.GADT.Internal where

    import Control.Applicative  (Applicative (..))
    import Data.Functor.Product (Product (..))
    import Data.Functor.Sum     (Sum (..))
    import Data.Kind            (Type)
    import Data.Maybe           (isJust, isNothing)
    import Data.Monoid          (Monoid (..))
    import Data.Semigroup       (Semigroup (..))
    import Data.Type.Equality   (TestEquality (..), (:~:) (..), (:~~:) (..))
    import GHC.Generics         ((:*:) (..), (:+:) (..))

    import qualified Type.Reflection as TR

    #if __GLASGOW_HASKELL__ >= 810
    import Data.Kind (Constraint)
    #endif

    -- $setup
    -- >>> :set -XKindSignatures -XGADTs -XTypeOperators -XStandaloneDeriving -XQuantifiedConstraints
    -- >>> import Data.Type.Equality
    -- >>> import Data.Functor.Sum
    -- >>> import Data.Maybe (isJust, isNothing)
    -- >>> import GHC.Generics

    -- |'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
    #if __GLASGOW_HASKELL__ >= 810
    type GShow :: (k -> Type) -> Constraint
    #endif
    class GShow t where
        gshowsPrec :: Int -> t a -> ShowS

    -- |If 'f' has a 'Show (f a)' instance, this function makes a suitable default
    -- implementation of 'gshowsPrec'.
    --
    -- @since 1.0.4
    defaultGshowsPrec :: Show (t a) => Int -> t a -> ShowS
    defaultGshowsPrec :: forall {k} (t :: k -> *) (a :: k).
    Show (t a) =>
    Int -> t a -> ShowS
    defaultGshowsPrec = Int -> t a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec

    gshows :: GShow t => t a -> ShowS
    gshows :: forall {k} (t :: k -> *) (a :: k). GShow t => t a -> ShowS
    gshows = Int -> t a -> ShowS
    forall (a :: k). Int -> t a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec (-Int
    1)

    gshow :: (GShow t) => t a -> String
    gshow :: forall {k} (t :: k -> *) (a :: k). GShow t => t a -> String
    gshow t a
    x = t a -> ShowS
    forall {k} (t :: k -> *) (a :: k). GShow t => t a -> ShowS
    gshows t a
    x String
    ""

    instance GShow ((:~:) a) where
        gshowsPrec :: forall (a :: k). Int -> (a :~: a) -> ShowS
    gshowsPrec Int
    _ a :~: a
    Refl = String -> ShowS
    showString String
    "Refl"

    -- | @since 1.0.4
    instance GShow ((:~~:) a) where
        gshowsPrec :: forall (a :: k). Int -> (a :~~: a) -> ShowS
    gshowsPrec Int
    _ a :~~: a
    HRefl = String -> ShowS
    showString String
    "HRefl"

    instance GShow TR.TypeRep where
        gshowsPrec :: forall (a :: k). Int -> TypeRep a -> ShowS
    gshowsPrec = Int -> TypeRep a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec

    --
    -- | >>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)
    -- "InL Refl"
    instance (GShow a, GShow b) => GShow (Sum a b) where
        gshowsPrec :: forall (a :: k). Int -> Sum a b a -> ShowS
    gshowsPrec Int
    d = \Sum a b a
    s -> case Sum a b a
    s of
            InL a a
    x -> Bool -> ShowS -> ShowS
    showParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10) (String -> ShowS
    showString String
    "InL " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> a a -> ShowS
    forall (a :: k). Int -> a a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    11 a a
    x)
            InR b a
    x -> Bool -> ShowS -> ShowS
    showParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10) (String -> ShowS
    showString String
    "InR " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> b a -> ShowS
    forall (a :: k). Int -> b a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    11 b a
    x)

    -- | >>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)
    -- "Pair Refl Refl"
    instance (GShow a, GShow b) => GShow (Product a b) where
        gshowsPrec :: forall (a :: k). Int -> Product a b a -> ShowS
    gshowsPrec Int
    d (Pair a a
    x b a
    y) = Bool -> ShowS -> ShowS
    showParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10)
            (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ String -> ShowS
    showString String
    "Pair "
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> a a -> ShowS
    forall (a :: k). Int -> a a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    11 a a
    x
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Char -> ShowS
    showChar Char
    ' '
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> b a -> ShowS
    forall (a :: k). Int -> b a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    11 b a
    y

    --
    -- | >>> gshow (L1 Refl :: ((:~:) Int :+: (:~:) Bool) Int)
    -- "L1 Refl"
    --
    -- @since 1.0.4
    instance (GShow a, GShow b) => GShow (a :+: b) where
        gshowsPrec :: forall (a :: k). Int -> (:+:) a b a -> ShowS
    gshowsPrec Int
    d = \(:+:) a b a
    s -> case (:+:) a b a
    s of
            L1 a a
    x -> Bool -> ShowS -> ShowS
    showParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10) (String -> ShowS
    showString String
    "L1 " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> a a -> ShowS
    forall (a :: k). Int -> a a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    11 a a
    x)
            R1 b a
    x -> Bool -> ShowS -> ShowS
    showParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10) (String -> ShowS
    showString String
    "R1 " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> b a -> ShowS
    forall (a :: k). Int -> b a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    11 b a
    x)

    -- | >>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)
    -- "Refl :*: Refl"
    --
    -- @since 1.0.4
    instance (GShow a, GShow b) => GShow (a :*: b) where
        gshowsPrec :: forall (a :: k). Int -> (:*:) a b a -> ShowS
    gshowsPrec Int
    d (a a
    x :*: b a
    y) = Bool -> ShowS -> ShowS
    showParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    6)
            (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Int -> a a -> ShowS
    forall (a :: k). Int -> a a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    6 a a
    x
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    " :*: "
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> b a -> ShowS
    forall (a :: k). Int -> b a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    6 b a
    y

    -- |@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@)
    #if __GLASGOW_HASKELL__ >= 810
    type GReadS :: (k -> Type) -> Type
    #endif
    type GReadS t = String -> [(Some t, String)]

    getGReadResult :: Some tag -> (forall a. tag a -> b) -> b
    getGReadResult :: forall {k} (tag :: k -> *) b.
    Some tag -> (forall (a :: k). tag a -> b) -> b
    getGReadResult Some tag
    t forall (a :: k). tag a -> b
    k = Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some tag
    t tag a -> b
    forall (a :: k). tag a -> b
    k

    mkGReadResult :: tag a -> Some tag
    mkGReadResult :: forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkGReadResult = tag a -> Some tag
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome

    -- |'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.
    #if __GLASGOW_HASKELL__ >= 810
    type GRead :: (k -> Type) -> Constraint
    #endif
    class GRead t where
        greadsPrec :: Int -> GReadS t

    greads :: GRead t => GReadS t
    greads :: forall {k} (t :: k -> *). GRead t => GReadS t
    greads = Int -> GReadS t
    forall k (t :: k -> *). GRead t => Int -> GReadS t
    greadsPrec (-Int
    1)

    gread :: GRead t => String -> (forall a. t a -> b) -> b
    gread :: forall {k} (t :: k -> *) b.
    GRead t =>
    String -> (forall (a :: k). t a -> b) -> b
    gread String
    s forall (a :: k). t a -> b
    g = Some t -> forall r. (forall (a :: k). t a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome ([Some t] -> Some t
    forall {a}. [a] -> a
    hd [Some t
    f | (Some t
    f, String
    "") <- GReadS t
    forall {k} (t :: k -> *). GRead t => GReadS t
    greads String
    s]) t a -> b
    forall (a :: k). t a -> b
    g where
        hd :: [a] -> a
    hd (a
    x:[a]
    _) = a
    x
        hd [a]
    _ = String -> a
    forall a. HasCallStack => String -> a
    error String
    "gread: no parse"

    -- |
    --
    -- >>> 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
    greadMaybe :: forall {k} (t :: k -> *) b.
    GRead t =>
    String -> (forall (a :: k). t a -> b) -> Maybe b
    greadMaybe String
    s forall (a :: k). t a -> b
    g = case [Some t
    f | (Some t
    f, String
    "") <- GReadS t
    forall {k} (t :: k -> *). GRead t => GReadS t
    greads String
    s] of
        (Some t
    x : [Some t]
    _) -> b -> Maybe b
    forall a. a -> Maybe a
    Just (Some t -> forall r. (forall (a :: k). t a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some t
    x t a -> b
    forall (a :: k). t a -> b
    g)
        [Some t]
    _       -> Maybe b
    forall a. Maybe a
    Nothing

    instance GRead ((:~:) a) where
        greadsPrec :: Int -> GReadS ((:~:) a)
    greadsPrec Int
    _ = Bool -> GReadS ((:~:) a) -> GReadS ((:~:) a)
    forall a. Bool -> ReadS a -> ReadS a
    readParen Bool
    False (\String
    s ->
            [ ((forall r. (forall (a :: k). (a :~: a) -> r) -> r)
    -> Some ((:~:) a)
    forall k (tag :: k -> *).
    (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    S ((forall r. (forall (a :: k). (a :~: a) -> r) -> r)
     -> Some ((:~:) a))
    -> (forall r. (forall (a :: k). (a :~: a) -> r) -> r)
    -> Some ((:~:) a)
    forall a b. (a -> b) -> a -> b
    $ \forall (a :: k). (a :~: a) -> r
    k -> (a :~: a) -> r
    forall (a :: k). (a :~: a) -> r
    k (a :~: a
    forall {k} (a :: k). a :~: a
    Refl :: a :~: a), String
    t)
            | (String
    "Refl", String
    t) <- ReadS String
    lex String
    s
            ])

    -- | @since 1.0.4
    instance k1 ~ k2 => GRead ((:~~:) (a :: k1) :: k2 -> Type) where
        greadsPrec :: Int -> GReadS ((:~~:) a)
    greadsPrec Int
    _ = Bool -> GReadS ((:~~:) a) -> GReadS ((:~~:) a)
    forall a. Bool -> ReadS a -> ReadS a
    readParen Bool
    False (\String
    s ->
            [ ((forall r. (forall (a :: k2). (a :~~: a) -> r) -> r)
    -> Some ((:~~:) a)
    forall k (tag :: k -> *).
    (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    S ((forall r. (forall (a :: k2). (a :~~: a) -> r) -> r)
     -> Some ((:~~:) a))
    -> (forall r. (forall (a :: k2). (a :~~: a) -> r) -> r)
    -> Some ((:~~:) a)
    forall a b. (a -> b) -> a -> b
    $ \forall (a :: k2). (a :~~: a) -> r
    k -> (a :~~: a) -> r
    forall (a :: k2). (a :~~: a) -> r
    k (a :~~: a
    forall {k1} (a :: k1). a :~~: a
    HRefl :: a :~~: a), String
    t)
            | (String
    "HRefl", String
    t) <- ReadS String
    lex String
    s
            ])

    instance (GRead a, GRead b) => GRead (Sum a b) where
        greadsPrec :: Int -> GReadS (Sum a b)
    greadsPrec Int
    d String
    s =
            Bool -> GReadS (Sum a b) -> GReadS (Sum a b)
    forall a. Bool -> ReadS a -> ReadS a
    readParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10)
                (\String
    s1 -> [ ((forall r. (forall (a :: k). Sum a b a -> r) -> r)
    -> Some (Sum a b)
    forall k (tag :: k -> *).
    (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    S ((forall r. (forall (a :: k). Sum a b a -> r) -> r)
     -> Some (Sum a b))
    -> (forall r. (forall (a :: k). Sum a b a -> r) -> r)
    -> Some (Sum a b)
    forall a b. (a -> b) -> a -> b
    $ \forall (a :: k). Sum a b a -> r
    k -> Some a -> forall r. (forall (a :: k). a a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some a
    r (Sum a b a -> r
    forall (a :: k). Sum a b a -> r
    k (Sum a b a -> r) -> (a a -> Sum a b a) -> a a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a a -> Sum a b a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL), String
    t)
                        | (String
    "InL", String
    s2) <- ReadS String
    lex String
    s1
                        , (Some a
    r, String
    t) <- Int -> GReadS a
    forall k (t :: k -> *). GRead t => Int -> GReadS t
    greadsPrec Int
    11 String
    s2 ]) String
    s
            [(Some (Sum a b), String)]
    -> [(Some (Sum a b), String)] -> [(Some (Sum a b), String)]
    forall a. [a] -> [a] -> [a]
    ++
            Bool -> GReadS (Sum a b) -> GReadS (Sum a b)
    forall a. Bool -> ReadS a -> ReadS a
    readParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10)
                (\String
    s1 -> [ ((forall r. (forall (a :: k). Sum a b a -> r) -> r)
    -> Some (Sum a b)
    forall k (tag :: k -> *).
    (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    S ((forall r. (forall (a :: k). Sum a b a -> r) -> r)
     -> Some (Sum a b))
    -> (forall r. (forall (a :: k). Sum a b a -> r) -> r)
    -> Some (Sum a b)
    forall a b. (a -> b) -> a -> b
    $ \forall (a :: k). Sum a b a -> r
    k -> Some b -> forall r. (forall (a :: k). b a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some b
    r (Sum a b a -> r
    forall (a :: k). Sum a b a -> r
    k (Sum a b a -> r) -> (b a -> Sum a b a) -> b a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b a -> Sum a b a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
    InR), String
    t)
                        | (String
    "InR", String
    s2) <- ReadS String
    lex String
    s1
                        , (Some b
    r, String
    t) <- Int -> GReadS b
    forall k (t :: k -> *). GRead t => Int -> GReadS t
    greadsPrec Int
    11 String
    s2 ]) String
    s

    -- | @since 1.0.4
    instance (GRead a, GRead b) => GRead (a :+: b) where
        greadsPrec :: Int -> GReadS (a :+: b)
    greadsPrec Int
    d String
    s =
            Bool -> GReadS (a :+: b) -> GReadS (a :+: b)
    forall a. Bool -> ReadS a -> ReadS a
    readParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10)
                (\String
    s1 -> [ ((forall r. (forall (a :: k). (:+:) a b a -> r) -> r)
    -> Some (a :+: b)
    forall k (tag :: k -> *).
    (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    S ((forall r. (forall (a :: k). (:+:) a b a -> r) -> r)
     -> Some (a :+: b))
    -> (forall r. (forall (a :: k). (:+:) a b a -> r) -> r)
    -> Some (a :+: b)
    forall a b. (a -> b) -> a -> b
    $ \forall (a :: k). (:+:) a b a -> r
    k -> Some a -> forall r. (forall (a :: k). a a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some a
    r ((:+:) a b a -> r
    forall (a :: k). (:+:) a b a -> r
    k ((:+:) a b a -> r) -> (a a -> (:+:) a b a) -> a a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a a -> (:+:) a b a
    forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
    L1), String
    t)
                        | (String
    "L1", String
    s2) <- ReadS String
    lex String
    s1
                        , (Some a
    r, String
    t) <- Int -> GReadS a
    forall k (t :: k -> *). GRead t => Int -> GReadS t
    greadsPrec Int
    11 String
    s2 ]) String
    s
            [(Some (a :+: b), String)]
    -> [(Some (a :+: b), String)] -> [(Some (a :+: b), String)]
    forall a. [a] -> [a] -> [a]
    ++
            Bool -> GReadS (a :+: b) -> GReadS (a :+: b)
    forall a. Bool -> ReadS a -> ReadS a
    readParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10)
                (\String
    s1 -> [ ((forall r. (forall (a :: k). (:+:) a b a -> r) -> r)
    -> Some (a :+: b)
    forall k (tag :: k -> *).
    (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    S ((forall r. (forall (a :: k). (:+:) a b a -> r) -> r)
     -> Some (a :+: b))
    -> (forall r. (forall (a :: k). (:+:) a b a -> r) -> r)
    -> Some (a :+: b)
    forall a b. (a -> b) -> a -> b
    $ \forall (a :: k). (:+:) a b a -> r
    k -> Some b -> forall r. (forall (a :: k). b a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some b
    r ((:+:) a b a -> r
    forall (a :: k). (:+:) a b a -> r
    k ((:+:) a b a -> r) -> (b a -> (:+:) a b a) -> b a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b a -> (:+:) a b a
    forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
    R1), String
    t)
                        | (String
    "R1", String
    s2) <- ReadS String
    lex String
    s1
                        , (Some b
    r, String
    t) <- Int -> GReadS b
    forall k (t :: k -> *). GRead t => Int -> GReadS t
    greadsPrec Int
    11 String
    s2 ]) String
    s

    -------------------------------------------------------------------------------
    -- GEq
    -------------------------------------------------------------------------------

    -- |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)
    --
    #if __GLASGOW_HASKELL__ >= 810
    type GEq :: (k -> Type) -> Constraint
    #endif
    class GEq f where
        -- |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 <https://hackage.haskell.org/package/dependent-sum/docs/Data-Dependent-Sum.html Data.Dependent.Sum> in both examples)
        geq :: f a -> f b -> Maybe (a :~: b)

    -- |If 'f' has a 'GCompare' instance, this function makes a suitable default
    -- implementation of 'geq'.
    --
    -- @since 1.0.4
    defaultGeq :: GCompare f => f a -> f b -> Maybe (a :~: b)
    defaultGeq :: forall {k} (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> Maybe (a :~: b)
    defaultGeq f a
    a f b
    b = case f a -> f b -> GOrdering a b
    forall (a :: k) (b :: k). f a -> f b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare f a
    a f b
    b of
        GOrdering a b
    GEQ -> (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl
        GOrdering a b
    _   -> Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    -- |If 'f' has a 'GEq' instance, this function makes a suitable default
    -- implementation of '(==)'.
    defaultEq :: GEq f => f a -> f b -> Bool
    defaultEq :: forall {k} (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Bool
    defaultEq f a
    x f b
    y = Maybe (a :~: b) -> Bool
    forall a. Maybe a -> Bool
    isJust (f a -> f b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq f a
    x f b
    y)

    -- |If 'f' has a 'GEq' instance, this function makes a suitable default
    -- implementation of '(/=)'.
    defaultNeq :: GEq f => f a -> f b -> Bool
    defaultNeq :: forall {k} (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Bool
    defaultNeq f a
    x f b
    y = Maybe (a :~: b) -> Bool
    forall a. Maybe a -> Bool
    isNothing (f a -> f b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq f a
    x f b
    y)

    instance GEq ((:~:) a) where
        geq :: forall (a :: k) (b :: k). (a :~: a) -> (a :~: b) -> Maybe (a :~: b)
    geq (a :~: a
    Refl :: a :~: b) (a :~: b
    Refl :: a :~: c) = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just (a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl :: b :~: c)

    -- | @since 1.0.4
    instance GEq ((:~~:) a) where
        geq :: forall (a :: k) (b :: k).
    (a :~~: a) -> (a :~~: b) -> Maybe (a :~: b)
    geq (a :~~: a
    HRefl :: a :~~: b) (a :~~: b
    HRefl :: a :~~: c) = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just (a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl :: b :~: c)

    instance (GEq a, GEq b) => GEq (Sum a b) where
        geq :: forall (a :: k) (b :: k). Sum a b a -> Sum a b b -> Maybe (a :~: b)
    geq (InL a a
    x) (InL a b
    y) = a a -> a b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). a a -> a b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq a a
    x a b
    y
        geq (InR b a
    x) (InR b b
    y) = b a -> b b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). b a -> b b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq b a
    x b b
    y
        geq Sum a b a
    _ Sum a b b
    _ = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    instance (GEq a, GEq b) => GEq (Product a b) where
        geq :: forall (a :: k) (b :: k).
    Product a b a -> Product a b b -> Maybe (a :~: b)
    geq (Pair a a
    x b a
    y) (Pair a b
    x' b b
    y') = do
            a :~: b
    Refl <- a a -> a b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). a a -> a b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq a a
    x a b
    x'
            a :~: b
    Refl <- b a -> b b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). b a -> b b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq b a
    y b b
    y'
            (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl

    -- | @since 1.0.4
    instance (GEq f, GEq g) => GEq (f :+: g) where
      geq :: forall (a :: k) (b :: k).
    (:+:) f g a -> (:+:) f g b -> Maybe (a :~: b)
    geq (L1 f a
    x) (L1 f b
    y) = f a -> f b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq f a
    x f b
    y
      geq (R1 g a
    x) (R1 g b
    y) = g a -> g b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). g a -> g b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq g a
    x g b
    y
      geq (:+:) f g a
    _ (:+:) f g b
    _ = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    -- | @since 1.0.4
    instance (GEq a, GEq b) => GEq (a :*: b) where
        geq :: forall (a :: k) (b :: k).
    (:*:) a b a -> (:*:) a b b -> Maybe (a :~: b)
    geq (a a
    x :*: b a
    y) (a b
    x' :*: b b
    y') = do
            a :~: b
    Refl <- a a -> a b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). a a -> a b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq a a
    x a b
    x'
            a :~: b
    Refl <- b a -> b b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). b a -> b b -> Maybe (a :~: b)
    forall k (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Maybe (a :~: b)
    geq b a
    y b b
    y'
            (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    Refl

    instance GEq TR.TypeRep where
        geq :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b)
    geq = TypeRep a -> TypeRep b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality

    -------------------------------------------------------------------------------
    -- GCompare
    -------------------------------------------------------------------------------

    -- This instance seems nice, but it's simply not right:
    --
    -- > instance GEq StableName where
    -- >     geq sn1 sn2
    -- >         | sn1 == unsafeCoerce sn2
    -- >             = Just (unsafeCoerce Refl)
    -- >         | otherwise     = Nothing
    --
    -- Proof:
    --
    -- > x <- makeStableName id :: IO (StableName (Int -> Int))
    -- > y <- makeStableName id :: IO (StableName ((Int -> Int) -> Int -> Int))
    -- >
    -- > let Just boom = geq x y
    -- > let coerce :: (a :~: b) -> a -> b; coerce Refl = id
    -- >
    -- > coerce boom (const 0) id 0
    -- > let "Illegal Instruction" = "QED."
    --
    -- The core of the problem is that 'makeStableName' only knows the closure
    -- it is passed to, not any type information.  Together with the fact that
    -- the same closure has the same StableName each time 'makeStableName' is
    -- called on it, there is serious potential for abuse when a closure can
    -- be given many incompatible types.

    -- |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.
    #if __GLASGOW_HASKELL__ >= 810
    type GOrdering :: k -> k -> Type
    #endif
    data GOrdering a b where
        GLT :: GOrdering a b
        GEQ :: GOrdering t t
        GGT :: GOrdering a b

    -- |TODO: Think of a better name
    --
    -- This operation forgets the phantom types of a 'GOrdering' value.
    weakenOrdering :: GOrdering a b -> Ordering
    weakenOrdering :: forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
    weakenOrdering GOrdering a b
    GLT = Ordering
    LT
    weakenOrdering GOrdering a b
    GEQ = Ordering
    EQ
    weakenOrdering GOrdering a b
    GGT = Ordering
    GT

    instance Eq (GOrdering a b) where
        GOrdering a b
    x == :: GOrdering a b -> GOrdering a b -> Bool
    == GOrdering a b
    y = GOrdering a b -> Ordering
    forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
    weakenOrdering GOrdering a b
    x Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == GOrdering a b -> Ordering
    forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
    weakenOrdering GOrdering a b
    y

    instance Ord (GOrdering a b) where
        compare :: GOrdering a b -> GOrdering a b -> Ordering
    compare GOrdering a b
    x GOrdering a b
    y = Ordering -> Ordering -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (GOrdering a b -> Ordering
    forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
    weakenOrdering GOrdering a b
    x) (GOrdering a b -> Ordering
    forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
    weakenOrdering GOrdering a b
    y)

    instance Show (GOrdering a b) where
        showsPrec :: Int -> GOrdering a b -> ShowS
    showsPrec Int
    _ GOrdering a b
    GGT = String -> ShowS
    showString String
    "GGT"
        showsPrec Int
    _ GOrdering a b
    GEQ = String -> ShowS
    showString String
    "GEQ"
        showsPrec Int
    _ GOrdering a b
    GLT = String -> ShowS
    showString String
    "GLT"

    instance GShow (GOrdering a) where
        gshowsPrec :: forall (a :: k). Int -> GOrdering a a -> ShowS
    gshowsPrec = Int -> GOrdering a a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec

    instance GRead (GOrdering a) where
        greadsPrec :: Int -> GReadS (GOrdering a)
    greadsPrec Int
    _ String
    s = case String
    con of
            String
    "GGT"   -> [(GOrdering a Any -> Some (GOrdering a)
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome GOrdering a Any
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT, String
    rest)]
            String
    "GEQ"   -> [(GOrdering a a -> Some (GOrdering a)
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome GOrdering a a
    forall {k} (t :: k). GOrdering t t
    GEQ, String
    rest)]
            String
    "GLT"   -> [(GOrdering a Any -> Some (GOrdering a)
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome GOrdering a Any
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT, String
    rest)]
            String
    _       -> []
            where (String
    con, String
    rest) = Int -> String -> (String, String)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    3 String
    s

    -- |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').
    #if __GLASGOW_HASKELL__ >= 810
    type GCompare :: (k -> Type) -> Constraint
    #endif
    class GEq f => GCompare f where
        gcompare :: f a -> f b -> GOrdering a b

    instance GCompare ((:~:) a) where
        gcompare :: forall (a :: k) (b :: k). (a :~: a) -> (a :~: b) -> GOrdering a b
    gcompare a :~: a
    Refl a :~: b
    Refl = GOrdering a a
    GOrdering a b
    forall {k} (t :: k). GOrdering t t
    GEQ

    -- | @since 1.0.4
    instance GCompare ((:~~:) a) where
        gcompare :: forall (a :: k) (b :: k). (a :~~: a) -> (a :~~: b) -> GOrdering a b
    gcompare a :~~: a
    HRefl a :~~: b
    HRefl = GOrdering a a
    GOrdering a b
    forall {k} (t :: k). GOrdering t t
    GEQ

    instance GCompare TR.TypeRep where
        gcompare :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> GOrdering a b
    gcompare TypeRep a
    t1 TypeRep b
    t2 =
          case TypeRep a -> TypeRep b -> Maybe (a :~: b)
    forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality TypeRep a
    t1 TypeRep b
    t2 of
            Just a :~: b
    Refl -> GOrdering a a
    GOrdering a b
    forall {k} (t :: k). GOrdering t t
    GEQ
            Maybe (a :~: b)
    Nothing ->
              case SomeTypeRep -> SomeTypeRep -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (TypeRep a -> SomeTypeRep
    forall k (a :: k). TypeRep a -> SomeTypeRep
    TR.SomeTypeRep TypeRep a
    t1) (TypeRep b -> SomeTypeRep
    forall k (a :: k). TypeRep a -> SomeTypeRep
    TR.SomeTypeRep TypeRep b
    t2) of
                Ordering
    LT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
                Ordering
    GT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT
                Ordering
    EQ -> String -> GOrdering a b
    forall a. HasCallStack => String -> a
    error "impossible: 'testEquality' and 'compare' \
                            \are inconsistent for TypeRep; report this \
                            \as a GHC bug"

    defaultCompare :: GCompare f => f a -> f b -> Ordering
    defaultCompare :: forall {k} (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> Ordering
    defaultCompare f a
    x f b
    y = GOrdering a b -> Ordering
    forall {k} (a :: k) (b :: k). GOrdering a b -> Ordering
    weakenOrdering (f a -> f b -> GOrdering a b
    forall (a :: k) (b :: k). f a -> f b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare f a
    x f b
    y)

    instance (GCompare a, GCompare b) => GCompare (Sum a b) where
        gcompare :: forall (a :: k) (b :: k). Sum a b a -> Sum a b b -> GOrdering a b
    gcompare (InL a a
    x) (InL a b
    y) = a a -> a b -> GOrdering a b
    forall (a :: k) (b :: k). a a -> a b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare a a
    x a b
    y
        gcompare (InL a a
    _) (InR b b
    _) = GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
        gcompare (InR b a
    _) (InL a b
    _) = GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT
        gcompare (InR b a
    x) (InR b b
    y) = b a -> b b -> GOrdering a b
    forall (a :: k) (b :: k). b a -> b b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare b a
    x b b
    y

    instance (GCompare a, GCompare b) => GCompare (Product a b) where
        gcompare :: forall (a :: k) (b :: k).
    Product a b a -> Product a b b -> GOrdering a b
    gcompare (Pair a a
    x b a
    y) (Pair a b
    x' b b
    y') = case a a -> a b -> GOrdering a b
    forall (a :: k) (b :: k). a a -> a b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare a a
    x a b
    x' of
            GOrdering a b
    GLT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
            GOrdering a b
    GGT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT
            GOrdering a b
    GEQ -> case b a -> b b -> GOrdering a b
    forall (a :: k) (b :: k). b a -> b b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare b a
    y b b
    y' of
                GOrdering a b
    GLT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
                GOrdering a b
    GEQ -> GOrdering a a
    GOrdering a b
    forall {k} (t :: k). GOrdering t t
    GEQ
                GOrdering a b
    GGT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT

    -- | @since 1.0.4
    instance (GCompare f, GCompare g) => GCompare (f :+: g) where
        gcompare :: forall (a :: k) (b :: k).
    (:+:) f g a -> (:+:) f g b -> GOrdering a b
    gcompare (L1 f a
    x) (L1 f b
    y) = f a -> f b -> GOrdering a b
    forall (a :: k) (b :: k). f a -> f b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare f a
    x f b
    y
        gcompare (L1 f a
    _) (R1 g b
    _) = GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
        gcompare (R1 g a
    _) (L1 f b
    _) = GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT
        gcompare (R1 g a
    x) (R1 g b
    y) = g a -> g b -> GOrdering a b
    forall (a :: k) (b :: k). g a -> g b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare g a
    x g b
    y

    -- | @since 1.0.4
    instance (GCompare a, GCompare b) => GCompare (a :*: b) where
        gcompare :: forall (a :: k) (b :: k).
    (:*:) a b a -> (:*:) a b b -> GOrdering a b
    gcompare (a a
    x :*: b a
    y) (a b
    x' :*: b b
    y') = case a a -> a b -> GOrdering a b
    forall (a :: k) (b :: k). a a -> a b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare a a
    x a b
    x' of
            GOrdering a b
    GLT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
            GOrdering a b
    GGT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT
            GOrdering a b
    GEQ -> case b a -> b b -> GOrdering a b
    forall (a :: k) (b :: k). b a -> b b -> GOrdering a b
    forall k (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> GOrdering a b
    gcompare b a
    y b b
    y' of
                GOrdering a b
    GLT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GLT
                GOrdering a b
    GEQ -> GOrdering a a
    GOrdering a b
    forall {k} (t :: k). GOrdering t t
    GEQ
                GOrdering a b
    GGT -> GOrdering a b
    forall {k} (a :: k) (b :: k). GOrdering a b
    GGT

    -------------------------------------------------------------------------------
    -- Some
    -------------------------------------------------------------------------------

    -- | 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
    --
    #if __GLASGOW_HASKELL__ >= 810
    type Some :: (k -> Type) -> Type
    #endif
    newtype Some tag = S
        { -- | Eliminator.
          forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome :: forall r. (forall a. tag a -> r) -> r
        }

    type role Some representational

    -- | Constructor.
    mkSome :: tag a -> Some tag
    mkSome :: forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome tag a
    t = (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    forall k (tag :: k -> *).
    (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    S (\forall (a :: k). tag a -> r
    f -> tag a -> r
    forall (a :: k). tag a -> r
    f tag a
    t)

    -- | Map over argument.
    mapSome :: (forall x. f x -> g x) ->  Some f -> Some g
    mapSome :: forall {k} (f :: k -> *) (g :: k -> *).
    (forall (x :: k). f x -> g x) -> Some f -> Some g
    mapSome forall (x :: k). f x -> g x
    nt (S forall r. (forall (a :: k). f a -> r) -> r
    fx) = (forall r. (forall (a :: k). g a -> r) -> r) -> Some g
    forall k (tag :: k -> *).
    (forall r. (forall (a :: k). tag a -> r) -> r) -> Some tag
    S (\forall (a :: k). g a -> r
    f -> (forall (a :: k). f a -> r) -> r
    forall r. (forall (a :: k). f a -> r) -> r
    fx (g a -> r
    forall (a :: k). g a -> r
    f (g a -> r) -> (f a -> g a) -> f a -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f a -> g a
    forall (x :: k). f x -> g x
    nt))

    -- | @'flip' 'withSome'@
    foldSome :: (forall a. tag a -> b) -> Some tag -> b
    foldSome :: forall {k} (tag :: k -> *) b.
    (forall (a :: k). tag a -> b) -> Some tag -> b
    foldSome forall (a :: k). tag a -> b
    some (S forall r. (forall (a :: k). tag a -> r) -> r
    thing) = (forall (a :: k). tag a -> b) -> b
    forall r. (forall (a :: k). tag a -> r) -> r
    thing tag a -> b
    forall (a :: k). tag a -> b
    some

    -- | Traverse over argument.
    traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g)
    traverseSome :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *).
    Functor m =>
    (forall (a :: k). f a -> m (g a)) -> Some f -> m (Some g)
    traverseSome forall (a :: k). f a -> m (g a)
    f Some f
    x = Some f -> forall r. (forall (a :: k). f a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some f
    x ((forall (a :: k). f a -> m (Some g)) -> m (Some g))
    -> (forall (a :: k). f a -> m (Some g)) -> m (Some g)
    forall a b. (a -> b) -> a -> b
    $ \f a
    x' -> (g a -> Some g) -> m (g a) -> m (Some g)
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap g a -> Some g
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome (f a -> m (g a)
    forall (a :: k). f a -> m (g a)
    f f a
    x')

    -- | Monadic 'withSome'.
    --
    -- @since 1.0.1
    withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r
    withSomeM :: forall {k} (m :: * -> *) (tag :: k -> *) r.
    Monad m =>
    m (Some tag) -> (forall (a :: k). tag a -> m r) -> m r
    withSomeM m (Some tag)
    m forall (a :: k). tag a -> m r
    k = m (Some tag)
    m m (Some tag) -> (Some tag -> m r) -> m r
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \Some tag
    s -> Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some tag
    s tag a -> m r
    forall (a :: k). tag a -> m r
    k

    -------------------------------------------------------------------------------
    -- Church Some instances
    -------------------------------------------------------------------------------

    instance GShow tag => Show (Some tag) where
        showsPrec :: Int -> Some tag -> ShowS
    showsPrec Int
    p Some tag
    some = Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some tag
    some ((forall (a :: k). tag a -> ShowS) -> ShowS)
    -> (forall (a :: k). tag a -> ShowS) -> ShowS
    forall a b. (a -> b) -> a -> b
    $ \tag a
    thing -> Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    10)
            ( String -> ShowS
    showString String
    "mkSome "
            ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> tag a -> ShowS
    forall (a :: k). Int -> tag a -> ShowS
    forall k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
    gshowsPrec Int
    11 tag a
    thing
            )

    instance GRead f => Read (Some f) where
        readsPrec :: Int -> ReadS (Some f)
    readsPrec Int
    p = Bool -> ReadS (Some f) -> ReadS (Some f)
    forall a. Bool -> ReadS a -> ReadS a
    readParen (Int
    pInt -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >Int
    10) (ReadS (Some f) -> ReadS (Some f))
    -> ReadS (Some f) -> ReadS (Some f)
    forall a b. (a -> b) -> a -> b
    $ \String
    s ->
            [ (Some f -> forall r. (forall (a :: k). f a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some f
    withTag f a -> Some f
    forall (a :: k). f a -> Some f
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome, String
    rest')
            | (String
    con, String
    rest) <- ReadS String
    lex String
    s
            , String
    con String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "Some" Bool -> Bool -> Bool
    || String
    con String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    "mkSome"
            , (Some f
    withTag, String
    rest') <- Int -> ReadS (Some f)
    forall k (t :: k -> *). GRead t => Int -> GReadS t
    greadsPrec Int
    11 String
    rest
            ]

    instance GEq tag => Eq (Some tag) where
        Some tag
    x == :: Some tag -> Some tag -> Bool
    == Some tag
    y =
            Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some tag
    x ((forall (a :: k). tag a -> Bool) -> Bool)
    -> (forall (a :: k). tag a -> Bool) -> Bool
    forall a b. (a -> b) -> a -> b
    $ \tag a
    x' ->
            Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some tag
    y ((forall (a :: k). tag a -> Bool) -> Bool)
    -> (forall (a :: k). tag a -> Bool) -> Bool
    forall a b. (a -> b) -> a -> b
    $ \tag a
    y' -> tag a -> tag a -> Bool
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    GEq f =>
    f a -> f b -> Bool
    defaultEq tag a
    x' tag a
    y'

    instance GCompare tag => Ord (Some tag) where
        compare :: Some tag -> Some tag -> Ordering
    compare Some tag
    x Some tag
    y =
            Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some tag
    x ((forall (a :: k). tag a -> Ordering) -> Ordering)
    -> (forall (a :: k). tag a -> Ordering) -> Ordering
    forall a b. (a -> b) -> a -> b
    $ \tag a
    x' ->
            Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some tag
    y ((forall (a :: k). tag a -> Ordering) -> Ordering)
    -> (forall (a :: k). tag a -> Ordering) -> Ordering
    forall a b. (a -> b) -> a -> b
    $ \tag a
    y' -> tag a -> tag a -> Ordering
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    GCompare f =>
    f a -> f b -> Ordering
    defaultCompare tag a
    x' tag a
    y'

    instance Control.Applicative.Applicative m => Data.Semigroup.Semigroup (Some m) where
        Some m
    m <> :: Some m -> Some m -> Some m
    <> Some m
    n =
            Some m -> forall r. (forall a. m a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some m
    m ((forall a. m a -> Some m) -> Some m)
    -> (forall a. m a -> Some m) -> Some m
    forall a b. (a -> b) -> a -> b
    $ \m a
    m' ->
            Some m -> forall r. (forall a. m a -> r) -> r
    forall k (tag :: k -> *).
    Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
    withSome Some m
    n ((forall a. m a -> Some m) -> Some m)
    -> (forall a. m a -> Some m) -> Some m
    forall a b. (a -> b) -> a -> b
    $ \m a
    n' ->
            m a -> Some m
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome (m a
    m' m a -> m a -> m a
    forall a b. m a -> m b -> m b
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> m a
    n')

    instance Applicative m => Data.Monoid.Monoid (Some m) where
        mempty :: Some m
    mempty = m () -> Some m
    forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
    mkSome (() -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ())
        mappend :: Some m -> Some m -> Some m
    mappend = Some m -> Some m -> Some m
    forall a. Semigroup a => a -> a -> a
    (<>)