diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs
--- a/examples/simple-arith.hs
+++ b/examples/simple-arith.hs
@@ -1,17 +1,19 @@
-{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts #-}
+{-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, ExplicitForAll, FlexibleContexts, EmptyCase #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}
+{-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-}
 module Main where
 import Data.Type.Equality
 import GHC.TypeLits       (Nat, type (<=), type (*), type (+), type (<=?), CmpNat)
 import Proof.Propositional (Empty(..))
 import Proof.Propositional (IsTrue(Witness))
 import Data.Singletons.Prelude
+import Data.Void
 
 type n <=! m = IsTrue (n <=? m)
 infix 4 <=!
 
--- natLeqZero :: (n <= 0) => proxy n -> n :~: 0
--- natLeqZero _ = Refl
+natLeqZero :: (n <= 0) => proxy n -> n :~: 0
+natLeqZero _ = Refl
 
 -- (%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)
 -- n %:<=? m = case sCompare n m of
diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal
--- a/ghc-typelits-presburger.cabal
+++ b/ghc-typelits-presburger.cabal
@@ -1,53 +1,56 @@
-name:                ghc-typelits-presburger
-version:             0.1.1.0
-synopsis:            Presburger Arithmetic Solver for GHC Type-level natural numbers.
-description: 
-  @ghc-typelits-presburger@ augments GHC type-system with Presburger Arithmetic Solver for Type-level natural numbers.
-  You can use by adding this package to @build-depends@ and add the following pragma to the head of .hs files:
-  .
-  > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger
-                  
-homepage:            https://github.com/konn/ghc-typelits-presburger#readme
-license:             BSD3
-license-file:        LICENSE
-author:              Hiromi ISHII
-maintainer:          konn.jinro _at_ gmail.com
-copyright:           2015 (c) Hiromi ISHII
-category:            Math, Type System
-build-type:          Simple
--- extra-source-files:
-cabal-version:       >=1.10
-tested-with:         GHC == 7.10.3, GHC == 8.0.1
+name: ghc-typelits-presburger
+version: 0.1.1.1
+cabal-version: >=1.10
+build-type: Simple
+license: BSD3
+license-file: LICENSE
+copyright: 2015 (c) Hiromi ISHII
+maintainer: konn.jinro _at_ gmail.com
+homepage: https://github.com/konn/ghc-typelits-presburger#readme
+synopsis: Presburger Arithmetic Solver for GHC Type-level natural numbers.
+description:
+    @ghc-typelits-presburger@ augments GHC type-system with Presburger Arithmetic Solver for Type-level natural numbers.
+    You can use by adding this package to @build-depends@ and add the following pragma to the head of .hs files:
+    .
+    > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger
+category: Math, Type System
+author: Hiromi ISHII
+tested-with: GHC ==8.0.2 GHC ==8.2.2
 
+source-repository head
+    type: git
+    location: https://github.com/konn/ghc-typelits-presburger
+
 flag examples
-    Default: False
+    default: False
 
 library
-  ghc-options:         -Wall
-  hs-source-dirs:      src
-  exposed-modules:     GHC.TypeLits.Presburger
-  other-modules:       GHC.Compat
-  build-depends:       base                >= 4.7  && < 5
-                     , ghc                 >= 7.10 && < 8.2
-                     , ghc-tcplugins-extra >= 0.2  && < 0.3
-                     , presburger          >= 1.3  && < 1.4
-                     , equational-reasoning >= 0.4.0.0
-                     , reflection
-  default-language:    Haskell2010
+    exposed-modules:
+        GHC.TypeLits.Presburger
+    build-depends:
+        base >=4.7 && <5,
+        ghc >=7.10 && <8.4,
+        ghc-tcplugins-extra ==0.2.*,
+        presburger ==1.3.*,
+        equational-reasoning >=0.4.0.0 && <0.6,
+        reflection >=2.1.2 && <2.2
+    default-language: Haskell2010
+    hs-source-dirs: src
+    other-modules:
+        GHC.Compat
+    ghc-options: -Wall
 
 executable simple-arith
-  if flag(examples)
-    buildable:         True
-  else
-    buildable:         False
-  hs-source-dirs:      examples
-  Main-is:             simple-arith.hs
-  build-depends:       base
-                     , ghc-typelits-presburger
-                     , equational-reasoning
-  default-language:    Haskell2010
-  ghc-options:         -Wall
+    
+    if !flag(examples)
+        buildable: False
+    main-is: simple-arith.hs
+    build-depends:
+        base >=4.10.1.0 && <4.11,
+        ghc-typelits-presburger >=0.1.1.1 && <0.2,
+        equational-reasoning >=0.5.0.0 && <0.6,
+        singletons >=2.3.1 && <2.4
+    default-language: Haskell2010
+    hs-source-dirs: examples
+    ghc-options: -Wall
 
-source-repository head
-  type:     git
-  location: https://github.com/konn/ghc-typelits-presburger
diff --git a/src/GHC/Compat.hs b/src/GHC/Compat.hs
--- a/src/GHC/Compat.hs
+++ b/src/GHC/Compat.hs
@@ -38,7 +38,7 @@
 import Unify      as GHC.Compat (tcUnifyTy)
 #endif
 import TcPluginM (lookupOrig)
-import Type      as GHC.Compat (isVoidTy, splitTyConApp_maybe)
+import Type      as GHC.Compat (splitTyConApp_maybe)
 import Unique    as GHC.Compat (getKey, getUnique)
 
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
@@ -71,9 +71,12 @@
   | Old.isFunTy t = Just (t1, t2)
 viewFunTy _ = Nothing
 
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 802
+#else
 pattern FunTy :: Type -> Type -> Type
 pattern FunTy t1 t2 <- (viewFunTy -> Just (t1, t2)) where
   FunTy t1 t2 = Old.mkFunTy t1 t2
+#endif
 
 tcUnifyTy :: Type -> Type -> Maybe TvSubst
 tcUnifyTy t1 t2 = fromTCv <$> Old.tcUnifyTy t1 t2
@@ -98,4 +101,4 @@
 
 decompFunTy :: Type -> [Type]
 decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2
-decompFunTy t = [t]
+decompFunTy t             = [t]
diff --git a/src/GHC/TypeLits/Presburger.hs b/src/GHC/TypeLits/Presburger.hs
--- a/src/GHC/TypeLits/Presburger.hs
+++ b/src/GHC/TypeLits/Presburger.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE FlexibleContexts, MultiWayIf, OverloadedStrings, PatternGuards #-}
-{-# LANGUAGE RankNTypes, TupleSections, ViewPatterns                        #-}
+{-# LANGUAGE RankNTypes, TupleSections                                      #-}
 module GHC.TypeLits.Presburger (plugin) where
 import GHC.Compat
 
@@ -9,7 +9,7 @@
 import           Data.Integer.SAT (assert, checkSat, noProps, toName)
 import qualified Data.Integer.SAT as SAT
 import           Data.List        (nub)
-import           Data.Maybe       (fromMaybe, isNothing, mapMaybe)
+import           Data.Maybe       (catMaybes, fromMaybe, isNothing, mapMaybe)
 import           Data.Reflection  (Given)
 import           Data.Reflection  (given)
 import           Data.Reflection  (give)
@@ -28,7 +28,7 @@
 
 isProved :: Proof -> Bool
 isProved Proved = True
-isProved _ = False
+isProved _      = False
 
 varsProp :: Prop -> [SAT.Name]
 varsProp (p :|| q) = nub $ varsProp p ++ varsProp q
@@ -36,11 +36,11 @@
 varsProp (Not p)   = varsProp p
 varsProp (e :== v) = nub $ varsExpr e ++ varsExpr v
 varsProp (e :/= v) = nub $ varsExpr e ++ varsExpr v
-varsProp (e :< v) = nub $ varsExpr e ++ varsExpr v
-varsProp (e :> v) = nub $ varsExpr e ++ varsExpr v
+varsProp (e :< v)  = nub $ varsExpr e ++ varsExpr v
+varsProp (e :> v)  = nub $ varsExpr e ++ varsExpr v
 varsProp (e :<= v) = nub $ varsExpr e ++ varsExpr v
 varsProp (e :>= v) = nub $ varsExpr e ++ varsExpr v
-varsProp _ = []
+varsProp _         = []
 
 varsExpr :: Expr -> [SAT.Name]
 varsExpr (e :+ v)   = nub $ varsExpr e ++ varsExpr v
@@ -73,6 +73,7 @@
                     , eqTyCon_      :: TyCon
                     , eqWitCon_     :: TyCon
                     , isTrueCon_    :: TyCon
+                    , voidTyCon     :: TyCon
                     }
 
 eqTyCon :: Given MyEnv => TyCon
@@ -102,6 +103,7 @@
         | Proved <- testIf prem p = (ct : ss, prem)
         | otherwise = (ss, assert' p prem)
 decidePresburger _ref gs ds ws = withTyCons $ do
+  tcPluginTrace "Env" $ ppr (emptyTyCon, eqTyCon, eqWitnessTyCon, isTrueTyCon)
   let subst = foldr unionTvSubst emptyTvSubst $ map genSubst (gs ++ ds)
   tcPluginTrace "Current subst" (ppr subst)
   tcPluginTrace "wanteds" $ ppr $ map (deconsPred) ws
@@ -116,7 +118,7 @@
                 | ct <- solved
                 , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct)
                 ]
-  tcPluginTrace "prems" (text $ show prems)
+  tcPluginTrace "prems" (text $ show $ map (toPresburgerPred subst .substTy subst . deconsPred) (gs ++ ds))
   tcPluginTrace "final goals" (text $ show $ map snd wants)
   case testIf prems (foldr (:&&) PTrue (map snd wants)) of
     Proved -> do
@@ -133,16 +135,22 @@
   eqcon <- getEqTyCon
   witcon <- getEqWitnessTyCon
   pmd <- lookupModule (mkModuleName "Proof.Propositional") (fsLit "equational-reasoning")
-  trucon <- (tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue"))
-  give (MyEnv emptyCon eqcon witcon trucon) act
+  trucon <- tcLookupTyCon =<< lookupOrig pmd (mkTcOcc "IsTrue")
+  vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")
+  voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")
+  give (MyEnv emptyCon eqcon witcon trucon voidTyCon) act
 
+isVoidTy :: Given MyEnv => Type -> Bool
+isVoidTy typ =
+  tyConAppTyCon_maybe typ == Just (voidTyCon given)
+
 (<=>) :: Prop -> Prop -> Prop
 p <=> q =  (p :&& q) :|| (Not p :&& Not q)
 
 genSubst :: Ct -> TvSubst
 genSubst ct = case classifyPredType (deconsPred ct) of
   EqPred NomEq t u -> fromMaybe emptyTvSubst $ tcUnifyTy t u
-  _ -> emptyTvSubst
+  _                -> emptyTvSubst
 
 withEv :: Ct -> (EvTerm, Ct)
 withEv ct
@@ -169,11 +177,6 @@
   , con == emptyTyCon = Not <$> toPresburgerPred subst l
   | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l =>
   , con == isTrueTyCon = toPresburgerPred subst l
-  | ts <- decompFunTy ty        -- v -> v' -> ... -> Void
-  , (args , [vd]) <- splitAt (length ts - 1) ts
-  , isVoidTy vd       = do
-      preds <- mapM (toPresburgerPred subst) args
-      return $ Not $ foldr (:&&) PTrue preds
   | otherwise = Nothing
 
 toPresburgerPredTree :: Given MyEnv => TvSubst -> PredTree -> Maybe Prop