diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,20 @@
 # Revision history for dependent-sum
 
+## 0.6 - 2019-03-21
+
+* Use constraints-extras ArgDict/Has' to define the instances of Eq, Ord, Read and Show for DSum.
+  This obviates the need for the EqTag, OrdTag, ReadTag and ShowTag classes.
+
+## 0.5.1.0
+
+* Add `mkSome` and `mapSome` to `Data.Some`.
+* Add `GEq`, `GCompare`, `GShow,` and `GRead` instances for `Sum` and `Product` (Except `GRead (Product a b)`).
+* Deprecate `(:=)` for `(:~:)` from `Data.Type.Equality`.
+  In GHC 7.8 and above, this is the same as `(:~:)`.
+  But now we no longer support earlier GHCs, so there's no point of the alias.
+* Remove support for GHC 7.x.
+* The git repositories for dependent-sum and dependent-sum-template are now the same, though the Haskell packages remain separate.
+
 ## 0.5.0.0
 
 * Make `Some` a `newtype` with associated pattern synonyms using `unsafeCoerce`
diff --git a/dependent-sum.cabal b/dependent-sum.cabal
--- a/dependent-sum.cabal
+++ b/dependent-sum.cabal
@@ -1,5 +1,5 @@
 name:                   dependent-sum
-version:                0.5
+version:                0.6
 stability:              provisional
 
 cabal-version:          >= 1.6
@@ -26,10 +26,11 @@
 
 tested-with:            GHC == 8.0.2,
                         GHC == 8.2.2,
-                        GHC == 8.4.4
+                        GHC == 8.4.4,
+                        GHC == 8.6.4
 
-extra-source-files:     examples/*.hs
-                        ChangeLog.md
+extra-source-files:     ChangeLog.md
+                      , examples/*.hs
 
 source-repository head
   type:     git
@@ -41,10 +42,8 @@
                         Data.GADT.Compare
                         Data.GADT.Show
                         Data.Some
-  
-  if impl(ghc < 7.8)
-    other-modules:      Data.Dependent.Sum.Typeable
-  
-  build-depends:        base >= 3 && <5
+  other-extensions:     PatternSynonyms
+  build-depends:        base >= 4.9 && <5
+                      , constraints-extras >= 0.2 && < 0.4
   if impl(ghc >= 7.2)
     ghc-options:        -trust base
diff --git a/examples/FooGADT.hs b/examples/FooGADT.hs
--- a/examples/FooGADT.hs
+++ b/examples/FooGADT.hs
@@ -1,11 +1,17 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TemplateHaskell #-}
+
 module FooGADT where
 
 import Data.Dependent.Sum
 import Data.Functor.Identity
 import Data.GADT.Show
 import Data.GADT.Compare
+import Data.Constraint.Extras
+import Data.Constraint.Extras.TH
+import Data.List (sort)
 
 data Foo a where
     Foo :: Foo Double
@@ -13,6 +19,20 @@
     Baz :: Foo String
     Qux :: Foo Double
 
+deriveArgDict ''Foo
+
+{-
+-- NB: The instance for ArgDict could be manually written as:
+
+instance ArgDict Foo where
+    type ConstraintsFor Foo c = (c Double, c Int, c String)
+    argDict x = case x of
+        Foo -> Dict
+        Bar -> Dict
+        Baz -> Dict
+        Qux -> Dict
+-}
+
 instance Eq (Foo a) where
     (==) = defaultEq
 
@@ -23,13 +43,6 @@
     geq Qux Qux = Just Refl
     geq _   _   = Nothing
 
-instance EqTag Foo Identity where
-    eqTagged Foo Foo = (==)
-    eqTagged Bar Bar = (==)
-    eqTagged Baz Baz = (==)
-    eqTagged Qux Qux = (==)
-    eqTagged _   _   = const (const False)
-
 instance GCompare Foo where
     gcompare Foo Foo = GEQ
     gcompare Foo _   = GLT
@@ -45,14 +58,6 @@
     
     gcompare Qux Qux = GEQ
 
-instance OrdTag Foo Identity where
-    compareTagged Foo Foo = compare
-    compareTagged Bar Bar = compare
-    compareTagged Baz Baz = compare
-    compareTagged Qux Qux = compare
-    
-    compareTagged _   _   = error "OrdTag (Foo): bad case"
-
 instance Show (Foo a) where
     showsPrec _ Foo      = showString "Foo"
     showsPrec _ Bar      = showString "Bar"
@@ -62,13 +67,6 @@
 instance GShow Foo where
     gshowsPrec = showsPrec
 
-instance ShowTag Foo Identity where
-    showTaggedPrec Foo = showsPrec
-    showTaggedPrec Bar = showsPrec
-    showTaggedPrec Baz = showsPrec
-    showTaggedPrec Qux = showsPrec
-
-
 instance GRead Foo where
     greadsPrec _ str = case tag of
         "Foo" -> [(GReadResult (\k -> k Foo), rest)]
@@ -78,12 +76,6 @@
         _     -> []
         where (tag, rest) = splitAt 3 str
 
-instance ReadTag Foo Identity where
-    readTaggedPrec Foo = readsPrec
-    readTaggedPrec Bar = readsPrec
-    readTaggedPrec Baz = readsPrec
-    readTaggedPrec Qux = readsPrec
-
 foo :: Double -> DSum Foo Identity
 foo x = Foo ==> x
 
@@ -96,5 +88,7 @@
 qux :: Double -> DSum Foo Identity
 qux x = Qux ==> x
 
-xs = [foo pi, bar 100, baz "hello world", qux (exp 1)]
+xs, xs', xs'' :: [DSum Foo Identity]
+xs = [bar 100, foo pi, qux (exp 1), baz "hello world"]
 xs' = read (show xs) `asTypeOf` xs
+xs'' = sort xs
diff --git a/src/Data/Dependent/Sum.hs b/src/Data/Dependent/Sum.hs
--- a/src/Data/Dependent/Sum.hs
+++ b/src/Data/Dependent/Sum.hs
@@ -1,51 +1,49 @@
-{-# LANGUAGE ExistentialQuantification, GADTs #-}
-{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Safe #-}
-#endif
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
 {-# LANGUAGE PolyKinds #-}
-#endif
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 module Data.Dependent.Sum where
 
 import Control.Applicative
 
-#if MIN_VERSION_base(4,7,0)
-import Data.Typeable (Typeable)
-#else
-import Data.Dependent.Sum.Typeable ({- instance Typeable ... -})
-#endif
+import Data.Constraint.Extras
+import Data.Type.Equality ((:~:) (..))
 
 import Data.GADT.Show
 import Data.GADT.Compare
 
 import Data.Maybe (fromMaybe)
 
--- |A basic dependent sum type; the first component is a tag that specifies 
+import Text.Read
+
+-- |A basic dependent sum type; the first component is a tag that specifies
 -- the type of the second;  for example, think of a GADT such as:
--- 
+--
 -- > data Tag a where
 -- >    AString :: Tag String
 -- >    AnInt   :: Tag Int
--- 
+--
 -- Then, we have the following valid expressions of type @Applicative f => DSum Tag f@:
 --
 -- > AString ==> "hello!"
 -- > AnInt   ==> 42
--- 
--- And we can write functions that consume @DSum Tag f@ values by matching, 
+--
+-- And we can write functions that consume @DSum Tag f@ values by matching,
 -- such as:
--- 
+--
 -- > toString :: DSum Tag Identity -> String
 -- > toString (AString :=> Identity str) = str
 -- > toString (AnInt   :=> Identity int) = show int
--- 
+--
 -- By analogy to the (key => value) construction for dictionary entries in
 -- many dynamic languages, we use (key :=> value) as the constructor for
 -- dependent sums.  The :=> and ==> operators have very low precedence and
@@ -55,162 +53,67 @@
 -- @DSum Identity Tag@.  Its precedence is just above that of '$', so
 -- @foo bar $ AString ==> "eep"@ is equivalent to @foo bar (AString ==> "eep")@.
 data DSum tag f = forall a. !(tag a) :=> f a
-#if MIN_VERSION_base(4,7,0)
-    deriving Typeable
-#endif
+
 infixr 1 :=>, ==>
 
 (==>) :: Applicative f => tag a -> a -> DSum tag f
 k ==> v = k :=> pure v
 
--- |In order to make a 'Show' instance for @DSum tag f@, @tag@ must be able
--- to show itself as well as any value of the tagged type.  'GShow' together
--- with this class provides the interface by which it can do so.
---
--- @ShowTag tag f => t@ is conceptually equivalent to something like this
--- imaginary syntax:  @(forall a. Inhabited (tag a) => Show (f a)) => t@,
--- where 'Inhabited' is an imaginary predicate that characterizes 
--- non-empty types, and 'f' and 'a' do not occur free in 't'.
---
--- The @Tag@ example type introduced in the 'DSum' section could be given the
--- following instances, among others:
--- 
--- > instance GShow Tag where
--- >     gshowsPrec _p AString = showString "AString"
--- >     gshowsPrec _p AnInt   = showString "AnInt"
--- > instance ShowTag Tag [] where
--- >     showTaggedPrec AString = showsPrec
--- >     showTaggedPrec AnInt   = showsPrec
--- 
-class GShow tag => ShowTag tag f where
-    -- |Given a value of type @tag a@, return the 'showsPrec' function for 
-    -- the type @f a@.
-    showTaggedPrec :: tag a -> Int -> f a -> ShowS
-
-instance Show (f a) => ShowTag ((:=) a) f where
-    showTaggedPrec Refl = showsPrec
-
--- This instance is questionable.  It works, but is pretty useless.
-instance Show (f a) => ShowTag (GOrdering a) f where
-    showTaggedPrec GEQ = showsPrec
-    showTaggedPrec _   = \p _ -> showParen (p > 10)
-        ( showString "error "
-        . shows "type information lost into the mists of oblivion"
-        )
-
-instance ShowTag tag f => Show (DSum tag f) where
+instance forall tag f. (GShow tag, Has' Show tag f) => Show (DSum tag f) where
     showsPrec p (tag :=> value) = showParen (p >= 10)
         ( gshowsPrec 0 tag
         . showString " :=> "
-        . showTaggedPrec tag 1 value
+        . has' @Show @f tag (showsPrec 1 value)
         )
 
-class GRead tag => ReadTag tag f where
-    readTaggedPrec :: tag a -> Int -> ReadS (f a)
-
--- |In order to make a 'Read' instance for @DSum tag f@, @tag@ must be able
--- to parse itself as well as any value of the tagged type.  'GRead' together
--- with this class provides the interface by which it can do so.
---
--- @ReadTag tag f => t@ is conceptually equivalent to something like this
--- imaginary syntax:  @(forall a. Inhabited (tag a) => Read (f a)) => t@,
--- where 'Inhabited' is an imaginary predicate that characterizes 
--- non-empty types, and 'f' and 'a' do not occur free in 't'.
---
--- The @Tag@ example type introduced in the 'DSum' section could be given the
--- following instances, among others:
--- 
--- > instance GRead Tag where
--- >     greadsPrec _p str = case tag of
--- >        "AString"   -> [(\k -> k AString, rest)]
--- >        "AnInt"     -> [(\k -> k AnInt,   rest)]
--- >        _           -> []
--- >        where (tag, rest) = break isSpace str
--- > instance ReadTag Tag [] where
--- >     readTaggedPrec AString = readsPrec
--- >     readTaggedPrec AnInt   = readsPrec
--- 
-instance Read (f a) => ReadTag ((:=) a) f where
-    readTaggedPrec Refl = readsPrec
-
--- This instance is questionable.  It works, but is partial (and is also pretty useless)
--- instance Read a => ReadTag (GOrdering a) where
---     readTaggedPrec GEQ = readsPrec
---     readTaggedPrec tag = \p -> readParen (p>10) $ \s ->
---         [ (error msg, rest')
---         | let (con, rest) = splitAt 6 s
---         , con == "error "
---         , (msg, rest') <- reads rest :: [(String, String)]
---         ]
-
-instance ReadTag tag f => Read (DSum tag f) where
-    readsPrec p = readParen (p > 1) $ \s -> 
+instance forall tag f. (GRead tag, Has' Read tag f) => Read (DSum tag f) where
+    readsPrec p = readParen (p > 1) $ \s ->
         concat
             [ getGReadResult withTag $ \tag ->
                 [ (tag :=> val, rest'')
-                | (val, rest'') <- readTaggedPrec tag 1 rest'
+                | (val, rest'') <- has' @Read @f tag (readsPrec 1 rest')
                 ]
             | (withTag, rest) <- greadsPrec p s
             , let (con, rest') = splitAt 5 rest
             , con == " :=> "
             ]
 
--- |In order to test @DSum tag f@ for equality, @tag@ must know how to test
--- both itself and its tagged values for equality.  'EqTag' defines
--- the interface by which they are expected to do so.
--- 
--- Continuing the @Tag@ example from the 'DSum' section, we can define:
--- 
--- > instance GEq Tag where
--- >     geq AString AString = Just Refl
--- >     geq AnInt   AnInt   = Just Refl
--- >     geq _       _       = Nothing
--- > instance EqTag Tag [] where
--- >     eqTagged AString AString = (==)
--- >     eqTagged AnInt   AnInt   = (==)
--- 
--- Note that 'eqTagged' is not called until after the tags have been
--- compared, so it only needs to consider the cases where 'gcompare' returns 'GEQ'.
-class GEq tag => EqTag tag f where
-    -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),
-    -- return the '==' function for the type @f a@.
-    eqTagged :: tag a -> tag a -> f a -> f a -> Bool
-
-instance Eq (f a) => EqTag ((:=) a) f where
-    eqTagged Refl Refl = (==)
-
-instance EqTag tag f => Eq (DSum tag f) where
+instance forall tag f. (GEq tag, Has' Eq tag f) => Eq (DSum tag f) where
     (t1 :=> x1) == (t2 :=> x2)  = fromMaybe False $ do
         Refl <- geq t1 t2
-        return (eqTagged t1 t2 x1 x2)
-
--- |In order to compare @DSum tag f@ values, @tag@ must know how to compare
--- both itself and its tagged values.  'OrdTag' defines the 
--- interface by which they are expected to do so.
--- 
--- Continuing the @Tag@ example from the 'EqTag' section, we can define:
--- 
--- > instance GCompare Tag where
--- >     gcompare AString AString = GEQ
--- >     gcompare AString AnInt   = GLT
--- >     gcompare AnInt   AString = GGT
--- >     gcompare AnInt   AnInt   = GEQ
--- > instance OrdTag Tag [] where
--- >     compareTagged AString AString = compare
--- >     compareTagged AnInt   AnInt   = compare
--- 
--- As with 'eqTagged', 'compareTagged' only needs to consider cases where
--- 'gcompare' returns 'GEQ'.
-class (EqTag tag f, GCompare tag) => OrdTag tag f where
-    -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),
-    -- return the 'compare' function for the type @f a@.
-    compareTagged :: tag a -> tag a -> f a -> f a -> Ordering
-
-instance Ord (f a) => OrdTag ((:=) a) f where
-    compareTagged Refl Refl = compare
+        return $ has' @Eq @f t1 (x1 == x2)
 
-instance OrdTag tag f => Ord (DSum tag f) where
+instance forall tag f. (GCompare tag, Has' Eq tag f, Has' Ord tag f) => Ord (DSum tag f) where
     compare (t1 :=> x1) (t2 :=> x2)  = case gcompare t1 t2 of
         GLT -> LT
         GGT -> GT
-        GEQ -> compareTagged t1 t2 x1 x2
+        GEQ -> has' @Ord @f t1 (x1 `compare` x2)
+
+{-# DEPRECATED ShowTag "Instead of 'ShowTag tag f', use '(GShow tag, Has' Show tag f)'" #-}
+type ShowTag tag f = (GShow tag, Has' Show tag f)
+
+showTaggedPrec :: forall tag f a. (GShow tag, Has' Show tag f) => tag a -> Int -> f a -> ShowS
+showTaggedPrec tag = has' @Show @f tag showsPrec
+
+{-# DEPRECATED ReadTag "Instead of 'ReadTag tag f', use '(GRead tag, Has' Read tag f)'" #-}
+type ReadTag tag f = (GRead tag, Has' Read tag f)
+
+readTaggedPrec :: forall tag f a. (GRead tag, Has' Read tag f) => tag a -> Int -> ReadS (f a)
+readTaggedPrec tag = has' @Read @f tag readsPrec
+
+{-# DEPRECATED EqTag "Instead of 'EqTag tag f', use '(GEq tag, Has' Eq tag f)'" #-}
+type EqTag tag f = (GEq tag, Has' Eq tag f)
+
+eqTaggedPrec :: forall tag f a. (GEq tag, Has' Eq tag f) => tag a -> tag a -> f a -> f a -> Bool
+eqTaggedPrec tag1 tag2 f1 f2 = case tag1 `geq` tag2 of
+  Nothing -> False
+  Just Refl -> has' @Eq @f tag1 $ f1 == f2
+
+{-# DEPRECATED OrdTag "Instead of 'OrdTag tag f', use '(GCompare tag, Has' Ord tag f)'" #-}
+type OrdTag tag f = (GCompare tag, Has' Ord tag f)
+
+compareTaggedPrec :: forall tag f a. (GCompare tag, Has' Ord tag f) => tag a -> tag a -> f a -> f a -> Ordering
+compareTaggedPrec tag1 tag2 f1 f2 = case tag1 `gcompare` tag2 of
+  GLT -> LT
+  GEQ -> has' @Ord @f tag1 $ f1 `compare` f2
+  GGT -> GT
diff --git a/src/Data/Dependent/Sum.hs-boot b/src/Data/Dependent/Sum.hs-boot
deleted file mode 100644
--- a/src/Data/Dependent/Sum.hs-boot
+++ /dev/null
@@ -1,5 +0,0 @@
-{-# LANGUAGE ExistentialQuantification, TypeOperators #-}
-module Data.Dependent.Sum where
-
-data DSum tag f = forall a. !(tag a) :=> f a
-infixr 1 :=>
diff --git a/src/Data/Dependent/Sum/Typeable.hs b/src/Data/Dependent/Sum/Typeable.hs
deleted file mode 100644
--- a/src/Data/Dependent/Sum/Typeable.hs
+++ /dev/null
@@ -1,26 +0,0 @@
-{-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Trustworthy #-}
-#endif
--- |Separate module for Typeable declaration, to minimize the amount of
--- visual inspection required to determine that this package is "safe"
--- 
--- This separation is not necessary with base >= 4.7, so this module will
--- not be compiled at all with GHC >= 7.8.
-module Data.Dependent.Sum.Typeable where
-
-import {-# SOURCE #-} Data.Dependent.Sum
-import Data.Typeable
-
-
-instance (Typeable1 t, Typeable1 f) => Typeable (DSum t f) where
-    typeOf ds = mkTyConApp dSumCon [typeOfF, typeOfT]
-        where
-            typeOfF = typeOf1 $ (undefined :: DSum f t -> f a) ds
-            typeOfT = typeOf1 $ (undefined :: DSum f t -> t a) ds
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-            dSumCon = mkTyCon3 "dependent-sum" "Data.Dependent.Sum" "DSum"
-#else 
-            dSumCon = mkTyCon "Data.Dependent.Sum.DSum"
-#endif
diff --git a/src/Data/GADT/Compare.hs b/src/Data/GADT/Compare.hs
--- a/src/Data/GADT/Compare.hs
+++ b/src/Data/GADT/Compare.hs
@@ -1,136 +1,110 @@
 {-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DeriveDataTypeable #-}
-{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}
 {-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
 {-# LANGUAGE PolyKinds #-}
-#endif
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Safe #-}
-#endif
 {-# LANGUAGE ScopedTypeVariables #-}
-
+{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}
 module Data.GADT.Compare
     ( module Data.GADT.Compare
-#if MIN_VERSION_base(4,7,0)
     , (:~:)(Refl)
-#endif
     ) where
 
 import Data.Maybe
 import Data.GADT.Show
+import Data.Type.Equality ((:~:) (..))
 import Data.Typeable
+import Data.Functor.Sum (Sum (..))
+import Data.Functor.Product (Product (..))
 
 #if MIN_VERSION_base(4,10,0)
 import qualified Type.Reflection as TR
 import Data.Type.Equality (testEquality)
 #endif
 
-#if MIN_VERSION_base(4,7,0)
 -- |Backwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`.
+{-# DEPRECATED (:=) "use '(:~:)' from 'Data.Type,Equality'." #-}
 type (:=) = (:~:)
 
-#else
-
--- |A GADT witnessing equality of two types.  Its only inhabitant is 'Refl'.
-data a := b where
-    Refl :: a := a
-    deriving Typeable
-
-instance Eq (a := b) where
-    Refl == Refl = True
-
-instance Ord (a := b) where
-    compare Refl Refl = EQ
-
-instance Show (a := b) where
-    showsPrec _ Refl = showString "Refl"
-
-instance Read (a := a) where
-    readsPrec _ s = case con of
-        "Refl"  -> [(Refl, rest)]
-        _       -> []
-        where (con,rest) = splitAt 4 s
-
-#endif
-
-instance GShow ((:=) a) where
-    gshowsPrec _ Refl = showString "Refl"
-
-instance GRead ((:=) a) where
-    greadsPrec p s = readsPrec p s >>= f
-        where
-            f :: forall x. (x := x, String) -> [(GReadResult ((:=) x), String)]
-            f (Refl, rest) = return (GReadResult (\x -> x Refl) , rest)
-
 -- |A class for type-contexts which contain enough information
--- to (at least in some cases) decide the equality of types 
+-- 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)
+    geq :: f a -> f b -> Maybe (a :~: b)
 
--- |If 'f' has a 'GEq' instance, this function makes a suitable default 
+-- |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 
+-- |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) 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
 
 -- 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
--- > 
+-- > 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 
+-- 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 
+-- 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
@@ -174,7 +148,7 @@
 class GEq f => GCompare f where
     gcompare :: f a -> f b -> GOrdering a b
 
-instance GCompare ((:=) a) where
+instance GCompare ((:~:) a) where
     gcompare Refl Refl = GEQ
 
 #if MIN_VERSION_base(4,10,0)
@@ -193,3 +167,18 @@
 
 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
diff --git a/src/Data/GADT/Show.hs b/src/Data/GADT/Show.hs
--- a/src/Data/GADT/Show.hs
+++ b/src/Data/GADT/Show.hs
@@ -1,17 +1,23 @@
-{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE CPP #-}
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
-{-# LANGUAGE Safe #-}
-#endif
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
-#endif
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 module Data.GADT.Show where
 
+import Data.Functor.Sum (Sum (..))
+import Data.Functor.Product (Product (..))
+import Data.Type.Equality ((:~:) (..))
+
 #if MIN_VERSION_base(4,10,0)
 import qualified Type.Reflection as TR
 #endif
 
+-- $setup
+-- >>> import Data.Some
+
 -- |'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:
@@ -20,17 +26,36 @@
 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
 
-gshows :: GShow t => t a -> ShowS
-gshows = gshowsPrec (-1)
+--
+-- | >>> 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 :: (GShow t) => t a -> String
-gshow x = gshows 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
 
 newtype GReadResult t = GReadResult
   { getGReadResult :: forall b . (forall a . t a -> b) -> b }
@@ -54,3 +79,34 @@
     where
         hd (x:_) = x
         hd _ = error "gread: no parse"
+
+-- |
+--
+-- >>> greadMaybe "InL Refl" mkSome :: Maybe (Some (Sum ((:~:) Int) ((:~:) Bool)))
+-- Just (Some (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
+    (GReadResult res : _) -> Just (res g)
+    _                     -> Nothing
+
+instance GRead ((:~:) a) where
+    greadsPrec p s = readsPrec p s >>= f
+        where
+            f :: forall x. (x :~: x, String) -> [(GReadResult ((:~:) x), String)]
+            f (Refl, rest) = return (GReadResult (\x -> x Refl) , rest)
+
+instance (GRead a, GRead b) => GRead (Sum a b) where
+    greadsPrec d s = concat
+        [ readParen (d > 10)
+            (\s1 -> [ (GReadResult $ \k -> getGReadResult r (k . InL), t)
+                    | ("InL", s2) <- lex s1
+                    , (r, t) <- greadsPrec 11 s2 ]) s
+        , readParen (d > 10)
+            (\s1 -> [ (GReadResult $ \k -> getGReadResult r (k . InR), t)
+                    | ("InR", s2) <- lex s1
+                    , (r, t) <- greadsPrec 11 s2 ]) s
+        ]
diff --git a/src/Data/Some.hs b/src/Data/Some.hs
--- a/src/Data/Some.hs
+++ b/src/Data/Some.hs
@@ -5,13 +5,51 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE ViewPatterns #-}
-module Data.Some (Some(Some, This), withSome) where
+{-# LANGUAGE Trustworthy #-}
+module Data.Some (Some(Some, This), mkSome, withSome, mapSome) where
 
 import Data.GADT.Show
 import Data.GADT.Compare
 import GHC.Exts (Any)
-import Unsafe.Coerce
+import Unsafe.Coerce (unsafeCoerce)
 
+-- $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"
+--
+-- You can either use @PatternSynonyms@
+--
+-- >>> 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
+--
 newtype Some tag = UnsafeSome (tag Any)
 
 #if __GLASGOW_HASKELL__ >= 801
@@ -28,6 +66,11 @@
 pattern This :: tag a -> Some tag
 pattern This x = Some x
 
+-- | Constructor.
+mkSome :: tag a -> Some tag
+mkSome = Some
+
+-- | Eliminator.
 withSome :: Some tag -> (forall a. tag a -> b) -> b
 withSome (Some thing) some = some thing
 
@@ -50,3 +93,6 @@
 
 instance GCompare tag => Ord (Some tag) where
     compare (Some x) (Some y) = defaultCompare x y
+
+mapSome :: (forall t. f t -> g t) -> Some f -> Some g
+mapSome f (UnsafeSome x) = UnsafeSome (f x)