diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -95,7 +95,7 @@
 
 It is tempting to reach for partial functions or "impossible" runtime errors here, because
 the programmer has proven that the key is a member of the map in some other way. They
-know that lookup` should return a `Just v` --- but the *compiler* doesnt know this!
+know that `lookup` should return a `Just v` --- but the *compiler* doesnt know this!
 
 The idea behind `Data.Map.Justified` is to encode the programmers knowledge that a key
 is present *within the type system*, where it can be checked at compile-time. Once a key
diff --git a/justified-containers.cabal b/justified-containers.cabal
--- a/justified-containers.cabal
+++ b/justified-containers.cabal
@@ -1,5 +1,5 @@
 name:                justified-containers
-version:             0.2.0.1
+version:             0.3.0.0
 synopsis:            Keyed container types with type-checked proofs of key presence.
 description:         This package contains wrappers around standard container types,
                      that provide guarantees about the presence of keys within the
diff --git a/src/Data/Map/Justified.hs b/src/Data/Map/Justified.hs
--- a/src/Data/Map/Justified.hs
+++ b/src/Data/Map/Justified.hs
@@ -128,8 +128,10 @@
     -- * Map and Key types
       Map
     , Key
-    , theKey
+    , Index
     , theMap
+    , theKey
+    , theIndex
 
     -- * Evaluation
     , withMap
@@ -234,15 +236,30 @@
 newtype Key ph k = Key k deriving (Eq, Ord, Show)
 type role Key phantom representational
 
+-- | An index that knows it is valid in certain @'Map'@s.
+--
+-- The evidence that the index is valid for a map is carried by
+-- the type system via the phantom type parameter @ph@. Indexing
+-- operations such as `elemAt` will only type-check if the @'Index'@
+-- and the @'Map'@ have the same phantom type parameter.
+newtype Index ph = Index Int deriving (Eq, Ord, Show)
+type role Index phantom
+
+-- | Get the underlying "Data.Map" @'Data.Map'@ out of a @'Map'@.
+theMap :: Map ph k v -> M.Map k v
+theMap (Map m) = m
+
 -- | Get a bare key out of a key-plus-evidence by forgetting
 -- what map the key can be found in.
 theKey :: Key ph k -> k
 theKey (Key k) = k
 
--- | Get the underlying "Data.Map" @'Data.Map'@ out of a @'Map'@.
-theMap :: Map ph k v -> M.Map k v
-theMap (Map m) = m
+-- | Get a bare index out of an index-plus-evidence by forgetting
+-- what map the index is valid for.
+theIndex :: Index ph -> Int
+theIndex (Index n) = n
 
+
 {--------------------------------------------------------------------
   Evaluation
 --------------------------------------------------------------------}
@@ -797,16 +814,16 @@
 --
 -- Unlike "Data.Map"'s @'Data.Map.findIndex'@, this function can not fail at runtime.
 
-findIndex :: Ord k => Key ph k -> Map ph k a -> Key ph Int
-findIndex (Key k) (Map m) = Key (M.findIndex k m)
+findIndex :: Ord k => Key ph k -> Map ph k a -> Index ph
+findIndex (Key k) (Map m) = Index (M.findIndex k m)
 
 -- | /O(log n)/. Retrieve an element by its /index/, i.e. by its zero-based
 -- index in the sequence sorted by keys.
 --
 -- Unlike "Data.Map"'s @'Data.Map.elemAt'@, this function can not fail at runtime.
 
-elemAt :: Key ph Int -> Map ph k v -> (Key ph k, v)
-elemAt (Key n) (Map m) = let (k,v) = M.elemAt n m in (Key k, v)
+elemAt :: Index ph -> Map ph k v -> (Key ph k, v)
+elemAt (Index n) (Map m) = let (k,v) = M.elemAt n m in (Key k, v)
 
 {--------------------------------------------------------------------
   Utilities
diff --git a/test/Data/Map/JustifiedSpec.hs b/test/Data/Map/JustifiedSpec.hs
--- a/test/Data/Map/JustifiedSpec.hs
+++ b/test/Data/Map/JustifiedSpec.hs
@@ -106,7 +106,17 @@
       shouldNotTypecheck $
         withMap letters $ \m -> deleting 'X' m $
           \(_, _, m') -> map (`lookup` m') (keys m)
+
+  describe "indices" $ do
     
+    it "cannot be used as keys" $
+      shouldNotTypecheck $
+        withSingleton (17 :: Int) () $ \(k,m) -> m ! findIndex k m
+
+    it "cannot be used instead of keys" $
+      shouldNotTypecheck $
+        withSingleton (17 :: Int) () $ \(k,m) -> snd (elemAt k m)
+
   describe "at runtime" $ do
 
     it "does not allocate map copies when gathering evidence" $ do