diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -157,7 +157,7 @@
 withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
 withRefl _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of
   Refl -> r
-{-# INLINE [1] withRefl #-}
+{-# NOINLINE withRefl #-}
 {-# RULES
 "withRefl/unsafeCoerce" [~1] forall x.
   withRefl x = unsafeCoerce
diff --git a/Proof/Propositional.hs b/Proof/Propositional.hs
--- a/Proof/Propositional.hs
+++ b/Proof/Propositional.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll     #-}
 {-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}
-{-# LANGUAGE LambdaCase, PolyKinds, StandaloneDeriving, TemplateHaskell   #-}
-{-# LANGUAGE TypeOperators, RankNTypes                                    #-}
+{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving        #-}
+{-# LANGUAGE TemplateHaskell, TypeOperators                               #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 -- | Provides type synonyms for logical connectives.
 module Proof.Propositional
@@ -76,7 +76,7 @@
 
 withWitness :: IsTrue b -> (b ~ 'True => r) -> r
 withWitness Witness r = r
-{-# INLINE [1] withWitness #-}
+{-# NOINLINE withWitness #-}
 {-# RULES
 "withWitness/coercion" [~1] forall x.
   withWitness x = unsafeCoerce
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -25,7 +25,6 @@
                                               dsReify, expandType, substTy,
                                               sweeten)
 
-
 -- | Macro to automatically derive @'Empty'@ instance for
 --   concrete (variable-free) types which may contain products.
 refute :: TypeQ -> DecsQ
@@ -121,7 +120,11 @@
 resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
 resolveSubsts args info =
   case info of
-    (DTyConI (DDataD _ cxt _ tvbs dcons _) _) -> do
+    (DTyConI (DDataD _ cxt _ tvbs
+#if MIN_VERSION_th_desugar(1,9,0)
+              _
+#endif
+             dcons _) _) -> do
       let dic = M.fromList $ zip (map dtvbToName tvbs) args
       (cxt , ) <$> mapM (substDCon dic) dcons
     -- (DTyConI (DOpenTypeFamilyD n) _) ->  return []
@@ -137,7 +140,11 @@
 substDCon dic (DCon forall'd cxt conName fields mPhantom) =
   DCon forall'd cxt conName
     <$> substFields dic fields
+#if MIN_VERSION_th_desugar(1,9,0)
+    <*> substTy dic mPhantom
+#else
     <*> mapM (substTy dic) mPhantom
+#endif
 
 substFields :: SubstDic -> DConFields -> Q DConFields
 substFields subst
@@ -169,8 +176,11 @@
 splitType DArrowT = Just ([], ''(->), [])
 splitType (DLitT _) = Nothing
 splitType DWildCardT = Nothing
+#if !MIN_VERSION_th_desugar(1,9,0)
 splitType DStarT = Nothing
+#endif
 
+
 data EqlJudge = NonEqual | Undecidable | Equal
               deriving (Read, Show, Eq, Ord)
 
@@ -225,7 +235,9 @@
   | t == s    = return Equal
   | otherwise = return NonEqual
 compareType' (DLitT _) _ = return NonEqual
+#if !MIN_VERSION_th_desugar(1,9,0)
 compareType' DStarT DStarT = return NonEqual
+#endif
 compareType' _ _ = return NonEqual
 
 compareCxt :: DCxt -> DCxt -> Q EqlJudge
@@ -251,6 +263,10 @@
   | l == r = return Equal
   | otherwise = return NonEqual
 comparePred (DConPr _) _ = return NonEqual
+#if MIN_VERSION_th_desugar(1,9,0)
+comparePred (DForallPr _ _ _) (DForallPr _ _ _) = return Undecidable
+comparePred (DForallPr{}) _ = return NonEqual
+#endif
 
 substPred :: SubstDic -> DPred -> Q DPred
 substPred dic (DAppPr p1 p2) = DAppPr <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -1,46 +1,39 @@
-name: equational-reasoning
-version: 0.5.1.0
-cabal-version: >=1.8
-build-type: Simple
-license: BSD3
-license-file: LICENSE
-copyright: (c) Hiromi ISHII 2013-2018
-maintainer: konn.jinro_at_gmail.com
-synopsis: Proof assistant for Haskell using DataKinds & PolyKinds
-description:
-    A simple convenient library to write equational / preorder proof as in Agda.
-category: Math
-author: Hiromi ISHII
-tested-with: GHC ==8.0.2 GHC ==8.2.2 GHC ==8.4.1
+-- Initial equational-reasoning.cabal generated by cabal init.  For further
+--  documentation, see http://haskell.org/cabal/users-guide/
 
+name:                equational-reasoning
+version:             0.5.1.1
+synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds
+description:         A simple convenient library to write equational / preorder proof as in Agda.
+license:             BSD3
+license-file:        LICENSE
+author:              Hiromi ISHII
+maintainer:          konn.jinro_at_gmail.com
+copyright:           (c) Hiromi ISHII 2013-2018
+category:            Math
+build-type:          Simple
+tested-with:         GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.6.3
+cabal-version:       >=1.8
+
 source-repository head
     type: git
     location: git://github.com/konn/equational-reasoning-in-haskell.git
 
 library
-    
-    if impl(ghc >=8.4)
-        build-depends:
-            th-desugar ==1.8.*
-    else
-        build-depends:
-            semigroups ==0.18.*,
-            th-desugar >=1.6 && <1.8
-    exposed-modules:
-        Proof.Equational
-        Proof.Propositional
-        Proof.Induction
-        Proof.Propositional.Inhabited
-        Proof.Propositional.Empty
-    build-depends:
-        base ==4.*,
-        containers ==0.5.*,
-        template-haskell >=2.11 && <2.14,
-        th-extras ==0.0.*,
-        void >=0.6 && <0.8,
-        singletons >=2.1 && <2.5
-    other-modules:
-        Proof.Internal.THCompat
-        Proof.Propositional.TH
-    ghc-options: -Wall
-
+  exposed-modules:     Proof.Equational, Proof.Propositional, Proof.Induction
+                     , Proof.Propositional.Inhabited
+                     , Proof.Propositional.Empty
+  other-modules:       Proof.Internal.THCompat
+                     , Proof.Propositional.TH
+  ghc-options:         -Wall
+  build-depends:       base             >= 4      && < 5
+                     , containers       >= 0.5    && < 0.7
+                     , template-haskell >= 2.11   && < 2.16
+                     , th-extras        == 0.0.*
+                     , void             >= 0.6    && < 0.8
+                     , singletons       >= 2.1    && < 2.6
+  if impl(ghc >= 8.4)
+     build-depends:    th-desugar       >= 1.6 && < 1.11
+  else
+     build-depends:    semigroups       == 0.18.*
+     build-depends:    th-desugar       >= 1.6 && < 1.11