diff --git a/src/Analysis/Abstract/BadAddresses.hs b/src/Analysis/Abstract/BadAddresses.hs
index f485b2a01..345ab93ca 100644
--- a/src/Analysis/Abstract/BadAddresses.hs
+++ b/src/Analysis/Abstract/BadAddresses.hs
@@ -2,32 +2,29 @@
 module Analysis.Abstract.BadAddresses where
 
 import Control.Abstract.Analysis
-import Analysis.Abstract.Evaluating
+import Data.Abstract.Address
 import Prologue
 
 newtype BadAddresses m (effects :: [* -> *]) a = BadAddresses (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (BadAddresses m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (BadAddresses m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (BadAddresses m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadAddresses m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (BadAddresses m effects)
+deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadAddresses m)
 
 instance ( Effectful m
          , Member (Resumable (AddressError location value)) effects
-         , Member (State (EvaluatingState location term value)) effects
-         , MonadAnalysis location term value (m effects)
-         , MonadValue location value (BadAddresses m effects)
+         , MonadAnalysis location term value effects m
+         , MonadValue location value effects (BadAddresses m)
+         , Monoid (Cell location value)
          , Show location
          )
-      => MonadAnalysis location term value (BadAddresses m effects) where
-  type Effects location term value (BadAddresses m effects) = Effects location term value (m effects)
+      => MonadAnalysis location term value effects (BadAddresses m) where
+  type Effects location term value (BadAddresses m) = Effects location term value m
 
   analyzeTerm eval term = resume @(AddressError location value) (liftAnalyze analyzeTerm eval term) (
         \yield error -> do
           traceM ("AddressError:" <> show error)
           case error of
-            (UninitializedAddress _) -> hole >>= yield)
+            UnallocatedAddress _ -> yield mempty
+            UninitializedAddress _ -> hole >>= yield)
 
   analyzeModule = liftAnalyze analyzeModule
diff --git a/src/Analysis/Abstract/BadModuleResolutions.hs b/src/Analysis/Abstract/BadModuleResolutions.hs
index 6e888ffec..be4eccba0 100644
--- a/src/Analysis/Abstract/BadModuleResolutions.hs
+++ b/src/Analysis/Abstract/BadModuleResolutions.hs
@@ -3,27 +3,21 @@ module Analysis.Abstract.BadModuleResolutions where
 
 import Control.Abstract.Analysis
 import Data.Abstract.Evaluatable
-import Analysis.Abstract.Evaluating
 import Prologue
 
 newtype BadModuleResolutions m (effects :: [* -> *]) a = BadModuleResolutions (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (BadModuleResolutions m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (BadModuleResolutions m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (BadModuleResolutions m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadModuleResolutions m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (BadModuleResolutions m effects)
+deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadModuleResolutions m)
 
 instance ( Effectful m
          , Member (Resumable (ResolutionError value)) effects
-         , Member (State (EvaluatingState location term value)) effects
          , Member (State [Name]) effects
-         , MonadAnalysis location term value (m effects)
-         , MonadValue location value (BadModuleResolutions m effects)
+         , MonadAnalysis location term value effects m
+         , MonadValue location value effects (BadModuleResolutions m)
          )
-      => MonadAnalysis location term value (BadModuleResolutions m effects) where
-  type Effects location term value (BadModuleResolutions m effects) = State [Name] ': Effects location term value (m effects)
+      => MonadAnalysis location term value effects (BadModuleResolutions m) where
+  type Effects location term value (BadModuleResolutions m) = State [Name] ': Effects location term value m
 
   analyzeTerm eval term = resume @(ResolutionError value) (liftAnalyze analyzeTerm eval term) (
         \yield error -> do
diff --git a/src/Analysis/Abstract/BadValues.hs b/src/Analysis/Abstract/BadValues.hs
index f4a026ccc..68eeb6b97 100644
--- a/src/Analysis/Abstract/BadValues.hs
+++ b/src/Analysis/Abstract/BadValues.hs
@@ -3,29 +3,23 @@ module Analysis.Abstract.BadValues where
 
 import Control.Abstract.Analysis
 import Data.Abstract.Evaluatable
-import Analysis.Abstract.Evaluating
 import Data.Abstract.Environment as Env
 import Prologue
 import Data.ByteString.Char8 (pack)
 
 newtype BadValues m (effects :: [* -> *]) a = BadValues (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (BadValues m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (BadValues m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (BadValues m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadValues m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (BadValues m effects)
+deriving instance MonadEvaluator location term value effects m   => MonadEvaluator location term value effects (BadValues m)
 
 instance ( Effectful m
          , Member (Resumable (ValueError location value)) effects
-         , Member (State (EvaluatingState location term value)) effects
          , Member (State [Name]) effects
-         , MonadAnalysis location term value (m effects)
-         , MonadValue location value (BadValues m effects)
+         , MonadAnalysis location term value effects m
+         , MonadValue location value effects (BadValues m)
          )
-      => MonadAnalysis location term value (BadValues m effects) where
-  type Effects location term value (BadValues m effects) = State [Name] ': Effects location term value (m effects)
+      => MonadAnalysis location term value effects (BadValues m) where
+  type Effects location term value (BadValues m) = State [Name] ': Effects location term value m
 
   analyzeTerm eval term = resume @(ValueError location value) (liftAnalyze analyzeTerm eval term) (
         \yield error -> do
diff --git a/src/Analysis/Abstract/BadVariables.hs b/src/Analysis/Abstract/BadVariables.hs
index 1fa891778..608f8515d 100644
--- a/src/Analysis/Abstract/BadVariables.hs
+++ b/src/Analysis/Abstract/BadVariables.hs
@@ -9,22 +9,18 @@ import Prologue
 
 -- An analysis that resumes from evaluation errors and records the list of unresolved free variables.
 newtype BadVariables m (effects :: [* -> *]) a = BadVariables (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (BadVariables m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (BadVariables m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (BadVariables m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (BadVariables m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (BadVariables m effects)
+deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (BadVariables m)
 
 instance ( Effectful m
          , Member (Resumable (EvalError value)) effects
          , Member (State [Name]) effects
-         , MonadAnalysis location term value (m effects)
-         , MonadValue location value (BadVariables m effects)
+         , MonadAnalysis location term value effects m
+         , MonadValue location value effects (BadVariables m)
          )
-      => MonadAnalysis location term value (BadVariables m effects) where
-  type Effects location term value (BadVariables m effects) = State [Name] ': Effects location term value (m effects)
+      => MonadAnalysis location term value effects (BadVariables m) where
+  type Effects location term value (BadVariables m) = State [Name] ': Effects location term value m
 
   analyzeTerm eval term = resume @(EvalError value) (liftAnalyze analyzeTerm eval term) (
         \yield err -> do
diff --git a/src/Analysis/Abstract/Caching.hs b/src/Analysis/Abstract/Caching.hs
index f87ef40f7..b6a949198 100644
--- a/src/Analysis/Abstract/Caching.hs
+++ b/src/Analysis/Abstract/Caching.hs
@@ -20,38 +20,34 @@ type CachingEffects location term value effects
 
 -- | A (coinductively-)cached analysis suitable for guaranteeing termination of (suitably finitized) analyses over recursive programs.
 newtype Caching m (effects :: [* -> *]) a = Caching (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (Caching m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (Caching m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (Caching m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Caching m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (Caching m effects)
+deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Caching m)
 
 -- | Functionality used to perform caching analysis. This is not exported, and exists primarily for organizational reasons.
-class MonadEvaluator location term value m => MonadCaching location term value m where
+class MonadEvaluator location term value effects m => MonadCaching location term value effects m where
   -- | Look up the set of values for a given configuration in the in-cache.
-  consultOracle :: Configuration location term value -> m (Set (value, Heap location value))
+  consultOracle :: Configuration location term value -> m effects (Set (value, Heap location value))
   -- | Run an action with the given in-cache.
-  withOracle :: Cache location term value -> m a -> m a
+  withOracle :: Cache location term value -> m effects a -> m effects a
 
   -- | Look up the set of values for a given configuration in the out-cache.
-  lookupCache :: Configuration location term value -> m (Maybe (Set (value, Heap location value)))
+  lookupCache :: Configuration location term value -> m effects (Maybe (Set (value, Heap location value)))
   -- | Run an action, caching its result and 'Heap' under the given configuration.
-  caching :: Configuration location term value -> Set (value, Heap location value) -> m value -> m value
+  caching :: Configuration location term value -> Set (value, Heap location value) -> m effects value -> m effects value
 
   -- | Run an action starting from an empty out-cache, and return the out-cache afterwards.
-  isolateCache :: m a -> m (Cache location term value)
+  isolateCache :: m effects a -> m effects (Cache location term value)
 
 instance ( Effectful m
          , Members (CachingEffects location term value '[]) effects
-         , MonadEvaluator location term value (m effects)
+         , MonadEvaluator location term value effects m
          , Ord (Cell location value)
          , Ord location
          , Ord term
          , Ord value
          )
-         => MonadCaching location term value (Caching m effects) where
+         => MonadCaching location term value effects (Caching m) where
   consultOracle configuration = raise (fromMaybe mempty . cacheLookup configuration <$> ask)
   withOracle cache = raise . local (const cache) . lower
 
@@ -68,17 +64,17 @@ instance ( Effectful m
 instance ( Alternative (m effects)
          , Corecursive term
          , Effectful m
+         , Member Fresh effects
          , Members (CachingEffects location term value '[]) effects
-         , MonadAnalysis location term value (m effects)
-         , MonadFresh (m effects)
+         , MonadAnalysis location term value effects m
          , Ord (Cell location value)
          , Ord location
          , Ord term
          , Ord value
          )
-      => MonadAnalysis location term value (Caching m effects) where
+      => MonadAnalysis location term value effects (Caching m) where
   -- We require the 'CachingEffects' in addition to the underlying analysis’ 'Effects'.
-  type Effects location term value (Caching m effects) = CachingEffects location term value (Effects location term value (m effects))
+  type Effects location term value (Caching m) = CachingEffects location term value (Effects location term value m)
 
   -- Analyze a term using the in-cache as an oracle & storing the results of the analysis in the out-cache.
   analyzeTerm recur e = do
@@ -121,5 +117,5 @@ converge f = loop
             loop x'
 
 -- | Nondeterministically write each of a collection of stores & return their associated results.
-scatter :: (Alternative m, Foldable t, MonadEvaluator location term value m) => t (a, Heap location value) -> m a
+scatter :: (Alternative (m effects), Foldable t, MonadEvaluator location term value effects m) => t (a, Heap location value) -> m effects a
 scatter = foldMapA (\ (value, heap') -> putHeap heap' $> value)
diff --git a/src/Analysis/Abstract/Collecting.hs b/src/Analysis/Abstract/Collecting.hs
index 92a3a155f..ab22cccd4 100644
--- a/src/Analysis/Abstract/Collecting.hs
+++ b/src/Analysis/Abstract/Collecting.hs
@@ -11,32 +11,27 @@ import Data.Abstract.Live
 import Prologue
 
 newtype Collecting m (effects :: [* -> *]) a = Collecting (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
-
-deriving instance MonadControl term (m effects)                    => MonadControl term (Collecting m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (Collecting m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (Collecting m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Collecting m effects)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
 instance ( Effectful m
          , Member (Reader (Live location value)) effects
-         , MonadEvaluator location term value (m effects)
+         , MonadEvaluator location term value effects m
          )
-      => MonadEvaluator location term value (Collecting m effects) where
+      => MonadEvaluator location term value effects (Collecting m) where
   getConfiguration term = Configuration term <$> askRoots <*> getEnv <*> getHeap
 
 
 instance ( Effectful m
          , Foldable (Cell location)
          , Member (Reader (Live location value)) effects
-         , MonadAnalysis location term value (m effects)
+         , MonadAnalysis location term value effects m
          , Ord location
          , ValueRoots location value
          )
-      => MonadAnalysis location term value (Collecting m effects) where
-  type Effects location term value (Collecting m effects)
+      => MonadAnalysis location term value effects (Collecting m) where
+  type Effects location term value (Collecting m)
     = Reader (Live location value)
-   ': Effects location term value (m effects)
+   ': Effects location term value m
 
   -- Small-step evaluation which garbage-collects any non-rooted addresses after evaluating each term.
   analyzeTerm recur term = do
diff --git a/src/Analysis/Abstract/Dead.hs b/src/Analysis/Abstract/Dead.hs
index 4ff837fd0..8a4541aa8 100644
--- a/src/Analysis/Abstract/Dead.hs
+++ b/src/Analysis/Abstract/Dead.hs
@@ -11,13 +11,9 @@ import Prologue
 
 -- | An analysis tracking dead (unreachable) code.
 newtype DeadCode m (effects :: [* -> *]) a = DeadCode (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (DeadCode m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (DeadCode m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (DeadCode m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (DeadCode m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (DeadCode m effects)
+deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (DeadCode m)
 
 -- | A set of “dead” (unreachable) terms.
 newtype Dead term = Dead { unDead :: Set term }
@@ -42,12 +38,12 @@ instance ( Corecursive term
          , Effectful m
          , Foldable (Base term)
          , Member (State (Dead term)) effects
-         , MonadAnalysis location term value (m effects)
+         , MonadAnalysis location term value effects m
          , Ord term
          , Recursive term
          )
-      => MonadAnalysis location term value (DeadCode m effects) where
-  type Effects location term value (DeadCode m effects) = State (Dead term) ': Effects location term value (m effects)
+      => MonadAnalysis location term value effects (DeadCode m) where
+  type Effects location term value (DeadCode m) = State (Dead term) ': Effects location term value m
 
   analyzeTerm recur term = do
     revive (embedSubterm term)
diff --git a/src/Analysis/Abstract/Evaluating.hs b/src/Analysis/Abstract/Evaluating.hs
index af17d95f9..3733d5374 100644
--- a/src/Analysis/Abstract/Evaluating.hs
+++ b/src/Analysis/Abstract/Evaluating.hs
@@ -1,33 +1,22 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving, RankNTypes, TypeFamilies, UndecidableInstances, ScopedTypeVariables #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
 module Analysis.Abstract.Evaluating
 ( Evaluating
-, EvaluatingState(..)
-, State
 ) where
 
-import           Control.Abstract.Analysis
-import           Control.Monad.Effect
-import           Data.Abstract.Address
-import           Data.Abstract.Configuration
-import           Data.Abstract.Environment as Env
-import           Data.Abstract.Evaluatable
-import           Data.Abstract.Exports
-import           Data.Abstract.Heap
-import           Data.Abstract.Module
-import           Data.Abstract.ModuleTable
-import           Data.Abstract.Origin
-import           Data.Empty
-import qualified Data.IntMap as IntMap
-import           Lens.Micro
-import           Prelude hiding (fail)
-import           Prologue
+import Control.Abstract.Analysis
+import Control.Monad.Effect
+import Data.Abstract.Configuration
+import Data.Abstract.Environment as Env
+import Data.Abstract.Evaluatable
+import Data.Abstract.Module
+import Data.Abstract.ModuleTable
+import Data.Abstract.Origin
+import Prologue
 
 -- | An analysis evaluating @term@s to @value@s with a list of @effects@ using 'Evaluatable', and producing incremental results of type @a@.
 newtype Evaluating location term value effects a = Evaluating (Eff effects a)
   deriving (Applicative, Functor, Effectful, Monad)
 
-deriving instance Member Fail   effects => MonadFail   (Evaluating location term value effects)
-deriving instance Member Fresh  effects => MonadFresh  (Evaluating location term value effects)
 deriving instance Member NonDet effects => Alternative (Evaluating location term value effects)
 
 -- | Effects necessary for evaluating (whether concrete or abstract).
@@ -40,133 +29,33 @@ type EvaluatingEffects location term value
      , Resumable (ValueError location value)
      , Resumable (Unspecialized value)
      , Resumable (AddressError location value)
-     , Fail                                         -- Failure with an error message
-     , Fresh                                        -- For allocating new addresses and/or type variables.
-     , Reader (SomeOrigin term)                     -- The current term’s origin.
-     , Reader (ModuleTable [Module term])           -- Cache of unevaluated modules
-     , Reader (Environment location value)          -- Default environment used as a fallback in lookupEnv
-     , State  (EvaluatingState location term value) -- Environment, heap, modules, exports, and jumps.
+     , Fail                                        -- Failure with an error message
+     , Fresh                                       -- For allocating new addresses and/or type variables.
+     , Reader (SomeOrigin term)                    -- The current term’s origin.
+     , Reader (ModuleTable [Module term])          -- Cache of unevaluated modules
+     , Reader (Environment location value)         -- Default environment used as a fallback in lookupEnv
+     , State  (EvaluatorState location term value) -- Environment, heap, modules, exports, and jumps.
      ]
 
-data EvaluatingState location term value = EvaluatingState
-  { environment :: Environment location value
-  , heap        :: Heap location value
-  , modules     :: ModuleTable (Environment location value, value)
-  , loadStack   :: LoadStack
-  , exports     :: Exports location value
-  , jumps       :: IntMap.IntMap term
-  , origin      :: SomeOrigin term
-  }
-
-deriving instance (Eq (Cell location value), Eq location, Eq term, Eq value, Eq (Base term ())) => Eq (EvaluatingState location term value)
-deriving instance (Ord (Cell location value), Ord location, Ord term, Ord value, Ord (Base term ())) => Ord (EvaluatingState location term value)
-deriving instance (Show (Cell location value), Show location, Show term, Show value, Show (Base term ())) => Show (EvaluatingState location term value)
-
-instance (Ord location, Semigroup (Cell location value)) => Semigroup (EvaluatingState location term value) where
-  EvaluatingState e1 h1 m1 l1 x1 j1 o1 <> EvaluatingState e2 h2 m2 l2 x2 j2 o2 = EvaluatingState (e1 <> e2) (h1 <> h2) (m1 <> m2) (l1 <> l2) (x1 <> x2) (j1 <> j2) (o1 <> o2)
-
-instance (Ord location, Semigroup (Cell location value)) => Empty (EvaluatingState location term value) where
-  empty = EvaluatingState mempty mempty mempty mempty mempty mempty mempty
-
-_environment :: Lens' (EvaluatingState location term value) (Environment location value)
-_environment = lens environment (\ s e -> s {environment = e})
-
-_heap :: Lens' (EvaluatingState location term value) (Heap location value)
-_heap = lens heap (\ s h -> s {heap = h})
-
-_modules :: Lens' (EvaluatingState location term value) (ModuleTable (Environment location value, value))
-_modules = lens modules (\ s m -> s {modules = m})
-
-_loadStack :: Lens' (EvaluatingState location term value) LoadStack
-_loadStack = lens loadStack (\ s l -> s {loadStack = l})
-
-_exports :: Lens' (EvaluatingState location term value) (Exports location value)
-_exports = lens exports (\ s e -> s {exports = e})
-
-_jumps :: Lens' (EvaluatingState location term value) (IntMap.IntMap term)
-_jumps = lens jumps (\ s j -> s {jumps = j})
-
-_origin :: Lens' (EvaluatingState location term value) (SomeOrigin term)
-_origin = lens origin (\ s o -> s {origin = o})
-
-
-(.=) :: Member (State (EvaluatingState location term value)) effects => ASetter (EvaluatingState location term value) (EvaluatingState location term value) a b -> b -> Evaluating location term value effects ()
-lens .= val = raise (modify' (lens .~ val))
-
-view :: Member (State (EvaluatingState location term value)) effects => Getting a (EvaluatingState location term value) a -> Evaluating location term value effects a
-view lens = raise (gets (^. lens))
-
-localEvaluatingState :: Member (State (EvaluatingState location term value)) effects => Lens' (EvaluatingState location term value) prj -> (prj -> prj) -> Evaluating location term value effects a -> Evaluating location term value effects a
-localEvaluatingState lens f action = do
-  original <- view lens
-  lens .= f original
-  v <- action
-  v <$ lens .= original
-
-
-instance Members '[Fail, State (EvaluatingState location term value)] effects => MonadControl term (Evaluating location term value effects) where
-  label term = do
-    m <- view _jumps
-    let i = IntMap.size m
-    _jumps .= IntMap.insert i term m
-    pure i
-
-  goto label = IntMap.lookup label <$> view _jumps >>= maybe (fail ("unknown label: " <> show label)) pure
-
-instance Members '[ State (EvaluatingState location term value)
-                  , Reader (Environment location value)
-                  ] effects
-      => MonadEnvironment location value (Evaluating location term value effects) where
-  getEnv = view _environment
-  putEnv = (_environment .=)
-  withEnv s = localEvaluatingState _environment (const s)
-
-  defaultEnvironment = raise ask
-  withDefaultEnvironment e = raise . local (const e) . lower
-
-  getExports = view _exports
-  putExports = (_exports .=)
-  withExports s = localEvaluatingState _exports (const s)
-
-  localEnv f a = do
-    modifyEnv (f . Env.push)
-    result <- a
-    result <$ modifyEnv Env.pop
-
-instance Member (State (EvaluatingState location term value)) effects
-      => MonadHeap location value (Evaluating location term value effects) where
-  getHeap = view _heap
-  putHeap = (_heap .=)
-
-instance Members '[ Reader (ModuleTable [Module term])
-                  , State (EvaluatingState location term value)
-                  , Reader (SomeOrigin term)
-                  , Fail
-                  ] effects
-      => MonadModuleTable location term value (Evaluating location term value effects) where
-  getModuleTable = view _modules
-  putModuleTable = (_modules .=)
-
-  askModuleTable = raise ask
-  localModuleTable f a = raise (local f (lower a))
-
-  getLoadStack = view _loadStack
-  putLoadStack = (_loadStack .=)
-
-  currentModule = do
-    o <- raise ask
-    maybeFail "unable to get currentModule" $ withSomeOrigin (originModule @term) o
-
-instance Members (EvaluatingEffects location term value) effects
-      => MonadEvaluator location term value (Evaluating location term value effects) where
+instance ( Member Fail effects
+         , Member (Reader (Environment location value)) effects
+         , Member (Reader (ModuleTable [Module term])) effects
+         , Member (Reader (SomeOrigin term)) effects
+         , Member (State (EvaluatorState location term value)) effects
+         )
+      => MonadEvaluator location term value effects (Evaluating location term value) where
   getConfiguration term = Configuration term mempty <$> getEnv <*> getHeap
 
 instance ( Corecursive term
-         , Members (EvaluatingEffects location term value) effects
+         , Member Fail effects
+         , Member (Reader (Environment location value)) effects
+         , Member (Reader (ModuleTable [Module term])) effects
+         , Member (Reader (SomeOrigin term)) effects
+         , Member (State (EvaluatorState location term value)) effects
          , Recursive term
          )
-      => MonadAnalysis location term value (Evaluating location term value effects) where
-  type Effects location term value (Evaluating location term value effects) = EvaluatingEffects location term value
+      => MonadAnalysis location term value effects (Evaluating location term value) where
+  type Effects location term value (Evaluating location term value) = EvaluatingEffects location term value
 
   analyzeTerm eval term = pushOrigin (termOrigin (embedSubterm term)) (eval term)
 
diff --git a/src/Analysis/Abstract/ImportGraph.hs b/src/Analysis/Abstract/ImportGraph.hs
index 1f44e71dc..b2c4496db 100644
--- a/src/Analysis/Abstract/ImportGraph.hs
+++ b/src/Analysis/Abstract/ImportGraph.hs
@@ -9,7 +9,7 @@ module Analysis.Abstract.ImportGraph
 import qualified Algebra.Graph as G
 import           Algebra.Graph.Class hiding (Vertex)
 import           Algebra.Graph.Export.Dot hiding (vertexName)
-import           Control.Abstract.Analysis
+import           Control.Abstract.Analysis hiding (origin)
 import           Data.Abstract.Address
 import           Data.Abstract.Evaluatable (LoadError (..))
 import           Data.Abstract.FreeVariables
@@ -55,13 +55,9 @@ style = (defaultStyle vertexName)
         edgeAttributes _          _          = []
 
 newtype ImportGraphing m (effects :: [* -> *]) a = ImportGraphing (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (ImportGraphing m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (ImportGraphing m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (ImportGraphing m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (ImportGraphing m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (ImportGraphing m effects)
+deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (ImportGraphing m)
 
 
 instance ( Effectful m
@@ -69,12 +65,12 @@ instance ( Effectful m
          , Member (Resumable (LoadError term value)) effects
          , Member (State ImportGraph) effects
          , Member Syntax.Identifier syntax
-         , MonadAnalysis (Located location term) term value (m effects)
+         , MonadAnalysis (Located location term) term value effects m
          , term ~ Term (Union syntax) ann
          , Show ann
          )
-      => MonadAnalysis (Located location term) term value (ImportGraphing m effects) where
-  type Effects (Located location term) term value (ImportGraphing m effects) = State ImportGraph ': Effects (Located location term) term value (m effects)
+      => MonadAnalysis (Located location term) term value effects (ImportGraphing m) where
+  type Effects (Located location term) term value (ImportGraphing m) = State ImportGraph ': Effects (Located location term) term value m
 
   analyzeTerm eval term@(In ann syntax) = do
     traceShowM ann
@@ -102,10 +98,8 @@ moduleGraph = maybe empty (vertex . Module . BC.pack . modulePath) . withSomeOri
 
 -- | Add an edge from the current package to the passed vertex.
 packageInclusion :: forall m location term value effects
-                 .  ( Effectful m
-                    , Member (Reader (SomeOrigin term)) effects
-                    , Member (State ImportGraph) effects
-                    , MonadEvaluator location term value (m effects)
+                 .  ( Member (State ImportGraph) effects
+                    , MonadEvaluator location term value effects m
                     )
                  => Vertex
                  -> ImportGraphing m effects ()
@@ -115,10 +109,8 @@ packageInclusion v = do
 
 -- | Add an edge from the current module to the passed vertex.
 moduleInclusion :: forall m location term value effects
-                .  ( Effectful m
-                   , Member (Reader (SomeOrigin term)) effects
-                   , Member (State ImportGraph) effects
-                   , MonadEvaluator location term value (m effects)
+                .  ( Member (State ImportGraph) effects
+                   , MonadEvaluator location term value effects m
                    )
                 => Vertex
                 -> ImportGraphing m effects ()
@@ -127,10 +119,11 @@ moduleInclusion v = do
   appendGraph (moduleGraph @term o `connect` vertex v)
 
 -- | Add an edge from the passed variable name to the module it originated within.
-variableDefinition :: ( Effectful m
-              , Member (State ImportGraph) effects
-              , MonadEvaluator (Located location term) term value (m effects)
-              ) => Name -> ImportGraphing m effects ()
+variableDefinition :: ( Member (State ImportGraph) effects
+                      , MonadEvaluator (Located location term) term value effects m
+                      )
+                   => Name
+                   -> ImportGraphing m effects ()
 variableDefinition name = do
   graph <- maybe empty (moduleGraph . origin . unAddress) <$> lookupEnv name
   appendGraph (vertex (Variable (unName name)) `connect` graph)
diff --git a/src/Analysis/Abstract/Quiet.hs b/src/Analysis/Abstract/Quiet.hs
index 1b7855cb8..523377ce7 100644
--- a/src/Analysis/Abstract/Quiet.hs
+++ b/src/Analysis/Abstract/Quiet.hs
@@ -15,21 +15,17 @@ import Prologue
 --
 --   Note that exceptions thrown by other analyses may not be caught if 'Quietly' doesn’t know about them, i.e. if they’re not part of the generic 'MonadValue', 'MonadAddressable', etc. machinery.
 newtype Quietly m (effects :: [* -> *]) a = Quietly (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (Quietly m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (Quietly m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (Quietly m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Quietly m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (Quietly m effects)
+deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Quietly m)
 
 instance ( Effectful m
          , Member (Resumable (Unspecialized value)) effects
-         , MonadAnalysis location term value (m effects)
-         , MonadValue location value (Quietly m effects)
+         , MonadAnalysis location term value effects m
+         , MonadValue location value effects (Quietly m)
          )
-      => MonadAnalysis location term value (Quietly m effects) where
-  type Effects location term value (Quietly m effects) = Effects location term value (m effects)
+      => MonadAnalysis location term value effects (Quietly m) where
+  type Effects location term value (Quietly m) = Effects location term value m
 
   analyzeTerm eval term = resume @(Unspecialized value) (liftAnalyze analyzeTerm eval term) (\yield err@(Unspecialized _) ->
           traceM ("Unspecialized:" <> show err) >> hole >>= yield)
diff --git a/src/Analysis/Abstract/Tracing.hs b/src/Analysis/Abstract/Tracing.hs
index c5258b903..244859bb7 100644
--- a/src/Analysis/Abstract/Tracing.hs
+++ b/src/Analysis/Abstract/Tracing.hs
@@ -14,23 +14,19 @@ import Prologue
 --
 --   Instantiating @trace@ to @[]@ yields a linear trace analysis, while @Set@ yields a reachable state analysis.
 newtype Tracing (trace :: * -> *) m (effects :: [* -> *]) a = Tracing (m effects a)
-  deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh)
+  deriving (Alternative, Applicative, Functor, Effectful, Monad)
 
-deriving instance MonadControl term (m effects)                    => MonadControl term (Tracing trace m effects)
-deriving instance MonadEnvironment location value (m effects)      => MonadEnvironment location value (Tracing trace m effects)
-deriving instance MonadHeap location value (m effects)             => MonadHeap location value (Tracing trace m effects)
-deriving instance MonadModuleTable location term value (m effects) => MonadModuleTable location term value (Tracing trace m effects)
-deriving instance MonadEvaluator location term value (m effects)   => MonadEvaluator location term value (Tracing trace m effects)
+deriving instance MonadEvaluator location term value effects m => MonadEvaluator location term value effects (Tracing trace m)
 
 instance ( Corecursive term
          , Effectful m
          , Member (Writer (trace (Configuration location term value))) effects
-         , MonadAnalysis location term value (m effects)
+         , MonadAnalysis location term value effects m
          , Ord location
          , Reducer (Configuration location term value) (trace (Configuration location term value))
          )
-      => MonadAnalysis location term value (Tracing trace m effects) where
-  type Effects location term value (Tracing trace m effects) = Writer (trace (Configuration location term value)) ': Effects location term value (m effects)
+      => MonadAnalysis location term value effects (Tracing trace m) where
+  type Effects location term value (Tracing trace m) = Writer (trace (Configuration location term value)) ': Effects location term value m
 
   analyzeTerm recur term = do
     config <- getConfiguration (embedSubterm term)
diff --git a/src/Control/Abstract/Addressable.hs b/src/Control/Abstract/Addressable.hs
index 87b904de2..c5f070e97 100644
--- a/src/Control/Abstract/Addressable.hs
+++ b/src/Control/Abstract/Addressable.hs
@@ -1,39 +1,39 @@
-{-# LANGUAGE TypeFamilies, UndecidableInstances, GADTs #-}
+{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances #-}
 module Control.Abstract.Addressable where
 
 import Control.Abstract.Evaluator
 import Control.Applicative
+import Control.Effect
 import Control.Effect.Fresh
+import Control.Monad.Effect.Resumable as Eff
 import Data.Abstract.Address
 import Data.Abstract.Environment (insert)
 import Data.Abstract.FreeVariables
 import Data.Semigroup.Reducer
-import Prelude hiding (fail)
 import Prologue
 
 -- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Heap.
-class (MonadFresh m, Ord location) => MonadAddressable location m where
-  derefCell :: Address location value -> Cell location value -> m value
+class (Effectful m, Member Fresh effects, Monad (m effects), Ord location) => MonadAddressable location effects m where
+  derefCell :: Address location value -> Cell location value -> m effects (Maybe value)
 
-  allocLoc :: Name -> m location
+  allocLoc :: Name -> m effects location
 
 -- | Look up or allocate an address for a 'Name'.
-lookupOrAlloc :: ( MonadAddressable location m
-                 , MonadEnvironment location value m
+lookupOrAlloc :: ( MonadAddressable location effects m
+                 , MonadEvaluator location term value effects m
                  )
               => Name
-              -> m (Address location value)
+              -> m effects (Address location value)
 lookupOrAlloc name = lookupEnv name >>= maybe (alloc name) pure
 
 
-letrec :: ( MonadAddressable location m
-          , MonadEnvironment location value m
-          , MonadHeap location value m
+letrec :: ( MonadAddressable location effects m
+          , MonadEvaluator location term value effects m
           , Reducer value (Cell location value)
           )
        => Name
-       -> m value
-       -> m (value, Address location value)
+       -> m effects value
+       -> m effects (value, Address location value)
 letrec name body = do
   addr <- lookupOrAlloc name
   v <- localEnv (insert name addr) body
@@ -41,12 +41,12 @@ letrec name body = do
   pure (v, addr)
 
 -- Lookup/alloc a name passing the address to a body evaluated in a new local environment.
-letrec' :: ( MonadAddressable location m
-           , MonadEnvironment location value m
+letrec' :: ( MonadAddressable location effects m
+           , MonadEvaluator location term value effects m
            )
         => Name
-        -> (Address location value -> m value)
-        -> m value
+        -> (Address location value -> m effects value)
+        -> m effects value
 letrec' name body = do
   addr <- lookupOrAlloc name
   v <- localEnv id (body addr)
@@ -55,27 +55,28 @@ letrec' name body = do
 -- Instances
 
 -- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
-instance (MonadFail m, MonadFresh m) => MonadAddressable Precise m where
-  derefCell addr = maybeM (uninitializedAddress addr) . unLatest
+instance (Effectful m, Member Fresh effects, Monad (m effects)) => MonadAddressable Precise effects m where
+  derefCell _ = pure . unLatest
   allocLoc _ = Precise <$> fresh
 
 -- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
-instance (Alternative m, MonadFresh m) => MonadAddressable Monovariant m where
-  derefCell _ = foldMapA pure
+instance (Alternative (m effects), Effectful m, Member Fresh effects, Monad (m effects)) => MonadAddressable Monovariant effects m where
+  derefCell _ cell | null cell = pure Nothing
+                   | otherwise = Just <$> foldMapA pure cell
   allocLoc = pure . Monovariant
 
 -- | Dereference the given 'Address'in the heap, or fail if the address is uninitialized.
-deref :: (MonadResume (AddressError location value) m, MonadAddressable location m, MonadHeap location value m) => Address location value -> m value
-deref addr = lookupHeap addr >>= maybe (throwAddressError $ UninitializedAddress addr) (derefCell addr)
+deref :: (Member (Resumable (AddressError location value)) effects, MonadAddressable location effects m, MonadEvaluator location term value effects m) => Address location value -> m effects value
+deref addr = do
+  cell <- lookupHeap addr >>= maybeM (throwAddressError (UnallocatedAddress addr))
+  derefed <- derefCell addr cell
+  maybeM (throwAddressError (UninitializedAddress addr)) derefed
 
-alloc :: MonadAddressable location m => Name -> m (Address location value)
+alloc :: MonadAddressable location effects m => Name -> m effects (Address location value)
 alloc = fmap Address . allocLoc
 
--- | Fail with a message denoting an uninitialized address (i.e. one which was 'alloc'ated, but never 'assign'ed a value before being 'deref'erenced).
-uninitializedAddress :: (MonadFail m, Show location) => Address location value -> m a
-uninitializedAddress addr = fail $ "uninitialized address: " <> show addr
-
 data AddressError location value resume where
+  UnallocatedAddress :: Address location value -> AddressError location value (Cell location value)
   UninitializedAddress :: Address location value -> AddressError location value value
 
 deriving instance Eq location => Eq (AddressError location value resume)
@@ -83,9 +84,10 @@ deriving instance Show location => Show (AddressError location value resume)
 instance Show location => Show1 (AddressError location value) where
   liftShowsPrec _ _ = showsPrec
 instance Eq location => Eq1 (AddressError location value) where
-  liftEq _ (UninitializedAddress a) (UninitializedAddress b)     = a == b
+  liftEq _ (UninitializedAddress a) (UninitializedAddress b) = a == b
+  liftEq _ (UnallocatedAddress a)   (UnallocatedAddress b)   = a == b
+  liftEq _ _                        _                        = False
 
 
-throwAddressError :: (MonadResume (AddressError location value) m) => AddressError location value resume -> m resume
-throwAddressError = throwResumable
-
+throwAddressError :: (Effectful m, Member (Resumable (AddressError location value)) effects) => AddressError location value resume -> m effects resume
+throwAddressError = raise . Eff.throwError
diff --git a/src/Control/Abstract/Analysis.hs b/src/Control/Abstract/Analysis.hs
index 37ca69d60..7e6c60b2b 100644
--- a/src/Control/Abstract/Analysis.hs
+++ b/src/Control/Abstract/Analysis.hs
@@ -29,20 +29,20 @@ import Prologue
 -- | A 'Monad' in which one can evaluate some specific term type to some specific value type.
 --
 --   This typeclass is left intentionally unconstrained to avoid circular dependencies between it and other typeclasses.
-class MonadEvaluator location term value m => MonadAnalysis location term value m where
+class MonadEvaluator location term value effects m => MonadAnalysis location term value effects m where
   -- | The effects necessary to run the analysis. Analyses which are composed on top of (wrap) other analyses should include the inner analyses 'Effects' in their own list.
   type family Effects location term value m :: [* -> *]
 
   -- | Analyze a term using the semantics of the current analysis.
-  analyzeTerm :: (Base term (Subterm term (outer value)) -> m value)
-              -> (Base term (Subterm term (outer value)) -> m value)
+  analyzeTerm :: (Base term (Subterm term (outer effects value)) -> m effects value)
+              -> (Base term (Subterm term (outer effects value)) -> m effects value)
 
   -- | Analyze a module using the semantics of the current analysis. This should generally only be called by 'evaluateModule' and by definitions of 'analyzeModule' in instances for composite analyses.
-  analyzeModule :: (Module (Subterm term (outer value)) -> m value)
-                -> (Module (Subterm term (outer value)) -> m value)
+  analyzeModule :: (Module (Subterm term (outer effects value)) -> m effects value)
+                -> (Module (Subterm term (outer effects value)) -> m effects value)
 
   -- | Isolate the given action with an empty global environment and exports.
-  isolate :: m a -> m a
+  isolate :: m effects a -> m effects a
   isolate = withEnv mempty . withExports mempty
 
 
@@ -57,8 +57,8 @@ liftAnalyze analyze recur term = coerce (analyze (coerceWith (sym Coercion) . r
 --
 --   This enables us to refer to the analysis type as e.g. @Analysis1 (Analysis2 Evaluating) Term Value@ without explicitly mentioning its effects (which are inferred to be simply its 'Effects').
 runAnalysis :: ( Effectful m
-               , Effects location term value (m effects) ~ effects
-               , MonadAnalysis location term value (m effects)
+               , Effects location term value m ~ effects
+               , MonadAnalysis location term value effects m
                , RunEffects effects a
                )
             => m effects a
@@ -69,8 +69,8 @@ runAnalysis = X.run
 -- | An abstraction over analyses.
 data SomeAnalysis m result where
   SomeAnalysis :: ( Effectful m
-                  , effects ~ Effects location term value (m effects)
-                  , MonadAnalysis location term value (m effects)
+                  , effects ~ Effects location term value m
+                  , MonadAnalysis location term value effects m
                   , RunEffects effects a
                   )
                => m effects a
diff --git a/src/Control/Abstract/Evaluator.hs b/src/Control/Abstract/Evaluator.hs
index 3b88a9590..6cf18eadb 100644
--- a/src/Control/Abstract/Evaluator.hs
+++ b/src/Control/Abstract/Evaluator.hs
@@ -1,27 +1,57 @@
-{-# LANGUAGE ConstrainedClassMethods, DataKinds, FunctionalDependencies, RankNTypes, TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE ConstrainedClassMethods, FunctionalDependencies, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
 module Control.Abstract.Evaluator
   ( MonadEvaluator(..)
-  , MonadEnvironment(..)
+  -- State
+  , EvaluatorState(..)
+  -- Environment
+  , getEnv
+  , putEnv
   , modifyEnv
+  , withEnv
+  , defaultEnvironment
+  , withDefaultEnvironment
+  , fullEnvironment
+  , localEnv
+  , localize
+  , lookupEnv
+  , lookupWith
+  -- Exports
+  , getExports
+  , putExports
   , modifyExports
   , addExport
-  , fullEnvironment
-  , MonadHeap(..)
+  , withExports
+  -- Heap
+  , getHeap
+  , putHeap
   , modifyHeap
-  , localize
   , lookupHeap
   , assign
-  , MonadModuleTable(..)
+  -- Module tables
+  , getModuleTable
+  , putModuleTable
   , modifyModuleTable
+  , askModuleTable
+  , localModuleTable
+  , getLoadStack
+  , putLoadStack
   , modifyLoadStack
-  , MonadControl(..)
-  , MonadResume(..)
-  , MonadExc(..)
+  , currentModule
+  -- Control
+  , label
+  , goto
+  -- Exceptions
+  , throwResumable
+  , throwException
+  , catchException
   ) where
 
 import Control.Effect
 import Control.Monad.Effect.Exception as Exception
+import Control.Monad.Effect.Fail
+import Control.Monad.Effect.Reader
 import Control.Monad.Effect.Resumable as Resumable
+import Control.Monad.Effect.State
 import Data.Abstract.Address
 import Data.Abstract.Configuration
 import Data.Abstract.Environment as Env
@@ -30,7 +60,12 @@ import Data.Abstract.FreeVariables
 import Data.Abstract.Heap
 import Data.Abstract.Module
 import Data.Abstract.ModuleTable
+import Data.Abstract.Origin
+import Data.Empty
+import qualified Data.IntMap as IntMap
 import Data.Semigroup.Reducer
+import Lens.Micro
+import Prelude hiding (fail)
 import Prologue
 
 -- | A 'Monad' providing the basic essentials for evaluation.
@@ -39,161 +74,265 @@ import Prologue
 --   - environments binding names to addresses
 --   - a heap mapping addresses to (possibly sets of) values
 --   - tables of modules available for import
-class ( MonadControl term m
-      , MonadEnvironment location value m
-      , MonadFail m
-      , MonadModuleTable location term value m
-      , MonadHeap location value m
+class ( Effectful m
+      , Member Fail effects
+      , Member (Reader (Environment location value)) effects
+      , Member (Reader (ModuleTable [Module term])) effects
+      , Member (Reader (SomeOrigin term)) effects
+      , Member (State (EvaluatorState location term value)) effects
+      , Monad (m effects)
       )
-      => MonadEvaluator location term value m | m -> location, m -> term, m -> value where
+   => MonadEvaluator location term value effects m | m effects -> location term value where
   -- | Get the current 'Configuration' with a passed-in term.
-  getConfiguration :: Ord location => term -> m (Configuration location term value)
+  getConfiguration :: Ord location => term -> m effects (Configuration location term value)
 
--- | A 'Monad' abstracting local and global environments.
-class Monad m => MonadEnvironment location value m | m -> value, m -> location where
-  -- | Retrieve the environment.
-  getEnv :: m (Environment location value)
-  -- | Set the environment.
-  putEnv :: Environment location value -> m ()
-  -- | Sets the environment for the lifetime of the given action.
-  withEnv :: Environment location value -> m a -> m a
 
-  -- | Retrieve the default environment.
-  defaultEnvironment :: m (Environment location value)
+-- State
 
-  -- | Set the default environment for the lifetime of an action.
-  --   Usually only invoked in a top-level evaluation function.
-  withDefaultEnvironment :: Environment location value -> m a -> m a
+data EvaluatorState location term value = EvaluatorState
+  { environment :: Environment location value
+  , heap        :: Heap location value
+  , modules     :: ModuleTable (Environment location value, value)
+  , loadStack   :: LoadStack
+  , exports     :: Exports location value
+  , jumps       :: IntMap.IntMap term
+  , origin      :: SomeOrigin term
+  }
 
-  -- | Get the global export state.
-  getExports :: m (Exports location value)
-  -- | Set the global export state.
-  putExports :: Exports location value -> m ()
-  -- | Sets the global export state for the lifetime of the given action.
-  withExports :: Exports location value -> m a -> m a
+deriving instance (Eq (Cell location value), Eq location, Eq term, Eq value, Eq (Base term ())) => Eq (EvaluatorState location term value)
+deriving instance (Ord (Cell location value), Ord location, Ord term, Ord value, Ord (Base term ())) => Ord (EvaluatorState location term value)
+deriving instance (Show (Cell location value), Show location, Show term, Show value, Show (Base term ())) => Show (EvaluatorState location term value)
 
-  -- | Run an action with a locally-modified environment.
-  localEnv :: (Environment location value -> Environment location value) -> m a -> m a
+instance (Ord location, Semigroup (Cell location value)) => Semigroup (EvaluatorState location term value) where
+  EvaluatorState e1 h1 m1 l1 x1 j1 o1 <> EvaluatorState e2 h2 m2 l2 x2 j2 o2 = EvaluatorState (e1 <> e2) (h1 <> h2) (m1 <> m2) (l1 <> l2) (x1 <> x2) (j1 <> j2) (o1 <> o2)
 
-  -- | Look a 'Name' up in the current environment, trying the default environment if no value is found.
-  lookupEnv :: Name -> m (Maybe (Address location value))
-  lookupEnv name = (<|>) <$> (Env.lookup name <$> getEnv) <*> (Env.lookup name <$> defaultEnvironment)
+instance (Ord location, Semigroup (Cell location value)) => Empty (EvaluatorState location term value) where
+  empty = EvaluatorState mempty mempty mempty mempty mempty mempty mempty
 
-  -- | Look up a 'Name' in the environment, running an action with the resolved address (if any).
-  lookupWith :: (Address location value -> m a) -> Name -> m (Maybe a)
-  lookupWith with name = do
-    addr <- lookupEnv name
-    maybe (pure Nothing) (fmap Just . with) addr
 
--- | Run a computation in a new local environment.
-localize :: MonadEnvironment location value m => m a -> m a
-localize = localEnv id
+-- Lenses
+
+_environment :: Lens' (EvaluatorState location term value) (Environment location value)
+_environment = lens environment (\ s e -> s {environment = e})
+
+_heap :: Lens' (EvaluatorState location term value) (Heap location value)
+_heap = lens heap (\ s h -> s {heap = h})
+
+_modules :: Lens' (EvaluatorState location term value) (ModuleTable (Environment location value, value))
+_modules = lens modules (\ s m -> s {modules = m})
+
+_loadStack :: Lens' (EvaluatorState location term value) LoadStack
+_loadStack = lens loadStack (\ s l -> s {loadStack = l})
+
+_exports :: Lens' (EvaluatorState location term value) (Exports location value)
+_exports = lens exports (\ s e -> s {exports = e})
+
+_jumps :: Lens' (EvaluatorState location term value) (IntMap.IntMap term)
+_jumps = lens jumps (\ s j -> s {jumps = j})
+
+_origin :: Lens' (EvaluatorState location term value) (SomeOrigin term)
+_origin = lens origin (\ s o -> s {origin = o})
+
+
+(.=) :: MonadEvaluator location term value effects m => ASetter (EvaluatorState location term value) (EvaluatorState location term value) a b -> b -> m effects ()
+lens .= val = raise (modify' (lens .~ val))
+
+view :: MonadEvaluator location term value effects m => Getting a (EvaluatorState location term value) a -> m effects a
+view lens = raise (gets (^. lens))
+
+localEvaluatorState :: MonadEvaluator location term value effects m => Lens' (EvaluatorState location term value) prj -> (prj -> prj) -> m effects a -> m effects a
+localEvaluatorState lens f action = do
+  original <- view lens
+  lens .= f original
+  v <- action
+  v <$ lens .= original
+
+
+-- Environment
+
+-- | Retrieve the environment.
+getEnv :: MonadEvaluator location term value effects m => m effects (Environment location value)
+getEnv = view _environment
+
+-- | Set the environment.
+putEnv :: MonadEvaluator location term value effects m => Environment location value -> m effects ()
+putEnv = (_environment .=)
 
 -- | Update the global environment.
-modifyEnv :: MonadEnvironment location value m => (Environment location value -> Environment location value) -> m ()
+modifyEnv :: MonadEvaluator location term value effects m => (Environment location value -> Environment location value) -> m effects ()
 modifyEnv f = do
   env <- getEnv
   putEnv $! f env
 
+-- | Sets the environment for the lifetime of the given action.
+withEnv :: MonadEvaluator location term value effects m => Environment location value -> m effects a -> m effects a
+withEnv s = localEvaluatorState _environment (const s)
+
+
+-- | Retrieve the default environment.
+defaultEnvironment :: MonadEvaluator location term value effects m => m effects (Environment location value)
+defaultEnvironment = raise ask
+
+-- | Set the default environment for the lifetime of an action.
+--   Usually only invoked in a top-level evaluation function.
+withDefaultEnvironment :: MonadEvaluator location term value effects m => Environment location value -> m effects a -> m effects a
+withDefaultEnvironment e = raise . local (const e) . lower
+
+-- | Obtain an environment that is the composition of the current and default environments.
+--   Useful for debugging.
+fullEnvironment :: MonadEvaluator location term value effects m => m effects (Environment location value)
+fullEnvironment = mappend <$> getEnv <*> defaultEnvironment
+
+-- | Run an action with a locally-modified environment.
+localEnv :: MonadEvaluator location term value effects m => (Environment location value -> Environment location value) -> m effects a -> m effects a
+localEnv f a = do
+  modifyEnv (f . Env.push)
+  result <- a
+  result <$ modifyEnv Env.pop
+
+-- | Run a computation in a new local environment.
+localize :: MonadEvaluator location term value effects m => m effects a -> m effects a
+localize = localEnv id
+
+-- | Look a 'Name' up in the current environment, trying the default environment if no value is found.
+lookupEnv :: MonadEvaluator location term value effects m => Name -> m effects (Maybe (Address location value))
+lookupEnv name = (<|>) <$> (Env.lookup name <$> getEnv) <*> (Env.lookup name <$> defaultEnvironment)
+
+-- | Look up a 'Name' in the environment, running an action with the resolved address (if any).
+lookupWith :: MonadEvaluator location term value effects m => (Address location value -> m effects a) -> Name -> m effects (Maybe a)
+lookupWith with name = do
+  addr <- lookupEnv name
+  maybe (pure Nothing) (fmap Just . with) addr
+
+
+-- Exports
+
+-- | Get the global export state.
+getExports :: MonadEvaluator location term value effects m => m effects (Exports location value)
+getExports = view _exports
+
+-- | Set the global export state.
+putExports :: MonadEvaluator location term value effects m => Exports location value -> m effects ()
+putExports = (_exports .=)
+
 -- | Update the global export state.
-modifyExports :: MonadEnvironment location value m => (Exports location value -> Exports location value) -> m ()
+modifyExports :: MonadEvaluator location term value effects m => (Exports location value -> Exports location value) -> m effects ()
 modifyExports f = do
   exports <- getExports
   putExports $! f exports
 
 -- | Add an export to the global export state.
-addExport :: MonadEnvironment location value m => Name -> Name -> Maybe (Address location value) -> m ()
+addExport :: MonadEvaluator location term value effects m => Name -> Name -> Maybe (Address location value) -> m effects ()
 addExport name alias = modifyExports . Export.insert name alias
 
--- | Obtain an environment that is the composition of the current and default environments.
---   Useful for debugging.
-fullEnvironment :: MonadEnvironment location value m => m (Environment location value)
-fullEnvironment = mappend <$> getEnv <*> defaultEnvironment
+-- | Sets the global export state for the lifetime of the given action.
+withExports :: MonadEvaluator location term value effects m => Exports location value -> m effects a -> m effects a
+withExports s = localEvaluatorState _exports (const s)
 
--- | A 'Monad' abstracting a heap of values.
-class Monad m => MonadHeap location value m | m -> value, m -> location where
-  -- | Retrieve the heap.
-  getHeap :: m (Heap location value)
-  -- | Set the heap.
-  putHeap :: Heap location value -> m ()
+
+-- Heap
+
+-- | Retrieve the heap.
+getHeap :: MonadEvaluator location term value effects m => m effects (Heap location value)
+getHeap = view _heap
+
+-- | Set the heap.
+putHeap :: MonadEvaluator location term value effects m => Heap location value -> m effects ()
+putHeap = (_heap .=)
 
 -- | Update the heap.
-modifyHeap :: MonadHeap location value m => (Heap location value -> Heap location value) -> m ()
+modifyHeap :: MonadEvaluator location term value effects m => (Heap location value -> Heap location value) -> m effects ()
 modifyHeap f = do
   s <- getHeap
   putHeap $! f s
 
 -- | Look up the cell for the given 'Address' in the 'Heap'.
-lookupHeap :: (MonadHeap location value m, Ord location) => Address location value -> m (Maybe (Cell location value))
+lookupHeap :: (MonadEvaluator location term value effects m, Ord location) => Address location value -> m effects (Maybe (Cell location value))
 lookupHeap = flip fmap getHeap . heapLookup
 
 -- | Write a value to the given 'Address' in the 'Store'.
 assign :: ( Ord location
-          , MonadHeap location value m
+          , MonadEvaluator location term value effects m
           , Reducer value (Cell location value)
           )
        => Address location value
        -> value
-       -> m ()
+       -> m effects ()
 assign address = modifyHeap . heapInsert address
 
 
--- | A 'Monad' abstracting tables of modules available for import.
-class Monad m => MonadModuleTable location term value m | m -> location, m -> term, m -> value where
-  -- | Retrieve the table of evaluated modules.
-  getModuleTable :: m (ModuleTable (Environment location value, value))
-  -- | Set the table of evaluated modules.
-  putModuleTable :: ModuleTable (Environment location value, value) -> m ()
+-- Module table
 
-  -- | Retrieve the table of unevaluated modules.
-  askModuleTable :: m (ModuleTable [Module term])
-  -- | Run an action with a locally-modified table of unevaluated modules.
-  localModuleTable :: (ModuleTable [Module term] -> ModuleTable [Module term]) -> m a -> m a
+-- | Retrieve the table of evaluated modules.
+getModuleTable :: MonadEvaluator location term value effects m => m effects (ModuleTable (Environment location value, value))
+getModuleTable = view _modules
 
-  -- | Retrieve the module load stack
-  getLoadStack :: m LoadStack
-  -- | Set the module load stack
-  putLoadStack :: LoadStack -> m ()
-
-  -- | Get the currently evaluating 'ModuleInfo'.
-  currentModule :: m ModuleInfo
+-- | Set the table of evaluated modules.
+putModuleTable :: MonadEvaluator location term value effects m => ModuleTable (Environment location value, value) -> m effects ()
+putModuleTable = (_modules .=)
 
 -- | Update the evaluated module table.
-modifyModuleTable :: MonadModuleTable location term value m => (ModuleTable (Environment location value, value) -> ModuleTable (Environment location value, value)) -> m ()
+modifyModuleTable :: MonadEvaluator location term value effects m => (ModuleTable (Environment location value, value) -> ModuleTable (Environment location value, value)) -> m effects ()
 modifyModuleTable f = do
   table <- getModuleTable
   putModuleTable $! f table
 
+
+-- | Retrieve the table of unevaluated modules.
+askModuleTable :: MonadEvaluator location term value effects m => m effects (ModuleTable [Module term])
+askModuleTable = raise ask
+
+-- | Run an action with a locally-modified table of unevaluated modules.
+localModuleTable :: MonadEvaluator location term value effects m => (ModuleTable [Module term] -> ModuleTable [Module term]) -> m effects a -> m effects a
+localModuleTable f a = raise (local f (lower a))
+
+
+-- | Retrieve the module load stack
+getLoadStack :: MonadEvaluator location term value effects m => m effects LoadStack
+getLoadStack = view _loadStack
+
+-- | Set the module load stack
+putLoadStack :: MonadEvaluator location term value effects m => LoadStack -> m effects ()
+putLoadStack = (_loadStack .=)
+
 -- | Update the module load stack.
-modifyLoadStack :: MonadModuleTable location term value m => (LoadStack -> LoadStack) -> m ()
+modifyLoadStack :: MonadEvaluator location term value effects m => (LoadStack -> LoadStack) -> m effects ()
 modifyLoadStack f = do
   stack <- getLoadStack
   putLoadStack $! f stack
 
 
--- | A 'Monad' abstracting jumps in imperative control.
-class Monad m => MonadControl term m where
-  -- | Allocate a 'Label' for the given @term@.
-  --
-  --   Labels must be allocated before being jumped to with 'goto', but are suitable for nonlocal jumps; thus, they can be used to implement coroutines, exception handling, call with current continuation, and other esoteric control mechanisms.
-  label :: term -> m Label
-  -- | “Jump” to a previously-allocated 'Label' (retrieving the @term@ at which it points, which can then be evaluated in e.g. a 'MonadAnalysis' instance).
-  goto :: Label -> m term
+-- | Get the currently evaluating 'ModuleInfo'.
+currentModule :: forall location term value effects m . MonadEvaluator location term value effects m => m effects ModuleInfo
+currentModule = do
+  o <- raise ask
+  maybeM (raise (fail "unable to get currentModule")) $ withSomeOrigin (originModule @term) o
 
 
--- | 'Monad's which can throw exceptions of type @exc v@ which can be resumed with a value of type @v@.
-class Monad m => MonadResume exc m where
-  throwResumable :: exc v -> m v
-  catchResumable :: m v -> (forall v1. exc v1 -> m v) -> m v
+-- Control
 
-instance (Effectful m1, Member (Resumable exc) effects, Monad (m1 effects)) => MonadResume exc (m1 effects) where
-  throwResumable = raise . Resumable.throwError
-  catchResumable c f = raise (Resumable.catchError (lower c) (lower . f))
+-- | Allocate a 'Label' for the given @term@.
+--
+--   Labels must be allocated before being jumped to with 'goto', but are suitable for nonlocal jumps; thus, they can be used to implement coroutines, exception handling, call with current continuation, and other esoteric control mechanisms.
+label :: MonadEvaluator location term value effects m => term -> m effects Label
+label term = do
+  m <- view _jumps
+  let i = IntMap.size m
+  _jumps .= IntMap.insert i term m
+  pure i
 
-class Monad m => MonadExc exc m where
-  throwException :: exc -> m v
-  catchException :: m v -> (exc -> m v) -> m v
+-- | “Jump” to a previously-allocated 'Label' (retrieving the @term@ at which it points, which can then be evaluated in e.g. a 'MonadAnalysis' instance).
+goto :: MonadEvaluator location term value effects m => Label -> m effects term
+goto label = IntMap.lookup label <$> view _jumps >>= maybe (raise (fail ("unknown label: " <> show label))) pure
 
-instance (Effectful m1, Member (Exc exc) effects, Monad (m1 effects)) => MonadExc exc (m1 effects) where
-  throwException = raise . Exception.throwError
-  catchException c f = raise (Exception.catchError (lower c) (lower . f))
+
+-- Exceptions
+
+throwResumable :: (Member (Resumable exc) effects, Effectful m) => exc v -> m effects v
+throwResumable = raise . Resumable.throwError
+
+throwException :: (Member (Exc exc) effects, Effectful m) => exc -> m effects a
+throwException = raise . Exception.throwError
+
+catchException :: (Member (Exc exc) effects, Effectful m) => m effects v -> (exc -> m effects v) -> m effects v
+catchException action handler = raise (lower action `Exception.catchError` (lower . handler))
diff --git a/src/Control/Abstract/Value.hs b/src/Control/Abstract/Value.hs
index 94bc80d1c..fa7fa1908 100644
--- a/src/Control/Abstract/Value.hs
+++ b/src/Control/Abstract/Value.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FunctionalDependencies, GADTs, Rank2Types, TypeFamilies, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, Rank2Types #-}
 module Control.Abstract.Value
 ( MonadValue(..)
 , Comparator(..)
@@ -34,151 +34,150 @@ data Comparator
 -- | A 'Monad' abstracting the evaluation of (and under) binding constructs (functions, methods, etc).
 --
 --   This allows us to abstract the choice of whether to evaluate under binders for different value types.
-class (Monad m, Show value) => MonadValue location value m | m value -> location where
+class (Monad (m effects), Show value) => MonadValue location value (effects :: [* -> *]) m | m effects value -> location where
   -- | Construct an abstract unit value.
   --   TODO: This might be the same as the empty tuple for some value types
-  unit :: m value
+  unit :: m effects value
 
   -- | Construct an abstract hole.
-  hole :: m value
+  hole :: m effects value
 
   -- | Construct an abstract integral value.
-  integer :: Prelude.Integer -> m value
+  integer :: Prelude.Integer -> m effects value
 
   -- | Lift a unary operator over a 'Num' to a function on 'value's.
   liftNumeric  :: (forall a . Num a => a -> a)
-               -> (value -> m value)
+               -> (value -> m effects value)
 
   -- | Lift a pair of binary operators to a function on 'value's.
   --   You usually pass the same operator as both arguments, except in the cases where
   --   Haskell provides different functions for integral and fractional operations, such
   --   as division, exponentiation, and modulus.
   liftNumeric2 :: (forall a b. Number a -> Number b -> SomeNumber)
-               -> (value -> value -> m value)
+               -> (value -> value -> m effects value)
 
   -- | Lift a Comparator (usually wrapping a function like == or <=) to a function on values.
-  liftComparison :: Comparator -> (value -> value -> m value)
+  liftComparison :: Comparator -> (value -> value -> m effects value)
 
   -- | Lift a unary bitwise operator to values. This is usually 'complement'.
   liftBitwise :: (forall a . Bits a => a -> a)
-              -> (value -> m value)
+              -> (value -> m effects value)
 
   -- | Lift a binary bitwise operator to values. The Integral constraint is
   --   necessary to satisfy implementation details of Haskell left/right shift,
   --   but it's fine, since these are only ever operating on integral values.
   liftBitwise2 :: (forall a . (Integral a, Bits a) => a -> a -> a)
-               -> (value -> value -> m value)
+               -> (value -> value -> m effects value)
 
   -- | Construct an abstract boolean value.
-  boolean :: Bool -> m value
+  boolean :: Bool -> m effects value
 
   -- | Construct an abstract string value.
-  string :: ByteString -> m value
+  string :: ByteString -> m effects value
 
   -- | Construct a self-evaluating symbol value.
   --   TODO: Should these be interned in some table to provide stronger uniqueness guarantees?
-  symbol :: ByteString -> m value
+  symbol :: ByteString -> m effects value
 
   -- | Construct a floating-point value.
-  float :: Scientific -> m value
+  float :: Scientific -> m effects value
 
   -- | Construct a rational value.
-  rational :: Prelude.Rational -> m value
+  rational :: Prelude.Rational -> m effects value
 
   -- | Construct an N-ary tuple of multiple (possibly-disjoint) values
-  multiple :: [value] -> m value
+  multiple :: [value] -> m effects value
 
   -- | Construct an array of zero or more values.
-  array :: [value] -> m value
+  array :: [value] -> m effects value
 
   -- | Construct a key-value pair for use in a hash.
-  kvPair :: value -> value -> m value
+  kvPair :: value -> value -> m effects value
 
   -- | Extract the contents of a key-value pair as a tuple.
-  asPair :: value -> m (value, value)
+  asPair :: value -> m effects (value, value)
 
   -- | Construct a hash out of pairs.
-  hash :: [(value, value)] -> m value
+  hash :: [(value, value)] -> m effects value
 
   -- | Extract a 'ByteString' from a given value.
-  asString :: value -> m ByteString
+  asString :: value -> m effects ByteString
 
   -- | Eliminate boolean values. TODO: s/boolean/truthy
-  ifthenelse :: value -> m value -> m value -> m value
+  ifthenelse :: value -> m effects value -> m effects value -> m effects value
 
   -- | Extract a 'Bool' from a given value.
-  asBool :: value -> m Bool
+  asBool :: value -> m effects Bool
 
   -- | Construct the nil/null datatype.
-  null :: m value
+  null :: m effects value
 
-  isHole :: value -> m Bool
+  isHole :: value -> m effects Bool
 
   -- | Build a class value from a name and environment.
   klass :: Name                       -- ^ The new class's identifier
         -> [value]                    -- ^ A list of superclasses
         -> Environment location value -- ^ The environment to capture
-        -> m value
+        -> m effects value
 
   -- | Build a namespace value from a name and environment stack
   --
   -- Namespaces model closures with monoidal environments.
   namespace :: Name                       -- ^ The namespace's identifier
             -> Environment location value -- ^ The environment to mappend
-            -> m value
+            -> m effects value
 
   -- | Extract the environment from any scoped object (e.g. classes, namespaces, etc).
-  scopedEnvironment :: value -> m (Environment location value)
+  scopedEnvironment :: value -> m effects (Environment location value)
 
   -- | Evaluate an abstraction (a binder like a lambda or method definition).
-  lambda :: (FreeVariables term, MonadControl term m) => [Name] -> Subterm term (m value) -> m value
+  lambda :: (FreeVariables term, MonadEvaluator location term value effects m) => [Name] -> Subterm term (m effects value) -> m effects value
   -- | Evaluate an application (like a function call).
-  call :: value -> [m value] -> m value
+  call :: value -> [m effects value] -> m effects value
 
   -- | Primitive looping combinator, approximately equivalent to 'fix'. This should be used in place of direct recursion, as it allows abstraction over recursion.
   --
   --   The function argument takes an action which recurs through the loop.
-  loop :: (m value -> m value) -> m value
+  loop :: (m effects value -> m effects value) -> m effects value
 
 
 -- | Attempt to extract a 'Prelude.Bool' from a given value.
-forLoop :: (MonadEnvironment location value m, MonadValue location value m)
-        => m value -- ^ Initial statement
-        -> m value -- ^ Condition
-        -> m value -- ^ Increment/stepper
-        -> m value -- ^ Body
-        -> m value
+forLoop :: (MonadEvaluator location term value effects m, MonadValue location value effects m)
+        => m effects value -- ^ Initial statement
+        -> m effects value -- ^ Condition
+        -> m effects value -- ^ Increment/stepper
+        -> m effects value -- ^ Body
+        -> m effects value
 forLoop initial cond step body =
   localize (initial *> while cond (body *> step))
 
 -- | The fundamental looping primitive, built on top of ifthenelse.
-while :: MonadValue location value m
-      => m value
-      -> m value
-      -> m value
+while :: MonadValue location value effects m
+      => m effects value
+      -> m effects value
+      -> m effects value
 while cond body = loop $ \ continue -> do
   this <- cond
   ifthenelse this (body *> continue) unit
 
 -- | Do-while loop, built on top of while.
-doWhile :: MonadValue location value m
-        => m value
-        -> m value
-        -> m value
+doWhile :: MonadValue location value effects m
+        => m effects value
+        -> m effects value
+        -> m effects value
 doWhile body cond = loop $ \ continue -> body *> do
   this <- cond
   ifthenelse this continue unit
 
-makeNamespace :: ( MonadValue location value m
-                 , MonadEnvironment location value m
-                 , MonadHeap location value m
+makeNamespace :: ( MonadValue location value effects m
+                 , MonadEvaluator location term value effects m
                  , Ord location
                  , Reducer value (Cell location value)
                  )
               => Name
               -> Address location value
               -> [value]
-              -> m value
+              -> m effects value
 makeNamespace name addr supers = do
   superEnv <- mconcat <$> traverse scopedEnvironment supers
   namespaceEnv <- Env.head <$> getEnv
diff --git a/src/Control/Effect/Fresh.hs b/src/Control/Effect/Fresh.hs
index 8db9ef609..6be171dea 100644
--- a/src/Control/Effect/Fresh.hs
+++ b/src/Control/Effect/Fresh.hs
@@ -11,17 +11,13 @@ data Fresh a where
   -- | Request a fresh variable name.
   Fresh :: Fresh Int
 
--- | 'Monad's offering a (resettable) sequence of guaranteed-fresh type variables.
-class Monad m => MonadFresh m where
-  -- | Get a fresh variable name, guaranteed unused (since the last 'reset').
-  fresh :: m Int
+-- | Get a fresh variable name, guaranteed unused (since the last 'reset').
+fresh :: (Effectful m, Member Fresh effects) => m effects Int
+fresh = raise (send Fresh)
 
-  -- | Reset the sequence of variable names. Useful to avoid complicated alpha-equivalence comparisons when iteratively recomputing the results of an analysis til convergence.
-  reset :: Int -> m ()
-
-instance (Fresh :< fs) => MonadFresh (Eff fs) where
-  fresh = send Fresh
-  reset = send . Reset
+-- | Reset the sequence of variable names. Useful to avoid complicated alpha-equivalence comparisons when iteratively recomputing the results of an analysis til convergence.
+reset :: (Effectful m, Member Fresh effects) => Int -> m effects ()
+reset = raise . send . Reset
 
 
 -- | 'Fresh' effects are interpreted starting from 0, incrementing the current name with each request for a fresh name, and overwriting the counter on reset.
diff --git a/src/Data/Abstract/Evaluatable.hs b/src/Data/Abstract/Evaluatable.hs
index e8fa87efd..7a036fa8f 100644
--- a/src/Data/Abstract/Evaluatable.hs
+++ b/src/Data/Abstract/Evaluatable.hs
@@ -28,6 +28,7 @@ module Data.Abstract.Evaluatable
 
 import           Control.Abstract.Addressable as X
 import           Control.Abstract.Analysis as X
+import qualified Control.Monad.Effect.Exception as Exc
 import           Data.Abstract.Address
 import           Data.Abstract.Declarations as X
 import           Data.Abstract.Environment as X
@@ -44,21 +45,23 @@ import           Data.Semigroup.Reducer hiding (unit)
 import           Data.Term
 import           Prologue
 
-type MonadEvaluatable location term value m =
-  ( Evaluatable (Base term)
+type MonadEvaluatable location term value effects m =
+  ( Declarations term
+  , Effectful m
+  , Evaluatable (Base term)
   , FreeVariables term
-  , Declarations term
-  , MonadAddressable location m
-  , MonadAnalysis location term value m
-  , MonadResume (Unspecialized value) m
-  , MonadResume (ValueError location value) m
-  , MonadResume (LoadError term value) m
-  , MonadResume (EvalError value) m
-  , MonadResume (ResolutionError value) m
-  , MonadResume (AddressError location value) m
-  , MonadExc (ReturnThrow value) m
-  , MonadExc (LoopThrow value) m
-  , MonadValue location value m
+  , Member (Exc.Exc (ReturnThrow value)) effects
+  , Member (Exc.Exc (LoopThrow value)) effects
+  , Member Fail effects
+  , Member (Resumable (Unspecialized value)) effects
+  , Member (Resumable (ValueError location value)) effects
+  , Member (Resumable (LoadError term value)) effects
+  , Member (Resumable (EvalError value)) effects
+  , Member (Resumable (ResolutionError value)) effects
+  , Member (Resumable (AddressError location value)) effects
+  , MonadAddressable location effects m
+  , MonadAnalysis location term value effects m
+  , MonadValue location value effects m
   , Recursive term
   , Reducer value (Cell location value)
   , Show location
@@ -112,7 +115,7 @@ data EvalError value resume where
 
 
 -- | Look up and dereference the given 'Name', throwing an exception for free variables.
-variable :: MonadEvaluatable location term value m => Name -> m value
+variable :: MonadEvaluatable location term value effects m => Name -> m effects value
 variable name = lookupWith deref name >>= maybeM (throwResumable (FreeVariableError name))
 
 deriving instance Eq (EvalError a b)
@@ -130,16 +133,16 @@ instance Eq1 (EvalError term) where
   liftEq _ _ _                                             = False
 
 
-throwValueError :: MonadEvaluatable location term value m => ValueError location value resume -> m resume
+throwValueError :: MonadEvaluatable location term value effects m => ValueError location value resume -> m effects resume
 throwValueError = throwResumable
 
-throwLoadError :: MonadEvaluatable location term value m => LoadError term value resume -> m resume
+throwLoadError :: MonadEvaluatable location term value effects m => LoadError term value resume -> m effects resume
 throwLoadError = throwResumable
 
-throwEvalError :: MonadEvaluatable location term value m => EvalError value resume -> m resume
+throwEvalError :: MonadEvaluatable location term value effects m => EvalError value resume -> m effects resume
 throwEvalError = throwResumable
 
-throwLoop :: MonadEvaluatable location term value m => LoopThrow value -> m a
+throwLoop :: MonadEvaluatable location term value effects m => LoopThrow value -> m effects a
 throwLoop = throwException
 
 data Unspecialized a b where
@@ -155,9 +158,9 @@ instance Show1 (Unspecialized a) where
 
 -- | The 'Evaluatable' class defines the necessary interface for a term to be evaluated. While a default definition of 'eval' is given, instances with computational content must implement 'eval' to perform their small-step operational semantics.
 class Evaluatable constr where
-  eval :: MonadEvaluatable location term value m
-       => SubtermAlgebra constr term (m value)
-  default eval :: (MonadResume (Unspecialized value) m, Show1 constr) => SubtermAlgebra constr term (m value)
+  eval :: MonadEvaluatable location term value effects m
+       => SubtermAlgebra constr term (m effects value)
+  default eval :: (MonadEvaluatable location term value effects m, Show1 constr) => SubtermAlgebra constr term (m effects value)
   eval expr = throwResumable (Unspecialized ("Eval unspecialized for " ++ liftShowsPrec (const (const id)) (const id) 0 expr ""))
 
 
@@ -181,9 +184,9 @@ instance Evaluatable [] where
   eval = maybe unit (runApp . foldMap1 (App . subtermValue)) . nonEmpty
 
 -- Resolve a list of module paths to a possible module table entry.
-resolve :: MonadEvaluatable location term value m
+resolve :: MonadEvaluatable location term value effects m
         => [FilePath]
-        -> m (Maybe ModulePath)
+        -> m effects (Maybe ModulePath)
 resolve names = do
   tbl <- askModuleTable
   pure $ find (`ModuleTable.member` tbl) names
@@ -191,25 +194,25 @@ resolve names = do
 traceResolve :: (Show a, Show b) => a -> b -> c -> c
 traceResolve name path = trace ("resolved " <> show name <> " -> " <> show path)
 
-listModulesInDir :: MonadEvaluatable location term value m
+listModulesInDir :: MonadEvaluatable location term value effects m
         => FilePath
-        -> m [ModulePath]
+        -> m effects [ModulePath]
 listModulesInDir dir = ModuleTable.modulePathsInDir dir <$> askModuleTable
 
 -- | Require/import another module by name and return it's environment and value.
 --
 -- Looks up the term's name in the cache of evaluated modules first, returns if found, otherwise loads/evaluates the module.
-require :: MonadEvaluatable location term value m
+require :: MonadEvaluatable location term value effects m
         => ModulePath
-        -> m (Environment location value, value)
+        -> m effects (Environment location value, value)
 require name = getModuleTable >>= maybeM (load name) . ModuleTable.lookup name
 
 -- | Load another module by name and return it's environment and value.
 --
 -- Always loads/evaluates.
-load :: MonadEvaluatable location term value m
+load :: MonadEvaluatable location term value effects m
      => ModulePath
-     -> m (Environment location value, value)
+     -> m effects (Environment location value, value)
 load name = askModuleTable >>= maybeM notFound . ModuleTable.lookup name >>= evalAndCache
   where
     notFound = throwLoadError (LoadError name)
@@ -249,30 +252,27 @@ load name = askModuleTable >>= maybeM notFound . ModuleTable.lookup name >>= eva
 -- | Evaluate a term to a value using the semantics of the current analysis.
 --
 --   This should always be called when e.g. evaluating the bodies of closures instead of explicitly folding either 'eval' or 'analyzeTerm' over subterms, except in 'MonadAnalysis' instances themselves. On the other hand, top-level evaluation should be performed using 'evaluateModule'.
-evaluateTerm :: MonadEvaluatable location term value m
+evaluateTerm :: MonadEvaluatable location term value effects m
              => term
-             -> m value
+             -> m effects value
 evaluateTerm = foldSubterms (analyzeTerm eval)
 
 -- | Evaluate a (root-level) term to a value using the semantics of the current analysis. This should be used to evaluate single-term programs, or (via 'evaluateModules') the entry point of multi-term programs.
-evaluateModule :: MonadEvaluatable location term value m
+evaluateModule :: MonadEvaluatable location term value effects m
                => Module term
-               -> m value
+               -> m effects value
 evaluateModule m = analyzeModule (subtermValue . moduleBody) (fmap (Subterm <*> evaluateTerm) m)
 
 -- | Evaluate a given package.
-evaluatePackage :: ( Effectful m
-                   , Member (Reader (SomeOrigin term)) effects
-                   , MonadEvaluatable location term value (m effects)
-                   )
+evaluatePackage :: MonadEvaluatable location term value effects m
                 => Package term
                 -> m effects [value]
 evaluatePackage p = pushOrigin (packageOrigin p) (evaluatePackageBody (packageBody p))
 
 -- | Evaluate a given package body (module table and entry points).
-evaluatePackageBody :: MonadEvaluatable location term value m
+evaluatePackageBody :: MonadEvaluatable location term value effects m
                     => PackageBody term
-                    -> m [value]
+                    -> m effects [value]
 evaluatePackageBody body = withPrelude (packagePrelude body) $
   localModuleTable (<> packageModules body) (traverse evaluateEntryPoint (ModuleTable.toPairs (packageEntryPoints body)))
   where
diff --git a/src/Data/Abstract/Located.hs b/src/Data/Abstract/Located.hs
index 7414f3041..fa2f367f3 100644
--- a/src/Data/Abstract/Located.hs
+++ b/src/Data/Abstract/Located.hs
@@ -19,10 +19,10 @@ instance (Location location, Ord (Base term ())) => Location (Located location t
 
 instance ( Effectful m
          , Member (Reader (SomeOrigin term)) effects
-         , MonadAddressable location (m effects)
+         , MonadAddressable location effects m
          , Ord (Base term ())
          )
-      => MonadAddressable (Located location term) (m effects) where
+      => MonadAddressable (Located location term) effects m where
   derefCell (Address (Located loc _)) = derefCell (Address loc)
 
   allocLoc name = Located <$> allocLoc name <*> raise ask
diff --git a/src/Data/Abstract/Type.hs b/src/Data/Abstract/Type.hs
index 95d8b900a..02c7e1255 100644
--- a/src/Data/Abstract/Type.hs
+++ b/src/Data/Abstract/Type.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- For the MonadValue instance, which requires MonadEvaluator to resolve its functional dependency.
 module Data.Abstract.Type
   ( Type (..)
   , TypeError (..)
@@ -58,7 +59,7 @@ instance Eq1 TypeError where
   liftEq _ _ _                                           = False
 
 -- | Unify two 'Type's.
-unify :: MonadResume TypeError m => Type -> Type -> m Type
+unify :: (Effectful m, Applicative (m effects), Member (Resumable TypeError) effects) => Type -> Type -> m effects Type
 unify (a1 :-> b1) (a2 :-> b2) = (:->) <$> unify a1 a2 <*> unify b1 b2
 unify a Null = pure a
 unify Null b = pure b
@@ -70,22 +71,18 @@ unify t1 t2
   | t1 == t2  = pure t2
   | otherwise = throwResumable (UnificationError t1 t2)
 
-
 instance Ord location => ValueRoots location Type where
   valueRoots _ = mempty
 
-
 -- | Discard the value arguments (if any), constructing a 'Type' instead.
-instance ( Alternative m
-         , MonadAddressable location m
-         , MonadEnvironment location Type m
-         , MonadFail m
-         , MonadFresh m
-         , MonadHeap location Type m
-         , MonadResume TypeError m
+instance ( Alternative (m effects)
+         , Member Fresh effects
+         , Member (Resumable TypeError) effects
+         , MonadAddressable location effects m
+         , MonadEvaluator location term Type effects m
          , Reducer Type (Cell location Type)
          )
-      => MonadValue location Type m where
+      => MonadValue location Type effects m where
   lambda names (Subterm _ body) = do
     (env, tvars) <- foldr (\ name rest -> do
       a <- alloc name
@@ -151,7 +148,9 @@ instance ( Alternative m
   call op params = do
     tvar <- fresh
     paramTypes <- sequenceA params
-    _ :-> ret <- op `unify` (Product paramTypes :-> Var tvar)
-    pure ret
+    unified <- op `unify` (Product paramTypes :-> Var tvar)
+    case unified of
+      _ :-> ret -> pure ret
+      _         -> raise (fail "unification with a function produced something other than a function")
 
   loop f = f empty
diff --git a/src/Data/Abstract/Value.hs b/src/Data/Abstract/Value.hs
index a45a67f20..256af31c5 100644
--- a/src/Data/Abstract/Value.hs
+++ b/src/Data/Abstract/Value.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances, ScopedTypeVariables #-}
+{-# LANGUAGE ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Data.Abstract.Value where
 
 import Control.Abstract.Analysis
@@ -198,7 +198,7 @@ instance Ord location => ValueRoots location (Value location) where
 
 
 -- | Construct a 'Value' wrapping the value arguments (if any).
-instance forall location term m. (Monad m, MonadEvaluatable location term (Value location) m) => MonadValue location (Value location) m where
+instance (Monad (m effects), MonadEvaluatable location term (Value location) effects m) => MonadValue location (Value location) effects m where
   hole     = pure . injValue $ Hole
   unit     = pure . injValue $ Unit
   integer  = pure . injValue . Integer . Number.Integer
@@ -277,7 +277,7 @@ instance forall location term m. (Monad m, MonadEvaluatable location term (Value
     | otherwise = throwValueError (Numeric2Error left right)
       where
         -- Dispatch whatever's contained inside a 'Number.SomeNumber' to its appropriate 'MonadValue' ctor
-        specialize :: MonadValue location value m => Number.SomeNumber -> m value
+        specialize :: MonadValue location value effects m => Number.SomeNumber -> m effects value
         specialize (Number.SomeNumber (Number.Integer i)) = integer i
         specialize (Number.SomeNumber (Number.Ratio r))          = rational r
         specialize (Number.SomeNumber (Number.Decimal d))        = float d
@@ -295,7 +295,7 @@ instance forall location term m. (Monad m, MonadEvaluatable location term (Value
       where
         -- Explicit type signature is necessary here because we're passing all sorts of things
         -- to these comparison functions.
-        go :: (Ord a, MonadValue location value m) => a -> a -> m value
+        go :: (Ord a, MonadValue location value effects m) => a -> a -> m effects value
         go l r = case comparator of
           Concrete f  -> boolean (f l r)
           Generalized -> integer (orderingToInt (compare l r))
@@ -331,13 +331,13 @@ instance forall location term m. (Monad m, MonadEvaluatable location term (Value
         localEnv (mappend bindings) (evalClosure label)
       Nothing -> throwValueError (CallError op)
     where
-      evalClosure :: Label -> m (Value location)
+      evalClosure :: Label -> m effects (Value location)
       evalClosure lab = catchException (goto lab >>= evaluateTerm) handleReturn
 
-      handleReturn :: ReturnThrow (Value location) -> m (Value location)
+      handleReturn :: ReturnThrow (Value location) -> m effects (Value location)
       handleReturn (Ret v) = pure v
 
   loop x = catchException (fix x) handleLoop where
-    handleLoop :: LoopThrow (Value location) -> m (Value location)
+    handleLoop :: LoopThrow (Value location) -> m effects (Value location)
     handleLoop (Brk v) = pure v
     handleLoop Con     = loop x
diff --git a/src/Data/Scientific/Exts.hs b/src/Data/Scientific/Exts.hs
index 9f43028f1..50df2a55d 100644
--- a/src/Data/Scientific/Exts.hs
+++ b/src/Data/Scientific/Exts.hs
@@ -3,16 +3,15 @@ module Data.Scientific.Exts
     , parseScientific
     ) where
 
-import Prelude hiding (filter, null, takeWhile)
-
 import Control.Applicative
-import Control.Monad
+import Control.Monad hiding (fail)
 import Data.Attoparsec.ByteString.Char8
 import Data.ByteString.Char8 hiding (readInt, takeWhile)
 import Data.Char (isOctDigit)
 import Data.Scientific
-import Data.Semigroup
 import Numeric
+import Prelude hiding (fail, filter, null, takeWhile)
+import Prologue hiding (null)
 import Text.Read (readMaybe)
 
 parseScientific :: ByteString -> Either String Scientific
@@ -38,9 +37,9 @@ parser = signed (choice [hex, oct, bin, dec]) where
   -- The ending stanza. Note the explicit endOfInput call to ensure we haven't left any dangling input.
   done = skipWhile (inClass "iIjJlL") *> endOfInput
 
-  -- Wrapper around readMaybe. Analogous to maybeFail in the Prologue, but no need to pull that in.
+  -- Wrapper around readMaybe.
   attempt :: Read a => String -> Parser a
-  attempt str = maybe (fail ("No parse: " <> str)) pure (readMaybe str)
+  attempt str = maybeM (fail ("No parse: " <> str)) (readMaybe str)
 
   -- Parse a hex value, leaning on the parser provided by Attoparsec.
   hex = fromIntegral <$> (string "0x" *> hexadecimal @Integer)
diff --git a/src/Language/Go/Syntax.hs b/src/Language/Go/Syntax.hs
index 70283df16..93c7c876e 100644
--- a/src/Language/Go/Syntax.hs
+++ b/src/Language/Go/Syntax.hs
@@ -22,7 +22,7 @@ defaultAlias :: ImportPath -> Name
 defaultAlias = name . BC.pack . takeFileName . unPath
 
 -- TODO: need to delineate between relative and absolute Go imports
-resolveGoImport :: MonadEvaluatable location term value m => FilePath -> m [ModulePath]
+resolveGoImport :: MonadEvaluatable location term value effects m => FilePath -> m effects [ModulePath]
 resolveGoImport relImportPath = do
   ModuleInfo{..} <- currentModule
   let relRootDir = takeDirectory modulePath
diff --git a/src/Language/PHP/Syntax.hs b/src/Language/PHP/Syntax.hs
index 088413995..4c8a6ff39 100644
--- a/src/Language/PHP/Syntax.hs
+++ b/src/Language/PHP/Syntax.hs
@@ -34,13 +34,13 @@ instance Evaluatable VariableName
 -- file, the complete contents of the included file are treated as though it
 -- were defined inside that function.
 
-resolvePHPName :: MonadEvaluatable location term value m => ByteString -> m ModulePath
-resolvePHPName n = resolve [name] >>= maybeFail notFound
+resolvePHPName :: MonadEvaluatable location term value effects m => ByteString -> m effects ModulePath
+resolvePHPName n = resolve [name] >>= maybeM (raise (fail notFound))
   where name = toName n
         notFound = "Unable to resolve: " <> name
         toName = BC.unpack . dropRelativePrefix . stripQuotes
 
-doInclude :: MonadEvaluatable location term value m => Subterm t (m value) -> m value
+doInclude :: MonadEvaluatable location term value effects m => Subterm t (m effects value) -> m effects value
 doInclude pathTerm = do
   name <- subtermValue pathTerm >>= asString
   path <- resolvePHPName name
@@ -48,7 +48,7 @@ doInclude pathTerm = do
   modifyEnv (mappend importedEnv)
   pure v
 
-doIncludeOnce :: MonadEvaluatable location term value m => Subterm t (m value) -> m value
+doIncludeOnce :: MonadEvaluatable location term value effects m => Subterm t (m effects value) -> m effects value
 doIncludeOnce pathTerm = do
   name <- subtermValue pathTerm >>= asString
   path <- resolvePHPName name
@@ -366,7 +366,7 @@ instance Evaluatable Namespace where
   eval Namespace{..} = go names
     where
       names = freeVariables (subterm namespaceName)
-      go [] = fail "expected at least one free variable in namespaceName, found none"
+      go [] = raise (fail "expected at least one free variable in namespaceName, found none")
       -- The last name creates a closure over the namespace body.
       go [name] = letrec' name $ \addr ->
         subtermValue namespaceBody *> makeNamespace name addr []
diff --git a/src/Language/Python/Syntax.hs b/src/Language/Python/Syntax.hs
index 245f06557..86d9ca63e 100644
--- a/src/Language/Python/Syntax.hs
+++ b/src/Language/Python/Syntax.hs
@@ -51,7 +51,7 @@ relativeQualifiedName prefix paths = RelativeQualifiedName (BC.unpack prefix) (J
 -- Subsequent imports of `parent.two` or `parent.three` will execute
 --     `parent/two/__init__.py` and
 --     `parent/three/__init__.py` respectively.
-resolvePythonModules :: MonadEvaluatable location term value m => QualifiedName -> m (NonEmpty ModulePath)
+resolvePythonModules :: MonadEvaluatable location term value effects m => QualifiedName -> m effects (NonEmpty ModulePath)
 resolvePythonModules q = do
   relRootDir <- rootDir q <$> currentModule
   for (moduleNames q) $ \name -> do
@@ -74,7 +74,7 @@ resolvePythonModules q = do
       let searchPaths = [ path </> "__init__.py"
                         , path <.> ".py"
                         ]
-      resolve searchPaths >>= maybeFail (notFound searchPaths)
+      resolve searchPaths >>= maybeM (raise (fail (notFound searchPaths)))
 
     friendlyName :: QualifiedName -> String
     friendlyName (QualifiedName xs)                = intercalate "." (NonEmpty.toList xs)
@@ -121,7 +121,7 @@ instance Show1 QualifiedImport where liftShowsPrec = genericLiftShowsPrec
 
 -- import a.b.c
 instance Evaluatable QualifiedImport where
-  eval (QualifiedImport (RelativeQualifiedName _ _))        = fail "technically this is not allowed in python"
+  eval (QualifiedImport (RelativeQualifiedName _ _))        = raise (fail "technically this is not allowed in python")
   eval (QualifiedImport name@(QualifiedName qualifiedName)) = do
     modulePaths <- resolvePythonModules name
     go (NonEmpty.zip (FV.name . BC.pack <$> qualifiedName) modulePaths)
diff --git a/src/Language/Ruby/Syntax.hs b/src/Language/Ruby/Syntax.hs
index cea8d57a9..158e2dcf1 100644
--- a/src/Language/Ruby/Syntax.hs
+++ b/src/Language/Ruby/Syntax.hs
@@ -16,14 +16,14 @@ import           System.FilePath.Posix
 -- TODO: Fully sort out ruby require/load mechanics
 --
 -- require "json"
-resolveRubyName :: forall value term location m. MonadEvaluatable location term value m => ByteString -> m ModulePath
+resolveRubyName :: forall value term location effects m. MonadEvaluatable location term value effects m => ByteString -> m effects ModulePath
 resolveRubyName name = do
   let name' = cleanNameOrPath name
   modulePath <- resolve [name' <.> "rb"]
   maybe (throwResumable @(ResolutionError value) $ RubyError name') pure modulePath
 
 -- load "/root/src/file.rb"
-resolveRubyPath :: forall value term location m. MonadEvaluatable location term value m => ByteString -> m ModulePath
+resolveRubyPath :: forall value term location effects m. MonadEvaluatable location term value effects m => ByteString -> m effects ModulePath
 resolveRubyPath path = do
   let name' = cleanNameOrPath path
   modulePath <- resolve [name']
@@ -68,9 +68,9 @@ instance Evaluatable Require where
     modifyEnv (`mergeNewer` importedEnv)
     pure v -- Returns True if the file was loaded, False if it was already loaded. http://ruby-doc.org/core-2.5.0/Kernel.html#method-i-require
 
-doRequire :: MonadEvaluatable location term value m
+doRequire :: MonadEvaluatable location term value effects m
           => ModulePath
-          -> m (Environment location value, value)
+          -> m effects (Environment location value, value)
 doRequire name = do
   moduleTable <- getModuleTable
   case ModuleTable.lookup name moduleTable of
@@ -93,9 +93,9 @@ instance Evaluatable Load where
     path <- subtermValue x >>= asString
     shouldWrap <- subtermValue wrap >>= asBool
     doLoad path shouldWrap
-  eval (Load _) = fail "invalid argument supplied to load, path is required"
+  eval (Load _) = raise (fail "invalid argument supplied to load, path is required")
 
-doLoad :: MonadEvaluatable location term value m => ByteString -> Bool -> m value
+doLoad :: MonadEvaluatable location term value effects m => ByteString -> Bool -> m effects value
 doLoad path shouldWrap = do
   path' <- resolveRubyPath path
   (importedEnv, _) <- traceResolve path path' $ isolate (load path')
diff --git a/src/Language/TypeScript/Syntax.hs b/src/Language/TypeScript/Syntax.hs
index 7596f8d98..82a5bb4b3 100644
--- a/src/Language/TypeScript/Syntax.hs
+++ b/src/Language/TypeScript/Syntax.hs
@@ -31,7 +31,7 @@ toName = FV.name . BC.pack . unPath
 
 -- Node.js resolution algorithm: https://nodejs.org/api/modules.html#modules_all_together
 -- TypeScript has a couple of different strategies, but the main one mimics Node.js.
-resolveWithNodejsStrategy :: forall value term location m. MonadEvaluatable location term value m => ImportPath -> [String] -> m ModulePath
+resolveWithNodejsStrategy :: MonadEvaluatable location term value effects m => ImportPath -> [String] -> m effects ModulePath
 resolveWithNodejsStrategy (ImportPath path Relative)    exts = resolveRelativePath path exts
 resolveWithNodejsStrategy (ImportPath path NonRelative) exts = resolveNonRelativePath path exts
 
@@ -42,7 +42,7 @@ resolveWithNodejsStrategy (ImportPath path NonRelative) exts = resolveNonRelativ
 -- /root/src/moduleB.ts
 -- /root/src/moduleB/package.json (if it specifies a "types" property)
 -- /root/src/moduleB/index.ts
-resolveRelativePath :: forall value term location m. MonadEvaluatable location term value m => FilePath -> [String] -> m ModulePath
+resolveRelativePath :: forall value term location effects m. MonadEvaluatable location term value effects m => FilePath -> [String] -> m effects ModulePath
 resolveRelativePath relImportPath exts = do
   ModuleInfo{..} <- currentModule
   let relRootDir = takeDirectory modulePath
@@ -61,7 +61,7 @@ resolveRelativePath relImportPath exts = do
 --
 -- /root/node_modules/moduleB.ts, etc
 -- /node_modules/moduleB.ts, etc
-resolveNonRelativePath :: forall value term location m. MonadEvaluatable location term value m => FilePath -> [String] -> m ModulePath
+resolveNonRelativePath :: forall value term location effects m. MonadEvaluatable location term value effects m => FilePath -> [String] -> m effects ModulePath
 resolveNonRelativePath name exts = do
   ModuleInfo{..} <- currentModule
   go "." modulePath mempty
@@ -76,7 +76,7 @@ resolveNonRelativePath name exts = do
         Right m -> traceResolve name m $ pure m
     notFound _ = throwResumable @(ResolutionError value) $ TypeScriptError name
 
-resolveTSModule :: MonadEvaluatable location term value m => FilePath -> [String] -> m (Either [FilePath] ModulePath)
+resolveTSModule :: MonadEvaluatable location term value effects m => FilePath -> [String] -> m effects (Either [FilePath] ModulePath)
 resolveTSModule path exts = maybe (Left searchPaths) Right <$> resolve searchPaths
   where searchPaths =
           ((path <.>) <$> exts)
@@ -91,7 +91,7 @@ typescriptExtensions = ["ts", "tsx", "d.ts"]
 javascriptExtensions :: [String]
 javascriptExtensions = ["js"]
 
-evalRequire :: MonadEvaluatable location term value m => ModulePath -> Name -> m value
+evalRequire :: MonadEvaluatable location term value effects m => ModulePath -> Name -> m effects value
 evalRequire modulePath alias = letrec' alias $ \addr -> do
   (importedEnv, _) <- isolate (require modulePath)
   modifyEnv (mappend importedEnv)
diff --git a/src/Prologue.hs b/src/Prologue.hs
index d4603dc8f..f91d501ab 100644
--- a/src/Prologue.hs
+++ b/src/Prologue.hs
@@ -3,7 +3,6 @@ module Prologue
   ( module X
   , foldMapA
   , maybeM
-  , maybeFail
   , maybeLast
   , fromMaybeLast
   ) where
@@ -73,7 +72,3 @@ fromMaybeLast b = fromMaybe b . getLast . foldMap (Last . Just)
 -- | Extract the 'Just' of a 'Maybe' in an 'Applicative' context or, given 'Nothing', run the provided action.
 maybeM :: Applicative f => f a -> Maybe a -> f a
 maybeM f = maybe f pure
-
--- | Either extract the 'Just' of a 'Maybe' or invoke 'fail' with the provided string.
-maybeFail :: MonadFail m => String -> Maybe a -> m a
-maybeFail s = maybeM (X.fail s)
diff --git a/src/Semantic/Util.hs b/src/Semantic/Util.hs
index 30e0ed413..058dbd84c 100644
--- a/src/Semantic/Util.hs
+++ b/src/Semantic/Util.hs
@@ -1,5 +1,5 @@
 -- MonoLocalBinds is to silence a warning about a simplifiable constraint.
-{-# LANGUAGE DataKinds, MonoLocalBinds, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
+{-# LANGUAGE MonoLocalBinds, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
 {-# OPTIONS_GHC -Wno-missing-signatures #-}
 module Semantic.Util where
 
diff --git a/test/SpecHelpers.hs b/test/SpecHelpers.hs
index e9cc3b47c..7bab8a4f4 100644
--- a/test/SpecHelpers.hs
+++ b/test/SpecHelpers.hs
@@ -12,7 +12,7 @@ module SpecHelpers (
 , TestEvaluating
 , ) where
 
-import Analysis.Abstract.Evaluating as X (EvaluatingState(..))
+import Control.Abstract.Evaluator as X (EvaluatorState(..))
 import Data.Abstract.Address as X
 import Data.Abstract.FreeVariables as X hiding (dropExtension)
 import Data.Abstract.Heap as X