diff --git a/semantic.cabal b/semantic.cabal
index 9cfc48023..bb32fa59e 100644
--- a/semantic.cabal
+++ b/semantic.cabal
@@ -39,8 +39,8 @@ library
                      , Control.Abstract.Environment
                      , Control.Abstract.Evaluator
                      , Control.Abstract.Exports
+                     , Control.Abstract.Goto
                      , Control.Abstract.Heap
-                     , Control.Abstract.Label
                      , Control.Abstract.Matching
                      , Control.Abstract.ModuleTable
                      , Control.Abstract.Roots
diff --git a/src/Analysis/Abstract/Evaluating.hs b/src/Analysis/Abstract/Evaluating.hs
index e17df35c8..912b7ae03 100644
--- a/src/Analysis/Abstract/Evaluating.hs
+++ b/src/Analysis/Abstract/Evaluating.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ScopedTypeVariables, TypeFamilies, TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Analysis.Abstract.Evaluating
 ( EvaluatingState(..)
 , evaluating
@@ -9,17 +9,16 @@ import Data.Abstract.Address
 import Data.Semilattice.Lower
 
 -- | An analysis evaluating @term@s to @value@s with a list of @effects@ using 'Evaluatable', and producing incremental results of type @a@.
-data EvaluatingState location term value = EvaluatingState
+data EvaluatingState location value = EvaluatingState
   { environment :: Environment location value
   , heap        :: Heap location value
   , modules     :: ModuleTable (Environment location value, value)
   , exports     :: Exports location value
-  , jumps       :: JumpTable term
   }
 
-deriving instance (Eq (Cell location value), Eq location, Eq term, Eq value) => Eq (EvaluatingState location term value)
-deriving instance (Ord (Cell location value), Ord location, Ord term, Ord value) => Ord (EvaluatingState location term value)
-deriving instance (Show (Cell location value), Show location, Show term, Show value) => Show (EvaluatingState location term value)
+deriving instance (Eq (Cell location value), Eq location, Eq value) => Eq (EvaluatingState location value)
+deriving instance (Ord (Cell location value), Ord location, Ord value) => Ord (EvaluatingState location value)
+deriving instance (Show (Cell location value), Show location, Show value) => Show (EvaluatingState location value)
 
 
 evaluating :: Evaluator location term value
@@ -30,12 +29,10 @@ evaluating :: Evaluator location term value
                 ': State (Heap location value)
                 ': State (ModuleTable (Environment location value, value))
                 ': State (Exports location value)
-                ': State (JumpTable term)
                 ': effects) result
-           -> Evaluator location term value effects (Either String result, EvaluatingState location term value)
+           -> Evaluator location term value effects (Either String result, EvaluatingState location value)
 evaluating
-  = fmap (\ (((((result, env), heap), modules), exports), jumps) -> (result, EvaluatingState env heap modules exports jumps))
-  . runState lowerBound -- State (JumpTable term)
+  = fmap (\ ((((result, env), heap), modules), exports) -> (result, EvaluatingState env heap modules exports))
   . runState lowerBound -- State (Exports location value)
   . runState lowerBound -- State (ModuleTable (Environment location value, value))
   . runState lowerBound -- State (Heap location value)
diff --git a/src/Control/Abstract.hs b/src/Control/Abstract.hs
index 6edd0594a..c452f6414 100644
--- a/src/Control/Abstract.hs
+++ b/src/Control/Abstract.hs
@@ -9,7 +9,7 @@ import Control.Abstract.Environment as X
 import Control.Abstract.Evaluator as X
 import Control.Abstract.Exports as X
 import Control.Abstract.Heap as X
-import Control.Abstract.Label as X
+import Control.Abstract.Goto as X
 import Control.Abstract.ModuleTable as X
 import Control.Abstract.Roots as X
 import Control.Abstract.Value as X
diff --git a/src/Control/Abstract/Context.hs b/src/Control/Abstract/Context.hs
index 189898c50..069ce60a5 100644
--- a/src/Control/Abstract/Context.hs
+++ b/src/Control/Abstract/Context.hs
@@ -2,7 +2,9 @@ module Control.Abstract.Context
 ( ModuleInfo
 , PackageInfo
 , currentModule
+, withCurrentModule
 , currentPackage
+, withCurrentPackage
 ) where
 
 import Control.Effect
@@ -15,6 +17,14 @@ import Prologue
 currentModule :: (Effectful m, Member (Reader ModuleInfo) effects) => m effects ModuleInfo
 currentModule = raise ask
 
+-- | Run an action with a locally-replaced 'ModuleInfo'.
+withCurrentModule :: (Effectful m, Member (Reader ModuleInfo) effects) => ModuleInfo -> m effects a -> m effects a
+withCurrentModule = raiseHandler . local . const
+
 -- | Get the currently evaluating 'PackageInfo'.
 currentPackage :: (Effectful m, Member (Reader PackageInfo) effects) => m effects PackageInfo
 currentPackage = raise ask
+
+-- | Run an action with a locally-replaced 'PackageInfo'.
+withCurrentPackage :: (Effectful m, Member (Reader PackageInfo) effects) => PackageInfo -> m effects a -> m effects a
+withCurrentPackage = raiseHandler . local . const
diff --git a/src/Control/Abstract/Evaluator.hs b/src/Control/Abstract/Evaluator.hs
index 2f6a7edc6..cca42222f 100644
--- a/src/Control/Abstract/Evaluator.hs
+++ b/src/Control/Abstract/Evaluator.hs
@@ -2,8 +2,6 @@
 module Control.Abstract.Evaluator
   ( Evaluator(..)
   -- * Effects
-  , Trace(..)
-  , traceE
   , EvalClosure(..)
   , evaluateClosureBody
   , runEvalClosure
@@ -30,14 +28,13 @@ module Control.Abstract.Evaluator
   ) where
 
 import Control.Effect
-import Control.Monad.Effect
+import Control.Monad.Effect (Eff, interpose, relay)
 import Control.Monad.Effect.Fail
 import Control.Monad.Effect.Fresh
 import Control.Monad.Effect.NonDet
 import Control.Monad.Effect.Reader hiding (runReader)
 import Control.Monad.Effect.Resumable
 import Control.Monad.Effect.State hiding (runState)
-import Control.Monad.Effect.Trace
 import Data.Abstract.Module
 import Prologue
 
@@ -54,18 +51,12 @@ deriving instance Member NonDet effects => Alternative (Evaluator location term
 
 -- Effects
 
--- | Trace into the current context.
--- TODO: Someday we can generalize this to work for Task and Graph.
-traceE :: Member Trace effects => String -> Evaluator location term value effects ()
-traceE = raise . trace
-
-
 -- | An effect to evaluate a closure’s body.
 data EvalClosure term value resume where
   EvalClosure :: term -> EvalClosure term value value
 
 evaluateClosureBody :: Member (EvalClosure term value) effects => term -> Evaluator location term value effects value
-evaluateClosureBody = raise . send . EvalClosure
+evaluateClosureBody = send . EvalClosure
 
 runEvalClosure :: (term -> Evaluator location term value effects value) -> Evaluator location term value (EvalClosure term value ': effects) a -> Evaluator location term value effects a
 runEvalClosure evalClosure = runEffect (\ (EvalClosure term) yield -> evalClosure term >>= yield)
@@ -76,7 +67,7 @@ data EvalModule term value resume where
   EvalModule :: Module term -> EvalModule term value value
 
 evaluateModule :: Member (EvalModule term value) effects => Module term -> Evaluator location term value effects value
-evaluateModule = raise . send . EvalModule
+evaluateModule = send . EvalModule
 
 runEvalModule :: (Module term -> Evaluator location term value effects value) -> Evaluator location term value (EvalModule term value ': effects) a -> Evaluator location term value effects a
 runEvalModule evalModule = runEffect (\ (EvalModule m) yield -> evalModule m >>= yield)
@@ -90,10 +81,10 @@ deriving instance Eq value => Eq (Return value a)
 deriving instance Show value => Show (Return value a)
 
 earlyReturn :: Member (Return value) effects => value -> Evaluator location term value effects value
-earlyReturn = raise . send . Return
+earlyReturn = send . Return
 
-catchReturn :: Member (Return value) effects => (forall x . Return value x -> Evaluator location term value effects a) -> Evaluator location term value effects a -> Evaluator location term value effects a
-catchReturn handler = raiseHandler (interpose pure (\ ret _ -> lower (handler ret)))
+catchReturn :: Member (Return value) effects => Evaluator location term value effects a -> (forall x . Return value x -> Evaluator location term value effects a) -> Evaluator location term value effects a
+catchReturn action handler = raiseHandler (interpose pure (\ ret _ -> lower (handler ret))) action
 
 runReturn :: Evaluator location term value (Return value ': effects) value -> Evaluator location term value effects value
 runReturn = runEffect (\ (Return value) _ -> pure value)
@@ -108,10 +99,10 @@ deriving instance Eq value => Eq (LoopControl value a)
 deriving instance Show value => Show (LoopControl value a)
 
 throwBreak :: Member (LoopControl value) effects => value -> Evaluator location term value effects value
-throwBreak = raise . send . Break
+throwBreak = send . Break
 
 throwContinue :: Member (LoopControl value) effects => value -> Evaluator location term value effects value
-throwContinue = raise . send . Continue
+throwContinue = send . Continue
 
 catchLoopControl :: Member (LoopControl value) effects => Evaluator location term value effects a -> (forall x . LoopControl value x -> Evaluator location term value effects a) -> Evaluator location term value effects a
 catchLoopControl action handler = raiseHandler (interpose pure (\ control _ -> lower (handler control))) action
diff --git a/src/Control/Abstract/Goto.hs b/src/Control/Abstract/Goto.hs
new file mode 100644
index 000000000..f765f59fc
--- /dev/null
+++ b/src/Control/Abstract/Goto.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE GADTs, TypeOperators #-}
+module Control.Abstract.Goto
+( GotoTable
+, Label
+, label
+, goto
+, Goto(..)
+, runGoto
+) where
+
+import           Control.Abstract.Evaluator
+import           Control.Monad.Effect (Eff, relayState)
+import qualified Data.IntMap as IntMap
+import           Prelude hiding (fail)
+import           Prologue
+
+type GotoTable effects value = IntMap.IntMap (Eff effects value)
+
+-- | The type of labels.
+--   TODO: This should be rolled into 'Name' and tracked in the environment, both so that we can abstract over labels like any other location, and so that we can garbage collect unreachable labels.
+type Label = Int
+
+
+-- | 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 :: Evaluator location term value (Goto effects value ': effects) value -> Evaluator location term value (Goto effects value ': effects) Label
+label = send . Label . lower
+
+-- | “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 -> Evaluator location term value (Goto effects value ': effects) (Evaluator location term value (Goto effects value ': effects) value)
+goto = fmap raise . send . Goto
+
+
+-- | 'Goto' effects embed an 'Eff' action which can be run in the environment under the 'Goto' itself.
+--
+--   It’s tempting to try to use a 'Member' constraint to require a 'Goto' effect:
+--
+--   @
+--   foo :: Member (Goto effects a) effects => Eff effects a
+--   @
+--
+--   However, using this type would require that the type of the effect list include a reference to itself, which is forbidden by the occurs check: we wouldn’t be able to write a handler for 'Goto' if it could be used at that type. Instead, one can either use a smaller, statically known effect list inside the 'Goto', e.g. @Member (Goto outer) inner@ where @outer@ is a suffix of @inner@ (and with some massaging to raise the @outer@ actions into the @inner@ context), or use 'Goto' when it’s statically known to be the head of the list: @Eff (Goto rest a ': rest) b@. In either case, the 'Eff' actions embedded in the effect are themselves able to contain further 'Goto' effects,
+data Goto effects value return where
+  Label :: Eff (Goto effects value ': effects) value -> Goto effects value Label
+  Goto  :: Label -> Goto effects value (Eff (Goto effects value ': effects) value)
+
+runGoto :: Member Fail effects => GotoTable (Goto effects value ': effects) value -> Evaluator location term value (Goto effects value ': effects) a -> Evaluator location term value effects (a, GotoTable (Goto effects value ': effects) value)
+runGoto initial = raiseHandler (relayState (IntMap.size initial, initial) (\ (_, table) a -> pure (a, table)) (\ (supremum, table) goto yield -> case goto of
+  Label action -> yield (succ supremum, IntMap.insert supremum action table) supremum
+  Goto label   -> maybe (fail ("unknown label: " <> show label)) (yield (supremum, table)) (IntMap.lookup label table)))
diff --git a/src/Control/Abstract/Label.hs b/src/Control/Abstract/Label.hs
deleted file mode 100644
index 14c3faed6..000000000
--- a/src/Control/Abstract/Label.hs
+++ /dev/null
@@ -1,42 +0,0 @@
-module Control.Abstract.Label
-( JumpTable
-, Label
-, label
-, goto
-) where
-
-import           Control.Abstract.Context
-import           Control.Abstract.Evaluator
-import qualified Data.IntMap as IntMap
-import           Prelude hiding (fail)
-import           Prologue
-
-type JumpTable term = IntMap.IntMap (PackageInfo, ModuleInfo, term)
-
--- | The type of labels.
---   TODO: This should be rolled into 'Name' and tracked in the environment, both so that we can abstract over labels like any other location, and so that we can garbage collect unreachable labels.
-type Label = Int
-
-
-getJumpTable :: Member (State (JumpTable term)) effects => Evaluator location term vlaue effects (JumpTable term)
-getJumpTable = raise get
-
--- | 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 :: Members '[Reader ModuleInfo, Reader PackageInfo, State (JumpTable term)] effects => term -> Evaluator location term value effects Label
-label term = do
-  m <- getJumpTable
-  moduleInfo <- currentModule
-  packageInfo <- currentPackage
-  let i = IntMap.size m
-  raise (put (IntMap.insert i (packageInfo, moduleInfo, term) m))
-  pure i
-
--- | “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 :: Members '[Fail, Reader ModuleInfo, Reader PackageInfo, State (JumpTable term)] effects => Label -> (term -> Evaluator location term value effects a) -> Evaluator location term value effects a
-goto label comp = do
-  maybeTerm <- IntMap.lookup label <$> getJumpTable
-  case maybeTerm of
-    Just (packageInfo, moduleInfo, term) -> raiseHandler (local (const packageInfo)) (raiseHandler (local (const moduleInfo)) (comp term))
-    Nothing -> raise (fail ("unknown label: " <> show label))
diff --git a/src/Control/Abstract/Value.hs b/src/Control/Abstract/Value.hs
index 38e87777d..8a615edd8 100644
--- a/src/Control/Abstract/Value.hs
+++ b/src/Control/Abstract/Value.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, KindSignatures, Rank2Types #-}
+{-# LANGUAGE Rank2Types #-}
 module Control.Abstract.Value
 ( AbstractValue(..)
 , AbstractHole(..)
@@ -40,7 +40,7 @@ class AbstractHole value where
 -- | 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 Show value => AbstractValue location term value (effects :: [* -> *]) where
+class Show value => AbstractValue location value effects where
   -- | Construct an abstract unit value.
   --   TODO: This might be the same as the empty tuple for some value types
   unit :: Evaluator location term value effects value
@@ -137,8 +137,11 @@ class Show value => AbstractValue location term value (effects :: [* -> *]) wher
   -- | Extract the environment from any scoped object (e.g. classes, namespaces, etc).
   scopedEnvironment :: value -> Evaluator location term value effects (Maybe (Environment location value))
 
-  -- | Evaluate an abstraction (a binder like a lambda or method definition).
-  lambda :: FreeVariables term => [Name] -> Subterm term (Evaluator location term value effects value) -> Evaluator location term value effects value
+  -- | Build a closure (a binder like a lambda or method definition).
+  closure :: [Name]                                      -- ^ The parameter names.
+          -> Set Name                                    -- ^ The set of free variables to close over.
+          -> Evaluator location term value effects value -- ^ The evaluator for the body of the closure.
+          -> Evaluator location term value effects value
   -- | Evaluate an application (like a function call).
   call :: value -> [Evaluator location term value effects value] -> Evaluator location term value effects value
 
@@ -149,7 +152,7 @@ class Show value => AbstractValue location term value (effects :: [* -> *]) wher
 
 
 -- | Attempt to extract a 'Prelude.Bool' from a given value.
-forLoop :: ( AbstractValue location term value effects
+forLoop :: ( AbstractValue location value effects
            , Member (State (Environment location value)) effects
            )
         => Evaluator location term value effects value -- ^ Initial statement
@@ -161,7 +164,7 @@ forLoop initial cond step body =
   localize (initial *> while cond (body *> step))
 
 -- | The fundamental looping primitive, built on top of ifthenelse.
-while :: AbstractValue location term value effects
+while :: AbstractValue location value effects
       => Evaluator location term value effects value
       -> Evaluator location term value effects value
       -> Evaluator location term value effects value
@@ -170,7 +173,7 @@ while cond body = loop $ \ continue -> do
   ifthenelse this (body *> continue) unit
 
 -- | Do-while loop, built on top of while.
-doWhile :: AbstractValue location term value effects
+doWhile :: AbstractValue location value effects
         => Evaluator location term value effects value
         -> Evaluator location term value effects value
         -> Evaluator location term value effects value
@@ -178,7 +181,7 @@ doWhile body cond = loop $ \ continue -> body *> do
   this <- cond
   ifthenelse this continue unit
 
-makeNamespace :: ( AbstractValue location term value effects
+makeNamespace :: ( AbstractValue location value effects
                  , Member (State (Environment location value)) effects
                  , Member (State (Heap location value)) effects
                  , Ord location
diff --git a/src/Control/Effect.hs b/src/Control/Effect.hs
index 955633570..0a47a0ce3 100644
--- a/src/Control/Effect.hs
+++ b/src/Control/Effect.hs
@@ -5,7 +5,10 @@ module Control.Effect
 , Eff.Reader
 , Eff.State
 , Fresh
+, Trace
+, send
 , throwResumable
+, traceE
 -- * Handlers
 , run
 , runM
@@ -45,9 +48,16 @@ instance Effectful Eff.Eff where
 
 -- Effects
 
+send :: (Effectful m, Member effect effects) => effect result -> m effects result
+send = raise . Eff.send
+
 throwResumable :: (Member (Resumable exc) effects, Effectful m) => exc v -> m effects v
 throwResumable = raise . throwError
 
+-- | Trace into the current context.
+traceE :: (Effectful m, Member Trace effects) => String -> m effects ()
+traceE = raise . trace
+
 
 -- Handlers
 
diff --git a/src/Data/Abstract/Evaluatable.hs b/src/Data/Abstract/Evaluatable.hs
index ecd31115f..379c0b05d 100644
--- a/src/Data/Abstract/Evaluatable.hs
+++ b/src/Data/Abstract/Evaluatable.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE ConstraintKinds, DefaultSignatures, GADTs, RankNTypes, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds, DefaultSignatures, GADTs, RankNTypes, ScopedTypeVariables, TypeOperators, UndecidableInstances #-}
 module Data.Abstract.Evaluatable
 ( module X
 , Evaluatable(..)
@@ -17,8 +17,9 @@ module Data.Abstract.Evaluatable
 , isolate
 ) where
 
-import Control.Abstract as X hiding (LoopControl(..), Return(..))
+import Control.Abstract as X hiding (LoopControl(..), Return(..), Goto(..))
 import Control.Abstract.Evaluator (LoopControl, Return(..))
+import Control.Abstract.Goto (Goto(..))
 import Control.Monad.Effect as Eff
 import Data.Abstract.Address
 import Data.Abstract.Declarations as X
@@ -46,7 +47,7 @@ class Evaluatable constr where
   eval expr = throwResumable (Unspecialized ("Eval unspecialized for " ++ liftShowsPrec (const (const id)) (const id) 0 expr ""))
 
 type EvaluatableConstraints location term value effects =
-  ( AbstractValue location term value effects
+  ( AbstractValue location value effects
   , Addressable location effects
   , Declarations term
   , FreeVariables term
@@ -93,7 +94,7 @@ runEvalErrorWith = runResumableWith
 
 -- | Evaluate a term within the context of the scoped environment of 'scopedEnvTerm'.
 --   Throws an 'EnvironmentLookupError' if @scopedEnvTerm@ does not have an environment.
-evaluateInScopedEnv :: ( AbstractValue location term value effects
+evaluateInScopedEnv :: ( AbstractValue location value effects
                        , Members '[ Resumable (EvalError value)
                                   , State (Environment location value)
                                   ] effects
@@ -169,41 +170,39 @@ traceResolve name path = traceE ("resolved " <> show name <> " -> " <> show path
 
 -- | Evaluate a given package.
 evaluatePackageWith :: ( Evaluatable (Base term)
-                       , EvaluatableConstraints location term value termEffects
+                       , EvaluatableConstraints location term value inner
                        , Members '[ Fail
                                   , Reader (Environment location value)
                                   , State (Environment location value)
                                   , Trace
-                                  ] effects
+                                  ] outer
                        , Recursive term
-                       , termEffects ~ (LoopControl value ': Return value ': EvalClosure term value ': moduleEffects)
-                       , moduleEffects ~ (Reader ModuleInfo ': EvalModule term value ': packageBodyEffects)
-                       , packageBodyEffects ~ (Reader LoadStack ': Reader (ModuleTable [Module term]) ': packageEffects)
-                       , packageEffects ~ (Reader PackageInfo ': effects)
+                       , inner ~ (Goto inner' value ': inner')
+                       , inner' ~ (LoopControl value ': Return value ': Reader ModuleInfo ': EvalModule term value ': Reader LoadStack ': Reader (ModuleTable [Module term]) ': Reader PackageInfo ': outer)
                        )
-                    => (SubtermAlgebra Module term (Evaluator location term value moduleEffects value) -> SubtermAlgebra Module term (Evaluator location term value moduleEffects value))
-                    -> (SubtermAlgebra (Base term) term (Evaluator location term value termEffects value) -> SubtermAlgebra (Base term) term (Evaluator location term value termEffects value))
+                    => (SubtermAlgebra Module term (Evaluator location term value inner value) -> SubtermAlgebra Module term (Evaluator location term value inner value))
+                    -> (SubtermAlgebra (Base term) term (Evaluator location term value inner value) -> SubtermAlgebra (Base term) term (Evaluator location term value inner value))
                     -> Package term
-                    -> Evaluator location term value effects [value]
+                    -> Evaluator location term value outer [value]
 evaluatePackageWith perModule perTerm = runReader . packageInfo <*> evaluatePackageBodyWith perModule perTerm . packageBody
 
 -- | Evaluate a given package body (module table and entry points).
-evaluatePackageBodyWith :: ( Evaluatable (Base term)
-                           , EvaluatableConstraints location term value termEffects
+evaluatePackageBodyWith :: forall location term value inner inner' outer
+                        .  ( Evaluatable (Base term)
+                           , EvaluatableConstraints location term value inner
                            , Members '[ Fail
                                       , Reader (Environment location value)
                                       , State (Environment location value)
                                       , Trace
-                                      ] effects
+                                      ] outer
                            , Recursive term
-                           , termEffects ~ (LoopControl value ': Return value ': EvalClosure term value ': moduleEffects)
-                           , moduleEffects ~ (Reader ModuleInfo ': EvalModule term value ': packageBodyEffects)
-                           , packageBodyEffects ~ (Reader LoadStack ': Reader (ModuleTable [Module term]) ': effects)
+                           , inner ~ (Goto inner' value ': inner')
+                           , inner' ~ (LoopControl value ': Return value ': Reader ModuleInfo ': EvalModule term value ': Reader LoadStack ': Reader (ModuleTable [Module term]) ': outer)
                            )
-                        => (SubtermAlgebra Module term (Evaluator location term value moduleEffects value) -> SubtermAlgebra Module term (Evaluator location term value moduleEffects value))
-                        -> (SubtermAlgebra (Base term) term (Evaluator location term value termEffects value) -> SubtermAlgebra (Base term) term (Evaluator location term value termEffects value))
+                        => (SubtermAlgebra Module term (Evaluator location term value inner value) -> SubtermAlgebra Module term (Evaluator location term value inner value))
+                        -> (SubtermAlgebra (Base term) term (Evaluator location term value inner value) -> SubtermAlgebra (Base term) term (Evaluator location term value inner value))
                         -> PackageBody term
-                        -> Evaluator location term value effects [value]
+                        -> Evaluator location term value outer [value]
 evaluatePackageBodyWith perModule perTerm body
   = runReader (packageModules body)
   . runReader lowerBound
@@ -212,17 +211,19 @@ evaluatePackageBodyWith perModule perTerm body
   $ traverse (uncurry evaluateEntryPoint) (ModuleTable.toPairs (packageEntryPoints body))
   where evalModule m
           = runEvalModule evalModule
-          . runReader (moduleInfo m)
+          . runInModule (moduleInfo m)
           . perModule (subtermValue . moduleBody)
-          . fmap (Subterm <*> evalTerm)
+          . fmap (Subterm <*> foldSubterms (perTerm eval))
           $ m
-        evalTerm
-          = runEvalClosure evalTerm
+        runInModule info
+          = runReader info
           . runReturn
           . runLoopControl
-          . foldSubterms (perTerm eval)
+          . fmap fst
+          . runGoto lowerBound
 
-        evaluateEntryPoint m sym = runReader (ModuleInfo m) . runEvalClosure evalTerm . runReturn . runLoopControl $ do
+        evaluateEntryPoint :: ModulePath -> Maybe Name -> Evaluator location term value (EvalModule term value ': Reader LoadStack ': Reader (ModuleTable [Module term]) ': outer) value
+        evaluateEntryPoint m sym = runInModule (ModuleInfo m) $ do
           v <- maybe unit (pure . snd) <$> require m
           maybe v ((`call` []) <=< variable) sym
 
diff --git a/src/Data/Abstract/Type.hs b/src/Data/Abstract/Type.hs
index 41b5aa74f..143c2583e 100644
--- a/src/Data/Abstract/Type.hs
+++ b/src/Data/Abstract/Type.hs
@@ -91,8 +91,8 @@ instance ( Addressable location effects
                     ] effects
          , Reducer (Type location) (Cell location (Type location))
          )
-      => AbstractValue location term (Type location) effects where
-  lambda names (Subterm _ body) = do
+      => AbstractValue location (Type location) effects where
+  closure names _ body = do
     (env, tvars) <- foldr (\ name rest -> do
       a <- alloc name
       tvar <- Var <$> raise fresh
diff --git a/src/Data/Abstract/Value.hs b/src/Data/Abstract/Value.hs
index 56a575efc..10ed0a636 100644
--- a/src/Data/Abstract/Value.hs
+++ b/src/Data/Abstract/Value.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE GADTs, RankNTypes, TypeOperators, UndecidableInstances #-}
 module Data.Abstract.Value where
 
 import Control.Abstract
@@ -6,9 +6,7 @@ import Data.Abstract.Address
 import Data.Abstract.Environment (Environment, emptyEnv, mergeEnvs)
 import qualified Data.Abstract.Environment as Env
 import Data.Abstract.FreeVariables
-import Data.Abstract.Module (ModuleInfo)
 import qualified Data.Abstract.Number as Number
-import Data.Abstract.Package (PackageInfo)
 import Data.List (genericIndex, genericLength)
 import Data.Scientific (Scientific)
 import Data.Scientific.Exts
@@ -59,8 +57,8 @@ prjPair = bitraverse prjValue prjValue
 
 -- TODO: Parameterize Value by the set of constructors s.t. each language can have a distinct value union.
 
--- | A function value consisting of a list of parameter 'Name's, a 'Label' to jump to the body of the function, and an 'Environment' of bindings captured by the body.
-data Closure location value = Closure [Name] Label (Environment location value)
+-- | A function value consisting of a package & module info, a list of parameter 'Name's, a 'Label' to jump to the body of the function, and an 'Environment' of bindings captured by the body.
+data Closure location value = Closure PackageInfo ModuleInfo [Name] Label (Environment location value)
   deriving (Eq, Generic1, Ord, Show)
 
 instance Eq location => Eq1 (Closure location) where liftEq = genericLiftEq
@@ -200,32 +198,30 @@ instance Show1 Null where liftShowsPrec = genericLiftShowsPrec
 
 instance Ord location => ValueRoots location (Value location) where
   valueRoots v
-    | Just (Closure _ _ env) <- prjValue v = Env.addresses env
-    | otherwise                            = mempty
+    | Just (Closure _ _ _ _ env) <- prjValue v = Env.addresses env
+    | otherwise                                = mempty
 
 
 instance AbstractHole (Value location) where
   hole = injValue Hole
 
 -- | Construct a 'Value' wrapping the value arguments (if any).
-instance ( Addressable location effects
-         , Members '[ EvalClosure term (Value location)
-                    , Fail
+instance ( Addressable location (Goto effects (Value location) ': effects)
+         , Members '[ Fail
                     , LoopControl (Value location)
                     , Reader (Environment location (Value location))
                     , Reader ModuleInfo
                     , Reader PackageInfo
                     , Resumable (AddressError location (Value location))
-                    , Resumable (ValueError location (Value location))
+                    , Resumable (ValueError location)
                     , Return (Value location)
                     , State (Environment location (Value location))
                     , State (Heap location (Value location))
-                    , State (JumpTable term)
                     ] effects
          , Reducer (Value location) (Cell location (Value location))
          , Show location
          )
-      => AbstractValue location term (Value location) effects where
+      => AbstractValue location (Value location) (Goto effects (Value location) ': effects) where
   unit     = pure . injValue $ Unit
   integer  = pure . injValue . Integer . Number.Integer
   boolean  = pure . injValue . Boolean
@@ -243,7 +239,7 @@ instance ( Addressable location effects
 
   asPair val
     | Just (KVPair k v) <- prjValue val = pure (k, v)
-    | otherwise = throwResumable @(ValueError location (Value location)) $ KeyValueError val
+    | otherwise = throwValueError $ KeyValueError val
 
   hash = pure . injValue . Hash . fmap (injValue . uncurry KVPair)
 
@@ -258,7 +254,7 @@ instance ( Addressable location effects
     pure (injValue (Namespace n (Env.mergeNewer env' env)))
     where asNamespaceEnv v
             | Just (Namespace _ env') <- prjValue v = pure env'
-            | otherwise                             = throwResumable $ NamespaceError ("expected " <> show v <> " to be a namespace")
+            | otherwise                             = throwValueError $ NamespaceError ("expected " <> show v <> " to be a namespace")
 
   scopedEnvironment o
     | Just (Class _ env) <- prjValue o = pure (Just env)
@@ -267,7 +263,7 @@ instance ( Addressable location effects
 
   asString v
     | Just (String n) <- prjValue v = pure n
-    | otherwise                     = throwResumable @(ValueError location (Value location)) $ StringError v
+    | otherwise                     = throwValueError $ StringError v
 
   ifthenelse cond if' else' = do
     isHole <- isHole cond
@@ -279,7 +275,7 @@ instance ( Addressable location effects
 
   asBool val
     | Just (Boolean b) <- prjValue val = pure b
-    | otherwise = throwResumable @(ValueError location (Value location)) $ BoolError val
+    | otherwise = throwValueError $ BoolError val
 
   isHole val = pure (prjValue val == Just Hole)
 
@@ -313,7 +309,7 @@ instance ( Addressable location effects
         tentative x i j = attemptUnsafeArithmetic (x i j)
 
         -- Dispatch whatever's contained inside a 'Number.SomeNumber' to its appropriate 'MonadValue' ctor
-        specialize :: Either ArithException Number.SomeNumber -> Evaluator location term (Value location) effects (Value location)
+        specialize :: (AbstractValue location (Value location) effects, Member (Resumable (ValueError location)) effects) => Either ArithException Number.SomeNumber -> Evaluator location term (Value location) effects (Value location)
         specialize (Left exc) = throwValueError (ArithmeticError exc)
         specialize (Right (Number.SomeNumber (Number.Integer i))) = integer i
         specialize (Right (Number.SomeNumber (Number.Ratio r)))   = rational r
@@ -332,7 +328,7 @@ instance ( Addressable location effects
       where
         -- Explicit type signature is necessary here because we're passing all sorts of things
         -- to these comparison functions.
-        go :: Ord a => a -> a -> Evaluator location term (Value location) effects (Value location)
+        go :: (AbstractValue location (Value location) effects, Ord a) => a -> a -> Evaluator location term (Value location) effects (Value location)
         go l r = case comparator of
           Concrete f  -> boolean (f l r)
           Generalized -> integer (orderingToInt (compare l r))
@@ -353,53 +349,53 @@ instance ( Addressable location effects
     | otherwise = throwValueError (Bitwise2Error left right)
       where pair = (left, right)
 
-  lambda names (Subterm body _) = do
+  closure parameters freeVariables body = do
+    packageInfo <- currentPackage
+    moduleInfo <- currentModule
     l <- label body
-    injValue . Closure names l . Env.bind (foldr Set.delete (Set.fromList (freeVariables body)) names) <$> getEnv
+    injValue . Closure packageInfo moduleInfo parameters l . Env.bind (foldr Set.delete freeVariables parameters) <$> getEnv
 
   call op params = do
     case prjValue op of
-      Just (Closure names label env) -> do
-        -- Evaluate the bindings and the body within a `goto` in order to
-        -- charge their origins to the closure's origin.
-        goto label $ \body -> do
+      Just (Closure packageInfo moduleInfo names label env) -> do
+        body <- goto label
+        -- Evaluate the bindings and body with the closure’s package/module info in scope in order to
+        -- charge them to the closure's origin.
+        withCurrentPackage packageInfo . withCurrentModule moduleInfo $ do
           bindings <- foldr (\ (name, param) rest -> do
             v <- param
             a <- alloc name
             assign a v
             Env.insert name a <$> rest) (pure env) (zip names params)
-          localEnv (mergeEnvs bindings) (evalClosure body)
+          localEnv (mergeEnvs bindings) (catchReturn body (\ (Return value) -> pure value))
       Nothing -> throwValueError (CallError op)
-    where
-      evalClosure term = catchReturn @(Value location) (\ (Return value) -> pure value) (evaluateClosureBody term)
 
-  loop x = catchLoopControl @(Value location) (fix x) (\ control -> case control of
+  loop x = catchLoopControl (fix x) (\ control -> case control of
     Break value -> pure value
     -- FIXME: Figure out how to deal with this. Ruby treats this as the result of the current block iteration, while PHP specifies a breakout level and TypeScript appears to take a label.
     Continue _  -> loop x)
 
 
 -- | The type of exceptions that can be thrown when constructing values in 'Value'’s 'MonadValue' instance.
-data ValueError location value resume where
-  StringError            :: value          -> ValueError location value ByteString
-  BoolError              :: value          -> ValueError location value Bool
-  IndexError             :: value -> value -> ValueError location value value
-  NamespaceError         :: Prelude.String -> ValueError location value (Environment location value)
-  CallError              :: value          -> ValueError location value value
-  NumericError           :: value          -> ValueError location value value
-  Numeric2Error          :: value -> value -> ValueError location value value
-  ComparisonError        :: value -> value -> ValueError location value value
-  BitwiseError           :: value          -> ValueError location value value
-  Bitwise2Error          :: value -> value -> ValueError location value value
-  KeyValueError          :: value          -> ValueError location value (value, value)
+data ValueError location resume where
+  StringError            :: Value location                   -> ValueError location ByteString
+  BoolError              :: Value location                   -> ValueError location Bool
+  IndexError             :: Value location -> Value location -> ValueError location (Value location)
+  NamespaceError         :: Prelude.String                   -> ValueError location (Environment location (Value location))
+  CallError              :: Value location                   -> ValueError location (Value location)
+  NumericError           :: Value location                   -> ValueError location (Value location)
+  Numeric2Error          :: Value location -> Value location -> ValueError location (Value location)
+  ComparisonError        :: Value location -> Value location -> ValueError location (Value location)
+  BitwiseError           :: Value location                   -> ValueError location (Value location)
+  Bitwise2Error          :: Value location -> Value location -> ValueError location (Value location)
+  KeyValueError          :: Value location                   -> ValueError location (Value location, Value location)
   -- Indicates that we encountered an arithmetic exception inside Haskell-native number crunching.
-  ArithmeticError :: ArithException -> ValueError location value value
+  ArithmeticError        :: ArithException                   -> ValueError location (Value location)
   -- Out-of-bounds error
-  BoundsError :: [value] -> Prelude.Integer -> ValueError location value value
+  BoundsError            :: [Value location] -> Prelude.Integer -> ValueError location (Value location)
 
 
-
-instance Eq value => Eq1 (ValueError location value) where
+instance Eq location => Eq1 (ValueError location) where
   liftEq _ (StringError a) (StringError b)                       = a == b
   liftEq _ (NamespaceError a) (NamespaceError b)                 = a == b
   liftEq _ (CallError a) (CallError b)                           = a == b
@@ -413,15 +409,15 @@ instance Eq value => Eq1 (ValueError location value) where
   liftEq _ (BoundsError a b) (BoundsError c d)                   = (a == c) && (b == d)
   liftEq _ _             _                                       = False
 
-deriving instance (Show value) => Show (ValueError location value resume)
-instance (Show value) => Show1 (ValueError location value) where
+deriving instance Show location => Show (ValueError location resume)
+instance Show location => Show1 (ValueError location) where
   liftShowsPrec _ _ = showsPrec
 
-throwValueError :: Member (Resumable (ValueError location value)) effects => ValueError location value resume -> Evaluator location term value effects resume
+throwValueError :: Member (Resumable (ValueError location)) effects => ValueError location resume -> Evaluator location term value effects resume
 throwValueError = throwResumable
 
-runValueError :: Evaluator location term value (Resumable (ValueError location value) ': effects) a -> Evaluator location term value effects (Either (SomeExc (ValueError location value)) a)
+runValueError :: Evaluator location term value (Resumable (ValueError location) ': effects) a -> Evaluator location term value effects (Either (SomeExc (ValueError location)) a)
 runValueError = raiseHandler runError
 
-runValueErrorWith :: (forall resume . ValueError location value resume -> Evaluator location term value effects resume) -> Evaluator location term value (Resumable (ValueError location value) ': effects) a -> Evaluator location term value effects a
+runValueErrorWith :: (forall resume . ValueError location resume -> Evaluator location term value effects resume) -> Evaluator location term value (Resumable (ValueError location) ': effects) a -> Evaluator location term value effects a
 runValueErrorWith = runResumableWith
diff --git a/src/Data/Syntax/Declaration.hs b/src/Data/Syntax/Declaration.hs
index bbbfedfd9..deb659b8a 100644
--- a/src/Data/Syntax/Declaration.hs
+++ b/src/Data/Syntax/Declaration.hs
@@ -3,6 +3,7 @@ module Data.Syntax.Declaration where
 
 import qualified Data.Abstract.Environment as Env
 import Data.Abstract.Evaluatable
+import qualified Data.Set as Set (fromList)
 import Diffing.Algorithm
 import Prologue
 
@@ -22,7 +23,7 @@ instance Show1 Function where liftShowsPrec = genericLiftShowsPrec
 instance Evaluatable Function where
   eval Function{..} = do
     name <- either (throwEvalError . FreeVariablesError) pure (freeVariable $ subterm functionName)
-    (v, addr) <- letrec name (lambda (paramNames functionParameters) functionBody)
+    (v, addr) <- letrec name (closure (paramNames functionParameters) (Set.fromList (freeVariables functionBody)) (subtermValue functionBody))
     modifyEnv (Env.insert name addr)
     pure v
     where paramNames = foldMap (freeVariables . subterm)
@@ -46,7 +47,7 @@ instance Show1 Method where liftShowsPrec = genericLiftShowsPrec
 instance Evaluatable Method where
   eval Method{..} = do
     name <- either (throwEvalError . FreeVariablesError) pure (freeVariable $ subterm methodName)
-    (v, addr) <- letrec name (lambda (paramNames methodParameters) methodBody)
+    (v, addr) <- letrec name (closure (paramNames methodParameters) (Set.fromList (freeVariables methodBody)) (subtermValue methodBody))
     modifyEnv (Env.insert name addr)
     pure v
     where paramNames = foldMap (freeVariables . subterm)
diff --git a/src/Language/PHP/Syntax.hs b/src/Language/PHP/Syntax.hs
index a34d26ca7..e16539b47 100644
--- a/src/Language/PHP/Syntax.hs
+++ b/src/Language/PHP/Syntax.hs
@@ -46,7 +46,7 @@ resolvePHPName n = do
   where name = toName n
         toName = BC.unpack . dropRelativePrefix . stripQuotes
 
-include :: ( AbstractValue location term value effects
+include :: ( AbstractValue location value effects
            , Members '[ Reader (ModuleTable [Module term])
                       , Resumable ResolutionError
                       , State (Environment location value)
diff --git a/src/Language/Ruby/Syntax.hs b/src/Language/Ruby/Syntax.hs
index 662f8ae8e..3d275dfaf 100644
--- a/src/Language/Ruby/Syntax.hs
+++ b/src/Language/Ruby/Syntax.hs
@@ -73,7 +73,7 @@ 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 :: ( AbstractValue location term value effects
+doRequire :: ( AbstractValue location value effects
              , Members '[ EvalModule term value
                         , Reader LoadStack
                         , Reader (ModuleTable [M.Module term])
@@ -111,7 +111,7 @@ instance Evaluatable Load where
     doLoad path shouldWrap
   eval (Load _) = raise (fail "invalid argument supplied to load, path is required")
 
-doLoad :: ( AbstractValue location term value effects
+doLoad :: ( AbstractValue location value effects
           , Members '[ EvalModule term value
                      , Reader LoadStack
                      , Reader (ModuleTable [M.Module term])
diff --git a/src/Language/TypeScript/Syntax.hs b/src/Language/TypeScript/Syntax.hs
index 81e28be8c..144a62492 100644
--- a/src/Language/TypeScript/Syntax.hs
+++ b/src/Language/TypeScript/Syntax.hs
@@ -118,7 +118,7 @@ typescriptExtensions = ["ts", "tsx", "d.ts"]
 javascriptExtensions :: [String]
 javascriptExtensions = ["js"]
 
-evalRequire :: ( AbstractValue location term value effects
+evalRequire :: ( AbstractValue location value effects
                , Addressable location effects
                , Members '[ EvalModule term value
                           , Reader (Environment location value)
diff --git a/src/Semantic/Graph.hs b/src/Semantic/Graph.hs
index 4d9c002e5..806146925 100644
--- a/src/Semantic/Graph.hs
+++ b/src/Semantic/Graph.hs
@@ -3,10 +3,9 @@ module Semantic.Graph where
 
 import           Analysis.Abstract.Evaluating
 import           Analysis.Abstract.Graph
-import           Control.Effect (runIgnoringTraces)
+import           Control.Effect (runIgnoringTraces, traceE)
 import qualified Control.Exception as Exc
-import           Control.Monad.Effect (relayState)
-import           Control.Monad.Effect.Trace (trace)
+import           Control.Monad.Effect (reinterpret)
 import           Data.Abstract.Address
 import           Data.Abstract.Evaluatable
 import           Data.Abstract.Located
@@ -70,7 +69,7 @@ parsePackage parser preludeFile project@Project{..} = do
   prelude <- traverse (parseModule parser Nothing) preludeFile
   p <- parseModules parser project
   let pkg = Package.fromModules n Nothing prelude (length projectEntryPoints) p
-  pkg <$ trace ("project: " <> show pkg)
+  pkg <$ traceE ("project: " <> show pkg)
 
   where
     n = name (projectName project)
@@ -87,7 +86,7 @@ parseModule parser rootDir file = do
 
 
 resumingResolutionError :: (Applicative (m effects), Effectful m, Member Trace effects) => m (Resumable ResolutionError ': effects) a -> m effects a
-resumingResolutionError = runResolutionErrorWith (\ err -> raise (trace ("ResolutionError:" <> show err)) *> case err of
+resumingResolutionError = runResolutionErrorWith (\ err -> traceE ("ResolutionError:" <> show err) *> case err of
   NotFoundError nameToResolve _ _ -> pure  nameToResolve
   GoImportError pathToResolve     -> pure [pathToResolve])
 
@@ -112,7 +111,7 @@ resumingAddressError = runAddressErrorWith (\ err -> traceE ("AddressError:" <>
   UnallocatedAddress _   -> pure lowerBound
   UninitializedAddress _ -> pure hole)
 
-resumingValueError :: (AbstractHole value, Member (State (Environment location value)) effects, Member Trace effects, Show value) => Evaluator location term value (Resumable (ValueError location value) ': effects) a -> Evaluator location term value effects a
+resumingValueError :: (Members '[State (Environment location (Value location)), Trace] effects, Show location) => Evaluator location term (Value location) (Resumable (ValueError location) ': effects) a -> Evaluator location term (Value location) effects a
 resumingValueError = runValueErrorWith (\ err -> traceE ("ValueError" <> show err) *> case err of
   CallError val     -> pure val
   StringError val   -> pure (pack (show val))
@@ -129,4 +128,6 @@ resumingValueError = runValueErrorWith (\ err -> traceE ("ValueError" <> show er
   ArithmeticError{} -> pure hole)
 
 resumingEnvironmentError :: AbstractHole value => Evaluator location term value (Resumable (EnvironmentError value) ': effects) a -> Evaluator location term value effects (a, [Name])
-resumingEnvironmentError = raiseHandler (relayState [] (fmap pure . flip (,)) (\ names (Resumable (FreeVariable name)) yield -> yield (name : names) hole))
+resumingEnvironmentError
+  = runState []
+  . raiseHandler (reinterpret (\ (Resumable (FreeVariable name)) -> modify' (name :) $> hole))
diff --git a/test/Analysis/Ruby/Spec.hs b/test/Analysis/Ruby/Spec.hs
index 8134aedc0..1099118ad 100644
--- a/test/Analysis/Ruby/Spec.hs
+++ b/test/Analysis/Ruby/Spec.hs
@@ -31,7 +31,7 @@ spec = parallel $ do
 
     it "evaluates load with wrapper" $ do
       res <- evaluate "load-wrap.rb"
-      fst res `shouldBe` Left (SomeExc (injectSum (FreeVariable "foo" :: EnvironmentError (Value Precise) (Value Precise))))
+      fst res `shouldBe` Left (SomeExc (injectSum @(EnvironmentError (Value Precise)) (FreeVariable "foo")))
       environment (snd res) `shouldBe` [ ("Object", addr 0) ]
 
     it "evaluates subclass" $ do
diff --git a/test/Control/Abstract/Evaluator/Spec.hs b/test/Control/Abstract/Evaluator/Spec.hs
index c743a1d98..439dc667a 100644
--- a/test/Control/Abstract/Evaluator/Spec.hs
+++ b/test/Control/Abstract/Evaluator/Spec.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeOperators #-}
 module Control.Abstract.Evaluator.Spec where
 
 import Analysis.Abstract.Evaluating (evaluating)
@@ -9,6 +10,7 @@ import qualified Data.Abstract.Value as Value
 import Data.Algebra
 import Data.Bifunctor (first)
 import Data.Functor.Const
+import Data.Semilattice.Lower
 import Data.Sum
 import SpecHelpers hiding (Term, reassociate)
 
@@ -20,7 +22,7 @@ spec = parallel $ do
 
   it "calls functions" $ do
     (expected, _) <- evaluate $ do
-      identity <- lambda [name "x"] (term (variable (name "x")))
+      identity <- closure [name "x"] lowerBound (variable (name "x"))
       call identity [integer 123]
     expected `shouldBe` Right (Value.injValue (Value.Integer (Number.Integer 123)))
 
@@ -33,23 +35,26 @@ evaluate
   . Value.runValueError
   . runEnvironmentError
   . runAddressError
-  . runValue
-runValue = runEvalClosure (runValue . runTerm) . runReturn . runLoopControl
+  . runReturn
+  . runLoopControl
+  . fmap fst
+  . runGoto lowerBound
+  . constraining
+
+constraining :: TermEvaluator Value -> TermEvaluator Value
+constraining = id
 
 reassociate :: Either String (Either (SomeExc exc1) (Either (SomeExc exc2) (Either (SomeExc exc3) result))) -> Either (SomeExc (Sum '[Const String, exc1, exc2, exc3])) result
 reassociate (Left s) = Left (SomeExc (injectSum (Const s)))
 reassociate (Right (Right (Right (Right a)))) = Right a
 
-term :: TermEvaluator Value -> Subterm Term (TermEvaluator Value)
-term eval = Subterm (Term eval) eval
-
-type TermEffects
+type TermEffects = Goto GotoEffects Value ': GotoEffects
+type GotoEffects
   = '[ LoopControl Value
      , Return Value
-     , EvalClosure Term Value
      , Resumable (AddressError Precise Value)
      , Resumable (EnvironmentError Value)
-     , Resumable (Value.ValueError Precise Value)
+     , Resumable (Value.ValueError Precise)
      , Reader ModuleInfo
      , Reader PackageInfo
      , Fail
@@ -59,7 +64,6 @@ type TermEffects
      , State (Heap Precise Value)
      , State (ModuleTable (Environment Precise Value, Value))
      , State (Exports Precise Value)
-     , State (JumpTable Term)
      , IO
      ]