diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,5 @@
+# 1
+
+- Split out of `dependent-sum`
+- Have `GADT`, `Newtype`, `Church` variants
+- Add `NFData` instance
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2019 Oleg Grenrus, James Cook
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Oleg Grenrus nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/some.cabal b/some.cabal
new file mode 100644
--- /dev/null
+++ b/some.cabal
@@ -0,0 +1,78 @@
+name:               some
+version:            1
+stability:          provisional
+cabal-version:      >=1.10
+build-type:         Simple
+author:             James Cook <mokus@deepbondi.net>, Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi>
+license:            BSD3
+license-file:       LICENSE
+homepage:           https://github.com/phadej/some
+category:           Data, Dependent Types
+synopsis:           Existential type: Some
+description:
+  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.
+
+tested-with:
+  GHC ==7.0.4
+   || ==7.2.2
+   || ==7.4.2
+   || ==7.6.3
+   || ==7.8.4
+   || ==7.10.3
+   || ==8.0.2
+   || ==8.2.2
+   || ==8.4.4
+   || ==8.6.5
+   || ==8.8.1
+
+extra-source-files: ChangeLog.md
+
+flag newtype-unsafe
+  description:
+    Use implementation using @newtype@ and unsafe @Any@, instead of GADT
+
+  manual:      True
+  default:     True
+
+source-repository head
+  type:     git
+  location: git://github.com/phadej/some.git
+  subdir:   some
+
+library
+  default-language: Haskell2010
+  hs-source-dirs:   src
+
+  if flag(newtype-unsafe)
+    cpp-options: -DSOME_NEWTYPE
+
+  exposed-modules:
+    Data.GADT.Compare
+    Data.GADT.DeepSeq
+    Data.GADT.Show
+    Data.Some
+    Data.Some.Church
+    Data.Some.GADT
+    Data.Some.Newtype
+
+  other-modules:    Data.GADT.Internal
+  build-depends:
+      base     >=4.3     && <4.14
+    , deepseq  >=1.3.0.0 && <1.5
+
+  if !impl(ghc >=7.8)
+    build-depends: type-equality >=1 && <1.1
+
+  if !impl(ghc >=8.0)
+    build-depends:
+        semigroups           >=0.18.5 && <0.20
+      , transformers         >=0.3    && <0.6
+      , transformers-compat  >=0.6    && <0.7
diff --git a/src/Data/GADT/Compare.hs b/src/Data/GADT/Compare.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GADT/Compare.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE CPP         #-}
+#if __GLASGOW_HASKELL__ >= 704
+{-# LANGUAGE Safe        #-}
+#elif __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+module Data.GADT.Compare (
+    -- * Equality
+    GEq (..),
+    defaultEq,
+    defaultNeq,
+    -- * Total order comparison
+    GCompare (..),
+    defaultCompare,
+    GOrdering (..),
+    ) where
+
+import Data.GADT.Internal
diff --git a/src/Data/GADT/DeepSeq.hs b/src/Data/GADT/DeepSeq.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GADT/DeepSeq.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ >= 704
+{-# LANGUAGE Safe         #-}
+#elif __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy  #-}
+#endif
+module Data.GADT.DeepSeq (
+    GNFData (..),
+    ) where
+
+import Data.Functor.Product (Product (..))
+import Data.Functor.Sum     (Sum (..))
+
+class GNFData f where
+    grnf :: f a -> ()
+
+instance (GNFData a, GNFData b) => GNFData (Product a b) where
+    grnf (Pair a b) = grnf a `seq` grnf b
+
+instance (GNFData a, GNFData b) => GNFData (Sum a b) where
+    grnf (InL x) = grnf x
+    grnf (InR y) = grnf y
diff --git a/src/Data/GADT/Internal.hs b/src/Data/GADT/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GADT/Internal.hs
@@ -0,0 +1,403 @@
+{-# 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 GH
+#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 = gshowsPrec (-1)
+
+gshow :: (GShow t) => t a -> String
+gshow x = gshows x ""
+
+instance GShow ((:~:) a) where
+    gshowsPrec _ Refl = showString "Refl"
+
+#if MIN_VERSION_base(4,10,0)
+instance GShow TR.TypeRep where
+    gshowsPrec = showsPrec
+#endif
+
+--
+-- | >>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)
+-- "InL Refl"
+instance (GShow a, GShow b) => GShow (Sum a b) where
+    gshowsPrec d = \s -> case s of
+        InL x -> showParen (d > 10) (showString "InL " . gshowsPrec 11 x)
+        InR x -> showParen (d > 10) (showString "InR " . gshowsPrec 11 x)
+
+-- | >>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)
+-- "Pair Refl Refl"
+instance (GShow a, GShow b) => GShow (Product a b) where
+    gshowsPrec d (Pair x y) = showParen (d > 10)
+        $ showString "Pair "
+        . gshowsPrec 11 x
+        . showChar ' '
+        . gshowsPrec 11 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 = withSome
+
+mkGReadResult :: tag a -> Some tag
+mkGReadResult = 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 = greadsPrec (-1)
+
+gread :: GRead t => String -> (forall a. t a -> b) -> b
+gread s g = withSome (hd [f | (f, "") <- greads s]) g where
+    hd (x:_) = x
+    hd _ = error "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 s g = case [f | (f, "") <- greads s] of
+    (x : _) -> Just (withSome x g)
+    _       -> Nothing
+
+instance GRead ((:~:) a) where
+    greadsPrec p s = readsPrec p s >>= f
+      where
+        f :: forall x. (x :~: x, String) -> [(Some ((:~:) x), String)]
+        f (Refl, rest) = return (mkSome Refl, rest)
+
+instance (GRead a, GRead b) => GRead (Sum a b) where
+    greadsPrec d s = concat
+        [ readParen (d > 10)
+            (\s1 -> [ (S $ \k -> withSome r (k . InL), t)
+                    | ("InL", s2) <- lex s1
+                    , (r, t) <- greadsPrec 11 s2 ]) s
+        , readParen (d > 10)
+            (\s1 -> [ (S $ \k -> withSome r (k . InR), t)
+                    | ("InR", s2) <- lex s1
+                    , (r, t) <- greadsPrec 11 s2 ]) 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 "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 x y = isJust (geq x y)
+
+-- |If 'f' has a 'GEq' instance, this function makes a suitable default
+-- implementation of '(/=)'.
+defaultNeq :: GEq f => f a -> f b -> Bool
+defaultNeq x y = isNothing (geq x y)
+
+instance GEq ((:~:) a) where
+    geq (Refl :: a :~: b) (Refl :: a :~: c) = Just (Refl :: b :~: c)
+
+instance (GEq a, GEq b) => GEq (Sum a b) where
+    geq (InL x) (InL y) = geq x y
+    geq (InR x) (InR y) = geq x y
+    geq _ _ = Nothing
+
+instance (GEq a, GEq b) => GEq (Product a b) where
+    geq (Pair x y) (Pair x' y') = do
+        Refl <- geq x x'
+        Refl <- geq y y'
+        return Refl
+
+#if MIN_VERSION_base(4,10,0)
+instance GEq TR.TypeRep where
+    geq = 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 GLT = LT
+weakenOrdering GEQ = EQ
+weakenOrdering GGT = GT
+
+instance Eq (GOrdering a b) where
+    x == y = weakenOrdering x == weakenOrdering y
+
+instance Ord (GOrdering a b) where
+    compare x y = compare (weakenOrdering x) (weakenOrdering y)
+
+instance Show (GOrdering a b) where
+    showsPrec _ GGT = showString "GGT"
+    showsPrec _ GEQ = showString "GEQ"
+    showsPrec _ GLT = showString "GLT"
+
+instance GShow (GOrdering a) where
+    gshowsPrec = showsPrec
+
+instance GRead (GOrdering a) where
+    greadsPrec _ s = case con of
+        "GGT"   -> [(mkSome GGT, rest)]
+        "GEQ"   -> [(mkSome GEQ, rest)]
+        "GLT"   -> [(mkSome GLT, rest)]
+        _       -> []
+        where (con, rest) = splitAt 3 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 Refl Refl = GEQ
+
+#if MIN_VERSION_base(4,10,0)
+instance GCompare TR.TypeRep where
+    gcompare t1 t2 =
+      case testEquality t1 t2 of
+        Just Refl -> GEQ
+        Nothing ->
+          case compare (TR.SomeTypeRep t1) (TR.SomeTypeRep t2) of
+            LT -> GLT
+            GT -> GGT
+            EQ -> 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 x y = weakenOrdering (gcompare x y)
+
+instance (GCompare a, GCompare b) => GCompare (Sum a b) where
+    gcompare (InL x) (InL y) = gcompare x y
+    gcompare (InL _) (InR _) = GLT
+    gcompare (InR _) (InL _) = GGT
+    gcompare (InR x) (InR y) = gcompare x y
+
+instance (GCompare a, GCompare b) => GCompare (Product a b) where
+    gcompare (Pair x y) (Pair x' y') = case gcompare x x' of
+        GLT -> GLT
+        GGT -> GGT
+        GEQ -> case gcompare y y' of
+            GLT -> GLT
+            GEQ -> GEQ
+            GGT -> 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.
+      withSome :: forall r. (forall a. tag a -> r) -> r
+    }
+
+-- | Constructor.
+mkSome :: tag a -> Some tag
+mkSome t = S (\f -> f t)
+
+-- | Map over argument.
+mapSome :: (forall x. f x -> g x) ->  Some f -> Some g
+mapSome nt (S fx) = S (\f -> fx (f . nt))
+
+-- | @'flip' 'withSome'@
+foldSome :: (forall a. tag a -> b) -> Some tag -> b
+foldSome some (S thing) = thing some
+
+-- | Traverse over argument.
+traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g)
+traverseSome f x = withSome x $ \x' -> fmap mkSome (f x')
+
+-------------------------------------------------------------------------------
+-- Church Some instances
+-------------------------------------------------------------------------------
+
+instance GShow tag => Show (Some tag) where
+    showsPrec p some = withSome some $ \thing -> showParen (p > 10)
+        ( showString "mkSome "
+        . gshowsPrec 11 thing
+        )
+
+instance GRead f => Read (Some f) where
+    readsPrec p = readParen (p>10) $ \s ->
+        [ (withSome withTag mkSome, rest')
+        | (con, rest) <- lex s
+        , con == "Some" || con == "mkSome"
+        , (withTag, rest') <- greadsPrec 11 rest
+        ]
+
+instance GEq tag => Eq (Some tag) where
+    x == y =
+        withSome x $ \x' ->
+        withSome y $ \y' -> defaultEq x' y'
+
+instance GCompare tag => Ord (Some tag) where
+    compare x y =
+        withSome x $ \x' ->
+        withSome y $ \y' -> defaultCompare x' y'
+
+instance Control.Applicative.Applicative m => Data.Semigroup.Semigroup (Some m) where
+    m <> n =
+        withSome m $ \m' ->
+        withSome n $ \n' ->
+        mkSome (m' *> n')
+
+instance Applicative m => Data.Monoid.Monoid (Some m) where
+    mempty = mkSome (pure ())
+    mappend = (<>)
diff --git a/src/Data/GADT/Show.hs b/src/Data/GADT/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/GADT/Show.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE CPP         #-}
+#if __GLASGOW_HASKELL__ >= 704
+{-# LANGUAGE Safe         #-}
+#elif __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy  #-}
+#endif
+module Data.GADT.Show (
+    -- * Showing
+    GShow  (..),
+    gshows,
+    gshow,
+    -- * Reading
+    GRead  (..),
+    GReadS,
+    greads,
+    gread,
+    greadMaybe,
+    getGReadResult,
+    mkGReadResult,
+    ) where
+
+import Data.GADT.Internal
diff --git a/src/Data/Some.hs b/src/Data/Some.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Some.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE CPP #-}
+-- | An existential type.
+--
+-- The constructor is exported only on GHC-8 and later.
+module Data.Some (
+#if __GLASGOW_HASKELL__ >= 801
+Some(Some),
+#else
+Some,
+#endif
+mkSome,
+withSome,
+mapSome,
+foldSome,
+traverseSome,
+) where
+
+#ifdef SOME_NEWTYPE
+import Data.Some.Newtype
+#else
+import Data.Some.GADT
+#endif
diff --git a/src/Data/Some/Church.hs b/src/Data/Some/Church.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Some/Church.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE CPP         #-}
+#if __GLASGOW_HASKELL__ >= 704
+{-# LANGUAGE Safe         #-}
+#elif __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy  #-}
+#endif
+module Data.Some.Church (
+    Some(..),
+    mkSome,
+    mapSome,
+    foldSome,
+    traverseSome,
+    ) where
+
+import Data.GADT.Internal
diff --git a/src/Data/Some/GADT.hs b/src/Data/Some/GADT.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Some/GADT.hs
@@ -0,0 +1,126 @@
+{-# LANGUAGE CPP         #-}
+{-# LANGUAGE GADTs       #-}
+{-# LANGUAGE RankNTypes  #-}
+#if __GLASGOW_HASKELL__ >= 706
+{-# LANGUAGE PolyKinds   #-}
+#endif
+#if __GLASGOW_HASKELL__ >= 704
+{-# LANGUAGE Safe        #-}
+#elif __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+module Data.Some.GADT (
+    Some(Some),
+    mkSome,
+    withSome,
+    mapSome,
+    foldSome,
+    traverseSome,
+    ) where
+
+import Control.Applicative (Applicative (..))
+import Control.DeepSeq     (NFData (..))
+import Data.Monoid         (Monoid (..))
+import Data.Semigroup      (Semigroup (..))
+
+import Data.GADT.Compare
+import Data.GADT.DeepSeq
+import Data.GADT.Show
+
+-- $setup
+-- >>> :set -XKindSignatures -XGADTs
+
+-- | 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 ]
+--
+-- 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 where
+    Some :: tag a -> Some tag
+
+-- | Constructor.
+mkSome :: tag a -> Some tag
+mkSome = Some
+
+-- | Eliminator.
+withSome :: Some tag -> (forall a. tag a -> b) -> b
+withSome (Some thing) some = some thing
+
+-- | @'flip' 'withSome'@
+foldSome :: (forall a. tag a -> b) -> Some tag -> b
+foldSome some (Some thing) = some thing
+
+-- | Map over argument.
+mapSome :: (forall x. f x -> g x) ->  Some f -> Some g
+mapSome nt (Some fx) = Some (nt fx)
+
+-- | Traverse over argument.
+traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g)
+traverseSome f (Some x) = fmap Some (f x)
+
+instance GShow tag => Show (Some tag) where
+    showsPrec p (Some thing) = showParen (p > 10)
+        $ showString "Some "
+        . gshowsPrec 11 thing
+
+-- |
+instance GRead f => Read (Some f) where
+    readsPrec p = readParen (p>10) $ \s ->
+        [ (getGReadResult withTag Some, rest')
+        | (con, rest) <- lex s
+        , con == "Some" || con == "mkSome"
+        , (withTag, rest') <- greadsPrec 11 rest
+        ]
+
+instance GEq tag => Eq (Some tag) where
+    Some x == Some y = defaultEq x y
+
+instance GCompare tag => Ord (Some tag) where
+    compare (Some x) (Some y) = defaultCompare x y
+
+instance GNFData tag => NFData (Some tag) where
+    rnf (Some x) = grnf x
+
+instance Control.Applicative.Applicative m => Data.Semigroup.Semigroup (Some m) where
+    Some m <> Some n = Some (m *> n)
+
+instance Applicative m => Data.Monoid.Monoid (Some m) where
+    mempty = Some (pure ())
+    mappend = (<>)
diff --git a/src/Data/Some/Newtype.hs b/src/Data/Some/Newtype.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Some/Newtype.hs
@@ -0,0 +1,147 @@
+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE GADTs           #-}
+{-# LANGUAGE RankNTypes      #-}
+#if __GLASGOW_HASKELL__ >= 801
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns    #-}
+#endif
+#if __GLASGOW_HASKELL__ >= 706
+{-# LANGUAGE PolyKinds       #-}
+#endif
+#if __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy     #-}
+#endif
+module Data.Some.Newtype (
+#if __GLASGOW_HASKELL__ >= 801
+    Some(Some),
+#else
+    Some,
+#endif
+    mkSome,
+    withSome,
+    mapSome,
+    foldSome,
+    traverseSome,
+    ) where
+
+import Control.Applicative (Applicative (..))
+import Control.DeepSeq     (NFData (..))
+import Data.Monoid         (Monoid (..))
+import Data.Semigroup      (Semigroup (..))
+import GHC.Exts            (Any)
+import Unsafe.Coerce       (unsafeCoerce)
+
+import Data.GADT.Compare
+import Data.GADT.DeepSeq
+import Data.GADT.Show
+
+-- $setup
+-- >>> :set -XKindSignatures -XGADTs
+
+-- | 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 ]
+--
+-- 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
+--
+newtype Some tag = UnsafeSome (tag Any)
+
+#if __GLASGOW_HASKELL__ >= 801
+{-# COMPLETE Some #-}
+pattern Some :: tag a -> Some tag
+pattern Some x <- UnsafeSome ((unsafeCoerce :: tag Any -> tag a) -> x)
+  where Some x = UnsafeSome ((unsafeCoerce :: tag a -> tag Any) x)
+#endif
+
+-- | Constructor.
+mkSome :: tag a -> Some tag
+mkSome = UnsafeSome . unsafeCoerce
+
+-- | Eliminator.
+withSome :: Some tag -> (forall a. tag a -> b) -> b
+withSome (UnsafeSome thing) some = some (unsafeCoerce thing)
+
+-- | @'flip' 'withSome'@
+foldSome :: (forall a. tag a -> b) -> Some tag -> b
+foldSome some (UnsafeSome thing) = some (unsafeCoerce thing)
+
+-- | Map over argument.
+mapSome :: (forall t. f t -> g t) -> Some f -> Some g
+mapSome f (UnsafeSome x) = UnsafeSome (unsafeCoerce f x)
+
+-- | Traverse over argument.
+traverseSome :: Functor m => (forall a. f a -> m (g a)) -> Some f -> m (Some g)
+traverseSome f x = withSome x $ \x' -> fmap mkSome (f x')
+
+instance GShow tag => Show (Some tag) where
+    showsPrec p some = withSome some $ \thing -> showParen (p > 10)
+        ( showString "Some "
+        . gshowsPrec 11 thing
+        )
+
+instance GRead f => Read (Some f) where
+    readsPrec p = readParen (p>10) $ \s ->
+        [ (getGReadResult withTag mkSome, rest')
+        | (con, rest) <- lex s
+        , con == "Some" || con == "mkSome"
+        , (withTag, rest') <- greadsPrec 11 rest
+        ]
+
+instance GEq tag => Eq (Some tag) where
+    x == y =
+        withSome x $ \x' ->
+        withSome y $ \y' -> defaultEq x' y'
+
+instance GCompare tag => Ord (Some tag) where
+    compare x y =
+        withSome x $ \x' ->
+        withSome y $ \y' -> defaultCompare x' y'
+
+instance GNFData tag => NFData (Some tag) where
+    rnf x = withSome x grnf
+
+instance Control.Applicative.Applicative m => Data.Semigroup.Semigroup (Some m) where
+    m <> n =
+        withSome m $ \m' ->
+        withSome n $ \n' ->
+        mkSome (m' *> n')
+
+instance Applicative m => Data.Monoid.Monoid (Some m) where
+    mempty = mkSome (pure ())
+    mappend = (<>)