diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,6 +1,15 @@
 # justified-containers
 Keyed container types with type-checked proofs of key presence.
 
+# Table of contents
+
+  * [Description](#description)
+    * [A simple example](#example)
+  * [Motivation](#motivation)
+  * [How it works](#how-it-works)
+    * [Phantom evidence](#phantom-evidence)
+
+
 # Description
 
 Have you ever *known* that a key could be found in a certain map? Were you tempted to
@@ -127,3 +136,104 @@
 `Data.Map.Justified` uses the same rank-2 polymorphism trick used in the `Control.Monad.ST` monad to
 ensure that the `ph` phantom type can not be extracted; in effect, the proof that a key is
 present can't leak to contexts where the proof would no longer be valid.
+
+## Phantom evidence
+
+You can interpret the `ph` phantom type as a concrete *set of keys*; under this interpretation,
+a value of type `Key ph k` is a key of type `k`, belonging to the subset described by `ph`.
+Similarly, a `Map ph k v` is a map whose keys are exactly the subset of `k` described by `ph`.
+From this perspective, the maps behave as if they were total, leading to their `Maybe`-free behavior.
+
+## Why all the continuations?
+
+Many of the functions in `justified-containers` make use of continuations, but why? As a case-study,
+consider the basic function `withMap` that promotes a standard `Data.Map.Map` to a `Data.Map.Justified.Map':
+
+```haskell
+import Data.Map.Justified
+import qualified Data.Map as M
+withMap :: M.Map k v -> (forall ph. Map ph k v -> t) -> t
+```
+
+The last `(forall ph. Map ph k v -> t) -> t` part is the continuation.
+
+The idea is that we know there is *some* set of keys `ph` belonging to this particular map, but
+at compile-time we may not know exactly what it is. But it does exist, after all, so we should be
+able to write
+
+```haskell
+withMap :: M.Map k v -> exists ph. Map ph k v
+```
+
+Similarly, the `inserting` function could look like
+
+```haskell
+inserting :: k -> v -> Map ph k v -> exists ph'. Map ph' k v
+```
+
+which can be read as "after inserting a key/value pair, we get a (possibly) different set of keys `ph'`".
+But in this case, we actually know a bit more: first, the inserted key will be found in the new map. And
+second, every key in `ph` can also be found in `ph'`. We
+can encode that knowledge by giving an explicit inclusion of `ph` into `ph'`, encoded as a function of
+type `Key ph k -> Key ph' k`. So we could re-write `inserting` with the type
+
+```haskell
+inserting :: k -> v -> Map ph k v -> exists ph'. (Key ph' k, Key ph k -> Key ph' k, Map ph' k v)
+--                                                \_______/  \___________________/  \_________/
+--                                   the new key______|                |                 |
+--                                                      the inclusion__|                 |
+--                                                                       the new map_____|
+```
+
+Likewise, when deleting a key from a map with keys `ph`, we get a new map with keys `ph'` along
+with a guarantee that `ph'` is a subset of `ph`. Compared to `inserting`, the inclusion goes the
+other way: there is an inclusion of `ph'` in `ph`, encoded as a function of type `Key ph' k -> Key ph l`.
+Altogether, we could give `deleting` the type
+
+```haskell
+deleting :: k -> Map ph k v -> exists ph'. (Key ph' k -> Key ph k, Map ph' k v)
+--                                          \___________________/  \_________/
+--                                                    |                 |
+--                            the reversed inclusion__|                 |
+--                                                      the new map_____|
+```
+
+A similar pattern works for other map operations like `union`, `intersection`, `difference`, and
+`filter`.
+
+## But what about the continuations?
+
+In the last section, we argued that `deleting` should have a type like
+
+```haskell
+deleting :: k -> Map ph k v -> exists ph'. (Key ph' k -> Key ph k, Map ph' k v)
+--                             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+```
+
+But if you check the documentation, you'll see the type
+
+```haskell
+deleting :: k -> Map ph k v -> (forall ph'. (Key ph' k -> Key ph k, Map ph' k v) -> t) -> t
+--                             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+```
+
+What happened to the underlined part of the type?
+
+The problem is that Haskell doesn't support existential types directly: the `exists` part of
+the type we wrote out is just wishful thinking. Instead, we have to go about things a little
+indirectly: we'll *encode* existentially-quantified types, via *rank-2 universally-quantified types*.
+
+
+The idea can be understood via the Curry-Howard correspondence:
+In classical logic, we have an equivalence between the propositions `∃X.P(X)`
+and `∀T. ((∀X.F(X) => T) => T)`.  It turns out that this equivalence remains valid
+in constructive logic, so we can transport it via the Curry-Howard correspondence to get
+an isomorphism between types:
+
+```haskell
+exists ph.  Map ph k v ~ (forall ph. Map ph k v -> t) -> t
+```
+
+In other words, instead of returning the existentially-quantified type directly
+we say "tell me what you wanted to do with that existentially-quantified type,
+and I'll do it for you". 
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.1.2.0
+version:             0.2.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
@@ -15,15 +15,34 @@
 extra-source-files:  README.md
 cabal-version:       >=1.10
 
+
+source-repository head
+  type:     git
+  location: https://github.com/matt-noonan/justified-containers
+
+
 library
   hs-source-dirs:      src
   exposed-modules:     Data.Map.Justified
                      , Data.Map.Justified.Tutorial
   ghc-options:         -O2 -Wall
   build-depends:       base >= 4.7 && < 5
-                     , containers                     
+                     , containers
+                     , roles >= 0.2
   default-language:    Haskell2010
 
-source-repository head
-  type:     git
-  location: https://github.com/matt-noonan/justified-containers
+
+test-suite justified-containers-spec
+  type:              exitcode-stdio-1.0
+  main-is:           Spec.hs
+  hs-source-dirs:    test
+  ghc-options:       -Wall -Wno-deferred-type-errors
+  build-depends:     base >= 4.7 && < 5
+                   , hspec
+                   , justified-containers
+                   , containers
+                   , QuickCheck
+                   , should-not-typecheck
+                   , ghc-prim
+  other-modules:     Data.Map.JustifiedSpec
+  default-language:  Haskell2010
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
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, DeriveTraversable #-}
+{-# LANGUAGE RankNTypes, DeriveTraversable, ScopedTypeVariables, RoleAnnotations #-}
 -- |
 -- Module      :  Data.Map.Justified
 -- Copyright   :  (c) Matt Noonan 2017
@@ -21,7 +21,7 @@
 -- None of the functions in this module can cause a run-time error, and very few
 -- of the operations return a @'Maybe'@ value.
 --
--- See the 'Data.Map.Justified.Tutorial' module for usage examples.
+-- See the "Data.Map.Justified.Tutorial" module for usage examples.
 --
 -- === Example
 -- @
@@ -141,6 +141,7 @@
     -- * Gathering evidence
     , member
     , keys
+    , lookupMay
     , lookupLT
     , lookupLE
     , lookupGT
@@ -206,6 +207,9 @@
 import Data.List (partition)
 import Control.Arrow ((&&&))
 
+import Data.Roles
+import Data.Type.Coercion
+
 {--------------------------------------------------------------------
   Map and Key types
 --------------------------------------------------------------------}
@@ -219,6 +223,7 @@
 -- @'Map'@ allows you to shift the burden of proof that a key exists
 -- in a map from "prove at every lookup" to "prove once per key".
 newtype Map ph k v = Map (M.Map k v) deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+type role Map phantom nominal representational
 
 -- | A key that knows it can be found in certain @'Map'@s.
 -- 
@@ -227,6 +232,7 @@
 -- operations such as lookup will only type-check if the @'Key'@
 -- and the @'Map'@ have the same phantom type parameter.
 newtype Key ph k = Key k deriving (Eq, Ord, Show)
+type role Key phantom representational
 
 -- | Get a bare key out of a key-plus-evidence by forgetting
 -- what map the key can be found in.
@@ -302,18 +308,35 @@
 -- > withRecMap memory2 (const ()) -- Left [(1, Cons (2,Present) (3,Missing))]
 --
 -- See @'Data.Map.Justified.Tutorial.example5'@ for more usage examples.
-withRecMap :: (Ord k, Traversable f)
+
+withRecMap :: forall k f t . (Ord k, Traversable f, Representational f)
            => M.Map k (f k) -- ^ A map with key references
            -> (forall ph. Map ph k (f (Key ph k)) -> t) -- ^ The checked continuation
            -> Either [MissingReference k f] t -- ^ Resulting value, or failure report.
+
 withRecMap m cont =
-  case bad of
-    [] -> Right $ cont (Map $ M.map (fmap Key) $ M.fromList ok)
-    _  -> Left (map (\(k,v) -> (k, fmap (id &&& locate) v)) bad)
+  
+  case snd (partition (allKeysPresent . snd) $ M.toList m) of
+    
+    -- All referenced keys are found in the map; coerce the map's type.
+    []   -> Right $ cont (Map $ (coerceWith mapCoercion) m)
+
+    -- There were some dangling key references; report them.
+    bads -> Left (map (\(k,v) -> (k, fmap (id &&& locate) v)) bads)
+
   where
-    (ok, bad) = partition (all ((== Present) . locate) . snd) (M.toList m)
+
+    allKeysPresent = all ((== Present) . locate)
+
     locate k = if M.member k m then Present else Missing
+    
+    nestedValueCoercion :: Coercion (f k) (f (Key ph0 k))
+    nestedValueCoercion = rep Coercion
+    
+    mapCoercion :: Coercion (M.Map k (f k)) (M.Map k (f (Key ph0 k)))
+    mapCoercion = rep nestedValueCoercion
 
+
 {--------------------------------------------------------------------
   Gathering evidence
 --------------------------------------------------------------------}
@@ -360,6 +383,12 @@
 lookup (Key k) (Map m) = case M.lookup k m of
   Just value -> value
   Nothing    -> error "Data.Map.Justified has been subverted!"
+
+-- | /O(log n)/. Lookup the value at a key that is /not/ already known
+-- to be in the map. Return @Just@ the value /and/ the key-with-evidence
+-- if the key was present, or @Nothing@ otherwise.
+lookupMay :: Ord k => k -> Map ph k v -> Maybe (Key ph k, v)
+lookupMay k (Map m) = fmap (\v -> (Key k, v)) (M.lookup k m)
 
 -- | /O(log n)/. Find the largest key smaller than the given one
 -- and return the corresponding (key,value) pair, with evidence for the key.
diff --git a/src/Data/Map/Justified/Tutorial.hs b/src/Data/Map/Justified/Tutorial.hs
--- a/src/Data/Map/Justified/Tutorial.hs
+++ b/src/Data/Map/Justified/Tutorial.hs
@@ -36,6 +36,8 @@
 import Data.Char (toUpper)
 import Control.Monad (forM_)
 
+import Data.Type.Coercion
+
 -- | A simple "Data.Map" value used in several examples below.
 --
 -- @
@@ -220,9 +222,9 @@
 -- "new key" data.
 --
 -- @
---  example4 = withMap test_table $ \table -> do
---    inserting 3 "NEW" table $ \(newKey, upgrade, table') -> do
---      forM_ (keys table) $ \key -> do
+--  example4 = withMap test_table $ \\table -> do
+--    inserting 3 "NEW" table $ \\(newKey, upgrade, table') -> do
+--      forM_ (keys table) $ \\key -> do
 --        putStrLn (show key ++ " maps to " ++ table  ! key ++ " in the old table.")
 --        putStrLn (show key ++ " maps to " ++ table' ! (upgrade key) ++ " in the new table.")
 --      putStrLn ("Also, the new table maps " ++ show newKey ++ " to " ++ table' ! newKey)
diff --git a/test/Data/Map/JustifiedSpec.hs b/test/Data/Map/JustifiedSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Data/Map/JustifiedSpec.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MagicHash #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+
+module Data.Map.JustifiedSpec (main, spec) where
+
+import Prelude hiding (lookup)
+
+import Test.Hspec
+import Test.QuickCheck
+import Test.ShouldNotTypecheck
+
+import Data.Map.Justified
+import qualified Data.Map as M
+import Data.Maybe
+
+import GHC.Prim
+import GHC.Int
+import System.Mem (performGC)
+import System.IO.Unsafe (unsafePerformIO)
+
+import Data.Map.Justified.Tutorial (adjacencies)
+
+import Data.Type.Coercion
+
+main :: IO ()
+main = hspec spec
+
+letters :: M.Map Char Int
+letters = M.fromList (Prelude.zip ['a'..'z'] [1..])
+
+newtype AlphaNum = AlphaNum Char deriving Show
+instance Arbitrary AlphaNum where
+  arbitrary = elements (map AlphaNum $ ['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'])
+  
+spec :: Spec
+spec = do
+
+  describe "using Data.Map.Justified.Map" $ do
+
+    it "wraps the underlying Data.Map.Map without modification" $ do
+      withMap letters theMap == letters
+
+    it "can create singleton maps" $ property $ do
+      \(k :: Int, v :: Int) -> withSingleton k v (uncurry lookup) == v
+      \(k :: Int, v :: Int) -> withSingleton k v (theMap . snd)   == M.fromList [(k,v)]
+      
+  describe "validated keys" $ do
+    
+    it "can be obtained iff a key is present" $ property $
+      \(AlphaNum c) -> isJust (M.lookup c letters) == withMap letters (isJust . member c)
+
+    it "will access the expected value" $ do
+      map (\k -> fromJust $ M.lookup k letters) (M.keys letters)
+      `shouldBe`
+      withMap letters (\m -> map (`lookup` m) (keys m))
+      
+    it "can degrade to the original key" $ do
+      M.keys letters `shouldBe` withMap letters (map theKey . keys)
+
+    it "can still be used in an adjusted map" $ do
+      withMap letters (\m -> let (k:k':_) = keys m in
+                                 (lookup k (reinsert k 17 m),
+                                  lookup k (reinsert k' 17 m),
+                                  lookup k (adjust (+1) k m),
+                                  lookup k (adjustWithKey
+                                              (\k v -> v + fromEnum (theKey k)) k m)))
+      `shouldBe` (17,1,2,98)
+      
+    it "can not escape `withMap`" $ shouldNotTypecheck $
+      withMap letters (head keys)
+
+    it "can not be used in unrelated maps" $ shouldNotTypecheck $
+      withMap letters (\m ->
+         let k = head (keys m) in withMap letters (lookup k))
+
+    it  "can not be directly created" $ shouldNotTypecheck $
+      let k = Key 'a' in withMap letters (lookup k)
+
+  describe "when adding keys" $ do
+
+    it "can translate old keys to new map" $ property $
+      \(AlphaNum c, AlphaNum c') -> withMap letters $
+        \m -> inserting c' 100 m $
+              \(_, upgrade, m') ->
+              let k  = member c m
+                  k' = member c m'
+              in c /= c' ==> fmap upgrade k == k'
+  
+    it "does not let a new key be used in the old map without translation" $
+      shouldNotTypecheck $
+        withMap letters $ \m -> inserting 'X' 100 m $
+          \(_, _, m') -> map (`lookup` m) (keys m')
+    
+  describe "when removing keys" $ do
+
+    it "can translate new keys to old map" $ property $
+      \(AlphaNum c, AlphaNum c') -> withMap letters $
+         \m -> deleting c' m $
+               \(downgrade, m') ->
+               let k  = member c m
+                   k' = member c m'
+               in c /= c' ==> k == fmap downgrade k'
+
+    it "does not let an old key be used in the new map without translation" $
+      shouldNotTypecheck $
+        withMap letters $ \m -> deleting 'X' m $
+          \(_, _, m') -> map (`lookup` m') (keys m)
+    
+  describe "at runtime" $ do
+
+    it "does not allocate map copies when gathering evidence" $ do
+      withMap letters $ \m -> m `isLiterally` letters
+
+    it "does not allocate map copies when forgetting evidence" $ do
+      withMap letters $ \m -> theMap m `isLiterally` letters
+        
+    it "does not allocate key copies when gathering key evidence" $ do
+      withMap letters $ \m ->
+        each (M.keys letters) $ \k -> fromJust (k `member` m) `isLiterally` k
+
+    it "does not allocate key copies when forgetting evidence" $ do
+      withMap letters $ \m ->
+        let ks = keys m
+              -- This depends on the Prelude rewrite rule "map coerce/coerce" firing, I think.
+        in map theKey ks `isLiterally` ks
+
+    it "does not allocate keys during evidence conversion for insertion" $ do
+      withMap letters $ \m ->
+        inserting 'X' 100 m $ \(_, upgraded, _) ->
+          each (keys m) $ \k -> upgraded k `isLiterally` k
+
+    it "does not allocate keys during evidence conversion for deletion" $ do
+      withMap letters $ \m ->
+        deleting 'X' m $ \(downgraded, m') ->
+          each (keys m') $ \k -> downgraded k `isLiterally` k
+                                                     
+    it "does not allocate values when performing lookup with a verified key" $ do
+      withMap letters $ \m ->
+        each (keys m) $ \k ->
+          (k `lookup` m) `isLiterally` fromJust (theKey k `M.lookup` letters)
+
+    it "does not allocate when verifying a recursive map" $ fromRight $ do
+      withRecMap adjacencies $ \m -> m `isLiterally` adjacencies
+      
+-- | Test if two values occupy the same location in memory.
+--   This is almost certainly flaky, especially if a GC occurs
+--   during evaluation of ans!
+isLiterally :: a -> b -> Bool
+isLiterally x y = unsafePerformIO $ do
+  let x' = unsafeCoerce# y
+  x `seq` x' `seq` performGC
+  return $ I64# (reallyUnsafePtrEquality# x x') == 1
+
+each :: Traversable t => t a -> (a -> Bool) -> Bool
+each = flip all
+
+fromRight :: Either a b -> b
+fromRight = either (error "expected Right, got Left") id
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}