diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs
--- a/Data/Type/Natural/Builtin.hs
+++ b/Data/Type/Natural/Builtin.hs
@@ -32,7 +32,7 @@
 
 import           Data.Singletons.Decide       (SDecide (..))
 import           Data.Singletons.Decide       (Decision (..))
-import           Data.Singletons.Prelude      (SNum (..), PNum(..), Sing (..))
+import           Data.Singletons.Prelude      (PNum (..), SNum (..), Sing (..))
 import           Data.Singletons.Prelude      (SingI (..))
 import           Data.Singletons.Prelude      (SingKind (..), SomeSing (..))
 import           Data.Singletons.Prelude.Enum (PEnum (..), SEnum (..))
@@ -52,7 +52,8 @@
 import           Proof.Equational             (coerce, withRefl)
 import           Proof.Equational             (start, sym, (===), (=~=))
 import           Proof.Equational             (because)
-import           Proof.Propositional          (Empty (..), IsTrue (..), withWitness)
+import           Proof.Propositional          (Empty (..), IsTrue (..),
+                                               withEmpty, withWitness)
 import           Unsafe.Coerce                (unsafeCoerce)
 
 -- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@.
@@ -69,11 +70,11 @@
 viewNat :: Sing (n :: TL.Nat) -> ZeroOrSucc n
 viewNat n =
   case n %~ (sing :: Sing 0) of
-    Proved _    -> IsZero
-    Disproved _ -> IsSucc (sPred n)
+    Proved Refl -> IsZero
+    Disproved t -> withEmpty t $ IsSucc (sPred n)
 
 sFromPeano :: Sing n -> Sing (FromPeano n)
-sFromPeano SZ = sing
+sFromPeano SZ      = sing
 sFromPeano (SS sn) = sSucc (sFromPeano sn)
 
 toPeanoInjective :: ToPeano n :~: ToPeano m -> n :~: m
@@ -250,9 +251,9 @@
 natSuccPred _ = Refl
 
 myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :~: (n :<= m)
-myLeqPred SZ _ = Refl
+myLeqPred SZ _          = Refl
 myLeqPred (SS _) (SS _) = Refl
-myLeqPred (SS _) SZ = Refl
+myLeqPred (SS _) SZ     = Refl
 
 toPeanoCong :: a :~: b -> ToPeano a :~: ToPeano b
 toPeanoCong Refl = Refl
@@ -281,7 +282,7 @@
 inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m + 1)) -> Sing n -> p n
 inductionNat base step sn =
   case viewNat sn of
-    IsZero -> base
+    IsZero    -> base
     IsSucc sl -> step (inductionNat base step sl)
 
 
@@ -291,7 +292,7 @@
   plusMinus _ _ = Refl
   succInj Refl = Refl
   succOneCong = Refl
-  succNonCyclic _ a = case a of { }
+  succNonCyclic _ a = case a of  _ -> error "Bug in GHC!"
   plusZeroR _ = Refl
   plusZeroL _ = Refl
   plusSuccL _ _ =  Refl
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -1,5 +1,5 @@
 name: type-natural
-version: 0.7.1.3
+version: 0.7.1.4
 cabal-version: >=1.10
 build-type: Simple
 license: BSD3
@@ -16,7 +16,7 @@
     __Use 0.5.* with ~ GHC 7.10.3__.
 category: Math
 author: Hiromi ISHII
-tested-with: GHC ==7.10.3
+tested-with: GHC ==8.0.2 GHC ==8.2.2
 
 source-repository head
     type: git
@@ -36,14 +36,14 @@
         Data.Type.Natural.Class.Arithmetic
         Data.Type.Natural.Class.Order
     build-depends:
-        base ==4.*,
-        equational-reasoning >=0.4.1.1 && <1,
+        base >=4 && <4.10,
+        equational-reasoning >=0.4.1.1 && <0.6,
         monomorphic >=0.0.3 && <0.1,
-        template-haskell >=2.8 && <3,
-        constraints >=0.3 && <0.9,
+        template-haskell >=2.8 && <2.12,
+        constraints >=0.3 && <0.10,
         ghc-typelits-natnormalise >=0.4 && <0.6,
-        ghc-typelits-presburger >=0.1.1 && <1,
-        singletons ==2.2.*
+        ghc-typelits-presburger >=0.1.1 && <0.2,
+        singletons >=2.2 && <2.4
     default-language: Haskell2010
     default-extensions: DataKinds PolyKinds ConstraintKinds GADTs
                         ScopedTypeVariables TemplateHaskell TypeFamilies TypeOperators