diff --git a/StrictCheck.cabal b/StrictCheck.cabal
--- a/StrictCheck.cabal
+++ b/StrictCheck.cabal
@@ -1,6 +1,6 @@
 name:                StrictCheck
-version:             0.2.0
-synopsis:            Keep Your Laziness In Check
+version:             0.2.1
+synopsis:            StrictCheck: Keep Your Laziness In Check
 description: StrictCheck is a property-based random testing framework for
              observing, specifying, and testing the strictness behaviors of Haskell
              functions. Strictness behavior is traditionally considered a non-functional
@@ -18,6 +18,12 @@
 cabal-version:       >=1.10
 extra-source-files:  README.md
 
+source-repository this
+  type: git
+  branch: master
+  tag: master
+  location: https://github.com/kwf/StrictCheck
+
 library
   hs-source-dirs:      src
   default-language:    Haskell2010
@@ -33,6 +39,7 @@
                        Test.StrictCheck.Produce,
                        Test.StrictCheck.Demand,
                        Test.StrictCheck.Observe,
+                       Test.StrictCheck.Observe.Unsafe,
                        Test.StrictCheck.Shaped,
                        Test.StrictCheck.Shaped.Flattened,
                        Test.StrictCheck.Internal.Inputs,
@@ -50,8 +57,7 @@
                        DeriveAnyClass, TypeOperators, PolyKinds,
                        GeneralizedNewtypeDeriving,
                        ViewPatterns, LambdaCase, TupleSections, ImplicitParams,
-                       NamedFieldPuns, PatternSynonyms,
-                       DeriveFoldable, DeriveTraversable
+                       NamedFieldPuns, PatternSynonyms
   ghc-options:         -Wall -Wno-unticked-promoted-constructors
                        -Wredundant-constraints
 
@@ -59,7 +65,7 @@
   type:                 exitcode-stdio-1.0
   hs-source-dirs:       tests
   main-is:              Tests.hs
-  other-modules:        Specs, RefTrans, Entangle
+  other-modules:        Specs, RefTrans
   default-language:     Haskell2010
   default-extensions:   DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes,
                         AllowAmbiguousTypes, UndecidableInstances,
diff --git a/src/Test/StrictCheck.hs b/src/Test/StrictCheck.hs
--- a/src/Test/StrictCheck.hs
+++ b/src/Test/StrictCheck.hs
@@ -62,9 +62,6 @@
   )
   where
 
-
--- TODO: IMPORTANT: Add short descriptions to Haddock module headers
-
 import Test.StrictCheck.Curry as Curry
 import Test.StrictCheck.Produce
 import Test.StrictCheck.Consume
diff --git a/src/Test/StrictCheck/Demand.hs b/src/Test/StrictCheck/Demand.hs
--- a/src/Test/StrictCheck/Demand.hs
+++ b/src/Test/StrictCheck/Demand.hs
@@ -58,7 +58,7 @@
 data Thunk a
   = Eval !a
   | Thunk
-  deriving (Eq, Ord, Show, Functor, Foldable, Traversable, GHC.Generic)
+  deriving (Eq, Ord, Show, Functor, GHC.Generic)
 
 instance Applicative Thunk where
   pure = Eval
@@ -265,16 +265,23 @@
     foldMapCompose :: (a -> (b -> b)) -> [a] -> (b -> b)
     foldMapCompose f = appEndo . foldMap (Endo . f)
 
+-- | Pretty-print a demand for display, given the precendence context
+prettyDemandPrec :: Shaped a => Int -> Demand a -> ShowS
+prettyDemandPrec prec d =
+  showPrettyFieldThunkS False "_" prec (renderfold d)
+
 -- | Pretty-print a demand for display
 prettyDemand :: Shaped a => Demand a -> String
-prettyDemand d =
-  showPrettyFieldThunkS False "_" 0 (renderfold d) ""
+prettyDemand d = prettyDemandPrec 0 d ""
 
 -- | Print a demand to standard output
 --
 -- > printDemand = putStrLn . prettyDemand
 printDemand :: Shaped a => Demand a -> IO ()
 printDemand = putStrLn . prettyDemand
+
+instance Shaped a => Show (Demand a) where
+  showsPrec = prettyDemandPrec
 
 -- TODO: Comparisons module?
 
diff --git a/src/Test/StrictCheck/Observe.hs b/src/Test/StrictCheck/Observe.hs
--- a/src/Test/StrictCheck/Observe.hs
+++ b/src/Test/StrictCheck/Observe.hs
@@ -11,23 +11,18 @@
   ( observe1
   , observe
   , observeNP
-  , instrument
-  , entangle
   ) where
 
 import Data.Bifunctor
 import Data.Functor.Product
-import Data.Functor.Compose
-import Data.IORef
-import System.IO.Unsafe (unsafePerformIO, unsafeInterleaveIO)
 
-import Generics.SOP hiding (Shape, Compose)
+import Generics.SOP hiding (Shape)
 
 import Test.StrictCheck.Curry hiding (curry, uncurry)
 import Test.StrictCheck.Shaped
+import Test.StrictCheck.Observe.Unsafe
 import Test.StrictCheck.Demand
 
-
 ------------------------------------------------------
 -- Observing demand behavior of arbitrary functions --
 ------------------------------------------------------
@@ -55,27 +50,23 @@
 -- This tells us that our context did indeed evaluate the result of @reverse@
 -- to force only its first constructor, and that doing so required the entire
 -- spine of the list to be evaluated, but did not evaluate any of its elements.
-
+{-# NOINLINE observe1 #-}
 observe1
   :: (Shaped a, Shaped b)
   => (b -> ()) -> (a -> b) -> a -> (Demand b, Demand a)
 observe1 context function input =
-  -- Using unsafePerformIO here and in observeNP is safe, as the result of the
-  -- IO action only depends on it's inputs and has no side-effects.
-  unsafePerformIO $ do
-
-    -- The numbered lines correspond to the NOTE below
-    (input',  inputD)  <- instrument input                -- (1)
-    (result', resultD) <- instrument (function input')    -- (2)
-    let !_ = context result'                              -- (3)
-    (,) <$> resultD <*> inputD                            -- (4)
-
-    -- NOTE: The observation function:
-    -- (1) instruments the input
-    -- (2) instruments the result of the function applied to the input
-    -- (3) evaluates the instrumented result of the function in the context, and
-    -- (4) returns the observed demands on the result and the input.
-
+  let (input', inputD)  =
+        instrument input              -- (1)
+      (result', resultD) =
+        instrument (function input')  -- (2)
+  in let !_ = context result'         -- (3)
+  in (resultD, inputD)                -- (4)
+  
+  -- NOTE: The observation function:
+  -- (1) instruments the input
+  -- (2) instruments the result of the function applied to the input
+  -- (3) evaluates the instrumented result of the function in the context, and
+  -- (4) returns the observed demands on the result and the input.
 
 -- | Observe the demand behavior
 --
@@ -92,7 +83,7 @@
 --
 -- This is mostly useful for implementing the internals of StrictCheck;
 -- 'observe' is more ergonomic for exploration by end-users.
-
+{-# NOINLINE observeNP #-}
 observeNP
   :: (All Shaped inputs, Shaped result)
   => (result -> ())
@@ -101,31 +92,17 @@
   -> ( Demand result
      , NP Demand inputs )
 observeNP context function inputs =
-  -- NOTE: See the comment in observe1 about the safety of unsafePerformIO here.
-  unsafePerformIO $ do
-    -- This function works identically to observe1, except it has more
-    -- line-noise to shuffle around newtypes and traverse heterogeneous lists.
-    -- To see this, compare the numbered comments below to their corresponding
-    -- line labels in observe1.
-
-    -- (1) instrument the inputs
-    entangled <-
-      hctraverse'
-        (Proxy @Shaped)
-        (fmap (uncurry Pair . bimap I Compose) . instrument . unI)
-        inputs
-    let inputs' = hliftA     (\(Pair r _) -> r           ) entangled
-    let inputsD = htraverse' (\(Pair _ l) -> getCompose l) entangled
-
-    -- (2) instrument the result of the function on the instrumented inputs
-    (result', resultD) <- instrument (function inputs')
-
-    -- (3) evaluate the instrumented result of the function in the context
-    let !_ = context result'
-
-    -- (4) return the resultant observed demands
-    (,) <$> resultD <*> inputsD
-
+  let entangled =
+        hcliftA
+          (Proxy @Shaped)
+          (uncurry Pair . first I . instrument . unI)
+          inputs
+      (inputs', inputsD) =
+        (hliftA (\(Pair r _) -> r) entangled,
+          hliftA (\(Pair _ l) -> l) entangled)
+      (result', resultD) = instrument (function inputs')
+  in let !_ = context result'
+  in (resultD, inputsD)
 
 -- | Observe the demand behavior
 --
@@ -156,7 +133,6 @@
 --
 -- If you haven't thought very carefully about the strictness behavior of @zip@,
 -- this may be a surprising result; this is part of the fun!
-
 observe
   :: ( All Shaped (Args function)
      , Shaped (Result function)
@@ -169,82 +145,4 @@
 observe context function =
   curryAll (observeNP context (uncurryAll function))
 
-
---------------------------------------------------------
--- Instrumenting values to determine their evaluation --
---------------------------------------------------------
-
--- | Creates a tuple of an instrumented thunk, and an @IO@ action whose return
--- value indicates whether that thunk has yet been evaluated.
---
--- >>> (x, d) <- entangle ()
--- >>> d
--- Thunk
--- >>> x
--- ()
--- >>> d
--- Eval ()
-
-entangle :: a -> IO (a, IO (Thunk a))
-entangle a = do
-  ref <- newIORef Thunk
-  -- Using unsafePerformIO here is safe, i.e. it is referentially transparent,
-  -- because the only handle to the mutated IORef is closed over by the IO
-  -- action returned as the second element of the resultant tuple, which means
-  -- the effect of the unsafePerformIO can only be observed from within IO.
-  return (unsafePerformIO $ do
-             writeIORef ref (Eval a)
-             return a,
-          readIORef ref)
-
--- | Recursively instruments a value, returning a tuple of an instrumented
--- value, and an @IO@ action returning a 'Demand' that corresponds to the
--- portion of the instrumented value which has already been evaluated at the
--- time the action was run.
---
--- >>> (x, d) <- instrument [1..]
--- >>> printDemand =<< d
--- _
--- >>> length . take 3 $ x
--- 3
--- >>> printDemand =<< d
--- _ : _ : _ : _
--- >>> take 2 x
--- [1,2]
--- >>> printDemand =<< d
--- 1 : 2 : _ : _
-
--- NOTE: There are a two properties we care about:
---
---   1. Running the Demand action should always result in a consistent state
---      and not depend on when its result is forced.
---   2. We want to evaluate the input as little as possible. Importantly
---      running the demand action should never force any previously unforced
---      parts of the input. This is especially important for the observe
---      functions and the hardest thing to get right.
-
-instrument :: forall a. Shaped a => a -> IO (a, IO (Demand a))
-instrument a = do
-   -- We need to use unsafeInterleaveIO here so that we do not force the value
-   -- by matching on it when we bind the result above to entangle it.
-   --
-   -- Using unsafeInterleaveIO here is safe, as the result of the IO action does
-   -- not depend on when it is performed and it doesn't matter if it is never
-   -- performed, if it's value is not forced.
-   (~(~(a', _), da)) <- entangle =<< unsafeInterleaveIO entangledFields
-   return (a', Wrap <$> (traverse snd =<< da))
-  where
-    -- The to-be-entangled value with all its recursive children entangled
-    -- We still need to entangle the value itself
-    entangledFields :: IO (a, IO (Shape a Demand))
-    entangledFields = do
-      entangled <- translateA (pairWithDemand . unI) (project I a)
-      let a' = embed unI (translate (I . demanded) entangled)
-      return (a', translateA getDemand entangled)
-
-    pairWithDemand :: forall x. Shaped x => x -> IO (WithDemand x)
-    pairWithDemand = fmap (uncurry WithDemand) . instrument
-
--- Auxiliary functor for the traversal in 'instrument'
-data WithDemand a
-  = WithDemand { demanded :: a, getDemand :: IO (Demand a) }
+-- NOTE: We don't need a NOINLINE annotation here because this wraps observeNP.
diff --git a/src/Test/StrictCheck/Observe/Unsafe.hs b/src/Test/StrictCheck/Observe/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/StrictCheck/Observe/Unsafe.hs
@@ -0,0 +1,76 @@
+{-| This module defines the underlying __unsafe__ primitives StrictCheck uses
+    to implement purely functional observation of evaluation.
+
+    The "functions" in this module are __not referentially transparent__!
+-}
+module Test.StrictCheck.Observe.Unsafe where
+
+import System.IO.Unsafe
+import Data.IORef
+
+import Data.Bifunctor
+import Generics.SOP (I(..), unI)
+
+import Test.StrictCheck.Shaped
+import Test.StrictCheck.Demand
+
+-- | From some value of any type, produce a pair: a copy of the original value,
+-- and a 'Thunk' of that same type, with their values determined by the
+-- /order/ in which their values themselves are evaluated
+--
+-- If the copy of the value is evaluated to weak-head normal form before the
+-- returned @Thunk@, then any future inspection of the @Thunk@ will show that it
+-- is equal to the original value wrapped in an @Eval@. However, if the copy of
+-- the value is /not/ evaluated by the time the @Thunk@ is evaluated, any future
+-- inspection of the @Thunk@ will show that it is equal to @Thunk@.
+--
+-- A picture may be worth 1000 words:
+--
+-- >>> x = "hello," ++ " world"
+-- >>> (x', t) = entangle x
+-- >>> x'
+-- "hello, world"
+-- >>> t
+-- Eval "hello, world"
+--
+-- >>> x = "hello," ++ " world"
+-- >>> (x', t) = entangle x
+-- >>> t
+-- Thunk
+-- >>> x'
+-- "hello, world"
+-- >>> t
+-- Thunk
+{-# NOINLINE entangle #-}
+entangle :: forall a. a -> (a, Thunk a)
+entangle a =
+  unsafePerformIO $ do
+    ref <- newIORef Thunk
+    return ( unsafePerformIO $ do
+               writeIORef ref (Eval a)
+               return a
+           , unsafePerformIO $ readIORef ref )
+
+-- | Recursively 'entangle' an @a@, producing not merely a @Thunk@, but an
+-- entire @Demand@ which is piecewise entangled with that value. Whatever
+-- portion of the entangled value is evaluated before the corresponding portion
+-- of the returned @Demand@ will be represented in the shape of that @Demand@.
+-- However, any part of the returned @Demand@ which is evaluated before the
+-- corresponding portion of the entangled value will be forever equal to
+-- @Thunk@.
+--
+-- The behavior of this function is even more tricky to predict than that of
+-- 'entangle', especially when evaluation of the entangled value and the
+-- corresponding @Demand@ happen at the same time. In StrictCheck, all
+-- evaluation of the entangled value occurs before any evaluation of the
+-- @Demand@; we never interleave their evaluation.
+{-# NOINLINE instrument #-}
+instrument :: Shaped a => a -> (a, Demand a)
+instrument =
+  first (fuse unI)
+  . unzipWith entangle'
+  . interleave I
+  where
+    entangle' :: I x -> (I x, Thunk x)
+    entangle' =
+      first I . entangle . unI
diff --git a/src/Test/StrictCheck/Shaped.hs b/src/Test/StrictCheck/Shaped.hs
--- a/src/Test/StrictCheck/Shaped.hs
+++ b/src/Test/StrictCheck/Shaped.hs
@@ -1,4 +1,4 @@
-{-# language InstanceSigs, DerivingStrategies, TypeFamilyDependencies #-}
+{-# language InstanceSigs, DerivingStrategies #-}
 {-# language PartialTypeSignatures #-}
 {-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}
 {-| This module defines the 'Shaped' typeclass, which is used to generically
@@ -50,13 +50,9 @@
   , (%)
   , fuse
   , translate
-  , translateA
   , fold
-  , foldM
   , unfold
-  , unfoldM
   , unzipWith
-  , unzipWithM
   -- , reshape
   -- * Rendering 'Shaped' things as structured text
   , QName
@@ -90,7 +86,6 @@
 import Data.Bifunctor
 import Data.Bifunctor.Flip
 import Data.Coerce
-import Control.Monad hiding (foldM)
 
 import Generics.SOP hiding ( Shape )
 
@@ -126,7 +121,7 @@
   -- | The @Shape@ of an @a@ is a type isomorphic to the outermost level of
   -- structure in an @a@, parameterized by the functor @f@, which is wrapped
   -- around any fields (of any type) in the original @a@.
-  type Shape a = (result :: (* -> *) -> *) | result -> a
+  type Shape a :: (* -> *) -> *
   type Shape a = GShape a
 
   -- | Given a function to expand any @Shaped@ @x@ into an @f x@, expand an @a@
@@ -236,17 +231,9 @@
 translate :: forall a f g. Shaped a
           => (forall x. Shaped x => f x -> g x)
           -> Shape a f -> Shape a g
-translate t d = match d d $ \flat _ ->
+translate t d = match @a d d $ \flat _ ->
   unflatten $ mapFlattened @Shaped t flat
 
--- | The 'Applicative' version of 'translate'; maps an effectful translation
--- over a given @Shape@.
-translateA :: forall a c f g. (Shaped a, Applicative c)
-           => (forall x. Shaped x => f x -> c (g x))
-           -> Shape a f -> c (Shape a g)
-translateA t d = match d d $ \flat _ ->
-  unflatten <$> traverseFlattened @Shaped t flat
-
 -- | The equivalent of a fold (catamorphism) over recursively 'Shaped' values
 --
 -- Given a function which folds an @f@ containing some @Shape x g@ into a @g x@,
@@ -254,13 +241,7 @@
 fold :: forall a f g. (Functor f, Shaped a)
      => (forall x. Shaped x => f (Shape x g) -> g x)
      -> f % a -> g a
-fold alg = alg . fmap (translate (fold alg)) . unwrap
-
--- | The 'Monad' version of 'fold'; folds an interleaved structure effectfully.
-foldM :: forall a m f g. (Traversable f, Shaped a, Monad m)
-      => (forall x. Shaped x => f (Shape x g) -> m (g x))
-      -> f % a -> m (g a)
-foldM alg = alg <=< traverse (translateA (foldM alg)) . unwrap
+fold alg = alg . fmap (translate @a (fold alg)) . unwrap
 
 -- | The equivalent of an unfold (anamorphism) over recursively 'Shaped' values
 --
@@ -269,14 +250,9 @@
 unfold :: forall a f g. (Functor g, Shaped a)
        => (forall x. Shaped x => f x -> g (Shape x f))
        -> f a -> g % a
-unfold coalg = Wrap . fmap (translate (unfold coalg)) . coalg
+unfold coalg = Wrap . fmap (translate @a (unfold coalg)) . coalg
 
--- | The 'Monad' version of 'unfold'; unfolds an interleaved structure
--- effectfully.
-unfoldM :: forall a m f g. (Traversable g, Shaped a, Monad m)
-         => (forall x. Shaped x => f x -> m (g (Shape x f)))
-         -> f a -> m (g % a)
-unfoldM coalg = fmap Wrap . traverse (translateA (unfoldM coalg)) <=< coalg
+-- TODO: mapM, foldM, unfoldM, ...
 
 -- | Fuse the interleaved @f@-structure out of a recursively interleaved @f %
 -- a@, given some way of fusing a single level @f x -> x@.
@@ -306,45 +282,35 @@
 
 -- | A higher-kinded @unzipWith@, operating over interleaved structures
 --
--- Given a function splitting some @f x@ into a @g x@ and a @h x@, unzip and
--- entire @f % a@ structure using this operation, yielding a @g % a@ and a
--- @h % a@.
+-- Given a function splitting some @f x@ into a functor-product @Product g h x@,
+-- recursively split an interleaved @f % a@ into two interleaved structures:
+-- one built of @g@-shapes and one of @h@-shapes.
+--
+-- Note that @Product ((%) g) ((%) h) a@ is isomorphic to @(g % a, h % a)@; to
+-- get the latter, pattern-match on the 'Pair' constructor of 'Product'.
 unzipWith
   :: (All Functor [f, g, h], Shaped a)
-  => (forall x sx. sx ~ (Shape x ((%) g), Shape x ((%) h))
-       => f sx -> (g sx, h sx))
+  => (forall x. f x -> (g x, h x))
   -> (f % a -> (g % a, h % a))
 unzipWith split =
-  unPair . fold (pair . bimap (Wrap . fmap fst) (Wrap . fmap snd)
-                 . split
-                 . fmap crunch)
-
--- | The monadic equivalent of @unzipWith@; effectfully unzips an interleaved
--- structure
-unzipWithM
-  :: (Traversable f, All Functor [g, h], Shaped a, Monad m)
-  => (forall x sx. sx ~ (Shape x ((%) g), Shape x ((%) h))
-       => f sx -> m (g sx, h sx))
-  -> (f % a -> m (g % a, h % a))
-unzipWithM split =
-  fmap unPair . foldM (fmap (pair . bimap (Wrap . fmap fst) (Wrap . fmap snd))
-                       . split
-                       . fmap crunch)
-
--- Some helpers for zipping and unzipping...
-
-crunch
-  :: forall x g h. Shaped x
-  => Shape x (Product ((%) g) ((%) h))
-  -> (Shape x ((%) g), Shape x ((%) h))
-crunch x =
-  (translate (fst . unPair) $ x, translate (snd . unPair) $ x)
+  unPair . fold (crunch . pair . split)
+  where
+    crunch
+      :: forall x g h.
+      (Shaped x, Functor g, Functor h)
+      => Product g h (Shape x (Product ((%) g) ((%) h)))
+      -> Product ((%) g) ((%) h) x
+    crunch =
+      pair
+      . bimap (Wrap . fmap (translate @x (fst . unPair)))
+              (Wrap . fmap (translate @x (snd . unPair)))
+      . unPair
 
-pair :: (l x, r x) -> Product l r x
-pair = uncurry Pair
+    pair :: (l x, r x) -> Product l r x
+    pair = uncurry Pair
 
-unPair :: Product l r x -> (l x, r x)
-unPair (Pair lx rx) = (lx, rx)
+    unPair :: Product l r x -> (l x, r x)
+    unPair (Pair lx rx) = (lx, rx)
 
 -- | TODO: document this strange function
 {-
@@ -357,7 +323,7 @@
     Nothing    -> hetero d
     Just HRefl ->
       Wrap
-      $ homo . fmap (translate (reshape homo hetero))
+      $ homo . fmap (translate @a (reshape @b homo hetero))
       $ unwrap d
 -}
 
@@ -375,7 +341,7 @@
     oneLevel :: forall x. Shaped x
              => f (Shape x (K (Rendered f)))
              -> K (Rendered f) x
-    oneLevel = K . RWrap . fmap render
+    oneLevel = K . RWrap . fmap (render @x)
 
 -- | A @QName@ is a qualified name
 --
diff --git a/tests/Entangle.hs b/tests/Entangle.hs
deleted file mode 100644
--- a/tests/Entangle.hs
+++ /dev/null
@@ -1,36 +0,0 @@
-module Entangle where
-
-import Test.HUnit
-import Test.StrictCheck
-import Data.Bifunctor (bimap)
-
-spec :: IO ()
-spec = do
-  putStrLn "Checking instrument"
-  _ <- runTestTT . test $ do
-    (x , d ) <- fmap (fmap prettyDemand) <$> instrument ()
-    (x', d') <- fmap (fmap prettyDemand) <$> instrument x
-    d1 <- d
-    d1 @=? "_"
-    d'1 <- d'
-    d'1 @=? "_"
-    d2 <- d
-    d2 @=? "_"
-    let !_ = x
-    d3 <- d
-    d3 @=? "()"
-    d'2 <- d'
-    d'2 @=? "_"
-    let !_ = x'
-    d'3 <- d'
-    d'3 @=? "()"
-
-  putStrLn "Checking observe"
-  _ <- runTestTT . test $ do
-    let strict = bimap prettyDemand prettyDemand (observe1 id (\() -> ()) ())
-    let lazy   = bimap prettyDemand prettyDemand (observe1 id (\_  -> ()) ())
-
-    strict @=? ("()", "()")
-    lazy   @=? ("()", "_")
-
-  pure ()
diff --git a/tests/Tests.hs b/tests/Tests.hs
--- a/tests/Tests.hs
+++ b/tests/Tests.hs
@@ -2,7 +2,6 @@
 
 import Specs
 import RefTrans
-import qualified Entangle
 
 main :: IO ()
 main = do
@@ -10,4 +9,3 @@
   runSpecs
   -- regression test for issue #2 (CSE breaks referential transparency)
   checkRefTrans
-  Entangle.spec