diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,6 @@
+## 0.4 [2018.01.09]
+* Require `singletons-2.4` and GHC 8.4.
+
 ## 0.3 [2017-11-07]
 * Migrate the old `elimNat` from `Data.Eliminator` (which worked over the `Nat`
   from `GHC.TypeNats`) to `Data.Eliminator.TypeNats`. There `elimNat` that now
diff --git a/eliminators.cabal b/eliminators.cabal
--- a/eliminators.cabal
+++ b/eliminators.cabal
@@ -1,5 +1,5 @@
 name:                eliminators
-version:             0.3
+version:             0.4
 synopsis:            Dependently typed elimination functions using singletons
 description:         This library provides eliminators for inductive data types,
                      leveraging the power of the @singletons@ library to allow
@@ -16,7 +16,7 @@
 build-type:          Simple
 extra-source-files:  CHANGELOG.md, README.md
 cabal-version:       >=1.10
-tested-with:         GHC == 8.2.1
+tested-with:         GHC == 8.4.1
 
 source-repository head
   type:                git
@@ -26,13 +26,13 @@
   exposed-modules:     Data.Eliminator
                        Data.Eliminator.TH
                        Data.Eliminator.TypeNats
-  build-depends:       base             >= 4.10    && < 4.11
+  build-depends:       base             >= 4.11    && < 4.12
                      , extra            >= 1.4.2   && < 1.7
-                     , singletons       >= 2.3     && < 2.4
+                     , singletons       >= 2.4     && < 2.5
                      , singleton-nats   >= 0.4.0.3 && < 0.5
-                     , template-haskell >= 2.12    && < 2.13
+                     , template-haskell >= 2.13    && < 2.14
                      , th-abstraction   >= 0.2.3   && < 0.3
-                     , th-desugar       >= 1.7     && < 1.8
+                     , th-desugar       >= 1.8     && < 1.9
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall -Wno-unticked-promoted-constructors
@@ -48,11 +48,12 @@
                        ListTypes
                        VecTypes
                        VecSpec
-  build-depends:       base           >= 4.10    && < 4.11
+  build-depends:       base           >= 4.11    && < 4.12
                      , eliminators
                      , hspec          >= 2       && < 3
-                     , singletons     >= 2.3     && < 2.4
+                     , singletons     >= 2.4     && < 2.5
                      , singleton-nats >= 0.4.0.3 && < 0.5
+  build-tool-depends:  hspec-discover:hspec-discover
   hs-source-dirs:      tests
   default-language:    Haskell2010
   ghc-options:         -Wall -Wno-unticked-promoted-constructors -threaded -rtsopts
diff --git a/src/Data/Eliminator/TH.hs b/src/Data/Eliminator/TH.hs
--- a/src/Data/Eliminator/TH.hs
+++ b/src/Data/Eliminator/TH.hs
@@ -346,14 +346,18 @@
   | nm == '(:)                                     = 'SCons
   | Just degree <- tupleNameDegree_maybe nm        = mkTupleDataName degree
   | Just degree <- unboxedTupleNameDegree_maybe nm = mkTupleDataName degree
-  | otherwise                                      = prefixUCName "S" ":%" nm
+  | otherwise                                      = prefixConName "S" "%" nm
 
 mkTupleDataName :: Int -> Name
 mkTupleDataName n = mkName $ "STuple" ++ (show n)
 
--- put an uppercase prefix on a name. Takes two prefixes: one for identifiers
--- and one for symbols
-prefixUCName :: String -> String -> Name -> Name
-prefixUCName pre tyPre n = case (nameBase n) of
-    (':' : rest) -> mkName (tyPre ++ rest)
+-- Put an uppercase prefix on a constructor name. Takes two prefixes:
+-- one for identifiers and one for symbols.
+--
+-- This is different from 'prefixName' in that infix constructor names always
+-- start with a colon, so we must insert the prefix after the colon in order
+-- for the new name to be syntactically valid.
+prefixConName :: String -> String -> Name -> Name
+prefixConName pre tyPre n = case (nameBase n) of
+    (':' : rest) -> mkName (':' : tyPre ++ rest)
     alpha -> mkName (pre ++ alpha)
diff --git a/tests/DecideSpec.hs b/tests/DecideSpec.hs
--- a/tests/DecideSpec.hs
+++ b/tests/DecideSpec.hs
@@ -39,8 +39,7 @@
       show (decEqNatList (SCons (sLit @0) SNil) SNil)                   `shouldBe` disproved
       show (decEqNatList SNil                   (SCons (sLit @0) SNil)) `shouldBe` disproved
       show (decEqNatList (SCons (sLit @0) SNil) (SCons (sLit @0) SNil)) `shouldBe` proved
-      -- TODO: Try this in the next version of singletons
-      -- show (decEqNatList (SCons (sLit @1) SNil) (SCons (sLit @0) SNil)) `shouldBe` disproved
+      show (decEqNatList (SCons (sLit @1) SNil) (SCons (sLit @0) SNil)) `shouldBe` disproved
 
 -----
 
@@ -86,14 +85,14 @@
   where
     left :: forall (x :: n :~: j).
             Sing x -> Decision (S n :~: S j)
-    left yes = Proved $ cong @Nat @Nat @(TyCon1 S) @n @j (fromSing yes)
+    left yes = Proved $ cong @Nat @Nat @(TyCon S) @n @j (fromSing yes)
 
     right :: forall (r :: (n :~: j) ~> Void).
              Sing r -> Decision (S n :~: S j)
     right no = Disproved $ fromSing no . sInjective @n @j sn
 
 decEqNat :: forall (n :: Nat) (j :: Nat). Sing n -> Sing j -> Decision (n :~: j)
-decEqNat sn = runWhyDecEqNat (elimNat @(TyCon1 WhyDecEqNat) @n sn base step)
+decEqNat sn = runWhyDecEqNat (elimNat @(TyCon WhyDecEqNat) @n sn base step)
   where
     base :: WhyDecEqNat Z
     base = WhyDecEqNat decEqZ
diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs
--- a/tests/DecideTypes.hs
+++ b/tests/DecideTypes.hs
@@ -9,18 +9,12 @@
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
--- TODO: Remove this in the next version of singletons
-{-# OPTIONS_GHC -Wno-orphans #-}
 module DecideTypes where
 
 import Data.Kind
 import Data.Nat
 import Data.Singletons.TH hiding (Decision(..))
 
--- TODO: Remove these in the next version of singletons
-$(genSingletons [''Void])
-$(genDefunSymbols [''(~>)])
-
 -- Due to https://github.com/goldfirere/singletons/issues/82, promoting the
 -- Decision data type from Data.Singletons.Decide is a tad awkward. To work
 -- around these, we define a more general Decision' data type here.
@@ -42,8 +36,8 @@
   showsPrec p (Disproved _) =
     showParen (p > 10) $ showString "Disproved <void>"
 
-type Decision  = Decision' (TyCon2 (->))
-type PDecision = Decision' (:~>$)
+type Decision  = Decision' (TyCon (->))
+type PDecision = Decision' (~>@#@$)
 
 data instance Sing (z :: PDecision a) where
   -- It would be lovely to not have to write those (:: PDecision a) kind
diff --git a/tests/ListSpec.hs b/tests/ListSpec.hs
--- a/tests/ListSpec.hs
+++ b/tests/ListSpec.hs
@@ -41,12 +41,12 @@
             Sing s -> Sing ss
          -> WhyMapPreservesLength f ss
          -> WhyMapPreservesLength f (s:ss)
-    step _ _ = cong @_ @_ @((:+$$) 1)
+    step _ _ = cong @_ @_ @((+@#@$$) 1)
 
 mapFusion :: forall (x :: Type) (y :: Type) (z :: Type)
                     (f :: y ~> z) (g :: x ~> y) (l :: [x]).
                     SingI l
-                 => Map f (Map g l) :~: Map (f :.$$$ g) l
+                 => Map f (Map g l) :~: Map (f .@#@$$$ g) l
 mapFusion
   = elimList @x @(WhyMapFusionSym2 f g) @l (sing @_ @l) base step
   where
@@ -57,4 +57,4 @@
             Sing s -> Sing ss
          -> WhyMapFusion f g ss
          -> WhyMapFusion f g (s:ss)
-    step _ _ = cong @_ @_ @((:$$) (f @@ (g @@ s)))
+    step _ _ = cong @_ @_ @((:@#@$$) (f @@ (g @@ s)))
diff --git a/tests/ListTypes.hs b/tests/ListTypes.hs
--- a/tests/ListTypes.hs
+++ b/tests/ListTypes.hs
@@ -15,5 +15,5 @@
 $(genDefunSymbols [''WhyMapPreservesLength])
 
 type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x])
-  = Map f (Map g l) :~: Map (f :.$$$ g) l
+  = Map f (Map g l) :~: Map (f .@#@$$$ g) l
 $(genDefunSymbols [''WhyMapFusion])
diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs
--- a/tests/VecSpec.hs
+++ b/tests/VecSpec.hs
@@ -6,7 +6,7 @@
 module VecSpec where
 
 import Data.Eliminator
-import Data.Kind
+import Data.Kind (Type)
 import Data.Nat
 import Data.Singletons
 import Data.Singletons.Prelude.Num
@@ -69,7 +69,7 @@
 
 replicateVec :: forall (e :: Type) (howMany :: Nat).
                 Sing howMany -> e -> Vec e howMany
-replicateVec s e = elimNat @(TyCon1 (Vec e)) @howMany s VNil step
+replicateVec s e = elimNat @(TyCon (Vec e)) @howMany s VNil step
   where
     step :: forall (k :: Nat). Sing k -> Vec e k -> Vec e (S k)
     step _ = (e :#)
@@ -102,7 +102,7 @@
 
 appendVec :: forall (e :: Type) (n :: Nat) (m :: Nat).
              SingI n
-          => Vec e n -> Vec e m -> Vec e (n :+ m)
+          => Vec e n -> Vec e m -> Vec e (n + m)
 appendVec = elimNat @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step
   where
     base :: WhyAppendVec e m Z
@@ -130,7 +130,7 @@
 
 concatVec :: forall (e :: Type) (n :: Nat) (j :: Nat).
              (SingKind e, SingI j, e ~ Demote e)
-          => Vec (Vec e j) n -> Vec e (n :* j)
+          => Vec (Vec e j) n -> Vec e (n * j)
 concatVec l = withSomeSing l $ \(singL :: Sing l) ->
                 elimVec @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step
   where
diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs
--- a/tests/VecTypes.hs
+++ b/tests/VecTypes.hs
@@ -11,7 +11,7 @@
 {-# LANGUAGE UndecidableInstances #-}
 module VecTypes where
 
-import Data.Kind
+import Data.Kind (Type)
 import Data.Nat
 import Data.Singletons.Prelude.Num
 import Data.Singletons.TH
@@ -65,7 +65,7 @@
 $(genDefunSymbols [''WhyZipWithVec])
 
 type WhyAppendVec (e :: Type) (m :: Nat) (n :: Nat)
-  = Vec e n -> Vec e m -> Vec e (n :+ m)
+  = Vec e n -> Vec e m -> Vec e (n + m)
 $(genDefunSymbols [''WhyAppendVec])
 
 type WhyTransposeVec (e :: Type) (m :: Nat) (n :: Nat)
@@ -73,7 +73,7 @@
 $(genDefunSymbols [''WhyTransposeVec])
 
 type WhyConcatVec (e :: Type) (j :: Nat) (n :: Nat) (l :: Vec (Vec e j) n)
-  = Vec e (n :* j)
+  = Vec e (n * j)
 data WhyConcatVecSym (e :: Type) (j :: Nat)
   :: forall (n :: Nat). Vec (Vec e j) n ~> Type
 type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l