diff --git a/src/Data/Summer.hs b/src/Data/Summer.hs
--- a/src/Data/Summer.hs
+++ b/src/Data/Summer.hs
@@ -56,11 +56,30 @@
 import Data.Proxy (Proxy(Proxy))
 import Data.Kind (Type)
 import Control.Monad (unless)
+import Generics.SOP (Generic(..))
+import qualified Generics.SOP as SOP
 
 -- | The extensible sum type, allowing inhabitants to be of any of the
 -- types in the given type list.
 data Sum (xs :: [*]) = UnsafeInj {-# UNPACK #-} !Word Any
 
+instance Generic (Sum '[]) where
+  type Code (Sum '[]) = '[]
+  from a = error "Generics.SOP.from: Impossible to create an empty sum"
+  to a = error "Generics.SOP.to: Impossible to create an empty sum"
+
+instance Generic (Sum xs) => Generic (Sum (x ': xs)) where
+  type Code (Sum (x ': xs)) = '[x] ': Code (Sum xs)
+  from (UnsafeInj 0 x) = SOP.SOP (SOP.Z (SOP.I (unsafeCoerce x) SOP.:* SOP.Nil))
+  from xs = SOP.SOP (SOP.S ns) where
+    SOP.SOP ns = from (unsafeForgetFirst xs)
+  to (SOP.SOP ns) = case ns of
+    SOP.Z (SOP.I x SOP.:* SOP.Nil) -> UnsafeInj 0 (unsafeCoerce x)
+    SOP.S s -> recall (to (SOP.SOP s))
+    where
+      recall :: Sum xs -> Sum (x ': xs)
+      recall (UnsafeInj i a) = UnsafeInj (i + 1) a
+
 type role Sum representational
 
 -- | A pattern to match on for convenience. Without this, the user facing
@@ -124,8 +143,8 @@
 {-# INLINE CONLIKE inmap #-}
 
 -- | Transform one type in one sum into another type in another sum.
-smap :: forall x y xs ys. (Weaken xs ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys
-smap f uv@(UnsafeInj tag' x) = if tag' == tag @x @xs then UnsafeInj (tag @y @ys) (unsafeCoerce (f (unsafeCoerce x))) else weaken uv
+smap :: forall x y xs ys. (Weaken (Delete x xs) ys, x `HasTagIn` xs, y `HasTagIn` ys) => (x -> y) -> Sum xs -> Sum ys
+smap f uv@(UnsafeInj tag' x) = if tag' == tag @x @xs then UnsafeInj (tag @y @ys) (unsafeCoerce (f (unsafeCoerce x))) else weaken (unsafeForget @x uv)
 {-# INLINE CONLIKE smap #-}
 
 -- | A class which checks that every type has the same tag in the first
@@ -141,8 +160,14 @@
 noOpWeaken = unsafeCoerce
 {-# INLINE CONLIKE noOpWeaken #-}
 
-unsafeForget :: Sum (x ': xs) -> Sum xs
-unsafeForget (UnsafeInj tag' x) = UnsafeInj (tag' - 1) x
+unsafeForget :: forall x xs. x `HasTagIn` xs => Sum xs -> Sum (Delete x xs)
+unsafeForget (UnsafeInj tag' x) = if tag' < tag @x @xs then UnsafeInj tag' x
+                             else if tag' == tag @x @xs then error "unsafeForget: you can't forget the truth"
+                             else UnsafeInj (tag' - 1) x
+
+
+unsafeForgetFirst :: Sum (x ': xs) -> Sum xs
+unsafeForgetFirst (UnsafeInj tag' x) = UnsafeInj (tag' - 1) x
 {-# INLINE CONLIKE unsafeForget #-}
 
 -- | Testing extensible sums for equality.
@@ -151,7 +176,7 @@
     | tag' == tag'' =
         if tag' == 0
           then unsafeCoerce @_ @x x == unsafeCoerce @_ @x x'
-          else unsafeForget uv == unsafeForget uv'
+          else unsafeForgetFirst uv == unsafeForgetFirst uv'
     | otherwise = False
   {-# INLINE CONLIKE (==) #-}
 instance Eq (Sum '[]) where
@@ -164,7 +189,7 @@
   weaken uv@(UnsafeInj tag' x) =
     if tag' == 0
       then UnsafeInj (tag @x @ys) x
-      else let UnsafeInj tag'' _ = weaken @xs @ys (unsafeForget uv) in UnsafeInj tag'' x
+      else let UnsafeInj tag'' _ = weaken @xs @ys (unsafeForgetFirst uv) in UnsafeInj tag'' x
   {-# INLINE CONLIKE weaken #-}
 instance Weaken '[] ys where
   weaken = error "weaken base case: impossible by construction"
@@ -183,7 +208,7 @@
 instance Match '[] where
   match = error "match base case: impossible by construction"
   {-# INLINE CONLIKE match #-}
-  unmatch = id
+  unmatch r = r
   {-# INLINE CONLIKE unmatch #-}
   override = const
   {-# INLINE CONLIKE override #-}
@@ -191,8 +216,8 @@
   match :: forall r. Sum (x ': xs) -> (x -> r) -> Matcher xs r
   match uv@(UnsafeInj tag' x) f =
     if tag' == 0
-      then override @xs @r (f (unsafeCoerce x)) $ match @xs @r (unsafeForget uv)
-      else match @xs @r (unsafeForget uv)
+      then override @xs @r (f (unsafeCoerce x)) $ match @xs @r (unsafeForgetFirst uv)
+      else match @xs @r (unsafeForgetFirst uv)
   {-# INLINE CONLIKE match #-}
   unmatch :: (forall r. (x -> r) -> Matcher xs r) -> Sum (x ': xs)
   unmatch g = unmatchGo @xs $ g @(Sum (x ': xs)) (UnsafeInj 0 . unsafeCoerce @x)
diff --git a/summer.cabal b/summer.cabal
--- a/summer.cabal
+++ b/summer.cabal
@@ -1,6 +1,6 @@
 cabal-version:       2.4
 name:                summer
-version:             0.1.2.0
+version:             0.2.0.1
 synopsis:            An implementation of extensible products and sums
 description:         An implementation of extensible products and sums.
 license:             MIT
@@ -20,7 +20,7 @@
 
 library
   exposed-modules:     Data.Summer, Data.Prodder
-  build-depends:       base >=4.12 && <4.15, vector >=0.12
+  build-depends:       base >=4.12 && <4.16, vector >=0.12, generics-sop >=0.5
   hs-source-dirs:      src
   default-language:    Haskell2010