diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,4 +1,9 @@
 # Revision history for boring
+
+## 0.0.1
+
+- GHC-8.4.1 / base-4.11 support
+
 ## 0
 
 - First version. Released on an unsuspecting world.
diff --git a/fin.cabal b/fin.cabal
--- a/fin.cabal
+++ b/fin.cabal
@@ -1,34 +1,49 @@
 name:                fin
-version:             0
-synopsis:            Nat and Fin
+version:             0.0.1
+synopsis:            Nat and Fin: peano naturals and finite numbers
 description:
   This package provides two simple types, and some tools to work with them.
   Also on type level as @DataKinds@.
   .
   @
+  \-- Peano naturals
   data Nat = Z | S Nat
+  .
+  \-- Finite naturals
   data Fin (n :: Nat) where
-    Z :: Fin n
-    S :: Fin n -> Fin ('Nat.S n)
+  \    Z :: Fin ('S n)
+  \    S :: Fin n -> Fin ('Nat.S n)
   @
   .
+  [vec](https://hackage.haskell.org/package/vec) implements length-indexed
+  (sized) lists using this package for indexes.
+  .
   The "Data.Fin.Enum" module let's work generically with enumerations.
   .
-  Differences to other packages:
+  See [Hasochism: the pleasure and pain of dependently typed haskell programming](https://doi.org/10.1145/2503778.2503786)
+  by Sam Lindley and Conor McBride for answers to /how/ and /why/.
+  Read [APLicative Programming with Naperian Functors](https://doi.org/10.1007/978-3-662-54434-1_21)
+  by Jeremy Gibbons for (not so) different ones.
   .
-  * [type-natural](http://hackage.haskell.org/package/type-natural) depends
-    on @singletons@ package. `fin` will try to stay light on the dependencies,
+  === Similar packages
+  .
+  * [finite-typelits](https://hackage.haskell.org/package/finite-typelits)
+  . Is a great package, but uses @GHC.TypeLits@.
+  .
+  * [type-natural](https://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
+  * [peano](https://hackage.haskell.org/package/peano) is very incomplete
   .
-  * [nat](http://hackage.haskell.org/package/nat) as well.
+  * [nat](https://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)
+  * [type-combinators](https://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
@@ -44,7 +59,8 @@
   GHC==7.8.4,
   GHC==7.10.3,
   GHC==8.0.2,
-  GHC==8.2.1
+  GHC==8.2.2,
+  GHC==8.4.1
 
 source-repository head
   type:      git
@@ -57,17 +73,17 @@
     Data.Nat
     Data.Type.Nat
   build-depends:
-    base     >=4.7     && <4.11,
+    base     >=4.7     && <4.12,
     deepseq  >=1.3.0.2 && <1.5,
-    hashable >=1.2.6.1 && <1.3
+    hashable >=1.2.7.0 && <1.3
 
   if !impl(ghc >= 8.0)
     build-depends:
-      semigroups >=0.18.3 && <0.18.4
+      semigroups >=0.18.4 && <0.19
 
   if !impl(ghc >= 7.10)
     build-depends:
-       nats >=1     && <1.2,
+       nats >=1.1.2 && <1.2,
        void >=0.7.2 && <0.8
 
   ghc-options:         -Wall -fprint-explicit-kinds
@@ -89,7 +105,7 @@
     base,
     fin,
     tagged,
-    inspection-testing >= 0.1.2 && <0.2
+    inspection-testing >= 0.2.0.1 && <0.3
 
   if !impl(ghc >= 8.0)
     buildable: False
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -43,7 +43,7 @@
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Type.Nat      as N
 
--- | Finite Numbers up to 'n'.
+-- | Finite numbers: @[0..n-1]@.
 data Fin (n :: N.Nat) where
     Z :: Fin ('N.S n)
     S :: Fin n -> Fin ('N.S n)
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
--- a/src/Data/Type/Nat.hs
+++ b/src/Data/Type/Nat.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                  #-}
 {-# LANGUAGE DataKinds            #-}
 {-# LANGUAGE GADTs                #-}
 {-# LANGUAGE KindSignatures       #-}
@@ -164,7 +165,9 @@
     EqNat ('S n) ('S m) = EqNat n m
     EqNat n      m      = 'False
 
+#if !MIN_VERSION_base(4,11,0)
 type instance n == m = EqNat n m
+#endif
 
 -------------------------------------------------------------------------------
 -- Induction
diff --git a/test/Inspection.hs b/test/Inspection.hs
--- a/test/Inspection.hs
+++ b/test/Inspection.hs
@@ -106,6 +106,23 @@
 inspect $  'lhsUnfold === 'rhsUnfold
 
 -------------------------------------------------------------------------------
+-- Power
+-------------------------------------------------------------------------------
+
+power :: forall n. N.InlineInduction n => Proxy n -> Int -> Int
+power _ k = unTagged impl where
+    impl :: Tagged n Int
+    impl = N.inlineInduction1 (Tagged 1) $ \(Tagged rec') -> Tagged (rec' * k)
+
+lhsPower5 :: Int -> Int
+lhsPower5 = power (Proxy :: Proxy N.Nat5)
+
+rhsPower5 :: Int -> Int
+rhsPower5 k = k * k * k * k * k
+
+inspect $ 'lhsPower5 === 'rhsPower5
+
+-------------------------------------------------------------------------------
 -- Main to make GHC happy
 -------------------------------------------------------------------------------