diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2008-2014, Bjorn Buckwalter.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above
+    copyright notice, this list of conditions and the following
+    disclaimer in the documentation and/or other materials provided
+    with the distribution.
+
+  * Neither the name of the copyright holder(s) nor the names of
+    contributors may be used to endorse or promote products derived
+    from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/Numeric/NumType/DK/Integers.hs b/Numeric/NumType/DK/Integers.hs
new file mode 100644
--- /dev/null
+++ b/Numeric/NumType/DK/Integers.hs
@@ -0,0 +1,459 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+
+{-# LANGUAGE AutoDeriveTypeable #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{- |
+   Copyright  : Copyright (C) 2006-2015 Bjorn Buckwalter
+   License    : BSD3
+
+   Maintainer : bjorn.buckwalter@gmail.com
+   Stability  : Stable
+   Portability: GHC only
+
+= Summary
+
+Type-level integers for GHC 7.8+.
+
+We provide type level arithmetic operations. We also provide term-level arithmetic operations on proxys, 
+and conversion from the type level to the term level.
+
+= Planned Obsolesence
+
+We commit this package to hackage in sure and certain hope of the coming of glorious GHC integer type literals,
+when the sea shall give up her dead, and this package shall be rendered unto obsolescence.
+
+-}
+module Numeric.NumType.DK.Integers
+(
+  -- * Type-Level Integers
+  type TypeInt(..),
+  -- * Type-level Arithmetic
+  Pred, Succ, Negate, Abs, Signum,
+  type (+), type (-), type (*), type (/), type (^),
+  -- * Arithmetic on Proxies
+  pred, succ, negate, abs, signum,
+  (+), (-), (*), (/), (^),
+  -- * Convenience Synonyms for Proxies
+  zero,
+  pos1, pos2, pos3, pos4, pos5, pos6, pos7, pos8, pos9,
+  neg1, neg2, neg3, neg4, neg5, neg6, neg7, neg8, neg9,
+  -- * Conversion from Types to Terms
+  KnownTypeInt(..)
+)
+where
+
+import Data.Proxy
+import Prelude hiding ((+), (-), (*), (/), (^), pred, succ, negate, abs, signum)
+import qualified Prelude
+
+#if MIN_VERSION_base(4, 8, 0)
+-- Use @Nat@s from @GHC.TypeLits@.
+import GHC.TypeLits hiding ((+)(), (*)(), (-)(), (^)())
+import qualified GHC.TypeLits as N
+
+type Z  = 0  -- GHC.TypeLits
+type N1 = 1  -- GHC.TypeLits
+#else
+-- Use custom @Typeable@ @Nat@s.
+import Numeric.NumType.DK.Naturals (Nat (S, Z))
+import qualified Numeric.NumType.DK.Naturals as N
+
+type N1 = 'S 'Z  -- TypeInt.DK.Nats
+#endif
+
+-- Use the same fixity for operators as the Prelude.
+infixr 8  ^
+infixl 7  *, /
+infixl 6  +, -
+
+
+-- Natural numbers
+-- ===============
+
+type family NatPred (n::Nat) :: Nat where NatPred n = n N.- N1
+type family NatSucc (n::Nat) :: Nat where NatSucc n = n N.+ N1
+
+
+-- Integers
+-- ========
+
+data TypeInt = Neg10Minus Nat  -- 10, 11, 12, 13, ...
+             | Neg9
+             | Neg8
+             | Neg7
+             | Neg6
+             | Neg5
+             | Neg4
+             | Neg3
+             | Neg2
+             | Neg1
+             | Zero -- 0
+             | Pos1
+             | Pos2
+             | Pos3
+             | Pos4
+             | Pos5
+             | Pos6
+             | Pos7
+             | Pos8
+             | Pos9
+             | Pos10Plus Nat  -- -10, -11, -12, -13, ...
+
+
+-- Unary operations
+-- ----------------
+
+type family Pred (i::TypeInt) :: TypeInt where
+  Pred ('Neg10Minus n) = 'Neg10Minus (NatSucc n)
+  Pred 'Neg9 = 'Neg10Minus Z
+  Pred 'Neg8 = 'Neg9
+  Pred 'Neg7 = 'Neg8
+  Pred 'Neg6 = 'Neg7
+  Pred 'Neg5 = 'Neg6
+  Pred 'Neg4 = 'Neg5
+  Pred 'Neg3 = 'Neg4
+  Pred 'Neg2 = 'Neg3
+  Pred 'Neg1 = 'Neg2
+  Pred 'Zero = 'Neg1
+  Pred 'Pos1 = 'Zero
+  Pred 'Pos2 = 'Pos1
+  Pred 'Pos3 = 'Pos2
+  Pred 'Pos4 = 'Pos3
+  Pred 'Pos5 = 'Pos4
+  Pred 'Pos6 = 'Pos5
+  Pred 'Pos7 = 'Pos6
+  Pred 'Pos8 = 'Pos7
+  Pred 'Pos9 = 'Pos8
+  Pred ('Pos10Plus Z) = 'Pos9
+  Pred ('Pos10Plus n) = 'Pos10Plus (NatPred n)
+
+type family Succ (i::TypeInt) :: TypeInt where
+  Succ ('Neg10Minus Z) = 'Neg9
+  Succ ('Neg10Minus n) = 'Neg10Minus (NatPred n)
+  Succ 'Neg9 = 'Neg8
+  Succ 'Neg8 = 'Neg7
+  Succ 'Neg7 = 'Neg6
+  Succ 'Neg6 = 'Neg5
+  Succ 'Neg5 = 'Neg4
+  Succ 'Neg4 = 'Neg3
+  Succ 'Neg3 = 'Neg2
+  Succ 'Neg2 = 'Neg1
+  Succ 'Neg1 = 'Zero
+  Succ 'Zero = 'Pos1
+  Succ 'Pos1 = 'Pos2
+  Succ 'Pos2 = 'Pos3
+  Succ 'Pos3 = 'Pos4
+  Succ 'Pos4 = 'Pos5
+  Succ 'Pos5 = 'Pos6
+  Succ 'Pos6 = 'Pos7
+  Succ 'Pos7 = 'Pos8
+  Succ 'Pos8 = 'Pos9
+  Succ 'Pos9 = 'Pos10Plus Z
+  Succ ('Pos10Plus n) = 'Pos10Plus (NatSucc n)
+
+-- | TypeInt negation.
+type family Negate (i::TypeInt) :: TypeInt where
+  Negate ('Neg10Minus n) = 'Pos10Plus  n
+  Negate 'Neg9 = 'Pos9
+  Negate 'Neg8 = 'Pos8
+  Negate 'Neg7 = 'Pos7
+  Negate 'Neg6 = 'Pos6
+  Negate 'Neg5 = 'Pos5
+  Negate 'Neg4 = 'Pos4
+  Negate 'Neg3 = 'Pos3
+  Negate 'Neg2 = 'Pos2
+  Negate 'Neg1 = 'Pos1
+  Negate 'Zero = 'Zero
+  Negate 'Pos1 = 'Neg1
+  Negate 'Pos2 = 'Neg2
+  Negate 'Pos3 = 'Neg3
+  Negate 'Pos4 = 'Neg4
+  Negate 'Pos5 = 'Neg5
+  Negate 'Pos6 = 'Neg6
+  Negate 'Pos7 = 'Neg7
+  Negate 'Pos8 = 'Neg8
+  Negate 'Pos9 = 'Neg9
+  Negate ('Pos10Plus  n) = 'Neg10Minus n
+
+-- | Absolute value.
+type family Abs (i::TypeInt) :: TypeInt where
+  Abs ('Neg10Minus n) = 'Pos10Plus  n
+  Abs 'Neg9 = 'Pos9
+  Abs 'Neg8 = 'Pos8
+  Abs 'Neg7 = 'Pos7
+  Abs 'Neg6 = 'Pos6
+  Abs 'Neg5 = 'Pos5
+  Abs 'Neg4 = 'Pos4
+  Abs 'Neg3 = 'Pos3
+  Abs 'Neg2 = 'Pos2
+  Abs 'Neg1 = 'Pos1
+  Abs i = i
+
+-- | Signum.
+type family Signum (i::TypeInt) :: TypeInt where
+  Signum ('Neg10Minus n) = 'Neg1
+  Signum 'Neg9 = 'Neg1
+  Signum 'Neg8 = 'Neg1
+  Signum 'Neg7 = 'Neg1
+  Signum 'Neg6 = 'Neg1
+  Signum 'Neg5 = 'Neg1
+  Signum 'Neg4 = 'Neg1
+  Signum 'Neg3 = 'Neg1
+  Signum 'Neg2 = 'Neg1
+  Signum 'Neg1 = 'Neg1
+  Signum 'Zero = 'Zero
+  Signum i = 'Pos1
+
+
+-- Binary operations
+-- -----------------
+
+-- | TypeInt addition.
+type family (i::TypeInt) + (i'::TypeInt) :: TypeInt where
+  'Zero + i = i
+  i + 'Neg10Minus n = Pred i + Succ ('Neg10Minus n)
+  i + 'Neg9 = Pred i + 'Neg8
+  i + 'Neg8 = Pred i + 'Neg7
+  i + 'Neg7 = Pred i + 'Neg6
+  i + 'Neg6 = Pred i + 'Neg5
+  i + 'Neg5 = Pred i + 'Neg4
+  i + 'Neg4 = Pred i + 'Neg3
+  i + 'Neg3 = Pred i + 'Neg2
+  i + 'Neg2 = Pred i + 'Neg1
+  i + 'Neg1 = Pred i
+  i + 'Zero = i
+  i + i' = Succ i + Pred i'  -- i + Pos
+
+-- | TypeInt subtraction.
+type family (i::TypeInt) - (i'::TypeInt) :: TypeInt where
+  i - i' = i + Negate i'
+
+-- | TypeInt multiplication.
+type family (i::TypeInt) * (i'::TypeInt) :: TypeInt
+  where
+    'Zero * i = 'Zero
+    i * 'Zero = 'Zero
+    i * 'Pos1 = i
+    i * 'Pos2 = i + i
+    i * 'Pos3 = i + i + i
+    i * 'Pos4 = i + i + i + i
+    i * 'Pos5 = i + i + i + i + i
+    i * 'Pos6 = i + i + i + i + i + i
+    i * 'Pos7 = i + i + i + i + i + i + i
+    i * 'Pos8 = i + i + i + i + i + i + i + i
+    i * 'Pos9 = i + i + i + i + i + i + i + i + i
+    i * 'Pos10Plus n = i + i * Pred ('Pos10Plus n)
+    i * i' = Negate (i * Negate i')
+
+-- | TypeInt exponentiation.
+type family (i::TypeInt) ^ (i'::TypeInt) :: TypeInt
+  where
+    i ^ 'Zero = 'Pos1
+    i ^ 'Pos1 = i
+    i ^ 'Pos2 = i * i
+    i ^ 'Pos3 = i * i * i
+    i ^ 'Pos4 = i * i * i * i
+    i ^ 'Pos5 = i * i * i * i * i
+    i ^ 'Pos6 = i * i * i * i * i * i
+    i ^ 'Pos7 = i * i * i * i * i * i * i
+    i ^ 'Pos8 = i * i * i * i * i * i * i * i
+    i ^ 'Pos9 = i * i * i * i * i * i * i * i * i
+    i ^ 'Pos10Plus n = i * i ^ Pred ('Pos10Plus n)
+
+-- | TypeInt division.
+type family (i::TypeInt) / (i'::TypeInt) :: TypeInt
+  where
+ 
+    i / 'Pos1 = i
+    i / 'Neg1 = Negate i
+    -- @Zero / n = Zero@ would allow division by zero.
+    -- @i / i = Pos1@ would allow division by zero.
+    'Zero / ('Neg10Minus n) = 'Zero
+    'Zero / 'Neg9 = 'Zero
+    'Zero / 'Neg8 = 'Zero
+    'Zero / 'Neg7 = 'Zero
+    'Zero / 'Neg6 = 'Zero
+    'Zero / 'Neg5 = 'Zero
+    'Zero / 'Neg4 = 'Zero
+    'Zero / 'Neg3 = 'Zero
+    'Zero / 'Neg2 = 'Zero
+    'Zero / 'Pos2 = 'Zero
+    'Zero / 'Pos3 = 'Zero
+    'Zero / 'Pos4 = 'Zero
+    'Zero / 'Pos5 = 'Zero
+    'Zero / 'Pos6 = 'Zero
+    'Zero / 'Pos7 = 'Zero
+    'Zero / 'Pos8 = 'Zero
+    'Zero / 'Pos9 = 'Zero
+    'Zero / ('Pos10Plus n) = 'Zero
+
+    'Neg2 / 'Neg2 = 'Pos1
+    'Neg3 / 'Neg3 = 'Pos1
+    'Neg4 / 'Neg4 = 'Pos1
+    'Neg5 / 'Neg5 = 'Pos1
+    'Neg6 / 'Neg6 = 'Pos1
+    'Neg7 / 'Neg7 = 'Pos1
+    'Neg8 / 'Neg8 = 'Pos1
+    'Neg9 / 'Neg9 = 'Pos1
+    'Neg10Minus n / 'Neg10Minus n = 'Pos1
+
+    'Neg2 / 'Pos2 = 'Neg1
+    'Neg3 / 'Pos3 = 'Neg1
+    'Neg4 / 'Pos4 = 'Neg1
+    'Neg5 / 'Pos5 = 'Neg1
+    'Neg6 / 'Pos6 = 'Neg1
+    'Neg7 / 'Pos7 = 'Neg1
+    'Neg8 / 'Pos8 = 'Neg1
+    'Neg9 / 'Pos9 = 'Neg1
+    'Neg10Minus n / 'Pos10Plus n = 'Neg1
+
+    'Pos2 / 'Neg2 = 'Neg1
+    'Pos3 / 'Neg3 = 'Neg1
+    'Pos4 / 'Neg4 = 'Neg1
+    'Pos5 / 'Neg5 = 'Neg1
+    'Pos6 / 'Neg6 = 'Neg1
+    'Pos7 / 'Neg7 = 'Neg1
+    'Pos8 / 'Neg8 = 'Neg1
+    'Pos9 / 'Neg9 = 'Neg1
+    'Pos10Plus n / 'Neg10Minus n = 'Neg1
+
+    'Pos2 / 'Pos2 = 'Pos1
+    'Pos3 / 'Pos3 = 'Pos1
+    'Pos4 / 'Pos4 = 'Pos1
+    'Pos5 / 'Pos5 = 'Pos1
+    'Pos6 / 'Pos6 = 'Pos1
+    'Pos7 / 'Pos7 = 'Pos1
+    'Pos8 / 'Pos8 = 'Pos1
+    'Pos9 / 'Pos9 = 'Pos1
+    'Pos10Plus n / 'Pos10Plus n = 'Pos1
+
+    'Neg4 / 'Neg2 = 'Pos2
+    'Neg6 / 'Neg2 = 'Pos3
+    'Neg8 / 'Neg2 = 'Pos4
+    'Neg6 / 'Neg3 = 'Pos2
+    'Neg9 / 'Neg3 = 'Pos3
+    'Neg8 / 'Neg4 = 'Pos2
+    'Neg10Minus n / i = ('Neg10Minus n + Abs i) / i - Signum i
+
+    'Neg4 / 'Pos2 = 'Neg2
+    'Neg6 / 'Pos2 = 'Neg3
+    'Neg8 / 'Pos2 = 'Neg4
+    'Neg6 / 'Pos3 = 'Neg2
+    'Neg9 / 'Pos3 = 'Neg3
+    'Neg8 / 'Pos4 = 'Neg2
+
+    'Pos4 / 'Neg2 = 'Neg2
+    'Pos6 / 'Neg2 = 'Neg3
+    'Pos8 / 'Neg2 = 'Neg4
+    'Pos6 / 'Neg3 = 'Neg2
+    'Pos9 / 'Neg3 = 'Neg3
+    'Pos8 / 'Neg4 = 'Neg2
+
+    'Pos4 / 'Pos2 = 'Pos2
+    'Pos6 / 'Pos2 = 'Pos3
+    'Pos8 / 'Pos2 = 'Pos4
+    'Pos6 / 'Pos3 = 'Pos2
+    'Pos9 / 'Pos3 = 'Pos3
+    'Pos8 / 'Pos4 = 'Pos2
+    'Pos10Plus n / i = ('Pos10Plus n - Abs i) / i + Signum i
+
+
+-- Term level
+-- ==========
+
+-- Term level operators
+-- --------------------
+
+pred   :: Proxy i -> Proxy (Pred   i); pred   _ = Proxy
+succ   :: Proxy i -> Proxy (Succ   i); succ   _ = Proxy
+negate :: Proxy i -> Proxy (Negate i); negate _ = Proxy
+abs    :: Proxy i -> Proxy (Abs    i); abs    _ = Proxy
+signum :: Proxy i -> Proxy (Signum i); signum _ = Proxy
+
+(+) :: Proxy i -> Proxy i' -> Proxy (i + i'); _ + _ = Proxy
+(-) :: Proxy i -> Proxy i' -> Proxy (i - i'); _ - _ = Proxy
+(*) :: Proxy i -> Proxy i' -> Proxy (i * i'); _ * _ = Proxy
+(/) :: Proxy i -> Proxy i' -> Proxy (i / i'); _ / _ = Proxy
+(^) :: Proxy i -> Proxy i' -> Proxy (i ^ i'); _ ^ _ = Proxy
+
+
+-- Term level TypeNats for convenience
+-- -----------------------------------
+
+neg9 :: Proxy 'Neg9
+neg9 = Proxy :: Proxy 'Neg9
+neg8 :: Proxy 'Neg8
+neg8 = Proxy :: Proxy 'Neg8
+neg7 :: Proxy 'Neg7
+neg7 = Proxy :: Proxy 'Neg7
+neg6 :: Proxy 'Neg6
+neg6 = Proxy :: Proxy 'Neg6
+neg5 :: Proxy 'Neg5
+neg5 = Proxy :: Proxy 'Neg5
+neg4 :: Proxy 'Neg4
+neg4 = Proxy :: Proxy 'Neg4
+neg3 :: Proxy 'Neg3
+neg3 = Proxy :: Proxy 'Neg3
+neg2 :: Proxy 'Neg2
+neg2 = Proxy :: Proxy 'Neg2
+neg1 :: Proxy 'Neg1
+neg1 = Proxy :: Proxy 'Neg1
+zero :: Proxy 'Zero
+zero = Proxy :: Proxy 'Zero
+pos1 :: Proxy 'Pos1
+pos1 = Proxy :: Proxy 'Pos1
+pos2 :: Proxy 'Pos2
+pos2 = Proxy :: Proxy 'Pos2
+pos3 :: Proxy 'Pos3
+pos3 = Proxy :: Proxy 'Pos3
+pos4 :: Proxy 'Pos4
+pos4 = Proxy :: Proxy 'Pos4
+pos5 :: Proxy 'Pos5
+pos5 = Proxy :: Proxy 'Pos5
+pos6 :: Proxy 'Pos6
+pos6 = Proxy :: Proxy 'Pos6
+pos7 :: Proxy 'Pos7
+pos7 = Proxy :: Proxy 'Pos7
+pos8 :: Proxy 'Pos8
+pos8 = Proxy :: Proxy 'Pos8
+pos9 :: Proxy 'Pos9
+pos9 = Proxy :: Proxy 'Pos9
+
+
+-- Reification
+-- -----------
+
+-- | Conversion to a @Num@.
+class KnownTypeInt (i::TypeInt) where toNum :: Num a => Proxy i -> a
+
+instance KnownTypeInt (Succ ('Neg10Minus n)) => KnownTypeInt ('Neg10Minus n)
+  where toNum = (Prelude.- 1) . toNum . succ
+
+instance KnownTypeInt 'Neg9 where toNum _ = -9
+instance KnownTypeInt 'Neg8 where toNum _ = -8
+instance KnownTypeInt 'Neg7 where toNum _ = -7
+instance KnownTypeInt 'Neg6 where toNum _ = -6
+instance KnownTypeInt 'Neg5 where toNum _ = -5
+instance KnownTypeInt 'Neg4 where toNum _ = -4
+instance KnownTypeInt 'Neg3 where toNum _ = -3
+instance KnownTypeInt 'Neg2 where toNum _ = -2
+instance KnownTypeInt 'Neg1 where toNum _ = -1
+instance KnownTypeInt 'Zero where toNum _ = 0
+instance KnownTypeInt 'Pos1 where toNum _ = 1
+instance KnownTypeInt 'Pos2 where toNum _ = 2
+instance KnownTypeInt 'Pos3 where toNum _ = 3
+instance KnownTypeInt 'Pos4 where toNum _ = 4
+instance KnownTypeInt 'Pos5 where toNum _ = 5
+instance KnownTypeInt 'Pos6 where toNum _ = 6
+instance KnownTypeInt 'Pos7 where toNum _ = 7
+instance KnownTypeInt 'Pos8 where toNum _ = 8
+instance KnownTypeInt 'Pos9 where toNum _ = 9
+
+instance KnownTypeInt (Pred ('Pos10Plus n)) => KnownTypeInt ('Pos10Plus n)
+  where toNum = (Prelude.+ 1) . toNum . pred
diff --git a/Numeric/NumType/DK/Naturals.hs b/Numeric/NumType/DK/Naturals.hs
new file mode 100644
--- /dev/null
+++ b/Numeric/NumType/DK/Naturals.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE AutoDeriveTypeable #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Numeric.NumType.DK.Naturals where
+
+import Prelude hiding (pred)
+
+-- Use the same fixity for operators as the Prelude.
+infixr 8  ^
+infixl 7  *
+infixl 6  +
+
+data Nat = Z | S Nat  -- Natural numbers starting at 0.
+
+-- | Nat addition.
+type family (n::Nat) + (n'::Nat) :: Nat where
+  -- Z + n = n  -- Redundant.
+  n + 'Z = n
+  n + 'S n' = 'S n + n'
+
+-- | Nat subtraction.
+type family (n::Nat) - (n'::Nat) :: Nat where
+  n - 'Z = n
+  'S n - 'S n' = n - n'
+
+-- | Nat multiplication.
+type family (n::Nat) * (n'::Nat) :: Nat
+  where
+    --Z * n = Z  -- Redundant
+    n * 'Z = 'Z
+    n * ('S n') = n + n * n'  -- i * Pos n
+
+-- | Nat exponentiation.
+type family (n::Nat) ^ (n'::Nat) :: Nat
+  where
+    --Zero ^ Pos n = Zero  -- Redundant.
+    n ^ 'Z = 'S 'Z
+    n ^ 'S n' = n * n ^ n'
+
+
+class KnownNat (n::Nat) where natVal :: proxy n -> Integer
+
+instance KnownNat 'Z where natVal _ = 0
+instance KnownNat n => KnownNat ('S n) where
+  natVal = (1 +) . natVal . pred
+    where
+      pred :: proxy ('S n) -> proxy n
+      pred = undefined
diff --git a/Numeric/NumType/DKTests.hs b/Numeric/NumType/DKTests.hs
new file mode 100644
--- /dev/null
+++ b/Numeric/NumType/DKTests.hs
@@ -0,0 +1,427 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+
+module Numeric.NumType.DKTests where
+
+import Numeric.NumType.DK.Integers
+import Prelude hiding ((*), (/), (+), (-), (^), pred, succ, negate, abs, signum)
+import qualified Prelude as P ((*), (/), (+), (-), (^), pred, succ, negate, abs, signum)
+import Data.Proxy
+import Test.HUnit
+
+-- Some “large” NumTypes.
+neg12 = pred neg11
+neg11 = pred neg10
+neg10 = pred neg9
+
+pos10 = succ pos9
+pos11 = succ pos10
+pos12 = succ pos11
+
+-- | Compares a type level unary function with a value level unary function
+  -- by converting 'NumType' to a @Num@. This assumes that the 'toNum'
+  -- function is solid.
+unaryTest :: (KnownNumType i, KnownNumType i', Num a, Eq a, Show a)
+          => (Proxy i -> Proxy i') -> (a -> a) -> Proxy i -> Test
+unaryTest f f' x = TestCase $ assertEqual
+    "Unary function Num equivalence"
+    (f' (toNum x)) (toNum (f x))
+
+-- | 'unaryTest' with @Num a@ fixed to @Integer@. This is needed by
+  -- 'testIncrDecr'.
+unaryTest' :: (KnownNumType i, KnownNumType i')
+          => (Proxy i -> Proxy i') -> (Integer -> Integer) -> Proxy i -> Test
+unaryTest' = unaryTest
+
+-- | Compares a type level binary function with a value level binary function
+  -- by converting 'NumType' to 'Num'. This assumes that the 'toNum'
+  -- function is solid.
+binaryTest :: (KnownNumType i, KnownNumType i', KnownNumType i'', Num a, Eq a, Show a)
+           => (Proxy i -> Proxy i' -> Proxy i'')
+           -> (a -> a -> a)
+           -> Proxy i -> Proxy i' -> Test
+binaryTest f f' x y = TestCase $ assertEqual
+    "Binary function Num equivalence"
+    (f' (toNum x) (toNum y)) (toNum (f x y))
+
+binaryTest' :: (KnownNumType i, KnownNumType i', KnownNumType i'', Num a, Eq a, Show a)
+           => (Proxy i -> Proxy i' -> Proxy i'')
+           -> (Integer -> Integer -> Integer)
+           -> Proxy i -> Proxy i' -> Test
+binaryTest' = binaryTest
+
+
+-- | Test that conversion to 'Num a' works as expected. This is sort of a
+  -- prerequisite for the other tests.
+testAsIntegral = TestLabel "Num equivalence tests" $ TestList
+    [ TestCase $ -12 @=? toNum neg12
+    , TestCase $ -11 @=? toNum neg11
+    , TestCase $ -10 @=? toNum neg10
+    , TestCase $  -9 @=? toNum neg9
+    , TestCase $  -8 @=? toNum neg8
+    , TestCase $  -7 @=? toNum neg7
+    , TestCase $  -6 @=? toNum neg6
+    , TestCase $  -5 @=? toNum neg5
+    , TestCase $  -4 @=? toNum neg4
+    , TestCase $  -3 @=? toNum neg3
+    , TestCase $  -2 @=? toNum neg2
+    , TestCase $  -1 @=? toNum neg1
+    , TestCase $   0 @=? toNum zero
+    , TestCase $   1 @=? toNum pos1
+    , TestCase $   2 @=? toNum pos2
+    , TestCase $   3 @=? toNum pos3
+    , TestCase $   4 @=? toNum pos4
+    , TestCase $   5 @=? toNum pos5
+    , TestCase $   6 @=? toNum pos6
+    , TestCase $   7 @=? toNum pos7
+    , TestCase $   8 @=? toNum pos8
+    , TestCase $   9 @=? toNum pos9
+    , TestCase $  10 @=? toNum pos10
+    , TestCase $  11 @=? toNum pos11
+    , TestCase $  12 @=? toNum pos12
+    ] -- By induction all other NumTypes should be good if these are.
+
+-- | Test incrementing and decrementing.
+testIncrDecr = TestLabel "Increment and decrement tests" $ TestList
+    [ t neg12
+    , t neg11
+    , t neg10
+    , t neg9
+    , t neg8
+    , t neg7
+    , t neg6
+    , t neg5
+    , t neg4
+    , t neg3
+    , t neg2
+    , t neg1
+    , t zero
+    , t pos1
+    , t pos2
+    , t pos3
+    , t pos4
+    , t pos5
+    , t pos6
+    , t pos7
+    , t pos8
+    , t pos9
+    , t pos10
+    , t pos11
+    , t pos12
+    ] where
+        t x = TestList [ unaryTest' (+ pos1) (P.+ 1) x
+                       , unaryTest' (+ neg1) (P.- 1) x
+                       , unaryTest' (\x -> x - neg1) (P.+ 1) x
+                       , unaryTest' (\x -> x - pos1) (P.- 1) x
+                       , unaryTest' pred P.pred x
+                       , unaryTest' succ P.succ x
+                       ]
+
+-- | Test negation.
+testNegate = TestLabel "Negation tests" $ TestList
+    [ unaryTest negate P.negate neg12
+    , unaryTest negate P.negate neg11
+    , unaryTest negate P.negate neg10
+    , unaryTest negate P.negate neg9
+    , unaryTest negate P.negate neg8
+    , unaryTest negate P.negate neg7
+    , unaryTest negate P.negate neg6
+    , unaryTest negate P.negate neg5
+    , unaryTest negate P.negate neg4
+    , unaryTest negate P.negate neg3
+    , unaryTest negate P.negate neg2
+    , unaryTest negate P.negate neg1
+    , unaryTest negate P.negate zero
+    , unaryTest negate P.negate pos1
+    , unaryTest negate P.negate pos2
+    , unaryTest negate P.negate pos3
+    , unaryTest negate P.negate pos4
+    , unaryTest negate P.negate pos5
+    , unaryTest negate P.negate pos6
+    , unaryTest negate P.negate pos7
+    , unaryTest negate P.negate pos8
+    , unaryTest negate P.negate pos9
+    , unaryTest negate P.negate pos10
+    , unaryTest negate P.negate pos11
+    , unaryTest negate P.negate pos12
+    ]
+
+-- | Test absolute value.
+testAbs = TestLabel "Absolute value tests" $ TestList
+    [ unaryTest abs P.abs neg12
+    , unaryTest abs P.abs neg11
+    , unaryTest abs P.abs neg10
+    , unaryTest abs P.abs neg9
+    , unaryTest abs P.abs neg8
+    , unaryTest abs P.abs neg7
+    , unaryTest abs P.abs neg6
+    , unaryTest abs P.abs neg5
+    , unaryTest abs P.abs neg4
+    , unaryTest abs P.abs neg3
+    , unaryTest abs P.abs neg2
+    , unaryTest abs P.abs neg1
+    , unaryTest abs P.abs zero
+    , unaryTest abs P.abs pos1
+    , unaryTest abs P.abs pos2
+    , unaryTest abs P.abs pos3
+    , unaryTest abs P.abs pos4
+    , unaryTest abs P.abs pos5
+    , unaryTest abs P.abs pos6
+    , unaryTest abs P.abs pos7
+    , unaryTest abs P.abs pos8
+    , unaryTest abs P.abs pos9
+    , unaryTest abs P.abs pos10
+    , unaryTest abs P.abs pos11
+    , unaryTest abs P.abs pos12
+    ]
+
+-- | Test signum.
+testSignum = TestLabel "Signum tests" $ TestList
+    [ unaryTest signum P.signum neg12
+    , unaryTest signum P.signum neg11
+    , unaryTest signum P.signum neg10
+    , unaryTest signum P.signum neg9
+    , unaryTest signum P.signum neg8
+    , unaryTest signum P.signum neg7
+    , unaryTest signum P.signum neg6
+    , unaryTest signum P.signum neg5
+    , unaryTest signum P.signum neg4
+    , unaryTest signum P.signum neg3
+    , unaryTest signum P.signum neg2
+    , unaryTest signum P.signum neg1
+    , unaryTest signum P.signum zero
+    , unaryTest signum P.signum pos1
+    , unaryTest signum P.signum pos2
+    , unaryTest signum P.signum pos3
+    , unaryTest signum P.signum pos4
+    , unaryTest signum P.signum pos5
+    , unaryTest signum P.signum pos6
+    , unaryTest signum P.signum pos7
+    , unaryTest signum P.signum pos8
+    , unaryTest signum P.signum pos9
+    , unaryTest signum P.signum pos10
+    , unaryTest signum P.signum pos11
+    , unaryTest signum P.signum pos12
+    ]
+
+-- | Test absolute value.
+testAbs = TestLabel "Absolute value tests" $ TestList
+    [ unaryTest abs P.abs neg2
+    , unaryTest abs P.abs neg1
+    , unaryTest abs P.abs zero
+    , unaryTest abs P.abs pos1
+    , unaryTest abs P.abs pos1
+    ]
+
+-- | Test signum.
+testSignum = TestLabel "Signum tests" $ TestList
+    [ unaryTest signum P.signum neg2
+    , unaryTest signum P.signum neg1
+    , unaryTest signum P.signum zero
+    , unaryTest signum P.signum pos1
+    , unaryTest signum P.signum pos1
+    ]
+
+-- | Test addition.
+testAddition = TestLabel "Addition tests" $ TestList
+    [ binaryTest (+) (P.+) pos2 pos5
+    , binaryTest (+) (P.+) pos12 pos2
+    , binaryTest (+) (P.+) pos11 pos2
+    , binaryTest (+) (P.+) pos10 pos2
+    , binaryTest (+) (P.+) pos2 pos12
+    , binaryTest (+) (P.+) pos2 pos11
+    , binaryTest (+) (P.+) pos2 pos10
+    , binaryTest (+) (P.+) neg2 pos5
+    , binaryTest (+) (P.+) pos2 neg5
+    , binaryTest (+) (P.+) neg2 neg5
+    , binaryTest (+) (P.+) neg2 neg12
+    , binaryTest (+) (P.+) neg2 neg11
+    , binaryTest (+) (P.+) neg2 neg10
+    , binaryTest (+) (P.+) neg12 neg2
+    , binaryTest (+) (P.+) neg11 neg2
+    , binaryTest (+) (P.+) neg10 neg2
+    , binaryTest (+) (P.+) zero zero
+    , binaryTest (+) (P.+) pos2 zero
+    , binaryTest (+) (P.+) neg2 zero
+    , binaryTest (+) (P.+) zero pos5
+    , binaryTest (+) (P.+) zero neg5
+    ]
+
+-- | Test subtraction.
+testSubtraction = TestLabel "Subtraction tests" $ TestList
+    [ binaryTest (-) (P.-) pos2 pos5
+    , binaryTest (-) (P.-) pos12 pos2
+    , binaryTest (-) (P.-) pos11 pos2
+    , binaryTest (-) (P.-) pos10 pos2
+    , binaryTest (-) (P.-) pos2 pos12
+    , binaryTest (-) (P.-) pos2 pos11
+    , binaryTest (-) (P.-) pos2 pos10
+    , binaryTest (-) (P.-) neg2 pos5
+    , binaryTest (-) (P.-) pos2 neg5
+    , binaryTest (-) (P.-) neg2 neg5
+    , binaryTest (-) (P.-) neg2 neg12
+    , binaryTest (-) (P.-) neg2 neg11
+    , binaryTest (-) (P.-) neg2 neg10
+    , binaryTest (-) (P.-) neg12 neg2
+    , binaryTest (-) (P.-) neg11 neg2
+    , binaryTest (-) (P.-) neg10 neg2
+    , binaryTest (-) (P.-) zero zero
+    , binaryTest (-) (P.-) pos2 zero
+    , binaryTest (-) (P.-) neg2 zero
+    , binaryTest (-) (P.-) zero pos5
+    , binaryTest (-) (P.-) zero neg5
+    ]
+
+-- | Test multiplication.
+testMultiplication = TestLabel "Multiplication tests" $ TestList
+    [ binaryTest (*) (P.*) pos2 pos5
+    , binaryTest (*) (P.*) pos12 pos2
+    , binaryTest (*) (P.*) pos11 pos2
+    , binaryTest (*) (P.*) pos10 pos2
+    , binaryTest (*) (P.*) pos2 pos12
+    , binaryTest (*) (P.*) pos2 pos11
+    , binaryTest (*) (P.*) pos2 pos10
+    , binaryTest (*) (P.*) neg2 pos5
+    , binaryTest (*) (P.*) pos2 neg5
+    , binaryTest (*) (P.*) neg2 neg5
+    , binaryTest (*) (P.*) neg2 neg12
+    , binaryTest (*) (P.*) neg2 neg11
+    , binaryTest (*) (P.*) neg2 neg10
+    , binaryTest (*) (P.*) neg12 neg2
+    , binaryTest (*) (P.*) neg11 neg2
+    , binaryTest (*) (P.*) neg10 neg2
+    , binaryTest (*) (P.*) zero zero
+    , binaryTest (*) (P.*) pos2 zero
+    , binaryTest (*) (P.*) neg2 zero
+    , binaryTest (*) (P.*) zero pos5
+    , binaryTest (*) (P.*) zero neg5
+    -- Probably some duplicates in the below.
+    , binaryTest (*) (P.*) pos10 pos2
+    , binaryTest (*) (P.*) pos9 pos3
+    , binaryTest (*) (P.*) pos8 pos4
+    , binaryTest (*) (P.*) pos8 pos2
+    , binaryTest (*) (P.*) pos6 pos3
+    , binaryTest (*) (P.*) pos6 pos2
+    , binaryTest (*) (P.*) pos4 pos2
+    , binaryTest (*) (P.*) pos9 neg3
+    , binaryTest (*) (P.*) pos8 neg4
+    , binaryTest (*) (P.*) pos8 neg2
+    , binaryTest (*) (P.*) pos6 neg3
+    , binaryTest (*) (P.*) pos6 neg2
+    , binaryTest (*) (P.*) pos4 neg2
+    , binaryTest (*) (P.*) zero pos5
+    , binaryTest (*) (P.*) zero neg3
+    , binaryTest (*) (P.*) neg4 pos2
+    , binaryTest (*) (P.*) neg6 pos2
+    , binaryTest (*) (P.*) neg6 pos3
+    , binaryTest (*) (P.*) neg8 pos2
+    , binaryTest (*) (P.*) neg8 pos4
+    , binaryTest (*) (P.*) neg9 pos3
+    , binaryTest (*) (P.*) neg4 neg2
+    , binaryTest (*) (P.*) neg6 neg2
+    , binaryTest (*) (P.*) neg6 neg3
+    , binaryTest (*) (P.*) neg8 neg2
+    , binaryTest (*) (P.*) neg8 neg4
+    , binaryTest (*) (P.*) neg9 neg3
+    , binaryTest (*) (P.*) neg12 pos4
+    ]
+
+-- | Test division.
+testDivision = TestLabel "Division tests" $ TestList
+    [ binaryTest (/) (P./) pos12 pos4
+    , binaryTest (/) (P./) pos12 neg4
+    , binaryTest (/) (P./) pos10 pos5
+    , binaryTest (/) (P./) pos10 pos2
+    , binaryTest (/) (P./) pos9 pos3
+    , binaryTest (/) (P./) pos8 pos4
+    , binaryTest (/) (P./) pos8 pos2
+    , binaryTest (/) (P./) pos6 pos3
+    , binaryTest (/) (P./) pos6 pos2
+    , binaryTest (/) (P./) pos4 pos2
+    , binaryTest (/) (P./) pos9 neg3
+    , binaryTest (/) (P./) pos8 neg4
+    , binaryTest (/) (P./) pos8 neg2
+    , binaryTest (/) (P./) pos6 neg3
+    , binaryTest (/) (P./) pos6 neg2
+    , binaryTest (/) (P./) pos4 neg2
+    , binaryTest (/) (P./) zero pos5
+    , binaryTest (/) (P./) zero neg3
+    , binaryTest (/) (P./) neg4 pos2
+    , binaryTest (/) (P./) neg6 pos2
+    , binaryTest (/) (P./) neg6 pos3
+    , binaryTest (/) (P./) neg8 pos2
+    , binaryTest (/) (P./) neg8 pos4
+    , binaryTest (/) (P./) neg9 pos3
+    , binaryTest (/) (P./) neg4 neg2
+    , binaryTest (/) (P./) neg6 neg2
+    , binaryTest (/) (P./) neg6 neg3
+    , binaryTest (/) (P./) neg8 neg2
+    , binaryTest (/) (P./) neg8 neg4
+    , binaryTest (/) (P./) neg9 neg3
+    , binaryTest (/) (P./) neg12 pos4
+    , binaryTest (/) (P./) neg12 neg4
+    , binaryTest (/) (P./) neg10 neg5
+    , binaryTest (/) (P./) neg10 neg2
+
+    , binaryTest (/) (P./) pos5 pos5
+    , binaryTest (/) (P./) neg5 pos5
+    , binaryTest (/) (P./) pos5 neg5
+    , binaryTest (/) (P./) zero neg5
+    , binaryTest (/) (P./) zero pos5
+    , binaryTest (/) (P./) pos5 pos1
+    , binaryTest (/) (P./) pos5 neg1
+
+    , binaryTest (/) (P./) pos12 pos12
+    , binaryTest (/) (P./) neg12 pos12
+    , binaryTest (/) (P./) pos12 neg12
+    , binaryTest (/) (P./) zero neg12
+    , binaryTest (/) (P./) zero pos12
+    , binaryTest (/) (P./) pos12 pos1
+    , binaryTest (/) (P./) pos12 neg1
+    ]
+
+-- | Test exponentiation.
+testExponentiation = TestLabel "Exponentiation tests" $ TestList
+    [ binaryTest (^) (P.^) pos2 pos3
+    , binaryTest (^) (P.^) zero pos5
+    , binaryTest (^) (P.^) neg2 pos3
+
+    , binaryTest (^) (P.^) pos3 pos3
+    , binaryTest (^) (P.^) pos3 pos2
+    , binaryTest (^) (P.^) pos3 pos1
+    , binaryTest (^) (P.^) pos2 pos4
+    , binaryTest (^) (P.^) pos2 pos3
+    , binaryTest (^) (P.^) pos2 pos2
+    , binaryTest (^) (P.^) pos2 pos1
+    , binaryTest (^) (P.^) pos1 pos12
+    , binaryTest (^) (P.^) pos1 pos9
+    , binaryTest (^) (P.^) pos1 zero
+
+    , binaryTest (^) (P.^) neg3 pos3
+    , binaryTest (^) (P.^) neg3 pos2
+    , binaryTest (^) (P.^) neg3 pos1
+    , binaryTest (^) (P.^) neg2 pos4
+    , binaryTest (^) (P.^) neg2 pos3
+    , binaryTest (^) (P.^) neg2 pos2
+    , binaryTest (^) (P.^) neg2 pos1
+    , binaryTest (^) (P.^) neg1 pos12
+    , binaryTest (^) (P.^) neg1 pos9
+    , binaryTest (^) (P.^) neg1 zero
+    ]
+
+-- | Collect the test cases.
+tests = TestList
+    [ testAsIntegral
+    , testIncrDecr
+    , testNegate
+    , testAbs
+    , testSignum
+    , testAddition
+    , testSubtraction
+    , testMultiplication
+    , testDivision
+    , testExponentiation
+    ]
+
+main = runTestTT tests
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,4 @@
+Experimental. Requires GHC 7.8 or later.
+
+For project information (issues, updates, wiki, examples) see:
+    http://github.com/bjornbm/numtype-dk
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/numtype-dk.cabal b/numtype-dk.cabal
new file mode 100644
--- /dev/null
+++ b/numtype-dk.cabal
@@ -0,0 +1,37 @@
+name:                numtype-dk
+version:             0.5
+license:             BSD3
+license-File:        LICENSE
+copyright:           Bjorn Buckwalter 2012-2014
+author:              Bjorn Buckwalter
+maintainer:          bjorn@buckwalter.se
+category:            Math
+stability:           provisional
+cabal-version:       >= 1.6
+build-type:          Simple
+homepage:            https://github.com/bjornbm/numtype-dk
+synopsis:            Type-level integers, using TypeNats, Data
+                     Kinds, and Closed Type Families.
+description:
+
+    This package provides type level representations of the
+    (positive and negative) integers and basic operations (addition,
+    subtraction, multiplication, division, exponentiation) on these.
+
+    The numtype-dk package differs from the numtype package in that
+    the NumTypes are implemented using Data Kinds, TypeNats, and
+    Closed Type Families rather than Functional Dependencies.
+
+    Requires GHC 7.8 or later.
+
+extra-source-files:  README,
+                     Numeric/NumType/DKTests.hs
+
+source-repository head
+  type:     git
+  location: https://github.com/bjornbm/numtype-dk/
+
+library
+  build-depends:       base < 5
+  exposed-modules:     Numeric.NumType.DK.Integers
+  other-modules:       Numeric.NumType.DK.Naturals