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