diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,4 @@
+# Revision history for boring
+## 0
+
+- First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2017, Oleg Grenrus
+
+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 Oleg Grenrus nor the names of other
+      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/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/fin.cabal b/fin.cabal
new file mode 100644
--- /dev/null
+++ b/fin.cabal
@@ -0,0 +1,104 @@
+name:                fin
+version:             0
+synopsis:            Nat and Fin
+description:
+  This package provides two simple types, and some tools to work with them.
+  Also on type level as @DataKinds@.
+  .
+  @
+  data Nat = Z | S Nat
+  data Fin (n :: Nat) where
+    Z :: Fin n
+    S :: Fin n -> Fin ('Nat.S n)
+  @
+  .
+  The "Data.Fin.Enum" module let's work generically with enumerations.
+  .
+  Differences to other packages:
+  .
+  * [type-natural](http://hackage.haskell.org/package/type-natural) depends
+    on @singletons@ package. `fin` will try to stay light on the dependencies,
+    and support as many GHC versions as practical.
+  .
+  * [peano](http://hackage.haskell.org/package/peano) is very incomplete
+  .
+  * [nat](http://hackage.haskell.org/package/nat) as well.
+  .
+  * [PeanoWitnesses](https://hackage.haskell.org/package/PeanoWitnesses)
+    doesn't use @DataKinds@.
+  .
+  * [type-combinators](http://hackage.haskell.org/package/type-combinators)
+    is big package too.
+homepage:            https://github.com/phadej/vec
+bug-reports:         https://github.com/phadej/vec/issues
+license:             BSD3
+license-file:        LICENSE
+author:              Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:          Oleg.Grenrus <oleg.grenrus@iki.fi>
+copyright:           (c) 2017 Oleg Grenrus
+category:            Data
+build-type:          Simple
+extra-source-files:  ChangeLog.md
+cabal-version:       >=1.10
+tested-with:
+  GHC==7.8.4,
+  GHC==7.10.3,
+  GHC==8.0.2,
+  GHC==8.2.1
+
+source-repository head
+  type:      git
+  location:  https://github.com/phadej/vec.git
+
+library
+  exposed-modules:
+    Data.Fin
+    Data.Fin.Enum
+    Data.Nat
+    Data.Type.Nat
+  build-depends:
+    base     >=4.7     && <4.11,
+    deepseq  >=1.3.0.2 && <1.5,
+    hashable >=1.2.6.1 && <1.3
+
+  if !impl(ghc >= 8.0)
+    build-depends:
+      semigroups >=0.18.3 && <0.18.4
+
+  if !impl(ghc >= 7.10)
+    build-depends:
+       nats >=1     && <1.2,
+       void >=0.7.2 && <0.8
+
+  ghc-options:         -Wall -fprint-explicit-kinds
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+
+  -- dump-core
+  -- if impl(ghc >= 8.0)
+  --  build-depends: dump-core
+  --  ghc-options: -fplugin=DumpCore -fplugin-opt DumpCore:core-html
+
+test-suite inspection
+  type:                exitcode-stdio-1.0
+  main-is:             Inspection.hs
+  ghc-options:         -Wall -fprint-explicit-kinds
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+  build-depends:
+    base,
+    fin,
+    tagged,
+    inspection-testing >= 0.1.2 && <0.2
+
+  if !impl(ghc >= 8.0)
+    buildable: False
+
+  -- useful for development
+  ghc-options:
+  -- -dsuppress-idinfo
+  -- -dsuppress-coercions
+  -- -dsuppress-type-applications
+  -- -dsuppress-module-prefixes
+  -- -dsuppress-type-signatures
+  -- -dsuppress-uniques
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Fin.hs
@@ -0,0 +1,311 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE EmptyCase            #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- | Finite numbers.
+--
+-- This module is designed to be imported qualified.
+module Data.Fin (
+    Fin (..),
+    cata,
+    -- * Showing
+    explicitShow,
+    explicitShowsPrec,
+    -- * Conversions
+    toNat,
+    fromNat,
+    toNatural,
+    toInteger,
+    -- * Interesting
+    inverse,
+    universe,
+    inlineUniverse,
+    universe1,
+    inlineUniverse1,
+    absurd,
+    boring,
+    -- * Aliases
+    fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,
+    ) where
+
+import Control.DeepSeq    (NFData (..))
+import Data.Hashable      (Hashable (..))
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Proxy         (Proxy (..))
+import Data.Typeable      (Typeable)
+import GHC.Exception      (ArithException (..), throw)
+import Numeric.Natural    (Natural)
+
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Type.Nat      as N
+
+-- | Finite Numbers up to 'n'.
+data Fin (n :: N.Nat) where
+    Z :: Fin ('N.S n)
+    S :: Fin n -> Fin ('N.S n)
+  deriving (Typeable)
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+deriving instance Eq (Fin n)
+deriving instance Ord (Fin n)
+
+-- | 'Fin' is printed as 'Natural'.
+--
+-- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'
+instance Show (Fin n) where
+    showsPrec d  = showsPrec d . toNatural
+
+-- | Operations module @n@.
+--
+-- >>> map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3]
+-- [0,1,2,0,1,1]
+--
+-- >>> fromInteger 42 :: Fin N.Nat0
+-- *** Exception: divide by zero
+-- ...
+--
+-- >>> signum (Z :: Fin N.Nat1)
+-- 0
+--
+-- >>> signum (3 :: Fin N.Nat4)
+-- 1
+--
+-- >>> 2 + 3 :: Fin N.Nat4
+-- 1
+--
+-- >>> 2 * 3 :: Fin N.Nat4
+-- 2
+--
+instance N.SNatI n => Num (Fin n) where
+    abs = id
+
+    signum Z         = Z
+    signum (S Z)     = S Z
+    signum (S (S _)) = S Z
+
+    fromInteger = unsafeFromNum . (`mod` (N.reflectToNum (Proxy :: Proxy n)))
+
+    n + m = fromInteger (toInteger n + toInteger m)
+    n * m = fromInteger (toInteger n * toInteger m)
+    n - m = fromInteger (toInteger n - toInteger m)
+
+    negate = fromInteger . negate . toInteger
+
+instance N.SNatI n => Real (Fin n) where
+    toRational = cata 0 succ
+
+-- | 'quot' works only on @'Fin' n@ where @n@ is prime.
+instance N.SNatI n => Integral (Fin n) where
+    toInteger = cata 0 succ
+
+    quotRem a b = (quot a b, 0)
+    quot a b = a * inverse b
+
+-- | Multiplicative inverse.
+--
+-- Works for @'Fin' n@ where @n@ is coprime with an argument, i.e. in general when @n@ is prime.
+--
+-- >>> map inverse universe :: [Fin N.Nat5]
+-- [0,1,3,2,4]
+--
+-- >>> zipWith (*) universe (map inverse universe) :: [Fin N.Nat5]
+-- [0,1,1,1,1]
+--
+-- Adaptation of [pseudo-code in Wikipedia](https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm#Modular_integers)
+--
+inverse :: forall n. N.SNatI n => Fin n -> Fin n
+inverse = fromInteger . iter 0 n 1 . toInteger where
+    n = N.reflectToNum (Proxy :: Proxy n)
+
+    iter t _ _  0
+        | t < 0     = t + n
+        | otherwise = t
+    iter t r t' r' =
+        let q = r `div` r'
+        in iter t' r' (t - q * t') (r - q * r')
+
+instance N.SNatI n => Enum (Fin n) where
+    fromEnum = go where
+        go :: Fin m -> Int
+        go Z     = 0
+        go (S n) = succ (go n)
+
+    toEnum = unsafeFromNum
+
+instance (n ~ 'N.S m, N.SNatI m) => Bounded (Fin n) where
+    minBound = Z
+    maxBound = getMaxBound $ N.induction
+        (MaxBound Z)
+        (MaxBound . S . getMaxBound)
+
+newtype MaxBound n = MaxBound { getMaxBound :: Fin ('N.S n) }
+
+instance NFData (Fin n) where
+    rnf Z     = ()
+    rnf (S n) = rnf n
+
+instance Hashable (Fin n) where
+    hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ
+
+-------------------------------------------------------------------------------
+-- Showing
+-------------------------------------------------------------------------------
+
+-- | 'show' displaying a structure of 'Fin'.
+--
+-- >>> explicitShow (0 :: Fin N.Nat1)
+-- "Z"
+--
+-- >>> explicitShow (2 :: Fin N.Nat3)
+-- "S (S Z)"
+--
+explicitShow :: Fin n -> String
+explicitShow n = explicitShowsPrec 0 n ""
+
+-- | 'showsPrec' displaying a structure of 'Fin'.
+explicitShowsPrec :: Int -> Fin n -> ShowS
+explicitShowsPrec _ Z     = showString "Z"
+explicitShowsPrec d (S n) = showParen (d > 10)
+    $ showString "S "
+    . explicitShowsPrec 11 n
+
+-------------------------------------------------------------------------------
+-- Conversions
+-------------------------------------------------------------------------------
+
+-- | Fold 'Fin'.
+cata :: forall a n. a -> (a -> a) -> Fin n -> a
+cata z f = go where
+    go :: Fin m -> a
+    go Z = z
+    go (S n) = f (go n)
+
+-- | Convert to 'Nat'.
+toNat :: Fin n -> N.Nat
+toNat = cata N.Z N.S
+
+-- | Convert from 'Nat'.
+--
+-- >>> fromNat N.nat1 :: Maybe (Fin N.Nat2)
+-- Just 1
+--
+-- >>> fromNat N.nat1 :: Maybe (Fin N.Nat1)
+-- Nothing
+--
+fromNat :: N.SNatI n => N.Nat -> Maybe (Fin n)
+fromNat = appNatToFin (N.induction start step) where
+    start :: NatToFin 'N.Z
+    start = NatToFin $ const Nothing
+
+    step :: NatToFin n -> NatToFin ('N.S n)
+    step (NatToFin f) = NatToFin $ \n -> case n of
+        N.Z   -> Just Z
+        N.S m -> fmap S (f m)
+
+newtype NatToFin n = NatToFin { appNatToFin :: N.Nat -> Maybe (Fin n) }
+
+-- | Convert to 'Natural'.
+toNatural :: Fin n -> Natural
+toNatural = cata 0 succ
+
+-- | Convert from any 'Ord' 'Num'.
+unsafeFromNum :: forall n i. (Num i, Ord i, N.SNatI n) => i -> Fin n
+unsafeFromNum = appUnsafeFromNum (N.induction start step) where
+    start :: UnsafeFromNum i 'N.Z
+    start = UnsafeFromNum $ \n -> case compare n 0 of
+        LT -> throw Underflow
+        EQ -> throw Overflow
+        GT -> throw Overflow
+
+    step :: UnsafeFromNum i m -> UnsafeFromNum i ('N.S m)
+    step (UnsafeFromNum f) = UnsafeFromNum $ \n -> case compare n 0 of
+        EQ -> Z
+        GT -> S (f (n - 1))
+        LT -> throw Underflow
+
+newtype UnsafeFromNum i n = UnsafeFromNum { appUnsafeFromNum :: i -> Fin n }
+
+-------------------------------------------------------------------------------
+-- "Interesting" stuff
+-------------------------------------------------------------------------------
+
+-- | All values. @[minBound .. maxBound]@ won't work for @'Fin' 'N.Nat0'@.
+--
+-- >>> universe :: [Fin N.Nat3]
+-- [0,1,2]
+universe :: N.SNatI n => [Fin n]
+universe = getUniverse $ N.induction (Universe []) step where
+    step :: Universe n -> Universe ('N.S n)
+    step (Universe xs) = Universe (Z : map S xs)
+
+-- | Like 'universe' but 'NonEmpty'.
+--
+-- >>> universe1 :: NonEmpty (Fin N.Nat3)
+-- 0 :| [1,2]
+universe1 :: N.SNatI n => NonEmpty (Fin ('N.S n))
+universe1 = getUniverse1 $ N.induction (Universe1 (Z :| [])) step where
+    step :: Universe1 n -> Universe1 ('N.S n)
+    step (Universe1 xs) = Universe1 (NE.cons Z (fmap S xs))
+
+-- | 'universe' which will be fully inlined, if @n@ is known at compile time.
+--
+-- >>> inlineUniverse :: [Fin N.Nat3]
+-- [0,1,2]
+inlineUniverse :: N.InlineInduction n => [Fin n]
+inlineUniverse = getUniverse $ N.inlineInduction (Universe []) step where
+    step :: Universe n -> Universe ('N.S n)
+    step (Universe xs) = Universe (Z : map S xs)
+
+-- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3)
+-- 0 :| [1,2]
+inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('N.S n))
+inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (Z :| [])) step where
+    step :: Universe1 n -> Universe1 ('N.S n)
+    step (Universe1 xs) = Universe1 (NE.cons Z (fmap S xs))
+
+newtype Universe  n = Universe  { getUniverse  :: [Fin n] }
+newtype Universe1 n = Universe1 { getUniverse1 :: NonEmpty (Fin ('N.S n)) }
+
+-- | @'Fin' 'N.Nat0'@ is inhabited.
+absurd :: Fin N.Nat0 -> b
+absurd n = case n of {}
+
+-- | Counting to one is boring.
+--
+-- >>> boring
+-- 0
+boring :: Fin N.Nat1
+boring = Z
+
+-------------------------------------------------------------------------------
+-- Aliases
+-------------------------------------------------------------------------------
+
+fin0 :: Fin (N.Plus N.Nat0 ('N.S n))
+fin1 :: Fin (N.Plus N.Nat1 ('N.S n))
+fin2 :: Fin (N.Plus N.Nat2 ('N.S n))
+fin3 :: Fin (N.Plus N.Nat3 ('N.S n))
+fin4 :: Fin (N.Plus N.Nat4 ('N.S n))
+fin5 :: Fin (N.Plus N.Nat5 ('N.S n))
+fin6 :: Fin (N.Plus N.Nat6 ('N.S n))
+fin7 :: Fin (N.Plus N.Nat7 ('N.S n))
+fin8 :: Fin (N.Plus N.Nat8 ('N.S n))
+fin9 :: Fin (N.Plus N.Nat9 ('N.S n))
+
+fin0 = Z
+fin1 = S fin0
+fin2 = S fin1
+fin3 = S fin2
+fin4 = S fin3
+fin5 = S fin4
+fin6 = S fin5
+fin7 = S fin6
+fin8 = S fin7
+fin9 = S fin8
diff --git a/src/Data/Fin/Enum.hs b/src/Data/Fin/Enum.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Fin/Enum.hs
@@ -0,0 +1,162 @@
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+-- |
+--
+-- This module is designed to be imported qualified:
+--
+-- @
+-- import qualified Data.Fin.Enum as E
+-- @
+--
+module Data.Fin.Enum (
+    Enum (..),
+    -- * Generic implementation
+    gfrom, GFrom,
+    gto, GTo,
+    GEnumSize,
+    ) where
+
+import Prelude hiding (Enum (..))
+
+import Data.Fin     (Fin)
+import Data.Nat     (Nat)
+import Data.Proxy   (Proxy (..))
+import GHC.Generics ((:+:) (..), M1 (..), U1 (..), V1)
+
+import qualified Data.Fin      as F
+import qualified Data.Type.Nat as N
+import qualified Data.Void     as V
+import qualified GHC.Generics  as G
+
+-- | Generic enumerations.
+--
+-- /Examples:/
+--
+-- >>> from ()
+-- 0
+--
+-- >>> to 0 :: ()
+-- ()
+--
+-- >>> to 0 :: Bool
+-- False
+--
+-- >>> map to F.universe :: [Bool]
+-- [False,True]
+--
+-- >>> map (to . (+1) . from) [LT, EQ, GT] :: [Ordering] -- Num Fin is modulo arithmetic
+-- [EQ,GT,LT]
+--
+class Enum a where
+    -- | The size of an enumeration.
+    type EnumSize a :: Nat
+    type EnumSize a = GEnumSize a
+
+    -- | Converts a value to its index.
+    from :: a -> Fin (EnumSize a)
+    default from :: (G.Generic a, GFrom a, EnumSize a ~ GEnumSize a) => a -> Fin (EnumSize a)
+    from = gfrom
+
+    -- | Converts from index to the original value.
+    to :: Fin (EnumSize a) -> a
+    default to :: (G.Generic a, GTo a, EnumSize a ~ GEnumSize a) => Fin (EnumSize a) -> a
+    to = gto
+
+-- | 'Void' ~ 0
+instance Enum V.Void where
+    -- this should be written by hand to work with all @base@
+    type EnumSize V.Void = N.Nat0
+    from = V.absurd
+    to   = F.absurd
+
+-- | () ~ 1
+instance Enum ()
+
+-- | 'Bool' ~ 2
+instance Enum Bool
+
+-- | 'Ordering' ~ 3
+instance Enum Ordering
+
+-------------------------------------------------------------------------------
+-- EnumSize
+-------------------------------------------------------------------------------
+
+-- | Compute the size from the type.
+type GEnumSize a = EnumSizeRep (G.Rep a) N.Nat0
+
+type family EnumSizeRep (a :: * -> *) (n :: Nat) :: Nat where
+    EnumSizeRep (a :+: b )   n = EnumSizeRep a (EnumSizeRep b n)
+    EnumSizeRep V1           n = n
+    EnumSizeRep (M1 _d _c a) n = EnumSizeRep a n
+    EnumSizeRep U1           n = 'N.S n
+    -- No instance for K1 or :*:
+
+-------------------------------------------------------------------------------
+-- From
+-------------------------------------------------------------------------------
+
+-- | Generic version of 'from'.
+gfrom :: (G.Generic a, GFrom a) => a -> Fin (GEnumSize a)
+gfrom = \x -> gfromRep (G.from x) (error "gfrom: internal error" :: Fin N.Nat0)
+
+-- | Constraint for the class that computes 'gfrom'.
+type GFrom a = GFromRep (G.Rep a)
+
+class GFromRep (a :: * -> *)  where
+    gfromRep  :: a x     -> Fin n -> Fin (EnumSizeRep a n)
+    gfromSkip :: Proxy a -> Fin n -> Fin (EnumSizeRep a n)
+
+instance (GFromRep a, GFromRep b) => GFromRep (a :+: b) where
+    gfromRep (L1 a) n = gfromRep a (gfromSkip (Proxy :: Proxy b) n)
+    gfromRep (R1 b) n = gfromSkip (Proxy :: Proxy a) (gfromRep b n)
+
+    gfromSkip _ n = gfromSkip (Proxy :: Proxy a) (gfromSkip (Proxy :: Proxy b) n)
+
+instance GFromRep a => GFromRep (M1 d c a) where
+    gfromRep (M1 a) n = gfromRep a n
+    gfromSkip _     n = gfromSkip (Proxy :: Proxy a) n
+
+instance GFromRep V1 where
+    gfromRep  _ n = n
+    gfromSkip _ n = n
+
+instance GFromRep U1 where
+    gfromRep U1 _ = F.Z
+    gfromSkip _ n = F.S n
+
+-------------------------------------------------------------------------------
+-- To
+-------------------------------------------------------------------------------
+
+-- | Generic version of 'to'.
+gto :: (G.Generic a, GTo a) => Fin (GEnumSize a) -> a
+gto = \x -> G.to $ gtoRep x id $ F.absurd
+
+-- | Constraint for the class that computes 'gto'.
+type GTo a = GToRep (G.Rep a)
+
+class GToRep (a :: * -> *) where
+    gtoRep :: Fin (EnumSizeRep a n) -> (a x -> r) -> (Fin n -> r) -> r
+
+instance (GToRep a, GToRep b) => GToRep (a :+: b) where
+    gtoRep n s k = gtoRep n (s . L1) $ \r -> gtoRep r (s . R1) k
+
+instance GToRep a => GToRep (M1 d c a) where
+    gtoRep n s = gtoRep n (s . M1)
+
+instance GToRep V1 where
+    gtoRep n _ k = k n
+
+instance GToRep U1 where
+    gtoRep F.Z     s _ = s U1
+    gtoRep (F.S n) _ k = k n
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Nat.hs
@@ -0,0 +1,170 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+-- | 'Nat' numbers.
+--
+-- This module is designed to be imported qualified.
+--
+module Data.Nat (
+    -- * Natural, Nat numbers
+    Nat(..),
+    toNatural,
+    fromNatural,
+    cata,
+    -- * Showing
+    explicitShow,
+    explicitShowsPrec,
+    -- * Aliases
+    nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9,
+    ) where
+
+import Control.DeepSeq (NFData (..))
+import Data.Data       (Data)
+import Data.Hashable   (Hashable (..))
+import Data.Typeable   (Typeable)
+import GHC.Exception   (ArithException (..), throw)
+import Numeric.Natural (Natural)
+
+-------------------------------------------------------------------------------
+-- Nat
+-------------------------------------------------------------------------------
+
+-- | Nat natural numbers.
+--
+-- Better than GHC's built-in 'GHC.TypeLits.Nat' for some use cases.
+--
+data Nat = Z | S Nat deriving (Eq, Ord, Typeable, Data)
+
+-- | 'Nat' is printed as 'Natural'.
+--
+-- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'
+--
+instance Show Nat where
+    showsPrec d = showsPrec d . toNatural
+
+instance Num Nat where
+    fromInteger = fromNatural . fromInteger
+
+    Z   + m = m
+    S n + m = S (n + m)
+
+    Z   * _ = Z
+    S n * m = (n * m) + m
+
+    abs = id
+
+    signum Z     = Z
+    signum (S _) = S Z
+
+    negate _ = error "negate @Nat"
+
+instance Real Nat where
+    toRational = toRational . toInteger
+
+instance Integral Nat where
+    toInteger = cata 0 succ
+
+    quotRem _ Z = throw DivideByZero
+    quotRem _ _ = error "un-implemented"
+
+{- TODO: make <= with witness
+instance Ix Nat where
+    range = _
+
+    inRange = _
+-}
+
+instance Enum Nat where
+    toEnum n
+        | n < 0     = throw Underflow
+        | otherwise = iterate S Z !! n
+
+    fromEnum = cata 0 succ
+
+    succ       = S
+    pred Z     = throw Underflow
+    pred (S n) = n
+
+instance NFData Nat where
+    rnf Z     = ()
+    rnf (S n) = rnf n
+
+instance Hashable Nat where
+    hashWithSalt salt = hashWithSalt salt . toInteger
+
+-------------------------------------------------------------------------------
+-- Showing
+-------------------------------------------------------------------------------
+
+-- | 'show' displaying a structure of 'Nat'.
+--
+-- >>> explicitShow 0
+-- "Z"
+--
+-- >>> explicitShow 2
+-- "S (S Z)"
+--
+explicitShow :: Nat -> String
+explicitShow n = explicitShowsPrec 0 n ""
+
+-- | 'showsPrec' displaying a structure of 'Nat'.
+explicitShowsPrec :: Int -> Nat -> ShowS
+explicitShowsPrec _ Z     = showString "Z"
+explicitShowsPrec d (S n) = showParen (d > 10)
+    $ showString "S "
+    . explicitShowsPrec 11 n
+
+-------------------------------------------------------------------------------
+-- Conversions
+-------------------------------------------------------------------------------
+
+-- | Fold 'Nat'.
+--
+-- >>> cata [] ('x' :) 2
+-- "xx"
+--
+cata :: a -> (a -> a) -> Nat -> a
+cata z f = go where
+    go Z     = z
+    go (S n) = f (go n)
+
+-- | Convert 'Nat' to 'Natural'
+--
+-- >>> toNatural 0
+-- 0
+--
+-- >>> toNatural 2
+-- 2
+--
+-- >>> toNatural $ S $ S $ Z
+-- 2
+--
+toNatural :: Nat -> Natural
+toNatural Z = 0
+toNatural (S n) = succ (toNatural n)
+
+-- | Convert 'Natural' to 'Nat'
+--
+-- >>> fromNatural 4
+-- 4
+--
+-- >>> explicitShow (fromNatural 4)
+-- "S (S (S (S Z)))"
+--
+fromNatural :: Natural -> Nat
+fromNatural 0 = Z
+fromNatural n = S (fromNatural (pred n))
+
+-------------------------------------------------------------------------------
+-- Aliases
+-------------------------------------------------------------------------------
+
+nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9 :: Nat
+nat0 = Z
+nat1 = S nat0
+nat2 = S nat1
+nat3 = S nat2
+nat4 = S nat3
+nat5 = S nat4
+nat6 = S nat5
+nat7 = S nat6
+nat8 = S nat7
+nat9 = S nat8
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Nat.hs
@@ -0,0 +1,390 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+-- | 'Nat' numbers. @DataKinds@ stuff.
+--
+-- This module re-exports "Data.Nat", and adds type-level things.
+module Data.Type.Nat (
+    -- * Natural, Nat numbers
+    Nat(..),
+    toNatural,
+    fromNatural,
+    cata,
+    -- * Showing
+    explicitShow,
+    explicitShowsPrec,
+    -- * Singleton
+    SNat(..),
+    snatToNat,
+    snatToNatural,
+    -- * Implicit
+    SNatI(..),
+    reify,
+    reflect,
+    reflectToNum,
+    -- * Equality
+    eqNat,
+    EqNat,
+    -- * Induction
+    induction,
+    induction1,
+    InlineInduction (..),
+    inlineInduction,
+    -- ** Example: unfoldedFix
+    unfoldedFix,
+    -- * Arithmetic
+    Plus,
+    Mult,
+    -- * Conversion to GHC Nat
+    ToGHC,
+    FromGHC,
+    -- * Aliases
+    -- ** Nat
+    nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9,
+    -- ** promoted Nat
+    Nat0, Nat1, Nat2, Nat3, Nat4, Nat5, Nat6, Nat7, Nat8, Nat9,
+    -- * Proofs
+    proofPlusZeroN,
+    proofPlusNZero,
+    proofMultZeroN,
+    proofMultNZero,
+    proofMultOneN,
+    proofMultNOne,
+    )  where
+
+import Data.Function      (fix)
+import Data.Nat
+import Data.Proxy         (Proxy (..))
+import Data.Type.Equality
+import Numeric.Natural    (Natural)
+
+import qualified GHC.TypeLits as GHC
+
+import Unsafe.Coerce (unsafeCoerce)
+
+-------------------------------------------------------------------------------
+-- SNat
+-------------------------------------------------------------------------------
+
+-- | Singleton of 'Nat'.
+data SNat (n :: Nat) where
+    SZ :: SNat 'Z
+    SS :: SNatI n => SNat ('S n)
+
+deriving instance Show (SNat p)
+
+-- | Convenience class to get 'SNat'.
+class               SNatI (n :: Nat) where snat :: SNat n
+instance            SNatI 'Z         where snat = SZ
+instance SNatI n => SNatI ('S n)     where snat = SS
+
+-- | Reflect type-level 'Nat' to the term level.
+reflect :: forall n proxy. SNatI n => proxy n -> Nat
+reflect _ = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)
+
+-- | As 'reflect' but with any 'Num'.
+reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m
+reflectToNum _ = unTagged (induction1 (Tagged 0) (retagMap (1+)) :: Tagged n m)
+
+-- | Reify 'Nat'.
+--
+-- >>> reify nat3 reflect
+-- 3
+reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r
+reify Z     f = f (Proxy :: Proxy 'Z)
+reify (S n) f =  reify n (\(_p :: Proxy n) -> f (Proxy :: Proxy ('S n)))
+
+-- | Convert 'SNat' to 'Nat'.
+--
+-- >>> snatToNat (snat :: SNat Nat1)
+-- 1
+--
+snatToNat :: forall n. SNat n -> Nat
+snatToNat SZ = Z
+snatToNat SS = unTagged (induction1 (Tagged Z) (retagMap S) :: Tagged n Nat)
+
+-- | Convert 'SNat' to 'Natural'
+--
+-- >>> snatToNatural (snat :: SNat Nat0)
+-- 0
+--
+-- >>> snatToNatural (snat :: SNat Nat2)
+-- 2
+--
+snatToNatural :: forall n. SNat n -> Natural
+snatToNatural SZ = 0
+snatToNatural SS = unTagged (induction1 (Tagged 0) (retagMap succ) :: Tagged n Natural)
+
+-------------------------------------------------------------------------------
+-- Equality
+-------------------------------------------------------------------------------
+
+-- | Decide equality of type-level numbers.
+--
+-- >>> eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)
+-- Just Refl
+--
+-- >>> eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)
+-- Nothing
+--
+eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m)
+eqNat = getNatEq $ induction (NatEq start) (\p -> NatEq (step p)) where
+    start :: forall p. SNatI p => Maybe ('Z :~: p)
+    start = case snat :: SNat p of
+        SZ -> Just Refl
+        SS -> Nothing
+
+    step :: forall p q. SNatI q => NatEq p -> Maybe ('S p :~: q)
+    step hind = case snat :: SNat q of
+        SZ -> Nothing
+        SS -> step' hind
+
+    step' :: forall p q. SNatI q => NatEq p -> Maybe ('S p :~: 'S q)
+    step' (NatEq hind) = do
+        Refl <- hind :: Maybe (p :~: q)
+        return Refl
+
+newtype NatEq n = NatEq { getNatEq :: forall m. SNatI m => Maybe (n :~: m) }
+
+instance TestEquality SNat where
+    testEquality SZ SZ = Just Refl
+    testEquality SZ SS = Nothing
+    testEquality SS SZ = Nothing
+    testEquality SS SS = eqNat
+
+-- | Type family used to implement 'Data.Type.Equality.==' from "Data.Type.Equality" module.
+type family EqNat (n :: Nat) (m :: Nat) where
+    EqNat 'Z     'Z     = 'True
+    EqNat ('S n) ('S m) = EqNat n m
+    EqNat n      m      = 'False
+
+type instance n == m = EqNat n m
+
+-------------------------------------------------------------------------------
+-- Induction
+-------------------------------------------------------------------------------
+
+-- | Induction on 'Nat', functor form. Useful for computation.
+--
+-- >>> induction1 (Tagged 0) $ retagMap (+2) :: Tagged Nat3 Int
+-- Tagged 6
+--
+induction1
+    :: forall n f a. SNatI n
+    => f 'Z a                                      -- ^ zero case
+    -> (forall m. SNatI m => f m a -> f ('S m) a)  -- ^ induction step
+    -> f n a
+induction1 z f = go where
+    go :: forall m. SNatI m => f m a
+    go = case snat :: SNat m of
+        SZ -> z
+        SS -> f go
+
+-- | Induction on 'Nat'.
+--
+-- Useful in proofs or with GADTs, see source of 'proofPlusNZero'.
+induction
+    :: forall n f. SNatI n
+    => f 'Z                                    -- ^ zero case
+    -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step
+    -> f n
+induction z f = go where
+    go :: forall m. SNatI m => f m
+    go = case snat :: SNat m of
+        SZ -> z
+        SS -> f go
+
+-- | The induction will be fully inlined.
+--
+-- See @test/Inspection.hs@.
+class SNatI n => InlineInduction (n :: Nat) where
+    inlineInduction1 :: f 'Z a -> (forall m. InlineInduction m => f m a -> f ('S m) a) -> f n a
+
+instance InlineInduction 'Z where
+    inlineInduction1 z _ = z
+
+instance InlineInduction n => InlineInduction ('S n) where
+    inlineInduction1 z f = f (inlineInduction1 z f)
+
+    -- Specialise this to few first numerals.
+    {-# SPECIALIZE instance InlineInduction ('S 'Z) #-}
+    {-# SPECIALIZE instance InlineInduction ('S ('S 'Z)) #-}
+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S 'Z))) #-}
+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S 'Z)))) #-}
+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S 'Z))))) #-}
+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S 'Z)))))) #-}
+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S 'Z))))))) #-}
+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) #-}
+    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) #-}
+
+-- | See 'InlineInduction'.
+inlineInduction
+    :: forall n f. InlineInduction n
+    => f 'Z                                              -- ^ zero case
+    -> (forall m. InlineInduction m => f m -> f ('S m))  -- ^ induction step
+    -> f n
+inlineInduction z f = unConst' $ inlineInduction1 (Const' z) (Const' . f . unConst')
+
+newtype Const' (f :: Nat -> *) (n :: Nat) a = Const' { unConst' :: f n }
+
+-- | Unfold @n@ steps of a general recursion.
+--
+-- /Note:/ Always __benchmark__. This function may give you both /bad/ properties:
+-- a lot of code (increased binary size), and worse performance.
+--
+-- For known @n@ 'unfoldedFix' will unfold recursion, for example
+--
+-- @
+-- 'unfoldedFix' ('Proxy' :: 'Proxy' 'Nat3') f = f (f (f (fix f)))
+-- @
+--
+unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a
+unfoldedFix _ = getFix (inlineInduction1 start step :: Fix n a) where
+    start :: Fix 'Z a
+    start = Fix fix
+
+    step :: Fix m a -> Fix ('S m) a
+    step (Fix go) = Fix $ \f -> f (go f)
+
+newtype Fix (n :: Nat) a = Fix { getFix :: (a -> a) -> a }
+
+-------------------------------------------------------------------------------
+-- Conversion to GHC Nat
+-------------------------------------------------------------------------------
+
+-- | Convert to GHC 'GHC.Nat'.
+--
+-- >>> :kind! ToGHC Nat5
+-- ToGHC Nat5 :: GHC.Nat
+-- = 5
+--
+type family ToGHC (n :: Nat) :: GHC.Nat where
+    ToGHC 'Z     = 0
+    ToGHC ('S n) = 1 GHC.+ ToGHC n
+
+-- | Convert from GHC 'GHC.Nat'.
+--
+-- >>> :kind! FromGHC 7
+-- FromGHC 7 :: Nat
+-- = 'S ('S ('S ('S ('S ('S ('S 'Z))))))
+--
+type family FromGHC (n :: GHC.Nat) :: Nat where
+    FromGHC 0 = 'Z
+    FromGHC n = 'S (FromGHC (n GHC.- 1))
+
+-------------------------------------------------------------------------------
+-- Arithmetic
+-------------------------------------------------------------------------------
+
+-- | Addition.
+--
+-- >>> reflect (snat :: SNat (Plus Nat1 Nat2))
+-- 3
+type family Plus (n :: Nat) (m :: Nat) :: Nat where
+    Plus 'Z     m = m
+    Plus ('S n) m = 'S (Plus n m)
+
+-- | Multiplication.
+--
+-- >>> reflect (snat :: SNat (Mult Nat2 Nat3))
+-- 6
+type family Mult (n :: Nat) (m :: Nat) :: Nat where
+    Mult 'Z     m = 'Z
+    Mult ('S n) m = Plus m (Mult n m)
+
+-------------------------------------------------------------------------------
+-- Aliases
+-------------------------------------------------------------------------------
+
+type Nat0  = 'Z
+type Nat1  = 'S Nat0
+type Nat2  = 'S Nat1
+type Nat3  = 'S Nat2
+type Nat4  = 'S Nat3
+type Nat5  = 'S Nat4
+type Nat6  = 'S Nat5
+type Nat7  = 'S Nat6
+type Nat8  = 'S Nat7
+type Nat9  = 'S Nat8
+
+-------------------------------------------------------------------------------
+-- proofs
+-------------------------------------------------------------------------------
+
+-- | @0 + n = n@
+proofPlusZeroN :: Plus Nat0 n :~: n
+proofPlusZeroN = Refl
+
+-- | @n + 0 = n@
+proofPlusNZero :: SNatI n => Plus n Nat0 :~: n
+proofPlusNZero = getProofPlusNZero $ induction (ProofPlusNZero Refl) step where
+    step :: forall m. ProofPlusNZero m -> ProofPlusNZero ('S m)
+    step (ProofPlusNZero Refl) = ProofPlusNZero Refl
+
+{-# NOINLINE [1] proofPlusNZero #-}
+{-# RULES "Nat: n + 0 = n" proofPlusNZero = unsafeCoerce (Refl :: () :~: ()) #-}
+
+newtype ProofPlusNZero n = ProofPlusNZero { getProofPlusNZero :: Plus n Nat0 :~: n }
+
+-- TODO: plusAssoc
+
+-- | @0 * n = 0@
+proofMultZeroN :: Mult Nat0 n :~: Nat0
+proofMultZeroN = Refl
+
+-- | @n * 0 = n@
+proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0
+proofMultNZero _ =
+    getProofMultNZero (induction (ProofMultNZero Refl) step :: ProofMultNZero n)
+  where
+    step :: forall m. ProofMultNZero m -> ProofMultNZero ('S m)
+    step (ProofMultNZero Refl) = ProofMultNZero Refl
+
+{-# NOINLINE [1] proofMultNZero #-}
+{-# RULES "Nat: n * 0 = n" proofMultNZero = unsafeCoerce (Refl :: () :~: ()) #-}
+
+newtype ProofMultNZero n = ProofMultNZero { getProofMultNZero :: Mult n Nat0 :~: Nat0 }
+
+-- | @1 * n = n@
+proofMultOneN :: SNatI n => Mult Nat1 n :~: n
+proofMultOneN = proofPlusNZero
+
+{-# NOINLINE [1] proofMultOneN #-}
+{-# RULES "Nat: 1 * n = n" proofMultOneN = unsafeCoerce (Refl :: () :~: ()) #-}
+
+-- | @n * 1 = n@
+proofMultNOne :: SNatI n => Mult n Nat1 :~: n
+proofMultNOne = getProofMultNOne $ induction (ProofMultNOne Refl) step where
+    step :: forall m. ProofMultNOne m -> ProofMultNOne ('S m)
+    step (ProofMultNOne Refl) = ProofMultNOne Refl
+
+{-# NOINLINE [1] proofMultNOne #-}
+{-# RULES "Nat: n * 1 = n" proofMultNOne = unsafeCoerce (Refl :: () :~: ()) #-}
+
+newtype ProofMultNOne n = ProofMultNOne { getProofMultNOne :: Mult n Nat1 :~: n }
+
+-- TODO: multAssoc
+
+-------------------------------------------------------------------------------
+-- Tagged
+-------------------------------------------------------------------------------
+
+-- Own 'Tagged', to not depend on @tagged@
+--
+-- We shouldn't export this in public interface.
+newtype Tagged (n :: Nat) a = Tagged a deriving Show
+
+unTagged :: Tagged n a -> a
+unTagged (Tagged a) = a
+
+retagMap :: (a -> b) -> Tagged n a -> Tagged m b
+retagMap f = Tagged . f . unTagged
+
+-- $setup
+-- >>> :set -XTypeOperators -XDataKinds
diff --git a/test/Inspection.hs b/test/Inspection.hs
new file mode 100644
--- /dev/null
+++ b/test/Inspection.hs
@@ -0,0 +1,113 @@
+{-# LANGUAGE DeriveGeneric       #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell     #-}
+{-# LANGUAGE TypeOperators       #-}
+{-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-}
+module Main (main) where
+
+import Data.Function      (fix)
+import Data.Proxy         (Proxy (..))
+import Data.Tagged        (Tagged (..), retag)
+import Data.Type.Equality
+import GHC.Generics       (Generic)
+import Test.Inspection
+
+import qualified Data.Fin      as F
+import qualified Data.Fin.Enum as E
+import qualified Data.Type.Nat as N
+
+import Unsafe.Coerce (unsafeCoerce)
+
+-------------------------------------------------------------------------------
+-- InlineInduction
+-------------------------------------------------------------------------------
+
+-- | This doesn't evaluate compile time.
+lhsInline :: Int
+lhsInline = unTagged (N.inlineInduction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)
+
+-- | This doesn't evaluate compile time.
+lhsNormal :: Int
+lhsNormal = unTagged (N.induction1 (pure 0) (retag . fmap succ) :: Tagged N.Nat5 Int)
+
+rhs :: Int
+rhs = 5
+
+inspect $ 'lhsInline === 'rhs
+inspect $ 'lhsNormal =/= 'rhs
+
+-------------------------------------------------------------------------------
+-- Enum
+-------------------------------------------------------------------------------
+
+-- | Note: GHC 8.0 (but not GHC 8.2?) seems to be
+-- so smart, it reuses dictionary value.
+--
+-- Therefore, we define own local Ordering'
+data Ordering' = LT' | EQ' | GT' deriving (Generic)
+
+lhsEnum :: Ordering' -> F.Fin N.Nat3
+lhsEnum = E.gfrom
+
+rhsEnum :: Ordering' -> F.Fin N.Nat3
+rhsEnum LT' = F.Z
+rhsEnum EQ' = F.S F.Z
+rhsEnum GT' = F.S (F.S F.Z)
+
+inspect $ 'lhsEnum ==- 'rhsEnum
+
+-------------------------------------------------------------------------------
+-- Proofs
+-------------------------------------------------------------------------------
+
+lhsProof :: forall n. N.SNatI n => F.Fin (N.Mult n N.Nat1) -> F.Fin n
+lhsProof x = case N.proofMultNOne :: N.Mult n N.Nat1 :~: n of
+    Refl -> x
+
+rhsProof :: forall n. N.SNatI n => F.Fin (N.Mult n N.Nat1) -> F.Fin n
+rhsProof x = unsafeCoerce x
+
+inspect $ 'lhsProof ==- 'rhsProof
+
+-------------------------------------------------------------------------------
+-- unfoldedFix
+-------------------------------------------------------------------------------
+
+foldrF :: (a -> b -> b) -> b -> ([a] -> b) -> [a] -> b
+foldrF _f  z _go []     = z
+foldrF  f _z  go (x : xs) = f x (go xs)
+
+superfold :: [Int] -> Int
+superfold = N.unfoldedFix (Proxy :: Proxy N.Nat5) (foldrF (+) 0)
+
+-- Note: we need to write list explicitly, cannot use shorthand [1..4]
+-- 'enumFromTo' is a recursive function!
+--
+-- Try to change [1,2,4,] to [1..4] to see the generated core :)
+lhsFold :: Int
+lhsFold = superfold [1,2,3,4]
+
+lhsFold' :: Int
+lhsFold' = fix (foldrF (+) 0) [1,2,3,4]
+
+rhsFold :: Int
+rhsFold = 10
+
+inspect $ 'lhsFold  === 'rhsFold
+inspect $ 'lhsFold' =/= 'rhsFold
+
+lhsUnfold :: (a -> a) -> a
+lhsUnfold f = N.unfoldedFix (Proxy :: Proxy N.Nat3) f
+
+rhsUnfold :: (a -> a) -> a
+rhsUnfold f = f (f (f (fix f)))
+
+inspect $  'lhsUnfold === 'rhsUnfold
+
+-------------------------------------------------------------------------------
+-- Main to make GHC happy
+-------------------------------------------------------------------------------
+
+main :: IO ()
+main = return ()