{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
#if __GLASGOW_HASKELL__ >= 706
{-# LANGUAGE PolyKinds           #-}
#endif
#if __GLASGOW_HASKELL__ >= 704
#define GHC __GLASGOW_HASKELL__
#if (GHC >= 704 && GHC <707) || GHC >= 801
{-# LANGUAGE Safe                #-}
#else
{-# LANGUAGE Trustworthy         #-}
#endif
#undef GHC
#endif
module Data.GADT.Internal where

import Control.Applicative  (Applicative (..))
import Data.Functor.Product (Product (..))
import Data.Functor.Sum     (Sum (..))
import Data.Maybe           (isJust, isNothing)
import Data.Monoid          (Monoid (..))
import Data.Semigroup       (Semigroup (..))
import Data.Type.Equality   ((:~:) (..))

#if __GLASGOW_HASKELL__ >=708
import Data.Typeable (Typeable)
#endif

#if MIN_VERSION_base(4,10,0)
import           Data.Type.Equality (testEquality)
import qualified Type.Reflection    as TR
#endif

-- $setup
-- >>> :set -XKindSignatures -XGADTs

-- |'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 = showsPrec
class GShow t where
    gshowsPrec :: Int -> t a -> ShowS

gshows :: GShow t => t a -> ShowS
gshows :: t a -> ShowS
gshows = 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 :: 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 :: Int -> (a :~: a) -> ShowS
gshowsPrec Int
_ a :~: a
Refl = String -> ShowS
showString String
"Refl"

#if MIN_VERSION_base(4,10,0)
instance GShow TR.TypeRep where
    gshowsPrec :: Int -> TypeRep a -> ShowS
gshowsPrec = Int -> TypeRep a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
#endif

--
-- | >>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)
-- "InL Refl"
instance (GShow a, GShow b) => GShow (Sum a b) where
    gshowsPrec :: 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 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 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 :: 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 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 k (t :: k -> *) (a :: k). GShow t => Int -> t a -> ShowS
gshowsPrec Int
11 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@)
type GReadS t = String -> [(Some t, String)]

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

mkGReadResult :: tag a -> Some tag
mkGReadResult :: 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.
class GRead t where
    greadsPrec :: Int -> GReadS t

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

-- |
--
-- >>> greadMaybe "InL Refl" mkSome :: Maybe (Some (Sum ((:~:) Int) ((:~:) Bool)))
-- Just (mkSome (InL Refl))
--
-- >>> greadMaybe "garbage" mkSome :: Maybe (Some ((:~:) Int))
-- Nothing
--
greadMaybe :: GRead t => String -> (forall a. t a -> b) -> Maybe b
greadMaybe :: 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 (a :: k). t a -> b) -> b
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some t
x 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
p String
s = Int -> ReadS (a :~: a)
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
s [(a :~: a, String)]
-> ((a :~: a, String) -> [(Some ((:~:) a), String)])
-> [(Some ((:~:) a), String)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a :~: a, String) -> [(Some ((:~:) a), String)]
forall k (x :: k). (x :~: x, String) -> [(Some ((:~:) x), String)]
f
      where
        f :: forall x. (x :~: x, String) -> [(Some ((:~:) x), String)]
        f :: (x :~: x, String) -> [(Some ((:~:) x), String)]
f (x :~: x
Refl, String
rest) = (Some ((:~:) x), String) -> [(Some ((:~:) x), String)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((x :~: x) -> Some ((:~:) x)
forall k (tag :: k -> *) (a :: k). tag a -> Some tag
mkSome x :~: x
forall k (a :: k). a :~: a
Refl, String
rest)

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

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

-- |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 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 'GEq' instance, this function makes a suitable default
-- implementation of '(==)'.
defaultEq :: GEq f => f a -> f b -> Bool
defaultEq :: 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 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 :: 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 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 :: (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 :~: b
forall k (a :: k). a :~: a
Refl :: b :~: c)

instance (GEq a, GEq b) => GEq (Sum a b) where
    geq :: 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 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 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 :: 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 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 k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
geq b a
y b b
y'
        (a :~: a) -> Maybe (a :~: a)
forall (m :: * -> *) a. Monad m => a -> m a
return a :~: a
forall k (a :: k). a :~: a
Refl

#if MIN_VERSION_base(4,10,0)
instance GEq TR.TypeRep where
    geq :: TypeRep a -> TypeRep b -> Maybe (a :~: b)
geq = 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
#endif

-------------------------------------------------------------------------------
-- 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.
data GOrdering a b where
    GLT :: GOrdering a b
    GEQ :: GOrdering t t
    GGT :: GOrdering a b
#if __GLASGOW_HASKELL__ >=708
  deriving Typeable
#endif

-- |TODO: Think of a better name
--
-- This operation forgets the phantom types of a 'GOrdering' value.
weakenOrdering :: GOrdering a b -> Ordering
weakenOrdering :: 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 :: 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').
class GEq f => GCompare f where
    gcompare :: f a -> f b -> GOrdering a b

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

#if MIN_VERSION_base(4,10,0)
instance GCompare TR.TypeRep where
    gcompare :: TypeRep a -> TypeRep b -> GOrdering a b
gcompare TypeRep a
t1 TypeRep b
t2 =
      case 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 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"
#endif

defaultCompare :: GCompare f => f a -> f b -> Ordering
defaultCompare :: 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 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 :: 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 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 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 :: 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 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 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 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
--
newtype Some tag = S
    { -- | Eliminator.
      Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome :: forall r. (forall a. tag a -> r) -> r
    }

-- | Constructor.
mkSome :: tag a -> Some tag
mkSome :: 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 (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 (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 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 (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 (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 :: 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Some tag
s -> Some tag -> (forall (a :: k). tag a -> m r) -> m r
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some tag
s 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 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 (a :: k). f a -> Some f) -> Some f
forall k (tag :: k -> *).
Some tag -> forall r. (forall (a :: k). tag a -> r) -> r
withSome Some f
withTag 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 (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 (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
(<>)