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.2.1.0
+version:                0.3.1.0
 stability:              provisional
 
 cabal-version:          >= 1.6
@@ -24,8 +24,6 @@
                         dependent sum types by using your own \"tag\"
                         types.
 
-tested-with:            GHC == 7.6.3, GHC == 7.8.0.20140228
-
 extra-source-files:     examples/*.hs
 
 source-repository head
@@ -40,6 +38,8 @@
   
   if impl(ghc < 7.8)
     other-modules:      Data.Dependent.Sum.Typeable
+                        Data.Some
+  
   build-depends:        base >= 3 && <5
   if impl(ghc >= 7.2)
     ghc-options:        -trust base
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,14 +1,23 @@
 {-# 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 #-}
 #endif
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+{-# LANGUAGE PolyKinds #-}
+#endif
 module Data.Dependent.Sum where
 
+import Control.Applicative
+
 #if MIN_VERSION_base(4,7,0)
 import Data.Typeable (Typeable)
 #else
@@ -47,12 +56,15 @@
 -- 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")@.
-data DSum tag = forall a. !(tag a) :=> a
+data DSum tag f = forall a. !(tag a) :=> f a
 #if MIN_VERSION_base(4,7,0)
     deriving Typeable
 #endif
-infixr 1 :=>
+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@, @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.
@@ -72,31 +84,31 @@
 -- >     showTaggedPrec AString = showsPrec
 -- >     showTaggedPrec AnInt   = showsPrec
 -- 
-class GShow tag => ShowTag tag where
+class GShow tag => ShowTag tag f where
     -- |Given a value of type @tag a@, return the 'showsPrec' function for 
     -- the type parameter @a@.
-    showTaggedPrec :: tag a -> Int ->     a -> ShowS
+    showTaggedPrec :: tag a -> Int -> f a -> ShowS
 
-instance Show a => ShowTag ((:=) a) where
+instance Show (f a) => ShowTag ((:=) a) f where
     showTaggedPrec Refl = showsPrec
 
 -- This instance is questionable.  It works, but is pretty useless.
-instance Show a => ShowTag (GOrdering a) where
+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 => Show (DSum tag) where
+instance ShowTag tag f => Show (DSum tag f) where
     showsPrec p (tag :=> value) = showParen (p >= 10)
         ( gshowsPrec 0 tag
         . showString " :=> "
         . showTaggedPrec tag 1 value
         )
 
-class GRead tag => ReadTag tag where
-    readTaggedPrec :: tag a -> Int -> ReadS a
+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
 -- to parse itself as well as any value of the tagged type.  'GRead' together
@@ -120,7 +132,7 @@
 -- >     readTaggedPrec AString = readsPrec
 -- >     readTaggedPrec AnInt   = readsPrec
 -- 
-instance Read a => ReadTag ((:=) a) where
+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)
@@ -133,7 +145,7 @@
 --         , (msg, rest') <- reads rest :: [(String, String)]
 --         ]
 
-instance ReadTag tag => Read (DSum tag) where
+instance ReadTag tag f => Read (DSum tag f) where
     readsPrec p = readParen (p > 1) $ \s -> 
         concat
             [ withTag $ \tag ->
@@ -161,15 +173,15 @@
 -- 
 -- 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 where
+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@.
-    eqTagged :: tag a -> tag a -> a -> a -> Bool
+    eqTagged :: tag a -> tag a -> f a -> f a -> Bool
 
-instance Eq a => EqTag ((:=) a) where
+instance Eq (f a) => EqTag ((:=) a) f where
     eqTagged Refl Refl = (==)
 
-instance EqTag tag => Eq (DSum tag) where
+instance EqTag tag f => Eq (DSum tag f) where
     (t1 :=> x1) == (t2 :=> x2)  = fromMaybe False $ do
         Refl <- geq t1 t2
         return (eqTagged t1 t2 x1 x2)
@@ -191,15 +203,15 @@
 -- 
 -- As with 'eqTagged', 'compareTagged' only needs to consider cases where
 -- 'gcompare' returns 'GEQ'.
-class (EqTag tag, GCompare tag) => OrdTag tag where
+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@.
-    compareTagged :: tag a -> tag a -> a -> a -> Ordering
+    compareTagged :: tag a -> tag a -> f a -> f a -> Ordering
 
-instance Ord a => OrdTag ((:=) a) where
+instance Ord (f a) => OrdTag ((:=) a) f where
     compareTagged Refl Refl = compare
 
-instance OrdTag tag => Ord (DSum tag) where
+instance OrdTag tag f => Ord (DSum tag f) where
     compare (t1 :=> x1) (t2 :=> x2)  = case gcompare t1 t2 of
         GLT -> LT
         GGT -> GT
diff --git a/src/Data/Dependent/Sum.hs-boot b/src/Data/Dependent/Sum.hs-boot
--- a/src/Data/Dependent/Sum.hs-boot
+++ b/src/Data/Dependent/Sum.hs-boot
@@ -1,5 +1,5 @@
 {-# LANGUAGE ExistentialQuantification, TypeOperators #-}
 module Data.Dependent.Sum where
 
-data DSum tag = forall a. !(tag a) :=> a
+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
--- a/src/Data/Dependent/Sum/Typeable.hs
+++ b/src/Data/Dependent/Sum/Typeable.hs
@@ -4,7 +4,7 @@
 #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
@@ -12,20 +12,15 @@
 import {-# SOURCE #-} Data.Dependent.Sum
 import Data.Typeable
 
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 
-instance Typeable1 t => Typeable (DSum t) where
-    typeOf ds = mkTyConApp dSumCon [typeOfT]
+instance (Typeable1 t, Typeable1 f) => Typeable (DSum t f) where
+    typeOf ds = mkTyConApp dSumCon [typeOfF, typeOfT]
         where
-            dSumCon = mkTyCon3 "dependent-sum" "Data.Dependent.Sum" "DSum"
-            typeOfT = typeOf1 $ (undefined :: DSum f -> f a) ds
+            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 
-
-instance Typeable1 t => Typeable (DSum t) where
-    typeOf ds = mkTyConApp dSumCon [typeOfT]
-        where
             dSumCon = mkTyCon "Data.Dependent.Sum.DSum"
-            typeOfT = typeOf1 $ (undefined :: DSum f -> f a) ds
-
 #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
@@ -159,8 +159,6 @@
         _       -> []
         where (con, rest) = splitAt 3 s
 
--- |Type class for orderable GADT-like structures.  When 2 things are equal,
--- must return a witness that their parameter types are equal as well (GEQ).
 -- |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
@@ -168,4 +166,8 @@
 
 instance GCompare ((:=) a) where
     gcompare Refl Refl = GEQ
+
+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
@@ -3,6 +3,9 @@
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
 {-# LANGUAGE Safe #-}
 #endif
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+{-# LANGUAGE PolyKinds #-}
+#endif
 module Data.GADT.Show where
 
 -- |'Show'-like class for 1-type-parameter GADTs.  @GShow t => ...@ is equivalent to something
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,38 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE CPP #-}
+#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 (This thing) some = some thing
+
+instance GShow tag => Show (Some tag) where
+    showsPrec p (This thing) = showParen (p > 10)
+        ( showString "This "
+        . gshowsPrec 11 thing
+        )
+
+instance GRead f => Read (Some f) where
+    readsPrec p = readParen (p>10) $ \s ->
+        [ (withTag This, rest')
+        | let (con, rest) = splitAt 5 s
+        , con == "This "
+        , (withTag, rest') <- greadsPrec 11 rest
+        ]
+
+instance GEq tag => Eq (Some tag) where
+    This x == This y = defaultEq x y
+
+instance GCompare tag => Ord (Some tag) where
+    compare (This x) (This y) = defaultCompare x y