diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs
index 87cbf8d..2b76131 100644
--- a/tests/EqualitySpec.hs
+++ b/tests/EqualitySpec.hs
@@ -33,6 +33,7 @@ spec = parallel $ do
 
 data instance Sing (z :: a :~: b) where
   SRefl :: Sing Refl
+type (%:~:) = (Sing :: (a :: k) :~: (b :: k) -> Type)
 
 instance SingKind (a :~: b) where
   type Demote (a :~: b) = a :~: b
@@ -50,6 +51,7 @@ instance SingI Refl where
 
 data instance Sing (z :: a :~~: b) where
   SHRefl :: Sing HRefl
+type (%:~~:) = (Sing :: (a :: j) :~~: (b :: k) -> Type)
 
 instance SingKind (a :~~: b) where
   type Demote (a :~~: b) = a :~~: b
diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs
index 8b70597..66efd8c 100644
--- a/tests/GADTSpec.hs
+++ b/tests/GADTSpec.hs
@@ -26,6 +26,7 @@ data So :: Bool -> Type where
 
 data instance Sing (z :: So what) where
   SOh :: Sing Oh
+type SSo = (Sing :: So what -> Type)
 
 elimSo :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker ~> Type).
           Sing s
@@ -40,6 +41,7 @@ data Flarble (a :: Type) (b :: Type) where
 data instance Sing (z :: Flarble a b) where
   SMkFlarble1 :: Sing x -> Sing (MkFlarble1 x)
   SMkFlarble2 :: Sing MkFlarble2
+type SFlarble = (Sing :: Flarble a b -> Type)
 
 elimFlarble :: forall (a :: Type) (b :: Type)
                       (p :: forall (x :: Type) (y :: Type). Flarble x y ~> Type)
@@ -60,6 +62,7 @@ data Obj :: Type where
 
 data instance Sing (z :: Obj) where
   SMkObj :: forall (obj :: obiwan). Sing obj -> Sing (MkObj obj)
+type SObj = (Sing :: Obj -> Type)
 
 elimObj :: forall (o :: Obj) (p :: Obj ~> Type).
            Sing o
diff --git a/tests/PeanoSpec.hs b/tests/PeanoSpec.hs
index ea05c63..84f674f 100644
--- a/tests/PeanoSpec.hs
+++ b/tests/PeanoSpec.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
 module PeanoSpec where
 
 import Data.Kind
@@ -89,7 +90,7 @@ zipWithVec f = elimPeano @n @(WhyZipWithVecSym3 a b c) (sing @_ @n) base step
 
 appendVec :: forall (e :: Type) (n :: Peano) (m :: Peano).
              SingI n
-          => Vec e n -> Vec e m -> Vec e (Plus n m)
+          => Vec e n -> Vec e m -> Vec e (n `Plus` m)
 appendVec = elimPeano @n @(WhyAppendVecSym2 e m) (sing @_ @n) base step
   where
     base :: WhyAppendVec e m Z
diff --git a/tests/PeanoTypes.hs b/tests/PeanoTypes.hs
index f6484bf..56e0b9b 100644
--- a/tests/PeanoTypes.hs
+++ b/tests/PeanoTypes.hs
@@ -17,10 +17,12 @@ import Data.Singletons.TH
 $(singletons [d|
   data Peano = Z | S Peano
 
+  infixl 6 `plus`
   plus :: Peano -> Peano -> Peano
   plus Z     m = m
   plus (S k) m = S (plus k m)
 
+  infixl 7 `times`
   times :: Peano -> Peano -> Peano
   times Z     _ = Z
   times (S k) m = plus m (times k m)
@@ -45,6 +47,7 @@ deriving instance Show a => Show (Vec a n)
 data instance Sing (z :: Vec a n) where
   SVNil :: Sing VNil
   (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs)
+type SVec = (Sing :: Vec a n -> Type)
 infixr 5 :%#
 
 instance SingKind a => SingKind (Vec a n) where
@@ -82,7 +85,7 @@ type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Peano)
 $(genDefunSymbols [''WhyZipWithVec])
 
 type WhyAppendVec (e :: Type) (m :: Peano) (n :: Peano)
-  = Vec e n -> Vec e m -> Vec e (Plus n m)
+  = Vec e n -> Vec e m -> Vec e (n `Plus` m)
 $(genDefunSymbols [''WhyAppendVec])
 
 type WhyTransposeVec (e :: Type) (m :: Peano) (n :: Peano)
@@ -90,7 +93,7 @@ type WhyTransposeVec (e :: Type) (m :: Peano) (n :: Peano)
 $(genDefunSymbols [''WhyTransposeVec])
 
 type WhyConcatVec (e :: Type) (j :: Peano) (n :: Peano) (l :: Vec (Vec e j) n)
-  = Vec e (Times n j)
+  = Vec e (n `Times` j)
 data WhyConcatVecSym (e :: Type) (j :: Peano)
   :: forall (n :: Peano). Vec (Vec e j) n ~> Type
 type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l
diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs
index 357514a..a651ecb 100644
--- a/tests/VecSpec.hs
+++ b/tests/VecSpec.hs
@@ -30,7 +30,7 @@ spec = parallel $ do
 
 concatVec :: forall (e :: Type) (n :: Peano) (j :: Peano).
              (SingKind e, SingI j, e ~ Demote e)
-          => Vec (Vec e j) n -> Vec e (Times n j)
+          => Vec (Vec e j) n -> Vec e (n `Times` j)
 concatVec l = withSomeSing l $ \(singL :: Sing l) ->
                 elimVec @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step
   where