diff --git a/Proof/Induction.hs b/Proof/Induction.hs
--- a/Proof/Induction.hs
+++ b/Proof/Induction.hs
@@ -1,21 +1,21 @@
-{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}
-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators              #-}
-{-# LANGUAGE UndecidableInstances, ViewPatterns                        #-}
+{-# LANGUAGE DataKinds, ExplicitNamespaces, FlexibleContexts, GADTs #-}
+{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies   #-}
+{-# LANGUAGE TypeOperators, UndecidableInstances, ViewPatterns      #-}
 module Proof.Induction (genInduction) where
 import Proof.Internal.THCompat
 
-import Control.Applicative
-import Control.Monad
-import Data.Char
-import Data.Either
-import Data.List
-import Data.Singletons
-import Language.Haskell.TH
-import Language.Haskell.TH.Lib
-
-capitalize :: String -> String
-capitalize (x :xs) = toUpper x : xs
-capitalize _ = error "capitalize"
+import Control.Monad           (forM, replicateM)
+import Data.Either             (rights)
+import Data.Singletons         (Sing)
+import Language.Haskell.TH     (Clause, Con (ForallC, InfixC, NormalC, RecC))
+import Language.Haskell.TH     (TypeQ, appT, appT, appsE, appsE, arrowT, arrowT)
+import Language.Haskell.TH     (clause, clause, conP, conP, cxt, cxt, forallT)
+import Language.Haskell.TH     (funD, funD, mkName, nameBase, newName)
+import Language.Haskell.TH     (normalB, normalB, promotedT, promotedT, reify)
+import Language.Haskell.TH     (sigD, sigD, varE, varE, varP, varP, varT, varT)
+import Language.Haskell.TH     (Dec, Info (TyConI), Name, Q)
+import Language.Haskell.TH     (Type (AppT, ConT, PromotedT, SigT))
+import Language.Haskell.TH.Lib (plainTV)
 
 -- | @genInduction ''Type "inductionT"@ defines the induction scheme for @Type@ named @inductionT@.
 genInduction :: Name -> String -> Q [Dec]
@@ -41,10 +41,9 @@
   eparams <- forM paramTs $ \ty ->
     case getTyConName ty of
       Just nm | nm == dName -> Right <$> newName "t"
-      _ -> Left <$> newName "a"
+      _       -> Left <$> newName "a"
   xs <- replicateM (length paramTs) $ newName "x"
-  let freeVars = lefts eparams
-      subCases = [[t| Sing $(varT t) -> $(varT p) $(varT t) |] | t <- rights eparams ]
+  let subCases = [[t| Sing $(varT t) -> $(varT p) $(varT t) |] | t <- rights eparams ]
   params <- mapM (either varT varT) eparams
   let promCon = foldl appT (promotedT conName) (map return params)
       tbdy | null subCases = foldr toT ([t| $(varT p `appT` promCon) |]) subCases
@@ -58,28 +57,17 @@
   cl <- clause (map varP cs ++ [conP sName $ map varP xs]) (normalB body) []
   return (cl, sig)
   where
-    extractName (NormalC n _) = n
-    extractName (RecC n _) = n
+    extractName (NormalC n _)  = n
+    extractName (RecC n _)     = n
     extractName (InfixC _ n _) = n
-    extractName _ = error "I don't know name!"
-    extractParams (NormalC _ sts) = map snd sts
-    extractParams (RecC _ vsts)   = map (\(_,_,c) -> c) vsts
+    extractName _              = error "I don't know name!"
+    extractParams (NormalC _ sts)          = map snd sts
+    extractParams (RecC _ vsts)            = map (\(_,_,c) -> c) vsts
     extractParams (InfixC (_, t) _ (_, s)) = [t,s]
-    extractParams _ = []
+    extractParams _                        = []
 
 toT :: TypeQ -> TypeQ -> TypeQ
 a `toT` b = arrowT `appT` a `appT` b
-
-getFreeVarT :: Type -> [Name]
-getFreeVarT (AppT a b) = getFreeVarT a ++ getFreeVarT b
-getFreeVarT (SigT a _) = getFreeVarT a
-getFreeVarT (ForallT tvs _ t) = getFreeVarT t \\ map tyVarName tvs
-getFreeVarT (VarT n)   = [n]
-getFreeVarT _          = []
-
-tyVarName :: TyVarBndr -> Name
-tyVarName (PlainTV n) = n
-tyVarName (KindedTV n _) = n
 
 getTyConName :: Type -> Maybe Name
 getTyConName (AppT a _)    = getTyConName a
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE ExplicitNamespaces, MultiWayIf, PatternGuards, TemplateHaskell #-}
-{-# LANGUAGE TupleSections                                                  #-}
+{-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}
+{-# LANGUAGE TemplateHaskell, TupleSections                     #-}
 module Proof.Propositional.TH where
 import Proof.Propositional.Empty
 import Proof.Propositional.Inhabited
@@ -10,20 +10,20 @@
 import           Data.Map                    (Map)
 import qualified Data.Map                    as M
 import           Data.Maybe                  (fromJust)
-import           Data.Monoid                 ((<>))
+import           Data.Semigroup              (Semigroup (..))
 import           Data.Type.Equality          ((:~:) (..))
-import           Language.Haskell.TH         (DecsQ, Lit (CharL, IntegerL))
-import           Language.Haskell.TH         (Name, Q, TypeQ, isInstance)
-import           Language.Haskell.TH         (newName, ppr)
-import           Language.Haskell.TH.Desugar (DClause (..), DCon (..))
-import           Language.Haskell.TH.Desugar (DConFields (..), DCxt, DDec (..))
-import           Language.Haskell.TH.Desugar (DExp (..), DInfo (..))
-import           Language.Haskell.TH.Desugar (DLetDec (DFunD))
-import           Language.Haskell.TH.Desugar (DPat (DConPa, DVarPa), DPred (..))
-import           Language.Haskell.TH.Desugar (DTyVarBndr (..), DType (..))
-import           Language.Haskell.TH.Desugar (Overlap (Overlapping), desugar)
-import           Language.Haskell.TH.Desugar (dsReify, expandType, substTy)
-import           Language.Haskell.TH.Desugar (sweeten)
+import           Language.Haskell.TH         (DecsQ, Lit (CharL, IntegerL),
+                                              Name, Q, TypeQ, isInstance,
+                                              newName, ppr)
+import           Language.Haskell.TH.Desugar (DClause (..), DCon (..),
+                                              DConFields (..), DCxt, DDec (..),
+                                              DExp (..), DInfo (..),
+                                              DLetDec (DFunD),
+                                              DPat (DConPa, DVarPa), DPred (..),
+                                              DTyVarBndr (..), DType (..),
+                                              Overlap (Overlapping), desugar,
+                                              dsReify, expandType, substTy,
+                                              sweeten)
 
 
 -- | Macro to automatically derive @'Empty'@ instance for
@@ -110,11 +110,16 @@
     (const $ const [])
 
 fieldsVars :: DConFields -> [DType]
-fieldsVars (DNormalC fs) = map snd fs
-fieldsVars (DRecC fs) = map (\(_,_,c) -> c) fs
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804
+fieldsVars (DNormalC fs)
+#else
+fieldsVars (DNormalC _ fs)
+#endif
+  = map snd fs
+fieldsVars (DRecC fs)    = map (\(_,_,c) -> c) fs
 
 resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
-resolveSubsts args info = do
+resolveSubsts args info =
   case info of
     (DTyConI (DDataD _ cxt _ tvbs dcons _) _) -> do
       let dic = M.fromList $ zip (map dtvbToName tvbs) args
@@ -135,12 +140,24 @@
     <*> mapM (substTy dic) mPhantom
 
 substFields :: SubstDic -> DConFields -> Q DConFields
-substFields subst (DNormalC fs) = DNormalC <$> mapM (runKleisli $ second $ Kleisli $ substTy subst) fs
+substFields subst
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804
+  (DNormalC fs)
+#else
+  (DNormalC fixi fs)
+#endif
+  =
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 804
+  DNormalC <$>
+#else
+  DNormalC fixi <$>
+#endif
+  mapM (runKleisli $ second $ Kleisli $ substTy subst) fs
 substFields subst (DRecC fs) =
   DRecC <$> forM fs (\(a,b,c) -> (a, b ,) <$> substTy subst c)
 
 dtvbToName :: DTyVarBndr -> Name
-dtvbToName (DPlainTV n) = n
+dtvbToName (DPlainTV n)    = n
 dtvbToName (DKindedTV n _) = n
 
 splitType :: DType -> Maybe ([Name], Name, [DType])
@@ -157,12 +174,14 @@
 data EqlJudge = NonEqual | Undecidable | Equal
               deriving (Read, Show, Eq, Ord)
 
-instance Monoid EqlJudge where
-  NonEqual    `mappend` _        = NonEqual
-  Undecidable `mappend` NonEqual = NonEqual
-  Undecidable `mappend` _        = Undecidable
-  Equal       `mappend` m        = m
+instance Semigroup EqlJudge where
+  NonEqual    <> _        = NonEqual
+  Undecidable <> NonEqual = NonEqual
+  Undecidable <> _        = Undecidable
+  Equal       <> m        = m
 
+instance Monoid EqlJudge where
+  mappend = (<>)
   mempty = Equal
 
 compareType :: DType -> DType -> Q EqlJudge
@@ -193,7 +212,7 @@
       bd <- compareType' t s'
       return (pd <> bd)
   | otherwise = return NonEqual
-compareType' (DForallT _ _ _) _   = return NonEqual
+compareType' DForallT{} _   = return NonEqual
 compareType' (DAppT t1 t2) (DAppT s1 s2)
   = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
 compareType' (DConT t) (DConT s)
@@ -241,3 +260,7 @@
   | Just (DConT t) <- M.lookup p dic = return $ DConPr t
   | otherwise = return prd
 substPred _ t = return t
+
+
+
+
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -1,23 +1,31 @@
 name: equational-reasoning
-version: 0.5.0.0
+version: 0.5.1.0
 cabal-version: >=1.8
 build-type: Simple
 license: BSD3
 license-file: LICENSE
-copyright: (c) Hiromi ISHII 2013-2014
+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 ==7.10.3 GHC ==8.0.1
+tested-with: GHC ==8.0.2 GHC ==8.2.2 GHC ==8.4.1
 
 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
@@ -26,12 +34,11 @@
         Proof.Propositional.Empty
     build-depends:
         base ==4.*,
-        containers >=0.5,
-        template-haskell >=2.11.1.0,
-        th-desugar >=1.6,
-        th-extras >=0.0.0.4,
+        containers ==0.5.*,
+        template-haskell >=2.11 && <2.14,
+        th-extras ==0.0.*,
         void >=0.6 && <0.8,
-        singletons >=2.1 && <2.4
+        singletons >=2.1 && <2.5
     other-modules:
         Proof.Internal.THCompat
         Proof.Propositional.TH