diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,6 +1,13 @@
 typelits-witnesses
 ==================
 
+[![typelits-witnesses on Stackage LTS 2](http://stackage.org/package/typelits-witnesses/badge/lts-2)](http://stackage.org/lts-2/package/typelits-witnesses)
+[![typelits-witnesses on Stackage LTS 3](http://stackage.org/package/typelits-witnesses/badge/lts-3)](http://stackage.org/lts-3/package/typelits-witnesses)
+[![typelits-witnesses on Stackage LTS 4](http://stackage.org/package/typelits-witnesses/badge/lts-4)](http://stackage.org/lts-4/package/typelits-witnesses)
+[![typelits-witnesses on Stackage LTS](http://stackage.org/package/typelits-witnesses/badge/lts)](http://stackage.org/lts/package/typelits-witnesses)
+[![typelits-witnesses on Stackage Nightly](http://stackage.org/package/typelits-witnesses/badge/nightly)](http://stackage.org/nightly/package/typelits-witnesses)
+
+
 Provides witnesses for `KnownNat` and `KnownSymbol` instances for various
 operations on GHC TypeLits --- in particular, the arithmetic operations
 defined in `GHC.TypeLits`, and also for type-level lists of `KnownNat` and
@@ -131,6 +138,19 @@
 2
 3
 ~~~
+
+Another thing you can do is provide witneses that two `[Nat]`s or `[Symbol]`s
+are the same/were instantiated with the same numbers/symbols.
+
+~~~haskell
+> reifyNats [1,2,3] $ \ns -> do
+  reifyNats [1,2,3] $ \ms -> do
+    case sameNats ns ms of
+      Just Refl -> -- in this branch, ns and ms are the same.
+      Nothing   -> -- in this branch, they aren't
+~~~
+
+The above would match on the `Just Refl` branch.
 
 See module documentation for more details and variations.
 
diff --git a/src/GHC/TypeLits/List.hs b/src/GHC/TypeLits/List.hs
--- a/src/GHC/TypeLits/List.hs
+++ b/src/GHC/TypeLits/List.hs
@@ -29,33 +29,42 @@
 -- existential types for dependent typing usage, and as an analogy with
 -- 'SomeNat' and 'SomeSymbol'.
 --
--- See typeclass documentations for more information.
+-- See typeclass documentations and README for more information.
 
 module GHC.TypeLits.List (
-  -- * @KnownNats@
+  -- * 'KnownNats'
     KnownNats(..)
   , SomeNats(..)
   , NatList(..)
   , someNatsVal
   , someNatsVal'
   , reifyNats
+  , sameNats
+  -- ** Traversals
   , traverseNatList
   , traverseNatList'
   , traverseNatList_
+  -- *** Maps
   , mapNatList
-  -- * @KnownSymbols@
+  , mapNatList'
+  -- * 'KnownSymbols'
   , KnownSymbols(..)
   , SomeSymbols(..)
   , SymbolList(..)
   , someSymbolsVal
   , reifySymbols
+  , sameSymbols
+  -- ** Traversals
   , traverseSymbolList
   , traverseSymbolList'
   , traverseSymbolList_
+  -- *** Maps
   , mapSymbolList
+  , mapSymbolList'
   ) where
 
 import Data.Proxy
+import Data.Type.Equality
 import Data.Reflection
 import GHC.TypeLits
 import Data.Functor.Identity
@@ -112,10 +121,11 @@
 -- a new one, in a 'SomeNat'.
 --
 -- Can be considered a form of a @Traversal' 'SomeNat' 'SomeNats'@.
-traverseNatList :: forall f ns. Applicative f
-                => (forall n. KnownNat n => Proxy n -> f SomeNat)
-                -> NatList ns
-                -> f SomeNats
+traverseNatList
+    :: forall f ns. Applicative f
+    => (forall n. KnownNat n => Proxy n -> f SomeNat)
+    -> NatList ns
+    -> f SomeNats
 traverseNatList f = go
   where
     go :: forall ms. NatList ms -> f SomeNats
@@ -129,13 +139,14 @@
                          SomeNats is ->
                            SomeNats (i :<# is)
 
--- | Like 'traverseNatList', but literally actually a
--- @Traversal' 'SomeNat' 'SomeNats'@, so is usable with lens-library
+-- | Like 'traverseNatList', but literally actually a @Traversal' 'SomeNat'
+-- 'SomeNats'@, avoiding the Rank-2 types, so is usable with lens-library
 -- machinery.
-traverseNatList' :: forall f. Applicative f
-                 => (SomeNat -> f SomeNat)
-                 -> SomeNats
-                 -> f SomeNats
+traverseNatList'
+    :: forall f. Applicative f
+    => (SomeNat -> f SomeNat)
+    -> SomeNats
+    -> f SomeNats
 traverseNatList' f ns =
     case ns of
       SomeNats ns' -> traverseNatList (f . SomeNat) ns'
@@ -143,10 +154,11 @@
 -- | Utility function for traversing over all of the @'Proxy' n@s in
 -- a 'NatList', each with the corresponding 'KnownNat' instance available.
 -- Results are ignored.
-traverseNatList_ :: forall f a ns. Applicative f
-                 => (forall n. KnownNat n => Proxy n -> f a)
-                 -> NatList ns
-                 -> f ()
+traverseNatList_
+    :: forall f a ns. Applicative f
+    => (forall n. KnownNat n => Proxy n -> f a)
+    -> NatList ns
+    -> f ()
 traverseNatList_ f = go
   where
     go :: forall ms. NatList ms -> f ()
@@ -156,11 +168,21 @@
 
 -- | Utility function for \"mapping\" over each of the 'Nat's in the
 -- 'NatList'.
-mapNatList :: (forall n. KnownNat n => Proxy n -> SomeNat)
-           -> NatList ns
-           -> SomeNats
+mapNatList
+    :: (forall n. KnownNat n => Proxy n -> SomeNat)
+    -> NatList ns
+    -> SomeNats
 mapNatList f = runIdentity . traverseNatList (Identity . f)
 
+-- | Like 'mapNatList', but avoids the Rank-2 types, so can be used with
+-- '.' (function composition) and in other situations where 'mapNatList'
+-- would cause problems.
+mapNatList'
+    :: (SomeNat -> SomeNat)
+    -> SomeNats
+    -> SomeNats
+mapNatList' f = runIdentity . traverseNatList' (Identity . f)
+
 -- | List equivalent of 'someNatVal'.  Convert a list of integers into an
 -- unknown type-level list of naturals.  Will return 'Nothing' if any of
 -- the given 'Integer's is negative.
@@ -191,6 +213,38 @@
 someNatsVal' :: [Integer] -> SomeNats
 someNatsVal' ns = reifyNats ns SomeNats
 
+-- | Get evidence that the two 'KnownNats' lists are actually the "same"
+-- list of 'Nat's (that they were instantiated with the same numbers).
+--
+-- Essentialy runs 'sameNat' over the lists:
+--
+-- @
+-- case 'sameNats' ns ms of
+--   Just 'Refl' -> -- in this branch, GHC recognizes that the two ['Nat']s
+--                  -- are the same.
+--   Nothing     -> -- in this branch, they aren't
+-- @
+sameNats
+    :: (KnownNats ns, KnownNats ms)
+    => NatList ns
+    -> NatList ms
+    -> Maybe (ns :~: ms)
+sameNats ns ms =
+    case ns of
+      ØNL ->
+        case ms of
+          ØNL     -> Just Refl
+          _ :<# _ -> Nothing
+      n :<# ns' ->
+        case ms of
+          ØNL     -> Nothing
+          m :<# ms' -> do
+            Refl <- sameNat n m
+            Refl <- sameNats ns' ms'
+            return Refl
+
+
+
 -- | @'KnownSymbols' ns@ is intended to represent that every 'Symbol' in the
 -- type-level list 'ns' is itself a 'KnownSymbol' (meaning, you can use
 -- 'symbolVal' to get its corresponding 'String').
@@ -239,10 +293,11 @@
 -- number to a new one, in a 'SomeSymbol'.
 --
 -- Can be considered a form of a @Traversal' 'SomeSymbol' 'SomeSymbols'@.
-traverseSymbolList :: forall f ns. Applicative f
-                   => (forall n. KnownSymbol n => Proxy n -> f SomeSymbol)
-                   -> SymbolList ns
-                   -> f SomeSymbols
+traverseSymbolList
+    :: forall f ns. Applicative f
+    => (forall n. KnownSymbol n => Proxy n -> f SomeSymbol)
+    -> SymbolList ns
+    -> f SomeSymbols
 traverseSymbolList f = go
   where
     go :: forall ms. SymbolList ms -> f SomeSymbols
@@ -257,12 +312,13 @@
                          SomeSymbols (ps :<$ sl')
 
 -- | Like 'traverseSymbolList', but literally actually a
--- @Traversal' 'SomeSymbol' 'SomeSymbols'@, so is usable with lens-library
--- machinery.
-traverseSymbolList' :: forall f. Applicative f
-                 => (SomeSymbol -> f SomeSymbol)
-                 -> SomeSymbols
-                 -> f SomeSymbols
+-- @Traversal' 'SomeSymbol' 'SomeSymbols'@, avoiding the Rank-2 types, so
+-- is usable with lens-library machinery.
+traverseSymbolList'
+    :: forall f. Applicative f
+    => (SomeSymbol -> f SomeSymbol)
+    -> SomeSymbols
+    -> f SomeSymbols
 traverseSymbolList' f ns =
     case ns of
       SomeSymbols ns' -> traverseSymbolList (f . SomeSymbol) ns'
@@ -270,10 +326,11 @@
 -- | Utility function for traversing over all of the @'Proxy' n@s in
 -- a 'SymbolList', each with the corresponding 'KnownSymbol' instance
 -- available. Results are ignored.
-traverseSymbolList_ :: forall f ns. Applicative f
-                    => (forall n a. KnownSymbol n => Proxy n -> f a)
-                    -> SymbolList ns
-                    -> f ()
+traverseSymbolList_
+    :: forall f ns. Applicative f
+    => (forall n a. KnownSymbol n => Proxy n -> f a)
+    -> SymbolList ns
+    -> f ()
 traverseSymbolList_ f = go
   where
     go :: forall ms. SymbolList ms -> f ()
@@ -283,11 +340,21 @@
 
 -- | Utility function for \"mapping\" over each of the 'Symbol's in the
 -- 'SymbolList'.
-mapSymbolList :: (forall n. KnownSymbol n => Proxy n -> SomeSymbol)
-              -> SymbolList ns
-              -> SomeSymbols
+mapSymbolList
+    :: (forall n. KnownSymbol n => Proxy n -> SomeSymbol)
+    -> SymbolList ns
+    -> SomeSymbols
 mapSymbolList f = runIdentity . traverseSymbolList (Identity . f)
 
+-- | Like 'mapSymbolList', but avoids the Rank-2 types, so can be used with
+-- '.' (function composition) and in other situations where 'mapSymbolList'
+-- would cause problems.
+mapSymbolList'
+    :: (SomeSymbol -> SomeSymbol)
+    -> SomeSymbols
+    -> SomeSymbols
+mapSymbolList' f = runIdentity . traverseSymbolList' (Identity . f)
+
 -- | List equivalent of 'someNatVal'.  Convert a list of integers into an
 -- unknown type-level list of naturals.  Will return 'Nothing' if any of
 -- the given 'Integer's is negative.
@@ -312,3 +379,33 @@
 reifySymbols (n:ns) f = reifySymbol n $ \m ->
                           reifySymbols ns $ \ms ->
                             f (m :<$ ms)
+
+-- | Get evidence that the two 'KnownSymbols' lists are actually the "same"
+-- list of 'Symboles's (that they were instantiated with the same strings).
+--
+-- Essentialy runs 'sameSymbol' over the lists:
+--
+-- @
+-- case 'sameSymbols' ns ms of
+--   Just 'Refl' -> -- in this branch, GHC recognizes that the
+--                  -- two ['Symbol']s are the same
+--   Nothing     -> -- in this branch, they aren't
+-- @
+sameSymbols
+    :: (KnownSymbols ns, KnownSymbols ms)
+    => SymbolList ns
+    -> SymbolList ms
+    -> Maybe (ns :~: ms)
+sameSymbols ns ms =
+    case ns of
+      ØSL ->
+        case ms of
+          ØSL     -> Just Refl
+          _ :<$ _ -> Nothing
+      n :<$ ns' ->
+        case ms of
+          ØSL     -> Nothing
+          m :<$ ms' -> do
+            Refl <- sameSymbol n m
+            Refl <- sameSymbols ns' ms'
+            return Refl
diff --git a/src/GHC/TypeLits/Witnesses.hs b/src/GHC/TypeLits/Witnesses.hs
--- a/src/GHC/TypeLits/Witnesses.hs
+++ b/src/GHC/TypeLits/Witnesses.hs
@@ -189,12 +189,13 @@
 -- are set to match that of normal addition and multiplication, etc.)
 --
 --
-withNatOp :: (KnownNat n, KnownNat m)
-          => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q))
-          -> Proxy n
-          -> Proxy m
-          -> (KnownNat q => r)
-          -> r
+withNatOp
+    :: (KnownNat n, KnownNat m)
+    => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q))
+    -> Proxy n
+    -> Proxy m
+    -> (KnownNat q => r)
+    -> r
 withNatOp op x y r = case natDict x `op` natDict y of
                        Dict -> r
 
diff --git a/typelits-witnesses.cabal b/typelits-witnesses.cabal
--- a/typelits-witnesses.cabal
+++ b/typelits-witnesses.cabal
@@ -1,5 +1,5 @@
 name:                typelits-witnesses
-version:             0.1.1.0
+version:             0.1.2.0
 synopsis:            Existential witnesses, singletons, and classes for operations on GHC TypeLits
 description:         Provides witnesses for 'KnownNat' and 'KnownSymbol'
                      instances for various operations on GHC TypeLits - in
@@ -38,7 +38,7 @@
                        GHC.TypeLits.List
   -- other-modules:       
   -- other-extensions:    
-  build-depends:       base >=4.8 && <4.9
+  build-depends:       base >=4.8 && <5
                      , reflection
                      , constraints
   hs-source-dirs:      src