diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+# Version 0.8
+
+* Builds with GHC 8.10 and `singletons-2.7`.
+
 # Version 0.7
 
 * BACKWARDS COMPATIBLE COMPILER ASSISTED CHANGE: All of the cabal flags
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/exinst.cabal b/exinst.cabal
--- a/exinst.cabal
+++ b/exinst.cabal
@@ -1,8 +1,8 @@
 name:                exinst
-version:             0.7
+version:             0.8
 author:              Renzo Carbonara
-maintainer:          renzoλcarbonara.com.ar
-copyright:           Renzo Carbonara 2015-2018
+maintainer:          renλren!zone
+copyright:           Renzo Carbonara 2015
 license:             BSD3
 license-file:        LICENSE.txt
 extra-source-files:  README.md CHANGELOG.md
@@ -35,7 +35,7 @@
     , deepseq
     , hashable
     , profunctors >=5.0
-    , singletons >=2.3.1
+    , singletons >=2.6
     , QuickCheck
   ghcjs-options: -Wall -O3
   ghc-options: -Wall -O2
diff --git a/lib/Exinst/Base.hs b/lib/Exinst/Base.hs
--- a/lib/Exinst/Base.hs
+++ b/lib/Exinst/Base.hs
@@ -23,11 +23,10 @@
 import Data.Kind (Type)
 import Data.Singletons
 import Data.Singletons.Prelude.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound))
-import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse))
+import Data.Singletons.Prelude.Bool (SBool(STrue, SFalse))
 import qualified Data.Singletons.Prelude.List as List
 import Data.Singletons.Prelude.Tuple (Tuple2Sym1)
 import Data.Singletons.Decide
-import Data.Type.Equality
 import qualified GHC.Generics as G
 import Prelude
 import qualified Text.Read as Read
@@ -45,7 +44,7 @@
 data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Show)
 data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Show)
 
-instance forall (f :: k1 -> Type)
+instance forall k1 (f :: k1 -> Type)
   . ( SingKind k1
     , Show (Demote k1)
     , Dict1 Show f
@@ -56,7 +55,7 @@
        case dict1 sa1 :: Dict (Show (f a1)) of
           Dict -> showsPrec n (Some1 (fromSing sa1) x)
 
-instance forall (f :: k2 -> k1 -> Type)
+instance forall k2 k1 (f :: k2 -> k1 -> Type)
   . ( SingKind k2
     , SingKind k1
     , Show (Demote k2)
@@ -69,7 +68,7 @@
        case dict2 sa2 sa1 :: Dict (Show (f a2 a1)) of
           Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x)
 
-instance forall (f :: k3 -> k2 -> k1 -> Type)
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
   . ( SingKind k3
     , SingKind k2
     , SingKind k1
@@ -84,7 +83,7 @@
        case dict3 sa3 sa2 sa1 :: Dict (Show (f a3 a2 a1)) of
           Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x)
 
-instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
   . ( SingKind k4
     , SingKind k3
     , SingKind k2
@@ -105,7 +104,7 @@
 --------------------------------------------------------------------------------
 -- Read
 
-instance forall (f :: k1 -> Type)
+instance forall k1 (f :: k1 -> Type)
   . ( SingKind k1
     , Read (Demote k1)
     , Dict1 Read f
@@ -121,7 +120,7 @@
                x :: f a1 <- Read.readPrec
                pure (Exinst.Some1 sa1 x)
 
-instance forall (f :: k2 -> k1 -> Type)
+instance forall k2 k1 (f :: k2 -> k1 -> Type)
   . ( SingKind k2
     , SingKind k1
     , Read (Demote k2)
@@ -141,7 +140,7 @@
                   x :: f a2 a1 <- Read.readPrec
                   pure (Exinst.Some2 sa2 sa1 x)
 
-instance forall (f :: k3 -> k2 -> k1 -> Type)
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
   . ( SingKind k3
     , SingKind k2
     , SingKind k1
@@ -165,7 +164,7 @@
                      x :: f a3 a2 a1 <- Read.readPrec
                      pure (Exinst.Some3 sa3 sa2 sa1 x)
 
-instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
   . ( SingKind k4
     , SingKind k3
     , SingKind k2
@@ -196,7 +195,7 @@
 --------------------------------------------------------------------------------
 -- Eq
 
-instance forall (f :: k1 -> Type).
+instance forall k1 (f :: k1 -> Type).
   ( SDecide k1
   , Dict1 Eq f
   ) => Eq (Exinst.Some1 f)
@@ -206,11 +205,11 @@
      withSome1Sing som1x $ \sa1x (x :: f a1x) ->
         withSome1Sing som1y $ \sa1y (y :: f a1y) ->
            maybe False id $ do
-              Refl <- testEquality sa1x sa1y
+              Refl <- decideEquality sa1x sa1y
               case dict1 sa1x :: Dict (Eq (f a1x)) of
                  Dict -> Just (x == y)
 
-instance forall (f :: k2 -> k1 -> Type)
+instance forall k2 k1 (f :: k2 -> k1 -> Type)
   . ( SDecide k2
     , SDecide k1
     , Dict2 Eq f
@@ -221,12 +220,12 @@
        withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) ->
           withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) ->
              maybe False id $ do
-                Refl <- testEquality sa2x sa2y
-                Refl <- testEquality sa1x sa1y
+                Refl <- decideEquality sa2x sa2y
+                Refl <- decideEquality sa1x sa1y
                 case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of
                    Dict -> Just (x == y)
 
-instance forall (f :: k3 -> k2 -> k1 -> Type)
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
   . ( SDecide k3
     , SDecide k2
     , SDecide k1
@@ -238,13 +237,13 @@
        withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) ->
           withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) ->
              maybe False id $ do
-                Refl <- testEquality sa3x sa3y
-                Refl <- testEquality sa2x sa2y
-                Refl <- testEquality sa1x sa1y
+                Refl <- decideEquality sa3x sa3y
+                Refl <- decideEquality sa2x sa2y
+                Refl <- decideEquality sa1x sa1y
                 case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of
                    Dict -> Just (x == y)
 
-instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
   . ( SDecide k4
     , SDecide k3
     , SDecide k2
@@ -257,17 +256,17 @@
        withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) ->
           withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) ->
              maybe False id $ do
-                Refl <- testEquality sa4x sa4y
-                Refl <- testEquality sa3x sa3y
-                Refl <- testEquality sa2x sa2y
-                Refl <- testEquality sa1x sa1y
+                Refl <- decideEquality sa4x sa4y
+                Refl <- decideEquality sa3x sa3y
+                Refl <- decideEquality sa2x sa2y
+                Refl <- decideEquality sa1x sa1y
                 case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of
                    Dict -> Just (x == y)
 
 --------------------------------------------------------------------------------
 -- Ord
 
-instance forall (f :: k1 -> Type)
+instance forall k1 (f :: k1 -> Type)
   . ( SingKind k1
     , SDecide k1
     , Ord (Demote k1)
@@ -281,11 +280,11 @@
           withSome1Sing som1y $ \sa1y (y :: f a1y) ->
              let termCompare = compare (fromSing sa1x) (fromSing sa1y)
              in maybe termCompare id $ do
-                  Refl <- testEquality sa1x sa1y
+                  Refl <- decideEquality sa1x sa1y
                   case dict1 sa1x :: Dict (Ord (f a1x)) of
                      Dict -> Just (compare x y)
 
-instance forall (f :: k2 -> k1 -> Type)
+instance forall k2 k1 (f :: k2 -> k1 -> Type)
   . ( SingKind k2
     , SingKind k1
     , SDecide k2
@@ -303,12 +302,12 @@
              let termCompare = compare (fromSing sa2x, fromSing sa1x)
                                        (fromSing sa2y, fromSing sa1y)
              in maybe termCompare id $ do
-                   Refl <- testEquality sa2x sa2y
-                   Refl <- testEquality sa1x sa1y
+                   Refl <- decideEquality sa2x sa2y
+                   Refl <- decideEquality sa1x sa1y
                    case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of
                       Dict -> Just (compare x y)
 
-instance forall (f :: k3 -> k2 -> k1 -> Type)
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
   . ( SingKind k3
     , SingKind k2
     , SingKind k1
@@ -330,13 +329,13 @@
                    (fromSing sa3x, fromSing sa2x, fromSing sa1x)
                    (fromSing sa3y, fromSing sa2y, fromSing sa1y)
              in maybe termCompare id $ do
-                  Refl <- testEquality sa3x sa3y
-                  Refl <- testEquality sa2x sa2y
-                  Refl <- testEquality sa1x sa1y
+                  Refl <- decideEquality sa3x sa3y
+                  Refl <- decideEquality sa2x sa2y
+                  Refl <- decideEquality sa1x sa1y
                   case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of
                      Dict -> Just (compare x y)
 
-instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
   . ( SingKind k4
     , SingKind k3
     , SingKind k2
@@ -361,10 +360,10 @@
                    (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x)
                    (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y)
              in maybe termCompare id $ do
-                  Refl <- testEquality sa4x sa4y
-                  Refl <- testEquality sa3x sa3y
-                  Refl <- testEquality sa2x sa2y
-                  Refl <- testEquality sa1x sa1y
+                  Refl <- decideEquality sa4x sa4y
+                  Refl <- decideEquality sa3x sa3y
+                  Refl <- decideEquality sa2x sa2y
+                  Refl <- decideEquality sa1x sa1y
                   case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of
                      Dict -> Just (compare x y)
 
@@ -523,7 +522,7 @@
                 , Cartesian4 xs4 xs3 xs2 xs1 ]
 
 
-instance forall k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
   . ( SingKind k4
     , SingKind k3
     , SingKind k2
@@ -566,31 +565,31 @@
 --------------------------------------------------------------------------------
 -- Out of the box 'DictX' instances for some @base@ types
 
-instance
+instance forall c.
   (c 'False, c 'True
   ) => Dict0 (c :: Bool -> Constraint) where
   {-# INLINABLE dict0 #-}
   dict0 = \case { SFalse -> Dict; STrue -> Dict }
 
-instance
+instance forall k0 c f.
   ( c (f 'False), c (f 'True)
   ) => Dict1 c (f :: Bool -> k0) where
   {-# INLINABLE dict1 #-}
   dict1 = \case { SFalse -> Dict; STrue -> Dict }
 
-instance
+instance forall k1 k0 c f.
   ( Dict1 c (f 'False), Dict1 c (f 'True)
   ) => Dict2 c (f :: Bool -> k1 -> k0) where
   {-# INLINABLE dict2 #-}
   dict2 = \x -> case x of { SFalse -> dict1; STrue -> dict1 }
 
-instance
+instance forall k2 k1 k0 c f.
   ( Dict2 c (f 'False), Dict2 c (f 'True)
   ) => Dict3 c (f :: Bool -> k2 -> k1 -> k0) where
   {-# INLINABLE dict3 #-}
   dict3 = \x -> case x of { SFalse -> dict2; STrue -> dict2 }
 
-instance
+instance forall k3 k2 k1 k0 c f.
   ( Dict3 c (f 'False), Dict3 c (f 'True)
   ) => Dict4 c (f :: Bool -> k3 -> k2 -> k1 -> k0) where
   {-# INLINABLE dict4 #-}
diff --git a/lib/Exinst/Binary.hs b/lib/Exinst/Binary.hs
--- a/lib/Exinst/Binary.hs
+++ b/lib/Exinst/Binary.hs
@@ -29,7 +29,7 @@
 -- | Compatible with the 'Data.Bytes.Serial.Serial' instance and
 -- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the
 -- fully applied @f@ instances are compatible as well.
-instance forall (f :: k1 -> Type).
+instance forall k1 (f :: k1 -> Type).
   ( SingKind k1
   , Bin.Binary (Demote k1)
   , Dict1 Bin.Binary f
@@ -53,7 +53,7 @@
 -- | Compatible with the 'Data.Bytes.Serial.Serial' instance and
 -- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the
 -- fully applied @f@ instances are compatible as well.
-instance forall (f :: k2 -> k1 -> Type).
+instance forall k2 k1 (f :: k2 -> k1 -> Type).
   ( SingKind k2
   , SingKind k1
   , Bin.Binary (Demote k2)
@@ -80,7 +80,7 @@
 -- | Compatible with the 'Data.Bytes.Serial.Serial' instance and
 -- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the
 -- fully applied @f@ instances are compatible as well.
-instance forall (f :: k3 -> k2 -> k1 -> Type).
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type).
   ( SingKind k3
   , SingKind k2
   , SingKind k1
@@ -110,7 +110,7 @@
 -- | Compatible with the 'Data.Bytes.Serial.Serial' instance and
 -- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the
 -- fully applied @f@ instances are compatible as well.
-instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type).
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type).
   ( SingKind k4
   , SingKind k3
   , SingKind k2
diff --git a/lib/Exinst/DeepSeq.hs b/lib/Exinst/DeepSeq.hs
--- a/lib/Exinst/DeepSeq.hs
+++ b/lib/Exinst/DeepSeq.hs
@@ -24,7 +24,7 @@
 
 --------------------------------------------------------------------------------
 
-instance forall (f :: k1 -> *).
+instance forall k1 (f :: k1 -> *).
   ( Dict1 NFData f
   ) => NFData (Some1 f) where
   {-# INLINABLE rnf #-}
@@ -33,7 +33,7 @@
        case dict1 sa1 :: Dict (NFData (f a1)) of
           Dict -> rnf x `seq` ()
 
-instance forall (f :: k2 -> k1 -> *).
+instance forall k2 k1 (f :: k2 -> k1 -> *).
   ( Dict2 NFData f
   ) => NFData (Some2 f) where
   {-# INLINABLE rnf #-}
@@ -42,7 +42,7 @@
        case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of
           Dict -> rnf x `seq` ()
 
-instance forall (f :: k3 -> k2 -> k1 -> *).
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> *).
   ( Dict3 NFData f
   ) => NFData (Some3 f) where
   {-# INLINABLE rnf #-}
@@ -51,7 +51,7 @@
        case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of
           Dict -> rnf x `seq` ()
 
-instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> *).
   ( Dict4 NFData f
   ) => NFData (Some4 f) where
   {-# INLINABLE rnf #-}
diff --git a/lib/Exinst/Hashable.hs b/lib/Exinst/Hashable.hs
--- a/lib/Exinst/Hashable.hs
+++ b/lib/Exinst/Hashable.hs
@@ -32,7 +32,7 @@
 
 --------------------------------------------------------------------------------
 
-instance forall (f :: k1 -> Type)
+instance forall k1 (f :: k1 -> Type)
   . ( SingKind k1
     , Hashable (Demote k1)
     , Dict1 Hashable f
@@ -45,7 +45,7 @@
                        `hashWithSalt` fromSing sa1
                        `hashWithSalt` x
 
-instance forall (f :: k2 -> k1 -> Type)
+instance forall k2 k1 (f :: k2 -> k1 -> Type)
   . ( SingKind k2
     , SingKind k1
     , Hashable (Demote k2)
@@ -61,7 +61,7 @@
                        `hashWithSalt` fromSing sa1
                        `hashWithSalt` x
 
-instance forall (f :: k3 -> k2 -> k1 -> Type)
+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
   . ( SingKind k3
     , SingKind k2
     , SingKind k1
@@ -80,7 +80,7 @@
                        `hashWithSalt` fromSing sa1
                        `hashWithSalt` x
 
-instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)
+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
   . ( SingKind k4
     , SingKind k3
     , SingKind k2
diff --git a/lib/Exinst/Internal.hs b/lib/Exinst/Internal.hs
--- a/lib/Exinst/Internal.hs
+++ b/lib/Exinst/Internal.hs
@@ -63,7 +63,6 @@
 import Data.Profunctor (dimap, Choice(right'))
 import Data.Singletons
 import Data.Singletons.Decide
-import Data.Type.Equality
 import Prelude
 
 --------------------------------------------------------------------------------
@@ -83,7 +82,7 @@
 --------------------------------------------------------------------------------
 
 some1
-  :: forall (f1 :: k1 -> Type) a1
+  :: forall k1 (f1 :: k1 -> Type) a1
   .  SingI a1
   => f1 a1
   -> Some1 f1 -- ^
@@ -91,7 +90,7 @@
 {-# INLINE some1 #-}
 
 some2
-  :: forall (f2 :: k2 -> k1 -> Type) a2 a1
+  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
   .  (SingI a2, SingI a1)
   => f2 a2 a1
   -> Some2 f2 -- ^
@@ -99,7 +98,7 @@
 {-# INLINE some2 #-}
 
 some3
-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
+  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
   .  (SingI a3, SingI a2, SingI a1)
   => f3 a3 a2 a1
   -> Some3 f3 -- ^
@@ -107,7 +106,7 @@
 {-# INLINE some3 #-}
 
 some4
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
+  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
   .  (SingI a4, SingI a3, SingI a2, SingI a1)
   => f4 a4 a3 a2 a1
   -> Some4 f4 -- ^
@@ -118,7 +117,7 @@
 --------------------------------------------------------------------------------
 
 withSome1
-  :: forall (f1 :: k1 -> Type) (r :: Type)
+  :: forall k1 (f1 :: k1 -> Type) (r :: Type)
    . Some1 f1
   -> (forall a1. SingI a1 => f1 a1 -> r)
   -> r -- ^
@@ -126,7 +125,7 @@
 {-# INLINABLE withSome1 #-}
 
 withSome2
-  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)
+  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) (r :: Type)
   .  Some2 f2
   -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)
   -> r -- ^
@@ -134,7 +133,7 @@
 {-# INLINABLE withSome2 #-}
 
 withSome3
-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
+  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
   .  Some3 f3
   -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)
   -> r -- ^
@@ -142,7 +141,7 @@
 {-# INLINABLE withSome3 #-}
 
 withSome4
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
+  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
   .  Some4 f4
   -> (forall a4 a3 a2 a1
         .  (SingI a4, SingI a3, SingI a2, SingI a1)
@@ -155,7 +154,7 @@
 
 -- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance.
 withSome1Sing
-  :: forall (f1 :: k1 -> Type) (r :: Type)
+  :: forall k1 (f1 :: k1 -> Type) (r :: Type)
    . Some1 f1
   -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r)
   -> r -- ^
@@ -164,7 +163,7 @@
 
 -- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances.
 withSome2Sing
-  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)
+  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) (r :: Type)
   .  Some2 f2
   -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
   -> r -- ^
@@ -173,7 +172,7 @@
 
 -- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances.
 withSome3Sing
-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
+  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
   .  Some3 f3
   -> (forall a3 a2 a1
          .  (SingI a3, SingI a2, SingI a1)
@@ -185,7 +184,7 @@
 
 -- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances.
 withSome4Sing
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
+  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
   .  Some4 f4
   -> (forall a4 a3 a2 a1
         .  (SingI a4, SingI a3, SingI a2, SingI a1)
@@ -199,43 +198,43 @@
 --------------------------------------------------------------------------------
 
 fromSome1
-   :: forall (f1 :: k1 -> Type) a1
+   :: forall k1 (f1 :: k1 -> Type) a1
     . (SingI a1, SDecide k1)
    => Some1 f1
    -> Maybe (f1 a1) -- ^
 fromSome1 = \(Some1 sa1' x) -> do
-   Refl <- testEquality sa1' (sing :: Sing a1)
+   Refl <- decideEquality sa1' (sing :: Sing a1)
    return x
 {-# INLINABLE fromSome1 #-}
 
 fromSome2
-   :: forall (f2 :: k2 -> k1 -> Type) a2 a1
+   :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
     . ( SingI a2, SDecide k2
       , SingI a1, SDecide k1 )
    => Some2 f2
    -> Maybe (f2 a2 a1) -- ^
 fromSome2 = \(Some2 sa2' sa1' x) -> do
-   Refl <- testEquality sa2' (sing :: Sing a2)
-   Refl <- testEquality sa1' (sing :: Sing a1)
+   Refl <- decideEquality sa2' (sing :: Sing a2)
+   Refl <- decideEquality sa1' (sing :: Sing a1)
    return x
 {-# INLINABLE fromSome2 #-}
 
 fromSome3
-   :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
+   :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
     . ( SingI a3, SDecide k3
       , SingI a2, SDecide k2
       , SingI a1, SDecide k1 )
    => Some3 f3
    -> Maybe (f3 a3 a2 a1) -- ^
 fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do
-   Refl <- testEquality sa3' (sing :: Sing a3)
-   Refl <- testEquality sa2' (sing :: Sing a2)
-   Refl <- testEquality sa1' (sing :: Sing a1)
+   Refl <- decideEquality sa3' (sing :: Sing a3)
+   Refl <- decideEquality sa2' (sing :: Sing a2)
+   Refl <- decideEquality sa1' (sing :: Sing a1)
    return x
 {-# INLINABLE fromSome3 #-}
 
 fromSome4
-   :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
+   :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
     . ( SingI a4, SDecide k4
       , SingI a3, SDecide k3
       , SingI a2, SDecide k2
@@ -243,10 +242,10 @@
    => Some4 f4
    -> Maybe (f4 a4 a3 a2 a1) -- ^
 fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do
-   Refl <- testEquality sa4' (sing :: Sing a4)
-   Refl <- testEquality sa3' (sing :: Sing a3)
-   Refl <- testEquality sa2' (sing :: Sing a2)
-   Refl <- testEquality sa1' (sing :: Sing a1)
+   Refl <- decideEquality sa4' (sing :: Sing a4)
+   Refl <- decideEquality sa3' (sing :: Sing a3)
+   Refl <- decideEquality sa2' (sing :: Sing a2)
+   Refl <- decideEquality sa1' (sing :: Sing a1)
    return x
 {-# INLINABLE fromSome4 #-}
 
@@ -254,7 +253,7 @@
 
 -- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'.
 _Some1
-  :: forall (f1 :: k1 -> Type) a1
+  :: forall k1 (f1 :: k1 -> Type) a1
   .  (SingI a1, SDecide k1)
   => Prism' (Some1 f1) (f1 a1)
 _Some1 = prism' some1 fromSome1
@@ -262,7 +261,7 @@
 
 -- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'.
 _Some2
-  :: forall (f2 :: k2 -> k1 -> Type) a2 a1
+  :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1
   .  ( SingI a2, SDecide k2
      , SingI a1, SDecide k1 )
   => Prism' (Some2 f2) (f2 a2 a1)
@@ -271,7 +270,7 @@
 
 -- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'.
 _Some3
-  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
+  :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
   .  ( SingI a3, SDecide k3
      , SingI a2, SDecide k2
      , SingI a1, SDecide k1 )
@@ -281,7 +280,7 @@
 
 -- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'.
 _Some4
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
+  :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
   .  ( SingI a4, SDecide k4
      , SingI a3, SDecide k3
      , SingI a2, SDecide k2
@@ -330,7 +329,8 @@
 -- Hint: @'same1' ('some1' . 'Exinst.P1') :: 'Some1' f -> 'Some1' g -> 'Some1' ('Exinst.P1' f g)@
 {-# INLINABLE same1 #-}
 same1
-  :: SDecide k1
+  :: forall k1 f g x
+  .  SDecide k1
   => (forall a1. SingI a1 => f a1 -> g a1 -> x)
   -> Some1 (f :: k1 -> Type)
   -> Some1 (g :: k1 -> Type)
@@ -338,7 +338,7 @@
 same1 z = \s1f s1g ->
   withSome1Sing s1f $ \sa1 f ->
     withSome1Sing s1g $ \sa1' g -> do
-       Refl <- testEquality sa1 sa1'
+       Refl <- decideEquality sa1 sa1'
        pure (z f g)
 
 -- | @'same2' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
@@ -347,7 +347,8 @@
 -- Hint: @'same2' ('some2' . 'Exinst.P2') :: 'Some2' f -> 'Some2' g -> 'Some2' ('Exinst.P2' f g)@
 {-# INLINABLE same2 #-}
 same2
-  :: (SDecide k2, SDecide k1)
+  :: forall k2 k1 f g x
+  .  (SDecide k2, SDecide k1)
   => (forall a2 a1. SingI a1 => f a2 a1 -> g a2 a1 -> x)
   -> Some2 (f :: k2 -> k1 -> Type)
   -> Some2 (g :: k2 -> k1 -> Type)
@@ -355,8 +356,8 @@
 same2 z = \s2l s2g ->
   withSome2Sing s2l $ \sa2 sa1 f ->
     withSome2Sing s2g $ \sa2' sa1' g -> do
-       Refl <- testEquality sa2 sa2'
-       Refl <- testEquality sa1 sa1'
+       Refl <- decideEquality sa2 sa2'
+       Refl <- decideEquality sa1 sa1'
        pure (z f g)
 
 -- | @'same3' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
@@ -365,7 +366,8 @@
 -- Hint: @'same3' ('some3' . 'Exinst.P3') :: 'Some3' f -> 'Some3' g -> 'Some3' ('Exinst.P3' f g)@
 {-# INLINABLE same3 #-}
 same3
-  :: (SDecide k3, SDecide k2, SDecide k1)
+  :: forall k3 k2 k1 f g x
+  .  (SDecide k3, SDecide k2, SDecide k1)
   => (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1)
         => f a3 a2 a1 -> g a3 a2 a1 -> x)
   -> Some3 (f :: k3 -> k2 -> k1 -> Type)
@@ -374,9 +376,9 @@
 same3 z = \s3l s3g ->
   withSome3Sing s3l $ \sa3 sa2 sa1 f ->
     withSome3Sing s3g $ \sa3' sa2' sa1' g -> do
-       Refl <- testEquality sa3 sa3'
-       Refl <- testEquality sa2 sa2'
-       Refl <- testEquality sa1 sa1'
+       Refl <- decideEquality sa3 sa3'
+       Refl <- decideEquality sa2 sa2'
+       Refl <- decideEquality sa1 sa1'
        pure (z f g)
 
 -- | @'same4' x a b@ applies @x@ to the contents of @a@ and @b@ if their type
@@ -385,7 +387,8 @@
 -- Hint: @'same4' ('some4' . 'Exinst.P4') :: 'Some4' f -> 'Some4' g -> 'Some4' ('Exinst.P4' f g)@
 {-# INLINABLE same4 #-}
 same4
-  :: (SDecide k4, SDecide k3, SDecide k2, SDecide k1)
+  :: forall k4 k3 k2 k1 f g x
+  .  (SDecide k4, SDecide k3, SDecide k2, SDecide k1)
   => (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1)
         => f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x)
   -> Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)
@@ -394,10 +397,10 @@
 same4 z = \s4l s4g ->
   withSome4Sing s4l $ \sa4 sa3 sa2 sa1 f ->
     withSome4Sing s4g $ \sa4' sa3' sa2' sa1' g -> do
-       Refl <- testEquality sa4 sa4'
-       Refl <- testEquality sa3 sa3'
-       Refl <- testEquality sa2 sa2'
-       Refl <- testEquality sa1 sa1'
+       Refl <- decideEquality sa4 sa4'
+       Refl <- decideEquality sa3 sa3'
+       Refl <- decideEquality sa2 sa2'
+       Refl <- decideEquality sa1 sa1'
        pure (z f g)
 
 --------------------------------------------------------------------------------