diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,6 @@
+### 0.5.1 [2019.04.26]
+* Support `th-abstraction-0.3.0.0` or later.
+
 ## 0.5 [2018.09.18]
 * Require `singletons-2.5` and GHC 8.6.
 
diff --git a/eliminators.cabal b/eliminators.cabal
--- a/eliminators.cabal
+++ b/eliminators.cabal
@@ -1,5 +1,5 @@
 name:                eliminators
-version:             0.5
+version:             0.5.1
 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.6.1
+tested-with:         GHC == 8.6.4
 
 source-repository head
   type:                git
@@ -26,16 +26,16 @@
   exposed-modules:     Data.Eliminator
                        Data.Eliminator.TH
                        Data.Eliminator.TypeNats
-  build-depends:       base             >= 4.12  && < 4.13
-                     , extra            >= 1.4.2 && < 1.7
-                     , singletons       >= 2.5   && < 2.6
-                     , singleton-nats   >= 0.4.2 && < 0.5
-                     , template-haskell >= 2.14  && < 2.15
-                     , th-abstraction   >= 0.2.3 && < 0.3
-                     , th-desugar       >= 1.9   && < 1.10
+  build-depends:       base             >= 4.12   && < 4.13
+                     , extra            >= 1.4.2  && < 1.7
+                     , singletons       >= 2.5    && < 2.6
+                     , singleton-nats   >= 0.4.2  && < 0.5
+                     , template-haskell >= 2.14   && < 2.15
+                     , th-abstraction   >= 0.2.11 && < 0.4
+                     , th-desugar       >= 1.9    && < 1.10
   hs-source-dirs:      src
   default-language:    Haskell2010
-  ghc-options:         -Wall -Wno-unticked-promoted-constructors
+  ghc-options:         -Wall -Wcompat -Wno-unticked-promoted-constructors
 
 test-suite spec
   type:                exitcode-stdio-1.0
@@ -45,6 +45,7 @@
                        EqualitySpec
                        EqualityTypes
                        GADTSpec
+                       Internal
                        ListSpec
                        ListTypes
                        VecTypes
@@ -57,4 +58,4 @@
   build-tool-depends:  hspec-discover:hspec-discover
   hs-source-dirs:      tests
   default-language:    Haskell2010
-  ghc-options:         -Wall -Wno-unticked-promoted-constructors -threaded -rtsopts
+  ghc-options:         -Wall -Wcompat -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
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE Unsafe #-}
 {-|
@@ -29,7 +30,7 @@
 
 import           Language.Haskell.TH
 import           Language.Haskell.TH.Datatype
-import           Language.Haskell.TH.Desugar (tupleNameDegree_maybe, unboxedTupleNameDegree_maybe)
+import           Language.Haskell.TH.Desugar hiding (NewOrData(..))
 
 {- $conventions
 'deriveElim' and 'deriveElimNamed' provide a way to automate the creation of
@@ -149,7 +150,12 @@
 -- function named @funName@ for the datatype @dataName@.
 deriveElimNamed :: String -> Name -> Q [Dec]
 deriveElimNamed funName dataName = do
-  info@(DatatypeInfo { datatypeVars    = vars
+  info@(DatatypeInfo { datatypeVars    =
+#if MIN_VERSION_th_abstraction(0,3,0)
+                                         dataVarBndrs
+#else
+                                         dataVars
+#endif
                      , datatypeVariant = variant
                      , datatypeCons    = cons
                      }) <- reifyDatatype dataName
@@ -163,7 +169,9 @@
   predVar <- newName "p"
   singVar <- newName "s"
   let elimN = mkName funName
-      dataVarBndrs = catMaybes $ map typeToTyVarBndr vars
+#if !(MIN_VERSION_th_abstraction(0,3,0))
+      dataVarBndrs = freeVariablesWellScoped dataVars
+#endif
       promDataKind = datatypeType info
       predVarBndr = KindedTV predVar (InfixT promDataKind ''(~>) (ConT ''Kind.Type))
       singVarBndr = KindedTV singVar promDataKind
@@ -283,10 +291,6 @@
   = "~>" ++ nStr
   where
     nStr = nameBase n
-
-typeToTyVarBndr :: Type -> Maybe TyVarBndr
-typeToTyVarBndr (SigT (VarT n) k) = Just $ KindedTV n k
-typeToTyVarBndr _                 = Nothing
 
 -- Reconstruct and arrow type from the list of types
 ravel :: [Type] -> Type -> Type
diff --git a/tests/DecideSpec.hs b/tests/DecideSpec.hs
--- a/tests/DecideSpec.hs
+++ b/tests/DecideSpec.hs
@@ -114,7 +114,7 @@
                  -> Decision (S k :~: S m)
         stepStep sm _ = decCongS sk (runWhyDecEqNat swhyK sm)
 
-listEqConsequencesSame :: forall (es :: [e]). Sing es -> ListEqConsequences es es
+listEqConsequencesSame :: forall e (es :: [e]). Sing es -> ListEqConsequences es es
 listEqConsequencesSame sl = elimList @e @WhyListEqConsequencesSameSym0 @es sl base step
   where
     base :: ListEqConsequences '[] '[]
@@ -126,24 +126,24 @@
          -> ListEqConsequences (x:xs) (x:xs)
     step _ _ _ = (Refl, Refl)
 
-useListEq :: forall (xs :: [e]) (ys :: [e]).
+useListEq :: forall e (xs :: [e]) (ys :: [e]).
              Sing xs -> xs :~: ys -> ListEqConsequences xs ys
 useListEq sxs xsEqYs = replace @[e] @xs @ys @(ListEqConsequencesSym1 xs)
                                (listEqConsequencesSame @e @xs sxs) xsEqYs
 
-nilNotCons :: forall (x :: e) (xs :: [e]). '[] :~: (x:xs) -> Void
+nilNotCons :: forall e (x :: e) (xs :: [e]). '[] :~: (x:xs) -> Void
 nilNotCons = useListEq @e @'[] @(x:xs) SNil
 
-consNotNil :: forall (x :: e) (xs :: [e]). (x:xs) :~: '[] -> Void
+consNotNil :: forall e (x :: e) (xs :: [e]). (x:xs) :~: '[] -> Void
 consNotNil eq = nilNotCons @e @x @xs (sym eq)
 
-consInjective :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
+consInjective :: forall e (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
                  Sing x -> Sing xs
               -> (x:xs) :~: (y:ys)
               -> (x :~: y, xs :~: ys)
 consInjective sx sxs = useListEq @e @(x:xs) @(y:ys) (SCons sx sxs)
 
-decEqNil :: forall (es :: [e]). Sing es -> Decision ('[] :~: es)
+decEqNil :: forall e (es :: [e]). Sing es -> Decision ('[] :~: es)
 decEqNil ses = elimList @e @WhyDecEqNilSym0 @es ses base step
   where
     base :: Decision ('[] :~: '[])
@@ -155,7 +155,7 @@
          -> Decision ('[] :~: (x:xs))
     step _ _ _ = Disproved (nilNotCons @e @x @xs)
 
-intermixListEqs :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
+intermixListEqs :: forall e (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
                    x :~: y -> xs :~: ys
                 -> (x:xs) :~: (y:ys)
 intermixListEqs xEqY xsEqYs =
@@ -163,7 +163,7 @@
           (replace @[e] @xs @ys @(WhyIntermixListEqs2Sym2 x xs) Refl xsEqYs)
           xEqY
 
-decCongCons :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
+decCongCons :: forall e (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).
                Sing x -> Sing xs
             -> Decision (x :~: y) -> Decision (xs :~: ys)
             -> Decision ((x:xs) :~: (y:ys))
@@ -193,7 +193,7 @@
     injective :: (x:xs) :~: (y:ys) -> (x :~: y, xs :~: ys)
     injective = consInjective @e @x @xs @y @ys sx sxs
 
-decEqList :: forall (es1 :: [e]) (es2 :: [e]).
+decEqList :: forall e (es1 :: [e]) (es2 :: [e]).
              (forall (e1 :: e) (e2 :: e).
                      Sing e1 -> Sing e2 -> Decision (e1 :~: e2))
           -> Sing es1 -> Sing es2 -> Decision (es1 :~: es2)
diff --git a/tests/DecideTypes.hs b/tests/DecideTypes.hs
--- a/tests/DecideTypes.hs
+++ b/tests/DecideTypes.hs
@@ -23,10 +23,10 @@
   = Proved a
   | Disproved (p @@ a @@ Void)
 
-elimDecision :: forall (a :: Type) (p :: PDecision a ~> Type) (d :: PDecision a).
+elimDecision :: forall a (p :: PDecision a ~> Type) (d :: PDecision a).
                 Sing d
-             -> (forall (yes :: a). Sing yes -> p @@ (Proved yes))
-             -> (forall (no :: a ~> Void). Sing no -> p @@ (Disproved no))
+             -> (forall (yes :: a). Sing yes -> p @@ Proved yes)
+             -> (forall (no :: a ~> Void). Sing no -> p @@ Disproved no)
              -> p @@ d
 elimDecision (SProved yes)   pProved _          = pProved yes
 elimDecision (SDisproved no) _       pDisproved = pDisproved no
@@ -40,12 +40,12 @@
 type Decision  = Decision' (TyCon (->))
 type PDecision = Decision' (~>@#@$)
 
-data instance Sing (z :: PDecision a) where
+data instance Sing :: forall a. PDecision a -> Type where
   -- It would be lovely to not have to write those (:: PDecision a) kind
   -- ascriptions in the return types of each constructor.
   -- See https://ghc.haskell.org/trac/ghc/ticket/14111.
-  SProved    :: forall (x :: a).         Sing x -> Sing (Proved x    :: PDecision a)
-  SDisproved :: forall (r :: a ~> Void). Sing r -> Sing (Disproved r :: PDecision a)
+  SProved    :: forall a (x :: a).         Sing x -> Sing (Proved x    :: PDecision a)
+  SDisproved :: forall a (r :: a ~> Void). Sing r -> Sing (Disproved r :: PDecision a)
 
 instance SingKind a => SingKind (PDecision a) where
   type Demote (PDecision a) = Decision (Demote a)
@@ -54,46 +54,41 @@
   toSing (Proved x)    = withSomeSing x $ SomeSing . SProved
   toSing (Disproved r) = withSomeSing r $ SomeSing . SDisproved
 
-type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where
-  NatEqConsequences Z      Z      = ()
-  NatEqConsequences Z      (S _)  = Void
-  NatEqConsequences (S _)  Z      = Void
-  NatEqConsequences (S k1) (S k2) = k1 :~: k2
-$(genDefunSymbols [''NatEqConsequences])
+$(singletons [d|
+  type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where
+    NatEqConsequences Z      Z      = ()
+    NatEqConsequences Z      (S _)  = Void
+    NatEqConsequences (S _)  Z      = Void
+    NatEqConsequences (S k1) (S k2) = k1 :~: k2
 
-type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a
-$(genDefunSymbols [''WhyNatEqConsequencesSame])
+  type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a
 
-type WhyDecEqZ (k :: Nat) = Decision (Z :~: k)
-$(genDefunSymbols [''WhyDecEqZ])
+  type WhyDecEqZ (k :: Nat) = Decision (Z :~: k)
 
-type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k)
-$(genDefunSymbols [''WhyDecEqS])
+  type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k)
+  |])
 
 -- The newtype wrapper is needed to work around
 -- https://github.com/goldfirere/singletons/issues/198
 newtype WhyDecEqNat (k :: Nat) = WhyDecEqNat
   { runWhyDecEqNat :: forall (j :: Nat). Sing j -> Decision (k :~: j) }
 
-type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where
-  ListEqConsequences '[]    '[]    = ()
-  ListEqConsequences '[]    (_:_)  = Void
-  ListEqConsequences (_:_)  '[]    = Void
-  ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys)
-$(genDefunSymbols [''ListEqConsequences])
+$(singletons [d|
+  type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where
+    ListEqConsequences '[]    '[]    = ()
+    ListEqConsequences '[]    (_:_)  = Void
+    ListEqConsequences (_:_)  '[]    = Void
+    ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys)
 
-type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es
-$(genDefunSymbols [''WhyListEqConsequencesSame])
+  type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es
 
-type WhyDecEqNil (es :: [e]) = Decision ('[] :~: es)
-$(genDefunSymbols [''WhyDecEqNil])
+  type WhyDecEqNil (es :: [e]) = Decision ('[] :~: es)
 
-type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es)
-$(genDefunSymbols [''WhyDecEqCons])
+  type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es)
 
-type WhyIntermixListEqs1 (x :: e) (xs :: [e]) (ys :: [e]) (k :: e) = (x:xs) :~: (k:ys)
-type WhyIntermixListEqs2 (x :: e) (xs :: [e]) (k :: [e])           = (x:xs) :~: (x:k)
-$(genDefunSymbols [''WhyIntermixListEqs1, ''WhyIntermixListEqs2])
+  type WhyIntermixListEqs1 (x :: e) (xs :: [e]) (ys :: [e]) (k :: e) = (x:xs) :~: (k:ys)
+  type WhyIntermixListEqs2 (x :: e) (xs :: [e]) (k :: [e])           = (x:xs) :~: (x:k)
+  |])
 
 -- The newtype wrapper is needed to work around
 -- https://github.com/goldfirere/singletons/issues/198
diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs
--- a/tests/EqualitySpec.hs
+++ b/tests/EqualitySpec.hs
@@ -16,6 +16,7 @@
 import           Data.Type.Equality ((:~:)(..), (:~~:)(..))
 
 import           EqualityTypes
+import           Internal
 
 import           Test.Hspec
 
@@ -33,23 +34,37 @@
 
 -----
 
-j :: forall (k :: Type) (a :: k) (b :: k)
-            (p :: forall (x :: k) (y :: k). x :~: y ~> Type)
+j :: forall k (p :: forall (x :: k) (y :: k). x :~: y ~> Type)
+            (a :: k) (b :: k)
             (r :: a :~: b).
      Sing r
   -> (forall (x :: k). p @@ (Refl :: x :~: x))
   -> p @@ r
 j SRefl pRefl = pRefl @a
 
-hj :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
-             (p :: forall (y :: Type) (z :: Type) (w :: y) (x :: z). w :~~: x ~> Type)
+jProp :: forall k (p :: k ~> k ~> Prop)
+                (a :: k) (b :: k).
+         a :~: b
+      -> (forall (x :: k). p @@ x @@ x)
+      -> p @@ a @@ b
+jProp Refl pRefl = pRefl @a
+
+hj :: forall (p :: forall y z (w :: y) (x :: z). w :~~: x ~> Type)
+             j k (a :: j) (b :: k)
              (r :: a :~~: b).
       Sing r
-   -> (forall (y :: Type) (w :: y). p @@ (HRefl :: w :~~: w))
+   -> (forall y (w :: y). p @@ (HRefl :: w :~~: w))
    -> p @@ r
-hj SHRefl pHRefl = pHRefl @k @a
+hj SHRefl pHRefl = pHRefl @j @a
 
-k :: forall (k :: Type) (a :: k)
+hjProp :: forall (p :: forall y z. y ~> z ~> Prop)
+                 j k (a :: j) (b :: k).
+          a :~~: b
+       -> (forall y (w :: y). p @@ w @@ w)
+       -> p @@ a @@ b
+hjProp HRefl pHRefl = pHRefl @j @a
+
+k :: forall k (a :: k)
             (p :: a :~: a ~> Type)
             (r :: a :~: a).
      Sing r
@@ -57,7 +72,7 @@
   -> p @@ r
 k SRefl pRefl = pRefl
 
-hk :: forall (k :: Type) (a :: k)
+hk :: forall k (a :: k)
              (p :: a :~~: a ~> Type)
              (r :: a :~~: a).
       Sing r
@@ -65,64 +80,64 @@
    -> p @@ r
 hk SHRefl pHRefl = pHRefl
 
-sym :: forall (t :: Type) (a :: t) (b :: t).
+sym :: forall t (a :: t) (b :: t).
        a :~: b -> b :~: a
 sym eq = withSomeSing eq $ \(singEq :: Sing r) ->
-           (~>:~:) @t @a @b @(WhySymSym1 a) @r singEq Refl
+           (~>:~:) @t @a @(WhySymSym1 a) @b @r singEq Refl
 
-hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
+hsym :: forall j k (a :: j) (b :: k).
         a :~~: b -> b :~~: a
 hsym eq = withSomeSing eq $ \(singEq :: Sing r) ->
-            (~>:~~:) @j @k @a @b @(WhyHsymSym1 a) @r singEq HRefl
+            (~>:~~:) @j @a @(WhyHsymSym1 a) @k @b @r singEq HRefl
 
-symIdempotent :: forall (t :: Type) (a :: t) (b :: t)
+symIdempotent :: forall t (a :: t) (b :: t)
                         (e :: a :~: b).
                  Sing e -> Symmetry (Symmetry e) :~: e
-symIdempotent se = (~>:~:) @t @a @b @(WhySymIdempotentSym1 a) @e se Refl
+symIdempotent se = (~>:~:) @t @a @(WhySymIdempotentSym1 a) @b @e se Refl
 
-hsymIdempotent :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
+hsymIdempotent :: forall j k (a :: j) (b :: k)
                          (e :: a :~~: b).
                   Sing e -> Hsymmetry (Hsymmetry e) :~: e
-hsymIdempotent se = (~>:~~:) @j @k @a @b @(WhyHsymIdempotentSym1 a) @e se Refl
+hsymIdempotent se = (~>:~~:) @j @a @(WhyHsymIdempotentSym1 a) @k @b @e se Refl
 
-replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
+replace :: forall t (from :: t) (to :: t) (p :: t ~> Type).
            p @@ from
         -> from :~: to
         -> p @@ to
 replace from eq =
   withSomeSing eq $ \(singEq :: Sing r) ->
-    (~>:~:) @t @from @to @(WhyReplaceSym2 from p) @r singEq from
+    (~>:~:) @t @from @(WhyReplaceSym2 from p) @to @r singEq from
 
 -- Doesn't work due to https://ghc.haskell.org/trac/ghc/ticket/11719
 {-
-hreplace :: forall (j :: Type) (k :: Type) (from :: j) (to :: k)
-                   (p :: forall (z :: Type). z ~> Type).
+hreplace :: forall j k (from :: j) (to :: k)
+                   (p :: forall z. z ~> Type).
             p @@ from
          -> from :~~: to
          -> p @@ to
 hreplace from heq =
-  withSomeSing eq $ \(singEq :: Sing r) ->
-    (@~>:~~:) @j @k @from @to @(WhyHreplaceSym2 from p) singEq from
+  withSomeSing heq $ \(singEq :: Sing r) ->
+    (~>:~~:) @j @from @(WhyHreplaceSym2 from p) @k @to @r singEq from
 -}
 
-leibniz :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
+leibniz :: forall t (f :: t ~> Type) (a :: t) (b :: t).
            a :~: b
         -> f @@ a
         -> f @@ b
 leibniz = replace @t @a @b @(WhyLeibnizSym2 f a) id
 
-cong :: forall (x :: Type) (y :: Type) (f :: x ~> y)
+cong :: forall x y (f :: x ~> y)
                (a :: x) (b :: x).
         a :~: b
      -> f @@ a :~: f @@ b
 cong eq =
   withSomeSing eq $ \(singEq :: Sing r) ->
-    (~>:~:) @x @a @b @(WhyCongSym2 f a) @r singEq Refl
+    (~>:~:) @x @a @(WhyCongSym2 f a) @b @r singEq Refl
 
-eqIsRefl :: forall (k :: Type) (a :: k) (b :: k) (e :: a :~: b).
+eqIsRefl :: forall k (a :: k) (b :: k) (e :: a :~: b).
             Sing e -> e :~~: (Refl :: a :~: a)
-eqIsRefl eq = (~>:~:) @k @a @b @(WhyEqIsReflSym1 a) @e eq HRefl
+eqIsRefl eq = (~>:~:) @k @a @(WhyEqIsReflSym1 a) @b @e eq HRefl
 
-heqIsHRefl :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (e :: a :~~: b).
+heqIsHRefl :: forall j k (a :: j) (b :: k) (e :: a :~~: b).
               Sing e -> e :~~: (HRefl :: a :~~: a)
-heqIsHRefl heq = (~>:~~:) @j @k @a @b @(WhyHEqIsHReflSym1 a) @e heq HRefl
+heqIsHRefl heq = (~>:~~:) @j @a @(WhyHEqIsHReflSym1 a) @k @b @e heq HRefl
diff --git a/tests/EqualityTypes.hs b/tests/EqualityTypes.hs
--- a/tests/EqualityTypes.hs
+++ b/tests/EqualityTypes.hs
@@ -16,7 +16,9 @@
 import           Data.Singletons.TH
 import           Data.Type.Equality ((:~:)(..), (:~~:)(..))
 
-data instance Sing (z :: a :~: b) where
+import           Internal
+
+data instance Sing :: forall k (a :: k) (b :: k). a :~: b -> Type where
   SRefl :: Sing Refl
 type (%:~:) = (Sing :: (a :: k) :~: (b :: k) -> Type)
 
@@ -29,15 +31,23 @@
   sing = SRefl
 
 -- | Christine Paulin-Mohring's version of the J rule.
-(~>:~:) :: forall (k :: Type) (a :: k) (b :: k)
+(~>:~:) :: forall k (a :: k)
                   (p :: forall (y :: k). a :~: y ~> Type)
-                  (r :: a :~: b).
+                  (b :: k) (r :: a :~: b).
            Sing r
         -> p @@ Refl
         -> p @@ r
 (~>:~:) SRefl pRefl = pRefl
 
-data instance Sing (z :: a :~~: b) where
+(~>!:~:) :: forall k (a :: k)
+                   (p :: k ~> Prop)
+                   (b :: k).
+            a :~: b
+         -> p @@ a
+         -> p @@ b
+(~>!:~:) Refl pRefl = pRefl
+
+data instance Sing :: forall j k (a :: j) (b :: k). a :~~: b -> Type where
   SHRefl :: Sing HRefl
 type (%:~~:) = (Sing :: (a :: j) :~~: (b :: k) -> Type)
 
@@ -50,14 +60,22 @@
   sing = SHRefl
 
 -- | Christine Paulin-Mohring's version of the J rule, but heterogeneously kinded.
-(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
-                   (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type)
-                   (r :: a :~~: b).
+(~>:~~:) :: forall j (a :: j)
+                   (p :: forall z (y :: z). a :~~: y ~> Type)
+                   k (b :: k) (r :: a :~~: b).
             Sing r
          -> p @@ HRefl
          -> p @@ r
 (~>:~~:) SHRefl pHRefl = pHRefl
 
+(~>!:~~:) :: forall j (a :: j)
+                    (p :: forall z. z ~> Prop)
+                    k (b :: k).
+             a :~~: b
+          -> p @@ a
+          -> p @@ b
+(~>!:~~:) HRefl pHRefl = pHRefl
+
 -----
 
 $(singletons [d|
@@ -85,7 +103,7 @@
 
   -- Doesn't work due to https://ghc.haskell.org/trac/ghc/ticket/11719
   {-
-  type family WhyHreplace (from :: j) (p :: forall (z :: Type). z ~> Type)
+  type family WhyHreplace (from :: j) (p :: forall z. z ~> Type)
                           (e :: from :~~: (y :: k)) :: Type where
     WhyHreplace from p (_ :: from :~~: y) = p @@ y
   -}
diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs
--- a/tests/GADTSpec.hs
+++ b/tests/GADTSpec.hs
@@ -12,6 +12,8 @@
 import Data.Kind
 import Data.Singletons
 
+import Internal
+
 import Test.Hspec
 
 main :: IO ()
@@ -25,31 +27,37 @@
 data So :: Bool -> Type where
   Oh :: So True
 
-data instance Sing (z :: So what) where
+data instance Sing :: forall (what :: Bool). So what -> Type 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).
+elimSo :: forall (p :: forall (long_sucker :: Bool). So long_sucker ~> Type)
+                 (what :: Bool) (s :: So what).
           Sing s
        -> p @@ Oh
        -> p @@ s
 elimSo SOh pOh = pOh
 
-data Flarble (a :: Type) (b :: Type) where
+elimPropSo :: forall (p :: Bool ~> Prop) (what :: Bool).
+              So what
+           -> p @@ True
+           -> p @@ what
+elimPropSo Oh pOh = pOh
+
+data Flarble :: Type -> Type -> Type where
   MkFlarble1 :: a -> Flarble a b
   MkFlarble2 :: a ~ Bool => Flarble a (Maybe b)
 
-data instance Sing (z :: Flarble a b) where
+data instance Sing :: forall a b. Flarble a b -> Type 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)
-                      (f :: Flarble a b).
+elimFlarble :: forall (p :: forall x y. Flarble x y ~> Type)
+                      a b (f :: Flarble a b).
                Sing f
-            -> (forall (a' :: Type) (b' :: Type) (x :: a'). Sing x -> p @@ (MkFlarble1 x :: Flarble a' b'))
-            -> (forall (b' :: Type). p @@ (MkFlarble2 :: Flarble Bool (Maybe b')))
+            -> (forall a' b' (x :: a'). Sing x -> p @@ (MkFlarble1 x :: Flarble a' b'))
+            -> (forall b'. p @@ (MkFlarble2 :: Flarble Bool (Maybe b')))
             -> p @@ f
 elimFlarble s@(SMkFlarble1 sx) pMkFlarble1 _ =
   case s of
@@ -58,15 +66,33 @@
   case s of
     (_ :: Sing (MkFlarble2 :: Flarble Bool (Maybe b'))) -> pMkFlarble2 @b'
 
+elimPropFlarble :: forall (p :: Type ~> Type ~> Prop) a b.
+                   Flarble a b
+                -> (forall a' b'. a -> p @@ a' @@ b')
+                -> (forall b'. p @@ Bool @@ Maybe b')
+                -> p @@ a @@ b
+elimPropFlarble f@(MkFlarble1 x) pMkFlarble1 _ =
+  case f of
+    (_ :: Flarble a' b') -> pMkFlarble1 @a' @b' x
+elimPropFlarble f@MkFlarble2 _ pMkFlarble2 =
+  case f of
+    (_ :: Flarble Bool (Maybe b')) -> pMkFlarble2 @b'
+
 data Obj :: Type where
   MkObj :: o -> Obj
 
-data instance Sing (z :: Obj) where
-  SMkObj :: forall (obj :: obiwan). Sing obj -> Sing (MkObj obj)
+data instance Sing :: Obj -> Type where
+  SMkObj :: forall obiwan (obj :: obiwan). Sing obj -> Sing (MkObj obj)
 type SObj = (Sing :: Obj -> Type)
 
-elimObj :: forall (o :: Obj) (p :: Obj ~> Type).
+elimObj :: forall (p :: Obj ~> Type) (o :: Obj).
            Sing o
-        -> (forall (obj :: Type) (x :: obj). Sing x -> p @@ (MkObj x))
+        -> (forall obj (x :: obj). Sing x -> p @@ MkObj x)
         -> p @@ o
-elimObj (SMkObj (x :: Sing (obj :: obiwan))) pMkObj = pMkObj @obiwan @obj x
+elimObj (SMkObj (sx :: Sing (x :: obj))) pMkObj = pMkObj @obj @x sx
+
+elimPropObj :: forall (p :: Prop).
+               Obj
+            -> (forall obj. obj -> p)
+            -> p
+elimPropObj (MkObj o) pMkObj = pMkObj o
diff --git a/tests/Internal.hs b/tests/Internal.hs
new file mode 100644
--- /dev/null
+++ b/tests/Internal.hs
@@ -0,0 +1,5 @@
+module Internal where
+
+import Data.Kind
+
+type Prop = Type
diff --git a/tests/ListSpec.hs b/tests/ListSpec.hs
--- a/tests/ListSpec.hs
+++ b/tests/ListSpec.hs
@@ -10,7 +10,6 @@
 module ListSpec where
 
 import Data.Eliminator
-import Data.Kind
 import Data.Singletons.Prelude
 import Data.Singletons.Prelude.List
 import Data.Type.Equality
@@ -29,7 +28,7 @@
 
 -----
 
-mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).
+mapPreservesLength :: forall x y (f :: x ~> y) (l :: [x]).
                       SingI l
                    => Length l :~: Length (Map f l)
 mapPreservesLength
@@ -44,7 +43,7 @@
          -> WhyMapPreservesLength f (s:ss)
     step _ _ = cong @_ @_ @((+@#@$$) 1)
 
-mapFusion :: forall (x :: Type) (y :: Type) (z :: Type)
+mapFusion :: forall x y z
                     (f :: y ~> z) (g :: x ~> y) (l :: [x]).
                     SingI l
                  => Map f (Map g l) :~: Map (f .@#@$$$ g) l
diff --git a/tests/ListTypes.hs b/tests/ListTypes.hs
--- a/tests/ListTypes.hs
+++ b/tests/ListTypes.hs
@@ -11,10 +11,10 @@
 import Data.Singletons.Prelude.List
 import Data.Singletons.TH
 
-type WhyMapPreservesLength (f :: x ~> y) (l :: [x])
-  = Length l :~: Length (Map f l)
-$(genDefunSymbols [''WhyMapPreservesLength])
+$(singletons [d|
+  type WhyMapPreservesLength (f :: x ~> y) (l :: [x])
+    = Length l :~: Length (Map f l)
 
-type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x])
-  = Map f (Map g l) :~: Map (f .@#@$$$ g) l
-$(genDefunSymbols [''WhyMapFusion])
+  type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x])
+    = Map f (Map g l) :~: Map (f .@#@$$$ g) l
+  |])
diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs
--- a/tests/VecSpec.hs
+++ b/tests/VecSpec.hs
@@ -8,7 +8,6 @@
 module VecSpec where
 
 import Data.Eliminator
-import Data.Kind (Type)
 import Data.Nat
 import Data.Singletons
 import Data.Singletons.Prelude.Num
@@ -69,14 +68,14 @@
 
 -----
 
-replicateVec :: forall (e :: Type) (howMany :: Nat).
+replicateVec :: forall e (howMany :: Nat).
                 Sing howMany -> e -> Vec e howMany
 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 :#)
 
-mapVec :: forall (a :: Type) (b :: Type) (n :: Nat).
+mapVec :: forall a b (n :: Nat).
           SingI n
        => (a -> b) -> Vec a n -> Vec b n
 mapVec f = elimNat @(WhyMapVecSym2 a b) @n (sing @n) base step
@@ -87,7 +86,7 @@
     step :: forall (k :: Nat). Sing k -> WhyMapVec a b k -> WhyMapVec a b (S k)
     step _ mapK vK = f (vhead vK) :# mapK (vtail vK)
 
-zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Nat).
+zipWithVec :: forall a b c (n :: Nat).
               SingI n
            => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n
 zipWithVec f = elimNat @(WhyZipWithVecSym3 a b c) @n (sing @n) base step
@@ -102,7 +101,7 @@
     step _ zwK vaK vbK = f   (vhead vaK) (vhead vbK)
                       :# zwK (vtail vaK) (vtail vbK)
 
-appendVec :: forall (e :: Type) (n :: Nat) (m :: Nat).
+appendVec :: forall e (n :: Nat) (m :: Nat).
              SingI n
           => Vec e n -> Vec e m -> Vec e (n + m)
 appendVec = elimNat @(WhyAppendVecSym2 e m) @n (sing @n) base step
@@ -116,7 +115,7 @@
          -> WhyAppendVec e m (S k)
     step _ avK vK1 vK2 = vhead vK1 :# avK (vtail vK1) vK2
 
-transposeVec :: forall (e :: Type) (n :: Nat) (m :: Nat).
+transposeVec :: forall e (n :: Nat) (m :: Nat).
                 (SingI n, SingI m)
              => Vec (Vec e m) n -> Vec (Vec e n) m
 transposeVec = elimNat @(WhyTransposeVecSym2 e m) @n (sing @n) base step
@@ -130,17 +129,17 @@
          -> WhyTransposeVec e m (S k)
     step _ transK vK = zipWithVec (:#) (vhead vK) (transK (vtail vK))
 
-concatVec :: forall (e :: Type) (n :: Nat) (j :: Nat).
+concatVec :: forall e (n :: Nat) (j :: Nat).
              (SingKind e, SingI j, e ~ Demote e)
           => 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
+                elimVec @(Vec e j) @(WhyConcatVecSym2 e j) @n @l singL base step
   where
-    base :: WhyConcatVec e j Z VNil
+    base :: WhyConcatVec e j VNil
     base = VNil
 
     step :: forall (k :: Nat) (x :: Vec e j) (xs :: Vec (Vec e j) k).
                    Sing x -> Sing xs
-                -> WhyConcatVec e j k     xs
-                -> WhyConcatVec e j (S k) (x :# xs)
+                -> WhyConcatVec e j xs
+                -> WhyConcatVec e j (x :# xs)
     step h _ vKJ = appendVec (fromSing h) vKJ
diff --git a/tests/VecTypes.hs b/tests/VecTypes.hs
--- a/tests/VecTypes.hs
+++ b/tests/VecTypes.hs
@@ -17,6 +17,7 @@
 import Data.Nat
 import Data.Singletons.Prelude.Num
 import Data.Singletons.TH
+import Internal
 
 data Vec :: Type -> Nat -> Type where
   VNil :: Vec a Z
@@ -26,7 +27,7 @@
 deriving instance Ord a  => Ord (Vec a n)
 deriving instance Show a => Show (Vec a n)
 
-data instance Sing (z :: Vec a n) where
+data instance Sing :: forall a (n :: Nat). Vec a n -> Type where
   SVNil :: Sing VNil
   (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs)
 type SVec = (Sing :: Vec a n -> Type)
@@ -48,8 +49,8 @@
 instance (SingI x, SingI xs) => SingI (x :# xs) where
   sing = sing :%# sing
 
-elimVec :: forall (a :: Type) (n :: Nat)
-                  (p :: forall (k :: Nat). Vec a k ~> Type) (v :: Vec a n).
+elimVec :: forall a (p :: forall (k :: Nat). Vec a k ~> Type)
+                  (n :: Nat) (v :: Vec a n).
            Sing v
         -> p @@ VNil
         -> (forall (k :: Nat) (x :: a) (xs :: Vec a k).
@@ -57,26 +58,29 @@
         -> p @@ v
 elimVec SVNil pVNil _ = pVNil
 elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =
-  pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons)
+  pVCons sx sxs (elimVec @a @p @k @xs sxs pVNil pVCons)
 
-type WhyMapVec (a :: Type) (b :: Type) (n :: Nat) = Vec a n -> Vec b n
-$(genDefunSymbols [''WhyMapVec])
+elimPropVec :: forall a (p :: Nat ~> Prop) (n :: Nat).
+               Vec a n
+            -> p @@ Z
+            -> (forall (k :: Nat). a -> Vec a k -> p @@ k -> p @@ S k)
+            -> p @@ n
+elimPropVec VNil pZ _ = pZ
+elimPropVec (x :# (xs :: Vec a k)) pZ pS =
+  pS x xs (elimPropVec @a @p @k xs pZ pS)
 
-type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Nat)
-  = Vec a n -> Vec b n -> Vec c n
-$(genDefunSymbols [''WhyZipWithVec])
+$(singletons [d|
+  type WhyMapVec a b (n :: Nat) = Vec a n -> Vec b n
 
-type WhyAppendVec (e :: Type) (m :: Nat) (n :: Nat)
-  = Vec e n -> Vec e m -> Vec e (n + m)
-$(genDefunSymbols [''WhyAppendVec])
+  type WhyZipWithVec a b c (n :: Nat)
+    = Vec a n -> Vec b n -> Vec c n
 
-type WhyTransposeVec (e :: Type) (m :: Nat) (n :: Nat)
-  = Vec (Vec e m) n -> Vec (Vec e n) m
-$(genDefunSymbols [''WhyTransposeVec])
+  type WhyAppendVec e (m :: Nat) (n :: Nat)
+    = Vec e n -> Vec e m -> Vec e (n + m)
 
-type WhyConcatVec (e :: Type) (j :: Nat) (n :: Nat) (l :: Vec (Vec e j) n)
-  = 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
-  = WhyConcatVec e j n l
+  type WhyTransposeVec e (m :: Nat) (n :: Nat)
+    = Vec (Vec e m) n -> Vec (Vec e n) m
+
+  type family WhyConcatVec e (j :: Nat) (l :: Vec (Vec e j) n) :: Type where
+    WhyConcatVec e j (l :: Vec (Vec e j) n) = Vec e (n * j)
+  |])