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.3.2.2
+version:                0.4
 stability:              provisional
 
 cabal-version:          >= 1.6
diff --git a/examples/FooGADT.hs b/examples/FooGADT.hs
--- a/examples/FooGADT.hs
+++ b/examples/FooGADT.hs
@@ -71,10 +71,10 @@
 
 instance GRead Foo where
     greadsPrec _ str = case tag of
-        "Foo" -> [(\k -> k Foo, rest)]
-        "Bar" -> [(\k -> k Bar, rest)]
-        "Baz" -> [(\k -> k Baz, rest)]
-        "Qux" -> [(\k -> k Qux, rest)]
+        "Foo" -> [(GReadResult (\k -> k Foo), rest)]
+        "Bar" -> [(GReadResult (\k -> k Bar), rest)]
+        "Baz" -> [(GReadResult (\k -> k Baz), rest)]
+        "Qux" -> [(GReadResult (\k -> k Qux), rest)]
         _     -> []
         where (tag, rest) = splitAt 3 str
 
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,12 +1,10 @@
 {-# LANGUAGE ExistentialQuantification, GADTs #-}
 {-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE CPP #-}
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Safe #-}
@@ -36,26 +34,26 @@
 -- >    AString :: Tag String
 -- >    AnInt   :: Tag Int
 -- 
--- Then, we have the following valid expressions of type @DSum Tag@:
+-- Then, we have the following valid expressions of type @Applicative f => DSum Tag f@:
 --
--- > AString :=> "hello!"
--- > AnInt   :=> 42
+-- > AString ==> "hello!"
+-- > AnInt   ==> 42
 -- 
--- And we can write functions that consume @DSum Tag@ values by matching, 
+-- And we can write functions that consume @DSum Tag f@ values by matching, 
 -- such as:
 -- 
--- > toString :: DSum Tag -> String
--- > toString (AString :=> str) = str
--- > toString (AnInt   :=> int) = show int
+-- > 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 :=> operator has very low precedence and binds to 
--- the right, so if the @Tag@ GADT is extended with an additional constructor
--- @Rec :: Tag (DSum Tag)@, then @Rec :=> AnInt :=> 3 + 4@ is parsed as
--- would be expected (@Rec :=> (AnInt :=> (3 + 4))@) and has type @DSum Tag@.
--- Its precedence is just above that of '$', so @foo bar $ AString :=> "eep"@
--- is equivalent to @foo bar (AString :=> "eep")@.
+-- 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
+-- bind to the right, so if the @Tag@ GADT is extended with an additional
+-- constructor @Rec :: Tag (DSum Tag Identity)@, then @Rec ==> AnInt ==> 3 + 4@
+-- is parsed as would be expected (@Rec ==> (AnInt ==> (3 + 4))@) and has type
+-- @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
@@ -65,28 +63,28 @@
 (==>) :: Applicative f => tag a -> a -> DSum tag f
 k ==> v = k :=> pure v
 
--- |In order to make a 'Show' instance for @DSum tag@, @tag@ must be able
+-- |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 => t@ is conceptually equivalent to something like this
--- imaginary syntax:  @(forall a. Inhabited (tag a) => Show a) => t@,
+-- @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 'a' does not occur free in 't'.
+-- 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:
+-- following instances, among others:
 -- 
 -- > instance GShow Tag where
 -- >     gshowsPrec _p AString = showString "AString"
 -- >     gshowsPrec _p AnInt   = showString "AnInt"
--- > instance ShowTag Tag where
+-- > 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 parameter @a@.
+    -- the type @f a@.
     showTaggedPrec :: tag a -> Int -> f a -> ShowS
 
 instance Show (f a) => ShowTag ((:=) a) f where
@@ -110,17 +108,17 @@
 class GRead tag => ReadTag tag f where
     readTaggedPrec :: tag a -> Int -> ReadS (f a)
 
--- |In order to make a 'Read' instance for @DSum tag@, @tag@ must be able
+-- |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 => t@ is conceptually equivalent to something like this
--- imaginary syntax:  @(forall a. Inhabited (tag a) => Read a) => t@,
+-- @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 'a' does not occur free in 't'.
+-- 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:
+-- following instances, among others:
 -- 
 -- > instance GRead Tag where
 -- >     greadsPrec _p str = case tag of
@@ -128,7 +126,7 @@
 -- >        "AnInt"     -> [(\k -> k AnInt,   rest)]
 -- >        _           -> []
 -- >        where (tag, rest) = break isSpace str
--- > instance ReadTag Tag where
+-- > instance ReadTag Tag [] where
 -- >     readTaggedPrec AString = readsPrec
 -- >     readTaggedPrec AnInt   = readsPrec
 -- 
@@ -148,7 +146,7 @@
 instance ReadTag tag f => Read (DSum tag f) where
     readsPrec p = readParen (p > 1) $ \s -> 
         concat
-            [ withTag $ \tag ->
+            [ getGReadResult withTag $ \tag ->
                 [ (tag :=> val, rest'')
                 | (val, rest'') <- readTaggedPrec tag 1 rest'
                 ]
@@ -157,7 +155,7 @@
             , con == " :=> "
             ]
 
--- |In order to test @DSum tag@ for equality, @tag@ must know how to test
+-- |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.
 -- 
@@ -167,7 +165,7 @@
 -- >     geq AString AString = Just Refl
 -- >     geq AnInt   AnInt   = Just Refl
 -- >     geq _       _       = Nothing
--- > instance EqTag Tag where
+-- > instance EqTag Tag [] where
 -- >     eqTagged AString AString = (==)
 -- >     eqTagged AnInt   AnInt   = (==)
 -- 
@@ -175,7 +173,7 @@
 -- 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 @a@.
+    -- 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
@@ -186,7 +184,7 @@
         Refl <- geq t1 t2
         return (eqTagged t1 t2 x1 x2)
 
--- |In order to compare @DSum tag@ values, @tag@ must know how to compare
+-- |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.
 -- 
@@ -197,7 +195,7 @@
 -- >     gcompare AString AnInt   = GLT
 -- >     gcompare AnInt   AString = GGT
 -- >     gcompare AnInt   AnInt   = GEQ
--- > instance OrdTag Tag where
+-- > instance OrdTag Tag [] where
 -- >     compareTagged AString AString = compare
 -- >     compareTagged AnInt   AnInt   = compare
 -- 
@@ -205,7 +203,7 @@
 -- '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 @a@.
+    -- 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
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
@@ -2,7 +2,6 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# OPTIONS_GHC -fno-warn-deprecated-flags #-}
-{-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE CPP #-}
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
 {-# LANGUAGE PolyKinds #-}
@@ -57,8 +56,8 @@
 instance GRead ((:=) a) where
     greadsPrec p s = readsPrec p s >>= f
         where
-            f :: forall x. (x := x, String) -> [(forall b. (forall a. x := a -> b) -> b, String)]
-            f (Refl, rest) = return ((\x -> x Refl) :: forall b. (forall a. x := a -> b) -> b, rest)
+            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 
@@ -154,9 +153,9 @@
 
 instance GRead (GOrdering a) where
     greadsPrec _ s = case con of
-        "GGT"   -> [(\x -> x GGT, rest)]
-        "GEQ"   -> [(\x -> x GEQ, rest)]
-        "GLT"   -> [(\x -> x GLT, rest)]
+        "GGT"   -> [(GReadResult (\x -> x GGT), rest)]
+        "GEQ"   -> [(GReadResult (\x -> x GEQ), rest)]
+        "GLT"   -> [(GReadResult (\x -> x GLT), rest)]
         _       -> []
         where (con, rest) = splitAt 3 s
 
@@ -170,5 +169,3 @@
 
 defaultCompare :: GCompare f => f a -> f b -> Ordering
 defaultCompare x y = weakenOrdering (gcompare x y)
-
-
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,4 +1,4 @@
-{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE CPP #-}
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Safe #-}
@@ -23,9 +23,12 @@
 gshow :: (GShow t) => t a -> String
 gshow x = gshows x ""
 
+newtype GReadResult t = GReadResult
+  { getGReadResult :: forall b . (forall a . t a -> b) -> b }
+
 -- |@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 -> [(forall b. (forall a. t a -> b) -> b, String)]
+type GReadS t = String -> [(GReadResult t, String)]
 
 -- |'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
@@ -37,7 +40,8 @@
 greads = greadsPrec (-1)
 
 gread :: GRead t => String -> (forall a. t a -> b) -> b
-gread s = hd [f | (f, "") <- greads s]
+gread s g = case hd [f | (f, "") <- greads s] of
+              GReadResult res -> res g
     where
         hd (x:_) = x
         hd _ = error "gread: no parse"
diff --git a/src/Data/Some.hs b/src/Data/Some.hs
--- a/src/Data/Some.hs
+++ b/src/Data/Some.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE CPP #-}
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Safe #-}
@@ -28,7 +27,7 @@
 
 instance GRead f => Read (Some f) where
     readsPrec p = readParen (p>10) $ \s ->
-        [ (withTag This, rest')
+        [ (getGReadResult withTag This, rest')
         | let (con, rest) = splitAt 5 s
         , con == "This "
         , (withTag, rest') <- greadsPrec 11 rest