diff --git a/Proof/Propositional/TH.hs b/Proof/Propositional/TH.hs
--- a/Proof/Propositional/TH.hs
+++ b/Proof/Propositional/TH.hs
@@ -186,7 +186,13 @@
 dtvbToName (DKindedTV n _) = n
 
 splitType :: DType -> Maybe ([Name], Name, [DType])
-splitType (DForallT vs _ t) = (\(a,b,c) -> (map dtvbToName vs ++ a, b, c)) <$> splitType t
+#if MIN_VERSION_th_desugar(1,11,0)
+splitType (DConstrainedT _ t) = splitType t
+splitType (DForallT _ vs t) 
+#else
+splitType (DForallT vs _ t) 
+#endif
+  = (\(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
@@ -234,6 +240,20 @@
 compareType' _ (DVarT _) = return Undecidable
 compareType' DWildCardT _ = return Undecidable
 compareType' _ DWildCardT = return Undecidable
+#if MIN_VERSION_th_desugar(1,11,0)
+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 _ tTvBs t) (DForallT _ sTvBs s)
+  | length tTvBs == length sTvBs = do
+      let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)
+      s' <- substTy dic s
+      bd <- compareType' t s'
+      return bd
+  | otherwise = return NonEqual
+#else
 compareType' (DForallT tTvBs tCxt t) (DForallT sTvBs sCxt s)
   | length tTvBs == length sTvBs = do
       let dic = M.fromList $ zip (map dtvbToName sTvBs) (map (DVarT . dtvbToName) tTvBs)
@@ -242,6 +262,7 @@
       bd <- compareType' t s'
       return (pd <> bd)
   | otherwise = return NonEqual
+#endif
 compareType' DForallT{} _   = return NonEqual
 compareType' (DAppT t1 t2) (DAppT s1 s2)
   = (<>) <$> compareType' t1 s1 <*> compareType' t2 s2
diff --git a/equational-reasoning.cabal b/equational-reasoning.cabal
--- a/equational-reasoning.cabal
+++ b/equational-reasoning.cabal
@@ -2,7 +2,7 @@
 --  documentation, see http://haskell.org/cabal/users-guide/
 
 name:                equational-reasoning
-version:             0.6.0.1
+version:             0.6.0.2
 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.
@@ -32,7 +32,7 @@
                      , th-extras        == 0.0.*
                      , void             >= 0.6    && < 0.8
   if impl(ghc >= 8.4)
-     build-depends:    th-desugar       >= 1.8 && < 1.11
+     build-depends:    th-desugar       >= 1.8 && < 1.12
   else
      build-depends:    semigroups       == 0.18.*
      build-depends:    th-desugar       >= 1.6 && < 1.8