{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Safe #-}
#endif
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
{-# LANGUAGE PolyKinds #-}
#endif
module Data.Some where

import Data.GADT.Show
import Data.GADT.Compare
import Data.Maybe

data Some tag where
    This :: !(tag t) -> Some tag

withSome :: Some tag -> (forall a. tag a -> b) -> b
withSome :: Some tag -> (forall (a :: k). tag a -> b) -> b
withSome (This thing :: tag t
thing) some :: forall (a :: k). tag a -> b
some = tag t -> b
forall (a :: k). tag a -> b
some tag t
thing

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

instance GRead f => Read (Some f) where
    readsPrec :: Int -> ReadS (Some f)
readsPrec p :: 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
>10) (ReadS (Some f) -> ReadS (Some f))
-> ReadS (Some f) -> ReadS (Some f)
forall a b. (a -> b) -> a -> b
$ \s :: String
s ->
        [ (GReadResult f -> (forall (a :: k). f a -> Some f) -> Some f
forall k (t :: k -> *).
GReadResult t -> forall b. (forall (a :: k). t a -> b) -> b
getGReadResult GReadResult f
withTag forall (a :: k). f a -> Some f
forall k (tag :: k -> *) (t :: k). tag t -> Some tag
This, String
rest')
        | let (con :: String
con, rest :: String
rest) = Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt 5 String
s
        , String
con String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "This "
        , (withTag :: GReadResult f
withTag, rest' :: String
rest') <- Int -> GReadS f
forall k (t :: k -> *). GRead t => Int -> GReadS t
greadsPrec 11 String
rest
        ]

instance GEq tag => Eq (Some tag) where
    This x :: tag t
x == :: Some tag -> Some tag -> Bool
== This y :: tag t
y = tag t -> tag t -> Bool
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq tag t
x tag t
y

instance GCompare tag => Ord (Some tag) where
    compare :: Some tag -> Some tag -> Ordering
compare (This x :: tag t
x) (This y :: tag t
y) = tag t -> tag t -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare tag t
x tag t
y