diff --git a/StrictCheck.cabal b/StrictCheck.cabal
--- a/StrictCheck.cabal
+++ b/StrictCheck.cabal
@@ -1,6 +1,6 @@
 name:                StrictCheck
-version:             0.1.1
-synopsis:            StrictCheck: Keep Your Laziness In Check
+version:             0.2.0
+synopsis:            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
@@ -33,7 +33,6 @@
                        Test.StrictCheck.Produce,
                        Test.StrictCheck.Demand,
                        Test.StrictCheck.Observe,
-                       Test.StrictCheck.Observe.Unsafe,
                        Test.StrictCheck.Shaped,
                        Test.StrictCheck.Shaped.Flattened,
                        Test.StrictCheck.Internal.Inputs,
@@ -51,7 +50,8 @@
                        DeriveAnyClass, TypeOperators, PolyKinds,
                        GeneralizedNewtypeDeriving,
                        ViewPatterns, LambdaCase, TupleSections, ImplicitParams,
-                       NamedFieldPuns, PatternSynonyms
+                       NamedFieldPuns, PatternSynonyms,
+                       DeriveFoldable, DeriveTraversable
   ghc-options:         -Wall -Wno-unticked-promoted-constructors
                        -Wredundant-constraints
 
@@ -59,7 +59,7 @@
   type:                 exitcode-stdio-1.0
   hs-source-dirs:       tests
   main-is:              Tests.hs
-  other-modules:        Specs, RefTrans
+  other-modules:        Specs, RefTrans, Entangle
   default-language:     Haskell2010
   default-extensions:   DataKinds, GADTs, BangPatterns, TypeFamilies, RankNTypes,
                         AllowAmbiguousTypes, UndecidableInstances,
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, GHC.Generic)
+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable, GHC.Generic)
 
 instance Applicative Thunk where
   pure = Eval
diff --git a/src/Test/StrictCheck/Internal/Inputs.hs b/src/Test/StrictCheck/Internal/Inputs.hs
--- a/src/Test/StrictCheck/Internal/Inputs.hs
+++ b/src/Test/StrictCheck/Internal/Inputs.hs
@@ -19,7 +19,6 @@
   ) where
 
 import Test.QuickCheck (Gen)
-import Data.Semigroup
 
 
 --------------------------------------------------
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,18 +11,23 @@
   ( 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)
+import Generics.SOP hiding (Shape, Compose)
 
 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 --
 ------------------------------------------------------
@@ -50,18 +55,28 @@
 -- 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 =
-  let (input', inputD)  =
-        entangleShape input              -- (1)
-      (result', resultD) =
-        entangleShape (function input')  -- (2)
-  in let !_ = context result'            -- (3)
-  in (resultD, inputD)                   -- (4)
+  -- 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.
+
+
 -- | Observe the demand behavior
 --
 -- * in a given evaluation context
@@ -77,7 +92,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 -> ())
@@ -86,18 +101,32 @@
   -> ( Demand result
      , NP Demand inputs )
 observeNP context function inputs =
-  let entangled =
-        hcliftA
-          (Proxy @Shaped)
-          (uncurry Pair . first I . entangleShape . unI)
-          inputs
-      (inputs', inputsD) =
-        (hliftA (\(Pair r _) -> r) entangled,
-          hliftA (\(Pair _ l) -> l) entangled)
-      (result', resultD) = entangleShape (function inputs')
-  in let !_ = context result'
-  in (resultD, inputsD)
+  -- 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
+
+
 -- | Observe the demand behavior
 --
 -- * in a given evaluation context
@@ -127,6 +156,7 @@
 --
 -- 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)
@@ -139,4 +169,82 @@
 observe context function =
   curryAll (observeNP context (uncurryAll function))
 
--- NOTE: We don't need a NOINLINE annotation here because this wraps observeNP.
+
+--------------------------------------------------------
+-- 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) }
diff --git a/src/Test/StrictCheck/Observe/Unsafe.hs b/src/Test/StrictCheck/Observe/Unsafe.hs
deleted file mode 100644
--- a/src/Test/StrictCheck/Observe/Unsafe.hs
+++ /dev/null
@@ -1,76 +0,0 @@
-{-| 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 entangleShape #-}
-entangleShape :: Shaped a => a -> (a, Demand a)
-entangleShape =
-  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 #-}
+{-# language InstanceSigs, DerivingStrategies, TypeFamilyDependencies #-}
 {-# language PartialTypeSignatures #-}
 {-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}
 {-| This module defines the 'Shaped' typeclass, which is used to generically
@@ -50,9 +50,13 @@
   , (%)
   , fuse
   , translate
+  , translateA
   , fold
+  , foldM
   , unfold
+  , unfoldM
   , unzipWith
+  , unzipWithM
   -- , reshape
   -- * Rendering 'Shaped' things as structured text
   , QName
@@ -86,6 +90,7 @@
 import Data.Bifunctor
 import Data.Bifunctor.Flip
 import Data.Coerce
+import Control.Monad hiding (foldM)
 
 import Generics.SOP hiding ( Shape )
 
@@ -121,7 +126,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 :: (* -> *) -> *
+  type Shape a = (result :: (* -> *) -> *) | result -> a
   type Shape a = GShape a
 
   -- | Given a function to expand any @Shaped@ @x@ into an @f x@, expand an @a@
@@ -231,9 +236,17 @@
 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 @a d d $ \flat _ ->
+translate t d = match 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@,
@@ -241,8 +254,14 @@
 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 @a (fold alg)) . unwrap
+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
+
 -- | The equivalent of an unfold (anamorphism) over recursively 'Shaped' values
 --
 -- Given a function which unfolds an @f x@ into a @g@ containing some @Shape x
@@ -250,9 +269,14 @@
 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 @a (unfold coalg)) . coalg
+unfold coalg = Wrap . fmap (translate (unfold coalg)) . coalg
 
--- TODO: mapM, foldM, unfoldM, ...
+-- | 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
 
 -- | Fuse the interleaved @f@-structure out of a recursively interleaved @f %
 -- a@, given some way of fusing a single level @f x -> x@.
@@ -282,36 +306,46 @@
 
 -- | A higher-kinded @unzipWith@, operating over interleaved structures
 --
--- 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'.
+-- 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@.
 unzipWith
   :: (All Functor [f, g, h], Shaped a)
-  => (forall x. f x -> (g x, h x))
+  => (forall x sx. sx ~ (Shape x ((%) g), Shape x ((%) h))
+       => f sx -> (g sx, h sx))
   -> (f % a -> (g % a, h % a))
 unzipWith split =
-  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
+  unPair . fold (pair . bimap (Wrap . fmap fst) (Wrap . fmap snd)
+                 . split
+                 . fmap crunch)
 
-    pair :: (l x, r x) -> Product l r x
-    pair = uncurry Pair
+-- | 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)
 
-    unPair :: Product l r x -> (l x, r x)
-    unPair (Pair lx rx) = (lx, rx)
+-- 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)
+
+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)
+
 -- | TODO: document this strange function
 {-
 reshape :: forall b a f g. (Shaped a, Shaped b, Functor f)
@@ -323,7 +357,7 @@
     Nothing    -> hetero d
     Just HRefl ->
       Wrap
-      $ homo . fmap (translate @a (reshape @b homo hetero))
+      $ homo . fmap (translate (reshape homo hetero))
       $ unwrap d
 -}
 
@@ -341,7 +375,7 @@
     oneLevel :: forall x. Shaped x
              => f (Shape x (K (Rendered f)))
              -> K (Rendered f) x
-    oneLevel = K . RWrap . fmap (render @x)
+    oneLevel = K . RWrap . fmap render
 
 -- | A @QName@ is a qualified name
 --
diff --git a/src/Test/StrictCheck/Shaped/Flattened.hs b/src/Test/StrictCheck/Shaped/Flattened.hs
--- a/src/Test/StrictCheck/Shaped/Flattened.hs
+++ b/src/Test/StrictCheck/Shaped/Flattened.hs
@@ -44,8 +44,14 @@
 
 -- | If all the fields in a @Flattened@ satisfy some constraint, map a function
 -- expecting that constraint across all the fields. This may change the functor
--- over which the @Flattened@ value is paramaterized.
+-- over which the @Flattened@ value is parameterized.
 mapFlattened :: forall c d f g xs. All c xs
   => (forall x. c x => f x -> g x) -> Flattened d f xs -> Flattened d g xs
 mapFlattened t (Flattened u p) =
   Flattened u (hcliftA (Proxy @c) t p)
+
+-- | 'traverseFlattened' is to 'traverse' like 'mapFlattened' is to 'fmap'.
+traverseFlattened :: forall c d f g h xs. (All c xs, Applicative h)
+  => (forall x. c x => f x -> h (g x)) -> Flattened d f xs -> h (Flattened d g xs)
+traverseFlattened t (Flattened u p) =
+  Flattened u <$> hctraverse' (Proxy @c) t p
diff --git a/tests/Entangle.hs b/tests/Entangle.hs
new file mode 100644
--- /dev/null
+++ b/tests/Entangle.hs
@@ -0,0 +1,36 @@
+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,6 +2,7 @@
 
 import Specs
 import RefTrans
+import qualified Entangle
 
 main :: IO ()
 main = do
@@ -9,3 +10,4 @@
   runSpecs
   -- regression test for issue #2 (CSE breaks referential transparency)
   checkRefTrans
+  Entangle.spec