diff --git a/Changelog.md b/Changelog.md
new file mode 100644
--- /dev/null
+++ b/Changelog.md
@@ -0,0 +1,25 @@
+Changelog
+==========
+
+## 0.7.1.0
+
+- Supports GHC 9.10 and 9.12
+- Drops support for GHC <9.2
+
+## 0.7.0.2
+
+- Supports GHC 9.8
+- Drops support for GHC <9
+
+## 0.6.0.3
+
+- Support for GHC >= 8.10
+
+## 0.6.0.2
+
+- Adds support for th-desugar-1.11
+
+## 0.6.0.1
+
+- Supports GHC 8.8.
+- Adds support for th-desugar-1.10 (Thanks: Justin Le @mstksg)
diff --git a/Proof/Equational.hs b/Proof/Equational.hs
--- a/Proof/Equational.hs
+++ b/Proof/Equational.hs
@@ -1,72 +1,117 @@
-{-# LANGUAGE CPP, DataKinds, FlexibleContexts, GADTs, KindSignatures #-}
-{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables              #-}
-{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators         #-}
-{-# LANGUAGE TypeSynonymInstances, UndecidableInstances              #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
 {-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-}
 #endif
-module Proof.Equational ( (:~:)(..), (:=:)
-                        , sym, trans
-                        , Equality(..), Preorder(..), reflexivity'
-                        , (:\/:), (:/\:), (=<=), (=>=), (=~=), Leibniz(..)
-                        , Reason(..), because, by, (===), start, byDefinition
-                        , admitted, Proxy(..), cong, cong'
-                        , Proposition(..), HVec(..), FromBool (..)
-                        , applyNAry, applyNAry', fromBool'
-                          -- * Conversion between equalities
-                        , fromRefl, fromLeibniz, reflToLeibniz, leibnizToRefl
-                          -- * Coercion
-                        , coerce, coerce', withRefl
-                          -- * Re-exported modules
-                        , module Data.Singletons, module Data.Proxy
-                        ) where
+module Proof.Equational (
+  (:~:) (..),
+  (:=:),
+  sym,
+  trans,
+  Equality (..),
+  Preorder (..),
+  reflexivity',
+  (:\/:),
+  (:/\:),
+  (=<=),
+  (=>=),
+  (=~=),
+  Leibniz (..),
+  Reason (..),
+  because,
+  by,
+  (===),
+  start,
+  byDefinition,
+  admitted,
+  Proxy (..),
+  cong,
+  cong',
+  Proposition (..),
+  HVec (..),
+  FromBool (..),
+  applyNAry,
+  applyNAry',
+  fromBool',
+
+  -- * Conversion between equalities
+  fromRefl,
+  fromLeibniz,
+  reflToLeibniz,
+  leibnizToRefl,
+
+  -- * Coercion
+  coerce,
+  coerceInner,
+  coerce',
+  withRefl,
+
+  -- * Re-exported modules
+  module Data.Proxy,
+) where
+
+import Data.Kind (Type)
 import Data.Proxy
-import Data.Singletons
 import Data.Type.Equality hiding (apply)
 import Unsafe.Coerce
 
 infix 4 :=:
+
 type a :\/: b = Either a b
+
 infixr 2 :\/:
 
 type a :/\: b = (a, b)
+
 infixr 3 :/\:
 
 type (:=:) = (:~:)
 
-data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }
+data Leibniz a b = Leibniz {apply :: forall f. f a -> f b}
 
 leibnizToRefl :: Leibniz a b -> a :=: b
 leibnizToRefl eq = apply eq Refl
 
-fromLeibniz :: (Preorder eq, SingI a) => Leibniz a b -> eq a b
-fromLeibniz eq = apply eq (reflexivity sing)
+fromLeibniz :: (Preorder eq) => Leibniz a b -> eq a b
+fromLeibniz eq = apply eq (reflexivity Proxy)
 
-fromRefl :: (Preorder eq, SingI b) => a :=: b -> eq a b
+fromRefl :: (Preorder eq) => a :=: b -> eq a b
 fromRefl Refl = reflexivity'
 
 reflToLeibniz :: a :=: b -> Leibniz a b
 reflToLeibniz Refl = Leibniz id
 
-class Preorder (eq :: k -> k -> *) where
-  reflexivity  :: Sing a -> eq a a
-  transitivity :: eq a b  -> eq b c -> eq a c
+class Preorder (eq :: k -> k -> Type) where
+  reflexivity :: proxy a -> eq a a
+  transitivity :: eq a b -> eq b c -> eq a c
 
-class Preorder eq => Equality (eq :: k -> k -> *) where
-  symmetry     :: eq a b  -> eq b a
+class (Preorder eq) => Equality (eq :: k -> k -> Type) where
+  symmetry :: eq a b -> eq b a
 
 instance Preorder (:=:) where
-  {-# SPECIALISE instance Preorder (:=:) #-}
+  {-# SPECIALIZE instance Preorder (:=:) #-}
   transitivity Refl Refl = Refl
-  {-# INLINE[1] transitivity #-}
+  {-# INLINE [1] transitivity #-}
 
-  reflexivity  _         = Refl
-  {-# INLINE[1] reflexivity #-}
+  reflexivity _ = Refl
+  {-# INLINE [1] reflexivity #-}
 
 instance Equality (:=:) where
-  {-# SPECIALISE instance Equality (:~:) #-}
-  symmetry     Refl      = Refl
-  {-# INLINE[1] symmetry #-}
+  {-# SPECIALIZE instance Equality (:~:) #-}
+  symmetry Refl = Refl
+  {-# INLINE [1] symmetry #-}
 
 instance Preorder (->) where
   reflexivity _ = id
@@ -80,46 +125,46 @@
   transitivity (Leibniz aEqb) (Leibniz bEqc) = Leibniz $ bEqc . aEqb
 
 instance Equality Leibniz where
-  symmetry eq  = unFlip $ apply eq $ Flip leibniz_refl
+  symmetry eq = unFlip $ apply eq $ Flip leibniz_refl
 
-newtype Flip f a b = Flip { unFlip :: f b a }
+newtype Flip f a b = Flip {unFlip :: f b a}
 
 data Reason eq x y where
-  Because :: Sing y -> eq x y -> Reason eq x y
+  Because :: proxy y -> eq x y -> Reason eq x y
 
-reflexivity' :: (SingI x, Preorder r) => r x x
-reflexivity' = reflexivity sing
+reflexivity' :: (Preorder r) => r x x
+reflexivity' = reflexivity Proxy
 
-by, because :: Sing y -> eq x y -> Reason eq x y
+by, because :: proxy y -> eq x y -> Reason eq x y
 because = Because
-by      = Because
+by = Because
 
 infixl 4 ===, =<=, =~=, =>=
+
 infix 5 `Because`
+
 infix 5 `because`
 
-(=<=) :: Preorder r => r x y -> Reason r y z -> r x z
+(=<=) :: (Preorder r) => r x y -> Reason r y z -> r x z
 eq =<= (_ `Because` eq') = transitivity eq eq'
-
-{-# SPECIALISE INLINE[1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
+{-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
-(=>=) :: Preorder r => r y z -> Reason r x y -> r x z
+(=>=) :: (Preorder r) => r y z -> Reason r x y -> r x z
 eq =>= (_ `Because` eq') = transitivity eq' eq
-
-{-# SPECIALISE INLINE[1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
+{-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
 
-(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
+(===) :: (Equality eq) => eq x y -> Reason eq y z -> eq x z
 (===) = (=<=)
-{-# SPECIALISE INLINE[1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
+{-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
 
-(=~=) :: r x y -> Sing y -> r x y
+(=~=) :: r x y -> proxy y -> r x y
 eq =~= _ = eq
 
-start :: Preorder eq => Sing a -> eq a a
+start :: (Preorder eq) => proxy a -> eq a a
 start = reflexivity
 
-byDefinition :: (SingI a, Preorder eq) => eq a a
-byDefinition = reflexivity sing
+byDefinition :: (Preorder eq) => eq a a
+byDefinition = reflexivity Proxy
 
 admitted :: Reason eq x y
 admitted = undefined
@@ -128,92 +173,95 @@
 cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b
 cong Proxy Refl = Refl
 
-cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b
-cong' _ Refl =  Refl
+cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b
+cong' _ Refl = Refl
 
--- | Type coercion. 'coerce' is using @unsafeCoerce a@.
--- So, please, please do not provide the @undefined@ as the proof.
--- Using this function instead of pattern-matching on equality proof,
--- you can reduce the overhead introduced by run-time proof.
-coerce :: (a :=: b) -> f a -> f b
-coerce _ a = unsafeCoerce a
-{-# INLINE[1] coerce #-}
+{- | Type coercion. 'coerce' is using @unsafeCoerce a@.
+ So, please, please do not provide the @undefined@ as the proof.
+ Using this function instead of pattern-matching on equality proof,
+ you can reduce the overhead introduced by run-time proof.
+-}
+coerceInner, coerce :: (a :=: b) -> f a -> f b
+{-# DEPRECATED coerce "Use coerceInner instead" #-}
+coerce = coerceInner
+{-# INLINE coerce #-}
+coerceInner _ = unsafeCoerce
+{-# INLINE [1] coerceInner #-}
 
 -- | Coercion for identity types.
 coerce' :: a :=: b -> a -> b
-coerce' _ a = unsafeCoerce a
-{-# INLINE[1] coerce' #-}
+coerce' _ = unsafeCoerce
+{-# INLINE [1] coerce' #-}
 
 {-# RULES
 "coerce/unsafeCoerce" [~1] forall xs.
-  coerce xs = unsafeCoerce
+  coerceInner xs =
+    unsafeCoerce
 "coerce'/unsafeCoerce" [~1] forall xs.
-  coerce' xs = unsafeCoerce
+  coerce' xs =
+    unsafeCoerce
   #-}
 
--- | Solves equality constraint without explicit coercion.
---   It has the same effect as @'Data.Type.Equality.gcastWith'@,
---   but some hacks is done to reduce runtime overhead.
-withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
-withRefl _ r = case unsafeCoerce (Refl :: () :~: ()) :: a :~: b of
-  Refl -> r
-{-# NOINLINE withRefl #-}
-{-# RULES
-"withRefl/unsafeCoerce" [~1] forall x.
-  withRefl x = unsafeCoerce
-  #-}
+{- | Solves equality constraint without explicit coercion.
+   It has the same effect as @'Data.Type.Equality.gcastWith'@,
+   but some hacks is done to reduce runtime overhead.
+-}
+withRefl :: forall a b r. a :~: b -> ((a ~ b) => r) -> r
+withRefl _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: a :~: b)
 
-class Proposition (f :: k -> *) where
-  type OriginalProp (f :: k -> *) (n :: k) :: *
+class Proposition (f :: k -> Type) where
+  type OriginalProp (f :: k -> Type) (n :: k) :: Type
   unWrap :: f n -> OriginalProp f n
-  wrap   :: OriginalProp f n -> f n
+  wrap :: OriginalProp f n -> f n
 
-data HVec (xs :: [*]) where
+data HVec (xs :: [Type]) where
   HNil :: HVec '[]
   (:-) :: x -> HVec xs -> HVec (x ': xs)
 
 infixr 9 :-
-type family (xs :: [*]) :~> (a :: *) :: * where
-  '[]       :~> a = a
+
+type family (xs :: [Type]) :~> (a :: Type) :: Type where
+  '[] :~> a = a
   (x ': xs) :~> a = x -> (xs :~> a)
 
 infixr 1 :~>
 
-data HVecView (xs :: [*]) :: * where
-  HNilView  :: HVecView '[]
+data HVecView (xs :: [Type]) :: Type where
+  HNilView :: HVecView '[]
   HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts)
 
 deriving instance Show (HVecView xs)
 
-class KnownTypeList (xs :: [*]) where
+class KnownTypeList (xs :: [Type]) where
   viewHVec' :: HVecView xs
 
 instance KnownTypeList '[] where
   viewHVec' = HNilView
 
-instance KnownTypeList ts => KnownTypeList (t ': ts) where
+instance (KnownTypeList ts) => KnownTypeList (t ': ts) where
   viewHVec' = HConsView Proxy viewHVec'
 
-newtype Magic (xs :: [*]) a = Magic { _viewHVec' :: KnownTypeList xs => a }
+newtype Magic (xs :: [Type]) a = Magic {_viewHVec' :: (KnownTypeList xs) => a}
 
-withKnownTypeList :: forall a xs. HVecView xs -> (KnownTypeList xs => a) -> a
+withKnownTypeList :: forall a xs. HVecView xs -> ((KnownTypeList xs) => a) -> a
 withKnownTypeList xs f = (unsafeCoerce (Magic f :: Magic xs a) :: HVecView xs -> a) xs
 
 apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c
 apply' HNilView f = f HNil
-apply' (HConsView Proxy ts) f = \a -> withKnownTypeList ts $
-  apply' ts (\ts' -> f $ a :- ts')
+apply' (HConsView Proxy ts) f = \a ->
+  withKnownTypeList ts $
+    apply' ts (\ts' -> f $ a :- ts')
 
-applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c
+applyNAry :: forall ts c. (KnownTypeList ts) => (HVec ts -> c) -> ts :~> c
 applyNAry = apply' (viewHVec' :: HVecView ts)
 
-applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
+applyNAry' :: (KnownTypeList ts) => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
 applyNAry' _ _ = applyNAry
 
-class FromBool (c :: *) where
+class FromBool (c :: Type) where
   type Predicate c :: Bool
-  type Args c :: [*]
-  fromBool :: Predicate c ~ 'True => HVec (Args c) -> c
+  type Args c :: [Type]
+  fromBool :: (Predicate c ~ 'True) => HVec (Args c) -> c
 
-fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c , Predicate c ~ 'True) => proxy c -> Args c :~> c
+fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) => proxy c -> Args c :~> c
 fromBool' pxyc = applyNAry' (Proxy :: Proxy (Args c)) pxyc fromBool
diff --git a/Proof/Induction.hs b/Proof/Induction.hs
deleted file mode 100644
--- a/Proof/Induction.hs
+++ /dev/null
@@ -1,82 +0,0 @@
-{-# 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.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]
-genInduction typ fname0 = do
-  let fname = mkName fname0
-  TyConI (normalizeDec -> DataDCompat _ dName _ dCons _) <- reify typ
-  p <- newName "p"
-  ans <- mapM (buildCase fname (length dCons) dName p) $ zip [0..] dCons
-  let (cls, ts) = unzip ans
-  t <- newName "t"
-  sig <- sigD fname $ forallT [plainTV p, plainTV t] (cxt []) $
-           foldr toT ([t| Sing $(varT t) -> $(varT p) $(varT t) |]) $ map return ts
-  dec <- funD fname (map return cls)
-  return [sig, dec]
-
-buildCase :: Name -> Int -> Name -> Name -> (Int, Con) -> Q (Clause, Type)
-buildCase _ _ _ _ (_, ForallC _ _ _) = error "Existential types are not supported yet."
-buildCase fname size dName p (nth, dCon) = do
-  let paramTs = extractParams dCon
-      conName = extractName dCon
-      sName = mkName $ 'S' : nameBase conName
-      ssName = mkName $ 's' : nameBase conName
-  eparams <- forM paramTs $ \ty ->
-    case getTyConName ty of
-      Just nm | nm == dName -> Right <$> newName "t"
-      _       -> Left <$> newName "a"
-  xs <- replicateM (length paramTs) $ newName "x"
-  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
-           | otherwise   = foldr toT ([t| Sing $(promCon) -> $(varT p `appT` promCon) |]) subCases
-  sig <- if null params then tbdy else forallT (map (either plainTV plainTV) eparams) (cxt []) tbdy
-  cs <- replicateM size $ newName "case"
-  let body | null subCases = varE (cs !! nth)
-           | otherwise = appsE $ varE (cs !! nth) :
-               replicate (length subCases) (appsE $ varE fname : map varE cs)
-               ++ [ appsE (varE ssName : map varE xs)]
-  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 (InfixC _ n _) = n
-    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 _                        = []
-
-toT :: TypeQ -> TypeQ -> TypeQ
-a `toT` b = arrowT `appT` a `appT` b
-
-getTyConName :: Type -> Maybe Name
-getTyConName (AppT a _)    = getTyConName a
-getTyConName (SigT a _)    = getTyConName a
-getTyConName (ConT nam)    = Just nam
-getTyConName (PromotedT n) = Just n
-getTyConName _             = Nothing
-
-normalizeDec :: Dec -> Dec
-normalizeDec d@DataDCompat {} = d
-normalizeDec (NewtypeDCompat ctx name tvbs con names) = mkDataD ctx name tvbs [con] names
-normalizeDec _ = error "not data definition."
diff --git a/Proof/Internal/THCompat.hs b/Proof/Internal/THCompat.hs
deleted file mode 100644
--- a/Proof/Internal/THCompat.hs
+++ /dev/null
@@ -1,87 +0,0 @@
-{-# LANGUAGE CPP, PatternSynonyms, TemplateHaskell, ViewPatterns #-}
-{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
-module Proof.Internal.THCompat where
-import Language.Haskell.TH
-import Language.Haskell.TH.Extras
-
-import GHC.Exts (Constraint)
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 802
-import GHC.Generics
-import Data.Data
-#endif
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 802
-data DerivClause = DerivClause (Maybe DerivStrategy) Cxt
-                 deriving (Eq, Data, Ord, Show, Generic)
-data  DerivStrategy = StockStrategy
-                    | AnyclassStrategy
-                    | NewtypeStrategy
-                    deriving (Eq, Data, Ord, Show, Generic)
-#endif
-
-dcToNames :: DerivClause -> [Name]
-dcToNames (DerivClause _ ct) = map headOfType ct
-
-dcToCxt :: DerivClause -> Cxt
-dcToCxt (DerivClause _ ct) = ct
-
-
-mkDataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [DerivClause] -> Dec
-mkDataD ctx name tvbndrs cons dc =
-  DataD ctx name tvbndrs
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
-        Nothing cons 
-#if __GLASGOW_HASKELL__ < 802
-        (concatMap dcToCxt dc)
-#else
-        dc
-#endif
-#else
-        cons (concatMap dcToNames dc)
-#endif
-
-
-typeName :: Type -> Name
-typeName (VarT n) = n
-typeName (ConT n) = n
-typeName (PromotedT n) = n
-typeName (TupleT n) = tupleTypeName n
-typeName (UnboxedTupleT n) = unboxedTupleTypeName n
-typeName ArrowT = ''(->)
-typeName EqualityT = ''(~)
-typeName ListT = ''[]
-typeName (PromotedTupleT n) = tupleDataName n
-typeName PromotedNilT = '[]
-typeName PromotedConsT = '(:)
-typeName ConstraintT = ''Constraint
-typeName _ = error "No names!"
-
-pattern DataDCompat :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [DerivClause] -> Dec
-pattern DataDCompat ctx name tvbndrs cons dcs <-
-  DataD ctx name tvbndrs
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
-        _ cons 
-#if __GLASGOW_HASKELL__ < 802
-        (pure . DerivClause Nothing -> dcs)
-#else 
-        dcs
-#endif
-#else
-        cons (DerivClause Nothing . map ConT -> dc)
-#endif
-
-pattern NewtypeDCompat :: Cxt -> Name -> [TyVarBndr] -> Con -> [DerivClause] -> Dec
-pattern NewtypeDCompat ctx name tvbndrs con dcs <-
-  NewtypeD ctx name tvbndrs
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
-        _ con
-#if __GLASGOW_HASKELL__ < 802
-        (pure . DerivClause Nothing -> dcs)
-#else
-        dcs
-#endif
-#else
-        con
-        (DerivClause Nothing . map ConT -> dcs)
-#endif
diff --git a/Proof/Propositional.hs b/Proof/Propositional.hs
--- a/Proof/Propositional.hs
+++ b/Proof/Propositional.hs
@@ -1,34 +1,64 @@
-{-# LANGUAGE DataKinds, DeriveDataTypeable, EmptyCase, ExplicitForAll     #-}
-{-# LANGUAGE ExplicitNamespaces, FlexibleInstances, GADTs, KindSignatures #-}
-{-# LANGUAGE LambdaCase, PolyKinds, RankNTypes, StandaloneDeriving        #-}
-{-# LANGUAGE TemplateHaskell, TypeOperators                               #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+
 -- | Provides type synonyms for logical connectives.
-module Proof.Propositional
-       ( type (/\), type (\/), Not, exfalso, orIntroL
-       , orIntroR, orElim, andIntro, andElimL
-       , andElimR, orAssocL, orAssocR
-       , andAssocL, andAssocR, IsTrue(..), withWitness
-       , Empty(..), withEmpty, withEmpty'
-       , refute
-       , Inhabited (..), withInhabited
-       , prove
-       ) where
+module Proof.Propositional (
+  type (/\),
+  type (\/),
+  Not,
+  exfalso,
+  orIntroL,
+  orIntroR,
+  orElim,
+  andIntro,
+  andElimL,
+  andElimR,
+  orAssocL,
+  orAssocR,
+  andAssocL,
+  andAssocR,
+  IsTrue (..),
+  withWitness,
+  Empty (..),
+  withEmpty,
+  withEmpty',
+  refute,
+  Inhabited (..),
+  withInhabited,
+  prove,
+) where
+
+import Data.Data (Data)
+import Data.Type.Equality (gcastWith, (:~:) (..))
+import Data.Typeable (Typeable)
+import Data.Void
 import Proof.Propositional.Empty
 import Proof.Propositional.Inhabited
 import Proof.Propositional.TH
-
-import Data.Data          (Data)
-import Data.Type.Equality ((:~:))
-import Data.Typeable      (Typeable)
-import Data.Void
 import Unsafe.Coerce
 
 type a /\ b = (a, b)
+
 type a \/ b = Either a b
-type Not a  = a -> Void
 
+type Not a = a -> Void
+
 infixr 2 \/
+
 infixr 3 /\
 
 exfalso :: a -> Not a -> b
@@ -53,69 +83,70 @@
 andElimR = snd
 
 andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c
-andAssocL (a,(b,c)) = ((a,b), c)
+andAssocL (a, (b, c)) = ((a, b), c)
 
 andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)
-andAssocR ((a,b),c) = (a,(b,c))
+andAssocR ((a, b), c) = (a, (b, c))
 
 orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c
-orAssocL (Left a)          = Left (Left a)
-orAssocL (Right (Left b))  = Left (Right b)
+orAssocL (Left a) = Left (Left a)
+orAssocL (Right (Left b)) = Left (Right b)
 orAssocL (Right (Right c)) = Right c
 
 orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)
-orAssocR (Left (Left a))  = Left a
+orAssocR (Left (Left a)) = Left a
 orAssocR (Left (Right b)) = Right (Left b)
-orAssocR (Right c)        = Right (Right c)
-
+orAssocR (Right c) = Right (Right c)
 
--- | Utility type to convert type-level (@'Bool'@-valued) predicate function
---   into concrete witness data-type.
+{- | Utility type to convert type-level (@'Bool'@-valued) predicate function
+   into concrete witness data-type.
+-}
 data IsTrue (b :: Bool) where
   Witness :: IsTrue 'True
 
-withWitness :: IsTrue b -> (b ~ 'True => r) -> r
-withWitness Witness r = r
+withWitness :: forall b r. IsTrue b -> ((b ~ 'True) => r) -> r
+withWitness _ = gcastWith (unsafeCoerce (Refl :: () :~: ()) :: b :~: 'True)
 {-# NOINLINE withWitness #-}
-{-# RULES
-"withWitness/coercion" [~1] forall x.
-  withWitness x = unsafeCoerce
-  #-}
 
 deriving instance Show (IsTrue b)
-deriving instance Eq   (IsTrue b)
-deriving instance Ord  (IsTrue b)
+
+deriving instance Eq (IsTrue b)
+
+deriving instance Ord (IsTrue b)
+
 deriving instance Read (IsTrue 'True)
+
 deriving instance Typeable IsTrue
+
 deriving instance Data (IsTrue 'True)
 
 instance {-# OVERLAPPABLE #-} (Inhabited a, Empty b) => Empty (a -> b) where
   eliminate f = eliminate (f trivial)
 
-refute [t| 0 :~: 1 |]
-refute [t| () :~: Int |]
-refute [t| 'True :~: 'False |]
-refute [t| 'False :~: 'True |]
-refute [t| 'LT :~: 'GT |]
-refute [t| 'LT :~: 'EQ |]
-refute [t| 'EQ :~: 'LT |]
-refute [t| 'EQ :~: 'GT |]
-refute [t| 'GT :~: 'LT |]
-refute [t| 'GT :~: 'EQ |]
+refute [t|0 :~: 1|]
+refute [t|() :~: Int|]
+refute [t|'True :~: 'False|]
+refute [t|'False :~: 'True|]
+refute [t|'LT :~: 'GT|]
+refute [t|'LT :~: 'EQ|]
+refute [t|'EQ :~: 'LT|]
+refute [t|'EQ :~: 'GT|]
+refute [t|'GT :~: 'LT|]
+refute [t|'GT :~: 'EQ|]
 
-prove [t| Bool |]
-prove [t| Int |]
-prove [t| Integer |]
-prove [t| Word |]
-prove [t| Double |]
-prove [t| Float |]
-prove [t| Char |]
-prove [t| Ordering |]
-prove [t| forall a. [a] |]
-prove [t| Rational |]
-prove [t| forall a. Maybe a |]
-prove [t| forall n. n :~: n |]
-prove [t| IsTrue 'True |]
+prove [t|Bool|]
+prove [t|Int|]
+prove [t|Integer|]
+prove [t|Word|]
+prove [t|Double|]
+prove [t|Float|]
+prove [t|Char|]
+prove [t|Ordering|]
+prove [t|forall a. [a]|]
+prove [t|Rational|]
+prove [t|forall a. Maybe a|]
+prove [t|forall n. n :~: n|]
+prove [t|IsTrue 'True|]
 
 instance Empty (IsTrue 'False) where
-  eliminate = \ case {}
+  eliminate = \case {}
diff --git a/Proof/Propositional/Empty.hs b/Proof/Propositional/Empty.hs
--- a/Proof/Propositional/Empty.hs
+++ b/Proof/Propositional/Empty.hs
@@ -1,59 +1,75 @@
-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
-{-# LANGUAGE DataKinds, DefaultSignatures, DeriveAnyClass, EmptyCase #-}
-{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-}
-{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PolyKinds            #-}
-{-# LANGUAGE StandaloneDeriving, TupleSections, TypeOperators        #-}
-module Proof.Propositional.Empty (Empty(..), withEmpty, withEmpty') where
-import Data.Void          (Void, absurd)
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Proof.Propositional.Empty (Empty (..), withEmpty, withEmpty') where
+
+import Data.Void (Void, absurd)
 import GHC.Generics
-import Unsafe.Coerce      (unsafeCoerce)
+import Unsafe.Coerce (unsafeCoerce)
 
--- | Type-class for types without inhabitants, dual to @'Proof.Propositional.Inhabited'@.
---   Current GHC doesn't provide selective-instance,
---   hence we don't @'Empty'@ provide instances
---   for product types in a generic deriving (DeriveAnyClass).
--- 
---   To derive an instance for each concrete types,
---   use @'Proof.Propositional.refute'@.
---
---   Since 0.4.0.0.
+{- | Type-class for types without inhabitants, dual to @'Proof.Propositional.Inhabited'@.
+  Current GHC doesn't provide selective-instance,
+  hence we don't @'Empty'@ provide instances
+  for product types in a generic deriving (DeriveAnyClass).
+
+  To derive an instance for each concrete types,
+  use @'Proof.Propositional.refute'@.
+
+  Since 0.4.0.0.
+-}
 class Empty a where
   eliminate :: a -> x
-
   default eliminate :: (Generic a, GEmpty (Rep a)) => a -> x
   eliminate = geliminate . from
 
 class GEmpty f where
   geliminate :: f a -> x
 
-instance GEmpty f => GEmpty (M1 i t f) where
+instance (GEmpty f) => GEmpty (M1 i t f) where
   geliminate (M1 a) = geliminate a
 
 instance (GEmpty f, GEmpty g) => GEmpty (f :+: g) where
   geliminate (L1 a) = geliminate a
   geliminate (R1 b) = geliminate b
 
-instance Empty c => GEmpty (K1 i c) where
+instance (Empty c) => GEmpty (K1 i c) where
   geliminate (K1 a) = eliminate a
 
 instance GEmpty V1 where
-  geliminate = \ case {}
+  geliminate = \case {}
 
 deriving instance (Empty a, Empty b) => Empty (Either a b)
+
 deriving instance Empty Void
 
-newtype MagicEmpty e a = MagicEmpty (Empty e => a)
+newtype MagicEmpty e a = MagicEmpty ((Empty e) => a)
 
--- | Giving falsity witness by proving @'Void'@ from @a@.
---   See also 'withEmpty''.
---
---   Since 0.4.0.0
-withEmpty :: forall a b. (a -> Void) -> (Empty a => b) -> b
+{- | Giving falsity witness by proving @'Void'@ from @a@.
+  See also 'withEmpty''.
+
+  Since 0.4.0.0
+-}
+withEmpty :: forall a b. (a -> Void) -> ((Empty a) => b) -> b
 withEmpty neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) (absurd . neg)
 
--- | Giving falsity witness by showing @a@ entails everything.
---   See also 'withEmpty'.
---
---   Since 0.4.0.0
-withEmpty' :: forall a b. (forall c. a -> c) -> (Empty a => b) -> b
+{- | Giving falsity witness by showing @a@ entails everything.
+  See also 'withEmpty'.
+
+  Since 0.4.0.0
+-}
+withEmpty' :: forall a b. (forall c. a -> c) -> ((Empty a) => b) -> b
 withEmpty' neg k = unsafeCoerce (MagicEmpty k :: MagicEmpty a b) neg
diff --git a/Proof/Propositional/Inhabited.hs b/Proof/Propositional/Inhabited.hs
--- a/Proof/Propositional/Inhabited.hs
+++ b/Proof/Propositional/Inhabited.hs
@@ -1,21 +1,35 @@
-{-# LANGUAGE DataKinds, DefaultSignatures, DeriveAnyClass, EmptyCase  #-}
-{-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances  #-}
-{-# LANGUAGE GADTs, KindSignatures, LambdaCase, PolyKinds, RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TupleSections   #-}
-{-# LANGUAGE TypeOperators                                            #-}
-module Proof.Propositional.Inhabited (Inhabited(..), withInhabited) where
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Proof.Propositional.Inhabited (Inhabited (..), withInhabited) where
+
 import GHC.Generics
 import Unsafe.Coerce (unsafeCoerce)
 
--- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.
---   Currently, GHC doesn't provide a selective-instance,
---   hence we can't generically derive @'Inhabited'@ instances
---   for sum types (i.e. by @DeriveAnyClass@).
---
---   To derive an instance for each concrete types,
---   use @'Proof.Propositional.prove'@.
---
---   Since 0.4.0.0.
+{- | Types with at least one inhabitant, dual to @'Proof.Propositional.Empty'@.
+  Currently, GHC doesn't provide a selective-instance,
+  hence we can't generically derive @'Inhabited'@ instances
+  for sum types (i.e. by @DeriveAnyClass@).
+
+  To derive an instance for each concrete types,
+  use @'Proof.Propositional.prove'@.
+
+  Since 0.4.0.0.
+-}
 class Inhabited a where
   -- | A /generic/ inhabitant of type @'a'@, which means that
   --   one cannot assume anything about the value of @'trivial'@
@@ -24,34 +38,36 @@
   --   * is of type @a@, and
   --   * doesn't contain any partial values.
   trivial :: a
-
   default trivial :: (Generic a, GInhabited (Rep a)) => a
   trivial = to gtrivial
 
 class GInhabited f where
   gtrivial :: f a
 
-instance GInhabited f => GInhabited (M1 i t f) where
+instance (GInhabited f) => GInhabited (M1 i t f) where
   gtrivial = M1 gtrivial
 
 instance (GInhabited f, GInhabited g) => GInhabited (f :*: g) where
   gtrivial = gtrivial :*: gtrivial
 
-instance Inhabited c => GInhabited (K1 i c) where
+instance (Inhabited c) => GInhabited (K1 i c) where
   gtrivial = K1 trivial
 
 instance GInhabited U1 where
   gtrivial = U1
 
 deriving instance Inhabited ()
+
 deriving instance (Inhabited a, Inhabited b) => Inhabited (a, b)
+
 deriving instance (Inhabited a, Inhabited b, Inhabited c) => Inhabited (a, b, c)
+
 deriving instance (Inhabited a, Inhabited b, Inhabited c, Inhabited d) => Inhabited (a, b, c, d)
 
-instance Inhabited b => Inhabited (a -> b) where
+instance (Inhabited b) => Inhabited (a -> b) where
   trivial = const trivial
 
-newtype MagicInhabited a b = MagicInhabited (Inhabited a => b)
+newtype MagicInhabited a b = MagicInhabited ((Inhabited a) => b)
 
-withInhabited :: forall a b. a -> (Inhabited a => b) -> b
+withInhabited :: forall a b. a -> ((Inhabited a) => b) -> b
 withInhabited wit k = unsafeCoerce (MagicInhabited k :: MagicInhabited a b) wit
diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -1,132 +1,182 @@
-{-# LANGUAGE CPP, ExplicitNamespaces, MultiWayIf, PatternGuards #-}
-{-# LANGUAGE TemplateHaskell, TupleSections                     #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+
 module Proof.Propositional.TH where
+
+import Control.Arrow (Kleisli (..), second)
+import Control.Monad (forM, zipWithM)
+import Data.Foldable (asum)
+import Data.Functor (void)
+import Data.Map (Map)
+import qualified Data.Map as M
+import Data.Maybe (fromJust)
+import Data.Type.Equality ((:~:) (..))
+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 (..), DForallTelescope (..), DInfo (..), DLetDec (DFunD), DPat (DConP, DVarP), DPred, DTyVarBndr (..), DType (..), Overlap (Overlapping), desugar, dsReify, expandType, substTy, sweeten)
 import Proof.Propositional.Empty
 import Proof.Propositional.Inhabited
 
-import           Control.Arrow               (Kleisli (..), second)
-import           Control.Monad               (forM, zipWithM)
-import           Data.Foldable               (asum)
-import           Data.Map                    (Map)
-import qualified Data.Map                    as M
-import           Data.Maybe                  (fromJust)
-import           Data.Semigroup              (Semigroup (..))
-import           Data.Type.Equality          ((:~:) (..))
-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)
+#if MIN_VERSION_th_desugar(1,18,0)
+import Language.Haskell.TH.Desugar (dLamE, dCaseE)
+#else
+import Language.Haskell.TH.Desugar (DMatch)
+#endif
 
--- | Macro to automatically derive @'Empty'@ instance for
---   concrete (variable-free) types which may contain products.
+mkDInstanceD ::
+  Maybe Overlap ->
+  DCxt ->
+  DType ->
+  [DDec] ->
+  DDec
+mkDInstanceD ovl ctx dtype ddecs = DInstanceD ovl Nothing ctx dtype ddecs
+
+{- | Macro to automatically derive @'Empty'@ instance for
+  concrete (variable-free) types which may contain products.
+-}
 refute :: TypeQ -> DecsQ
 refute tps = do
   tp <- expandType =<< desugar =<< tps
   let Just (_, tyName, args) = splitType tp
-      mkInst dxt cls = return $ sweeten
-                       [DInstanceD (Just Overlapping) dxt
-                        (DAppT (DConT ''Empty) (foldl DAppT (DConT tyName) args))
-                        [DLetDec $ DFunD 'eliminate cls]
-                         ]
+      mkInst dxt cls =
+        return $
+          sweeten
+            [ mkDInstanceD
+                (Just Overlapping)
+                dxt
+                (DAppT (DConT ''Empty) (foldl DAppT (DConT tyName) args))
+                [DLetDec $ DFunD 'eliminate cls]
+            ]
   if tyName == ''(:~:)
     then do
       let [l, r] = args
-      v    <- newName "_v"
+      v <- newName "_v"
       dist <- compareType l r
       case dist of
-        NonEqual    -> mkInst [] [DClause [] $ DLamE [v] (DCaseE (DVarE v) []) ]
-        Equal       -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
-        Undecidable -> fail $ "No enough info to check non-equality: " ++
-                         show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
+        NonEqual -> mkInst [] [DClause [] $ dLamE' [v] (dCaseE (DVarE v) [])]
+        Equal -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
+        Undecidable ->
+          fail $
+            "No enough info to check non-equality: "
+              ++ show (ppr $ sweeten l)
+              ++ " ~ "
+              ++ show (ppr $ sweeten r)
     else do
       (dxt, cons) <- resolveSubsts args . fromJust =<< dsReify tyName
       Just cls <- sequence <$> mapM buildRefuteClause cons
       mkInst dxt cls
 
--- | Macro to automatically derive @'Inhabited'@ instance for
---   concrete (variable-free) types which may contain sums.
+#if !MIN_VERSION_th_desugar(1,18,0)
+dCaseE :: DExp -> [DMatch] -> DExp
+dCaseE = DCaseE
+#endif
+
+dLamE' :: [Name] -> DExp -> DExp
+#if MIN_VERSION_th_desugar(1,18,0)
+dLamE' = dLamE . map DVarP
+#else
+dLamE' = DLamE
+#endif
+
+{- | Macro to automatically derive @'Inhabited'@ instance for
+  concrete (variable-free) types which may contain sums.
+-}
 prove :: TypeQ -> DecsQ
 prove tps = do
   tp <- expandType =<< desugar =<< tps
   let Just (_, tyName, args) = splitType tp
-      mkInst dxt cls = return $ sweeten
-                       [DInstanceD (Just Overlapping) dxt
-                        (DAppT (DConT ''Inhabited) (foldl DAppT (DConT tyName) args))
-                        [DLetDec $ DFunD 'trivial cls]
-                         ]
+      mkInst dxt cls =
+        return $
+          sweeten
+            [ mkDInstanceD
+                (Just Overlapping)
+                dxt
+                (DAppT (DConT ''Inhabited) (foldl DAppT (DConT tyName) args))
+                [DLetDec $ DFunD 'trivial cls]
+            ]
   isNum <- isInstance ''Num [sweeten tp]
 
-  if | isNum -> mkInst [] [DClause [] $ DLitE $ IntegerL 0 ]
-     | tyName == ''Char  -> mkInst [] [DClause [] $ DLitE $ CharL '\NUL']
-     | tyName == ''(:~:) -> do
+  if
+    | isNum -> mkInst [] [DClause [] $ DLitE $ IntegerL 0]
+    | tyName == ''Char -> mkInst [] [DClause [] $ DLitE $ CharL '\NUL']
+    | tyName == ''(:~:) -> do
         let [l, r] = args
         dist <- compareType l r
         case dist of
-          NonEqual    -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
-          Equal       -> mkInst [] [DClause [] $ DConE 'Refl ]
-          Undecidable -> fail $ "No enough info to check non-equality: " ++
-                           show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
-     | otherwise -> do
+          NonEqual -> fail $ "Equal: " ++ show (ppr $ sweeten l) ++ " ~ " ++ show (ppr $ sweeten r)
+          Equal -> mkInst [] [DClause [] $ DConE 'Refl]
+          Undecidable ->
+            fail $
+              "No enough info to check non-equality: "
+                ++ show (ppr $ sweeten l)
+                ++ " ~ "
+                ++ show (ppr $ sweeten r)
+    | otherwise -> do
         (dxt, cons) <- resolveSubsts args . fromJust =<< dsReify tyName
         Just cls <- asum <$> mapM buildProveClause cons
         mkInst dxt [cls]
 
-buildClause :: Name -> (DType -> Q b) -> (DType -> b -> DExp)
-            -> (Name -> [Maybe DExp] -> Maybe DExp) -> (Name -> [b] -> [DPat])
-            -> DCon -> Q (Maybe DClause)
+buildClause ::
+  Name ->
+  (DType -> Q b) ->
+  (DType -> b -> DExp) ->
+  (Name -> [Maybe DExp] -> Maybe DExp) ->
+  (Name -> [b] -> [DPat]) ->
+  DCon ->
+  Q (Maybe DClause)
 buildClause clsName genPlaceHolder buildFactor flattenExps toPats (DCon _ _ cName flds _) = do
   let tys = fieldsVars flds
   varDic <- mapM genPlaceHolder tys
   fmap (DClause $ toPats cName varDic) . flattenExps cName <$> zipWithM tryProc tys varDic
   where
     tryProc ty name = do
-      isEmpty <- isInstance clsName . (:[]) $ sweeten ty
-      return $ if isEmpty
-        then Just $ buildFactor ty name
-        else Nothing
+      isEmpty <- isInstance clsName . (: []) $ sweeten ty
+      return $
+        if isEmpty
+          then Just $ buildFactor ty name
+          else Nothing
 
 buildRefuteClause :: DCon -> Q (Maybe DClause)
 buildRefuteClause =
   buildClause
-    ''Empty (const $ newName "_x")
-    (const $ (DVarE 'eliminate `DAppE`) . DVarE) (const asum)
-    (\cName ps -> [DConPa cName $ map DVarPa ps])
+    ''Empty
+    (const $ newName "_x")
+    (const $ (DVarE 'eliminate `DAppE`) . DVarE)
+    (const asum)
+    (\cName ps -> [DConP cName [] $ map DVarP ps])
 
 buildProveClause :: DCon -> Q (Maybe DClause)
-buildProveClause  =
+buildProveClause =
   buildClause
-    ''Inhabited (const $ return ())
+    ''Inhabited
+    (const $ return ())
     (const $ const $ DVarE 'trivial)
-    (\ con args -> foldl DAppE (DConE con) <$> sequence args )
+    (\con args -> foldl DAppE (DConE con) <$> sequence args)
     (const $ const [])
 
 fieldsVars :: DConFields -> [DType]
-#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
+fieldsVars (DNormalC _ fs) = map snd fs
+fieldsVars (DRecC fs) = map (\(_, _, c) -> c) fs
 
 resolveSubsts :: [DType] -> DInfo -> Q (DCxt, [DCon])
 resolveSubsts args info =
   case info of
-    (DTyConI (DDataD _ cxt _ tvbs
-#if MIN_VERSION_th_desugar(1,9,0)
-              _
-#endif
-             dcons _) _) -> do
+    DTyConI (DDataD _ cxt _ tvbs _ dcons _) _ -> do
       let dic = M.fromList $ zip (map dtvbToName tvbs) args
-      (cxt , ) <$> mapM (substDCon dic) dcons
+      (cxt,) <$> mapM (substDCon dic) dcons
     -- (DTyConI (DOpenTypeFamilyD n) _) ->  return []
     -- (DTyConI (DClosedTypeFamilyD _ ddec2) minst) ->  return []
     -- (DTyConI (DDataFamilyD _ ddec2) minst) ->  return []
@@ -140,55 +190,38 @@
 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
-#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
+  (DNormalC fixi fs) =
+    DNormalC fixi
+      <$> 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 (DKindedTV n _) = n
+  DRecC <$> forM fs (\(a, b, c) -> (a,b,) <$> substTy subst c)
 
 splitType :: DType -> Maybe ([Name], Name, [DType])
-splitType (DForallT vs _ t) = (\(a,b,c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t
-splitType (DAppT t1 t2) = (\(a,b,c) -> (a, b, c ++ [t2])) <$> splitType t1
+splitType (DConstrainedT _ t) = splitType t
+splitType (DForallT (unTelescope -> vs) t) =
+  (\(a, b, c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t
+splitType (DAppT t1 t2) = (\(a, b, c) -> (a, b, c ++ [t2])) <$> splitType t1
 splitType (DSigT t _) = splitType t
 splitType (DVarT _) = Nothing
 splitType (DConT n) = Just ([], n, [])
 splitType DArrowT = Just ([], ''(->), [])
 splitType (DLitT _) = Nothing
 splitType DWildCardT = Nothing
-#if !MIN_VERSION_th_desugar(1,9,0)
-splitType DStarT = Nothing
-#endif
-
+splitType (DAppKindT _ _) = Nothing
 
 data EqlJudge = NonEqual | Undecidable | Equal
-              deriving (Read, Show, Eq, Ord)
+  deriving (Read, Show, Eq, Ord)
 
 instance Semigroup EqlJudge where
-  NonEqual    <> _        = NonEqual
+  NonEqual <> _ = NonEqual
   Undecidable <> NonEqual = NonEqual
-  Undecidable <> _        = Undecidable
-  Equal       <> m        = m
+  Undecidable <> _ = Undecidable
+  Equal <> m = m
 
 instance Monoid EqlJudge where
   mappend = (<>)
@@ -201,82 +234,86 @@
   compareType' t s
 
 compareType' :: DType -> DType -> Q EqlJudge
-compareType' (DSigT t1 t2) (DSigT s1 s2)
-  = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
-compareType' (DSigT t _) s
-  = compareType' t s
-compareType' t (DSigT s _)
-  = compareType' t s
+compareType' (DSigT t1 t2) (DSigT s1 s2) =
+  (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
+compareType' (DSigT t _) s =
+  compareType' t s
+compareType' t (DSigT s _) =
+  compareType' t s
 compareType' (DVarT t) (DVarT s)
-  | t == s    = return Equal
+  | t == s = return Equal
   | otherwise = return Undecidable
 compareType' (DVarT _) _ = return Undecidable
 compareType' _ (DVarT _) = return Undecidable
 compareType' DWildCardT _ = return Undecidable
 compareType' _ DWildCardT = return Undecidable
-compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)
+compareType' (DConstrainedT tCxt t) (DConstrainedT sCxt s) = do
+  pd <- compareCxt tCxt sCxt
+  bd <- compareType' t s
+  return (pd <> bd)
+compareType' DConstrainedT {} _ = return NonEqual
+compareType' (DForallT (unTelescope -> tTvBs) t) (DForallT (unTelescope -> sTvBs) s)
   | length tTvBs == length sTvBs = do
       let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)
       s' <- substTy dic s
-      pd <- compareCxt tCxt =<< mapM (substPred dic) sCxt
       bd <- compareType' t s'
-      return (pd <> bd)
+      return bd
   | otherwise = return NonEqual
-compareType' DForallT{} _   = return NonEqual
-compareType' (DAppT t1 t2) (DAppT s1 s2)
-  = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
+compareType' DForallT {} _ = return NonEqual
+compareType' (DAppT t1 t2) (DAppT s1 s2) =
+  (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
 compareType' (DConT t) (DConT s)
-  | t == s    = return Equal
+  | t == s = return Equal
   | otherwise = return NonEqual
 compareType' (DConT _) _ = return NonEqual
 compareType' DArrowT DArrowT = return Equal
 compareType' DArrowT _ = return NonEqual
 compareType' (DLitT t) (DLitT s)
-  | t == s    = return Equal
+  | 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
 compareCxt l r = mconcat <$> zipWithM comparePred l r
 
 comparePred :: DPred -> DPred -> Q EqlJudge
-comparePred DWildCardPr _ = return Undecidable
-comparePred _ DWildCardPr = return Undecidable
-comparePred (DVarPr l) (DVarPr r)
+comparePred DWildCardT _ = return Undecidable
+comparePred _ DWildCardT = return Undecidable
+comparePred (DVarT l) (DVarT r)
   | l == r = return Equal
-comparePred (DVarPr _) _ = return Undecidable
-comparePred _ (DVarPr _) = return Undecidable
-comparePred (DSigPr l t) (DSigPr r s) =
+comparePred (DVarT _) _ = return Undecidable
+comparePred _ (DVarT _) = return Undecidable
+comparePred (DSigT l t) (DSigT r s) =
   (<>) <$> compareType' t s <*> comparePred l r
-comparePred (DSigPr l _) r = comparePred l r
-comparePred l (DSigPr r _) = comparePred l r
-comparePred (DAppPr l1 l2) (DAppPr r1 r2) = do
+comparePred (DSigT l _) r = comparePred l r
+comparePred l (DSigT r _) = comparePred l r
+comparePred (DAppT l1 l2) (DAppT r1 r2) = do
   l2' <- expandType l2
   r2' <- expandType r2
   (<>) <$> comparePred l1 r1 <*> compareType' l2' r2'
-comparePred (DAppPr _ _) _ = return NonEqual
-comparePred (DConPr l) (DConPr r)
+comparePred (DAppT _ _) _ = return NonEqual
+comparePred (DConT l) (DConT r)
   | 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
+comparePred (DConT _) _ = return NonEqual
+comparePred (DForallT _ _) (DForallT _ _) = return Undecidable
+comparePred (DForallT {}) _ = return NonEqual
+comparePred _ _ = fail "Kind error: Expecting type-level predicate"
 
 substPred :: SubstDic -> DPred -> Q DPred
-substPred dic (DAppPr p1 p2) = DAppPr <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
-substPred dic (DSigPr p knd) = DSigPr <$> substPred dic p  <*> (expandType =<< substTy dic knd)
-substPred dic prd@(DVarPr p)
-  | Just (DVarT t) <- M.lookup p dic = return $ DVarPr t
-  | Just (DConT t) <- M.lookup p dic = return $ DConPr t
+substPred dic (DAppT p1 p2) = DAppT <$> substPred dic p1 <*> (expandType =<< substTy dic p2)
+substPred dic (DSigT p knd) = DSigT <$> substPred dic p <*> (expandType =<< substTy dic knd)
+substPred dic prd@(DVarT p)
+  | Just (DVarT t) <- M.lookup p dic = return $ DVarT t
+  | Just (DConT t) <- M.lookup p dic = return $ DConT t
   | otherwise = return prd
 substPred _ t = return t
 
-
-
+dtvbToName :: DTyVarBndr flag -> Name
+dtvbToName (DPlainTV n _) = n
+dtvbToName (DKindedTV n _ _) = n
 
+unTelescope :: DForallTelescope -> [DTyVarBndr ()]
+unTelescope (DForallVis vis) = map void vis
+unTelescope (DForallInvis vis) = map void vis
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,30 @@
+Agda-style Equational Reasoning in Haskell by Data Kinds
+=========================================================
+[![Build Status](https://travis-ci.org/konn/equational-reasoning-in-haskell.svg)](https://travis-ci.org/konn/equational-reasoning-in-haskell) [![Hackage](https://img.shields.io/hackage/v/equational-reasoning.svg)](https://hackage.haskell.org/package/equational-reasoning)
+
+What is this?
+--------------
+This library provides means to prove equations in Haskell.
+You can prove equations in Agda's EqReasoning like style.
+
+See blow for an example:
+
+```haskell
+plusZeroL :: SNat m -> Zero :+: m :=: m
+plusZeroL SZero = Refl
+plusZeroL (SSucc m) =
+  start (SZero %+ (SSucc m))
+    === SSucc (SZero %+ m)    `because`   plusSuccR SZero m
+    === SSucc m               `because`   succCongEq (plusZeroL m)
+
+```
+
+It also provides some utility functions to use an induction.
+
+For more detail, please read source codes!
+
+
+TODOs
+------
+
+* Automatic generation for induction schema for any inductive types.
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -1,39 +1,44 @@
--- Initial equational-reasoning.cabal generated by cabal init.  For further
---  documentation, see http://haskell.org/cabal/users-guide/
+cabal-version: 3.4
+name: equational-reasoning
+version: 0.7.1.0
+synopsis: Proof assistant for Haskell using DataKinds & PolyKinds
+description:
+  A simple convenient library to write equational / preorder proof as in Agda.
+  Since 0.6.0.0, this no longer depends on @singletons@ package, and the @Proof.Induction@ module goes to @equational-reasoning-induction@ package.
 
-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
+license: BSD-3-Clause
+license-file: LICENSE
+author: Hiromi ISHII
+maintainer: konn.jinro_at_gmail.com
+copyright: (c) Hiromi ISHII 2013-2020
+category: Math
+build-type: Simple
+tested-with:
+  ghc ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.4 || ==9.10.1 || ==9.12.1
 
+extra-doc-files:
+  Changelog.md
+  README.md
+
 source-repository head
-    type: git
-    location: git://github.com/konn/equational-reasoning-in-haskell.git
+  type: git
+  location: git://github.com/konn/equational-reasoning-in-haskell.git
 
 library
-  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
+  -- cabal-gild: discover ./Proof/**/*.hs --exclude Proof/Propositional/TH.hs
+  exposed-modules:
+    Proof.Equational
+    Proof.Propositional
+    Proof.Propositional.Empty
+    Proof.Propositional.Inhabited
+
+  other-modules: Proof.Propositional.TH
+  ghc-options: -Wall
+  build-depends:
+    base >=4.13 && <5,
+    containers >=0.5 && <0.8,
+    template-haskell >=2.11 && <2.24,
+    th-desugar >=1.13 && <1.19,
+    void >=0.6 && <0.8,
+
+  default-language: Haskell2010