diff --git a/primer-rel8/test/TestUtils.hs b/primer-rel8/test/TestUtils.hs
index 984887b6a..8f80a10c0 100644
--- a/primer-rel8/test/TestUtils.hs
+++ b/primer-rel8/test/TestUtils.hs
@@ -90,6 +90,13 @@ import Primer.Database.Rel8.Rel8Db (
   runRel8Db,
  )
 import Primer.Database.Rel8.Schema as Schema hiding (app)
+import Primer.Module (
+  Module (
+    Module,
+    moduleDefs,
+    moduleTypes
+  ),
+ )
 import Primer.Name (Name)
 import Primer.Primitives (
   allPrimDefs,
@@ -366,6 +373,9 @@ testApp =
     testProg :: Prog
     testProg =
       newEmptyProg
-        { progTypes = defaultTypeDefs
-        , progDefs = defs
+        { progModule =
+            Module
+              { moduleTypes = defaultTypeDefs
+              , moduleDefs = defs
+              }
         }
diff --git a/primer/primer.cabal b/primer/primer.cabal
index e166a7c77..fbe57708e 100644
--- a/primer/primer.cabal
+++ b/primer/primer.cabal
@@ -26,6 +26,7 @@ library
     Primer.Database
     Primer.Eval
     Primer.EvalFull
+    Primer.Module
     Primer.Name
     Primer.Name.Fresh
     Primer.Primitives
diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs
index af75d5c62..4d627d34c 100644
--- a/primer/src/Primer/API.hs
+++ b/primer/src/Primer/API.hs
@@ -70,8 +70,7 @@ import Primer.App (
   handleMutationRequest,
   handleQuestion,
   initialApp,
-  progDefs,
-  progTypes,
+  progModule,
   runEditAppM,
   runQueryAppM,
  )
@@ -119,6 +118,7 @@ import qualified Primer.Database as Database (
     Success
   ),
  )
+import Primer.Module (Module (moduleDefs, moduleTypes))
 import Primer.Name (Name, unName)
 import qualified StmContainers.Map as StmMap
 
@@ -326,7 +326,7 @@ instance ToJSON Def
 viewProg :: App.Prog -> Prog
 viewProg p =
   Prog
-    { types = typeDefName <$> progTypes p
+    { types = typeDefName <$> moduleTypes (progModule p)
     , defs =
         ( \d ->
             Def
@@ -336,7 +336,7 @@ viewProg p =
               , term = viewTreeExpr . astDefExpr <$> defAST d
               }
         )
-          <$> Map.elems (progDefs p)
+          <$> Map.elems (moduleDefs $ progModule p)
     }
 
 -- | A simple method to extract 'Tree's from 'Expr's. This is injective.
diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs
index d028d6cf0..91da88c2e 100644
--- a/primer/src/Primer/Action.hs
+++ b/primer/src/Primer/Action.hs
@@ -25,7 +25,7 @@ module Primer.Action (
   uniquifyDefName,
 ) where
 
-import Foreword
+import Foreword hiding (mod)
 
 import Control.Monad.Fresh (MonadFresh)
 import Data.Aeson (Value)
@@ -80,6 +80,7 @@ import Primer.Core.DSL (
 import Primer.Core.Transform (renameTyVar, renameTyVarExpr, renameVar)
 import Primer.Core.Utils (forgetTypeIDs, generateTypeIDs)
 import Primer.JSON
+import Primer.Module (Module (moduleDefs, moduleTypes))
 import Primer.Name (Name, NameCounter, unName, unsafeMkName)
 import Primer.Name.Fresh (
   isFresh,
@@ -90,6 +91,7 @@ import Primer.Name.Fresh (
 import Primer.Questions (Question)
 import Primer.Refine (Inst (InstAPP, InstApp, InstUnconstrainedAPP), refine)
 import Primer.Typecheck (
+  CheckEverythingRequest (CheckEverything, toCheck, trusted),
   SmartHoles,
   TypeError,
   buildTypingContext,
@@ -352,6 +354,12 @@ data ActionError
     -- a bug. It does not get thrown for "no valid refinement found"
     -- - see Note [No valid refinement]
     RefineError Text
+  | -- | Importing some modules failed.
+    -- This should be impossible as long as the requested modules are well-typed
+    -- and all of their dependencies are already imported
+    ImportFailed () TypeError
+  -- The extra unit is to avoid having two constructors with a single
+  -- TypeError field, breaking our MonadNestedError machinery...
   deriving (Eq, Show, Generic)
   deriving (FromJSON, ToJSON) via VJSON ActionError
 
@@ -398,34 +406,48 @@ type ActionM m =
   , MonadReader TC.Cxt m -- has access to a typing context
   )
 
--- Apply a sequence of actions to the type signature of a definition
+-- | Apply a sequence of actions to the type signature of a definition
 -- We apply the actions to the type, then typecheck the body of the definition against the new type.
 -- We must then typecheck the whole program to check any uses of the definition.
+-- Note that this may introduce new holes when using SmartHoles, and thus we return a whole module
+-- as well as the one definition we wanted to change.
 applyActionsToTypeSig ::
   (MonadFresh ID m, MonadFresh NameCounter m) =>
   SmartHoles ->
-  [TypeDef] ->
-  Map ID Def ->
+  [Module] ->
+  Module ->
+  -- | This must be one of the definitions in the @Module@
   ASTDef ->
   [Action] ->
-  m (Either ActionError (ASTDef, Map ID Def, TypeZ))
-applyActionsToTypeSig smartHoles typeDefs defs def actions =
-  runReaderT go (buildTypingContext typeDefs defs smartHoles)
+  m (Either ActionError (ASTDef, Module, TypeZ))
+applyActionsToTypeSig smartHoles imports mod def actions =
+  runReaderT
+    go
+    ( buildTypingContext
+        (concatMap moduleTypes $ mod : imports)
+        (foldMap moduleDefs $ mod : imports)
+        smartHoles
+    )
     & runExceptT
   where
-    go :: ActionM m => m (ASTDef, Map ID Def, TypeZ)
+    go :: ActionM m => m (ASTDef, Module, TypeZ)
     go = do
       zt <- withWrappedType (astDefType def) (\zt -> foldM (flip applyActionAndSynth) (InType zt) actions)
       let t = target (top zt)
       e <- check (forgetTypeIDs t) (astDefExpr def)
       let def' = def{astDefExpr = exprTtoExpr e, astDefType = t}
-          defs' = Map.insert (astDefID def) (DefAST def') defs
+          defs' = Map.insert (astDefID def) (DefAST def') $ moduleDefs mod
+          mod' = mod{moduleDefs = defs'}
       -- The actions were applied to the type successfully, and the definition body has been
       -- typechecked against the new type.
       -- Now we need to typecheck the whole program again, to check any uses of the definition
       -- We make sure that the updated type is present in the global context.
-      checkedDefs <- checkEverything smartHoles typeDefs defs'
-      pure (def', checkedDefs, zt)
+      -- Here we just check the whole of the mutable prog, excluding imports.
+      -- (for efficiency, we need not check the type definitions, but we do not implement this optimisation)
+      checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = [mod']}) >>= \case
+        [checkedMod] -> pure (def', checkedMod, zt)
+        -- This internal error will go away when we allow Progs to contain multiple mutable modules
+        _ -> throwError $ CustomFailure NoOp "Internal error: checkEverything returned a different number of module as were passed in"
     -- Actions expect that all ASTs have a top-level expression of some sort.
     -- Signatures don't have this: they're just a type.
     -- We fake it by wrapping the type in a top-level annotation node, then unwrapping afterwards.
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index aa92166d9..ffc2123eb 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -31,6 +31,7 @@ module Primer.App (
   handleEditRequest,
   handleEvalRequest,
   handleEvalFullRequest,
+  importModules,
   MutationRequest (..),
   Selection (..),
   NodeSelection (..),
@@ -47,7 +48,7 @@ module Primer.App (
   defaultTypeDefs,
 ) where
 
-import Foreword
+import Foreword hiding (mod)
 
 import Control.Monad.Fresh (MonadFresh (..))
 import Data.Aeson (
@@ -62,10 +63,10 @@ import Data.Generics.Uniplate.Zipper (
  )
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
-import Optics (re, traverseOf, view, (%), (.~), (^.), _Left, _Right)
+import Optics (re, traverseOf, view, (%), (%~), (.~), (^.), _Left, _Right)
 import Primer.Action (
   Action,
-  ActionError (IDNotFound),
+  ActionError (IDNotFound, ImportFailed),
   ProgAction (..),
   applyActionsToBody,
   applyActionsToTypeSig,
@@ -107,6 +108,7 @@ import Primer.Eval (EvalDetail, EvalError)
 import qualified Primer.Eval as Eval
 import Primer.EvalFull (Dir, EvalFullError (TimedOut), TerminationBound, evalFull)
 import Primer.JSON
+import Primer.Module (Module (Module, moduleDefs, moduleTypes))
 import Primer.Name (Name, NameCounter, freshName, unsafeMkName)
 import Primer.Primitives (allPrimDefs, allPrimTypeDefs)
 import Primer.Questions (
@@ -117,6 +119,7 @@ import Primer.Questions (
   variablesInScopeTy,
  )
 import Primer.Typecheck (
+  CheckEverythingRequest (CheckEverything, toCheck, trusted),
   Cxt,
   SmartHoles (NoSmartHoles, SmartHoles),
   TypeError,
@@ -156,8 +159,10 @@ import Primer.Zipper (
 --  need to send the log back and forth.
 --  But for now, to keep things simple, that's how it works.
 data Prog = Prog
-  { progTypes :: [TypeDef]
-  , progDefs :: Map ID Def -- The current program: a set of definitions indexed by ID
+  { progImports :: [Module]
+  -- ^ Some immutable imported modules
+  , progModule :: Module
+  -- ^ The one editable "current" module
   , progSelection :: Maybe Selection
   , progSmartHoles :: SmartHoles
   , progLog :: Log -- The log of all actions
@@ -165,6 +170,68 @@ data Prog = Prog
   deriving (Eq, Show, Generic)
   deriving (FromJSON, ToJSON) via VJSON Prog
 
+-- Note [Modules]
+-- The invariant is that the @progImports@ modules are never edited, but
+-- one can insert new ones (and perhaps delete unneeded ones).
+--
+-- Currently we assume that all Names and IDs are globally unique (across
+-- all the imported and editable modules). We intend to lift this restriction
+-- shortly by introducing unique module identifiers. Since the user has no
+-- control over IDs, this means that importing modules is unsafe: either it may
+-- break this invariant, or it could fail with no way for a end-user to fix it.
+-- (Or it would have to do a lot of work to uniquify names and ids, and then
+-- bear this in mind when importing further modules that may reference these.)
+-- Since we do not yet expose any way for an end-user to import modules, this
+-- restriction is not particularly severe in practice.
+--
+-- All modules in a @Prog@ shall be well-typed, in the appropriate scope:
+-- all the imports are in one mutual dependency group
+-- the @progModule@ has all the imports in scope
+
+-- | Imports some explicitly-given modules, ensuring that they are well-typed
+-- (and all their dependencies are already imported)
+importModules :: MonadEditApp m => [Module] -> m ()
+importModules ms = do
+  -- NB: we do not enforce the invariant that IDs and Names are globally unique
+  -- (see Note [Modules]), because we plan to only use this function internally
+  -- until we add unique names to modules.
+  -- This means that any call to this function should ensure that the IDs/Names
+  -- in the imported module are distinct from those already existing in the
+  -- App.
+  p <- gets appProg
+  checkedImports' <- runExceptT $ checkEverything NoSmartHoles $ CheckEverything{trusted = progImports p, toCheck = ms}
+  checkedImports <- case checkedImports' of
+    Left err -> throwError $ ActionError $ ImportFailed () err
+    Right ci -> pure ci
+  let p' = p & #progImports %~ (<> checkedImports)
+  modify (\a -> a{appProg = p'})
+
+-- | Get all type definitions from all modules (including imports)
+allTypes :: Prog -> [TypeDef]
+allTypes = moduleTypes . progModule
+
+-- | Get all definitions from all modules (including imports)
+allDefs :: Prog -> Map ID Def
+allDefs p = foldMap moduleDefs $ progModule p : progImports p
+
+-- | Add a definition to the editable module
+addDef :: ASTDef -> Prog -> Prog
+addDef d p =
+  let mod = progModule p
+      defs = moduleDefs mod
+      defs' = Map.insert (astDefID d) (DefAST d) defs
+      mod' = mod{moduleDefs = defs'}
+   in p{progModule = mod'}
+
+-- | Add a type definition to the editable module
+addTypeDef :: ASTTypeDef -> Prog -> Prog
+addTypeDef t p =
+  let mod = progModule p
+      tydefs = moduleTypes mod
+      tydefs' = tydefs <> [TypeDefAST t]
+      mod' = mod{moduleTypes = tydefs'}
+   in p{progModule = mod'}
+
 -- | The action log
 --  This is the canonical store of the program - we can recreate any current or
 --  past program state by replaying this log.
@@ -263,18 +330,21 @@ data EvalFullResp
 -- * Request handlers
 
 -- | Handle a question
+-- Note that these only consider the non-imported module as a location of which
+-- to ask a question. However, they will return variables which are in scope by
+-- dint of being imported.
 handleQuestion :: MonadQueryApp m => Question a -> m a
 handleQuestion = \case
   VariablesInScope defid exprid -> do
     node <- focusNode' defid exprid
-    progDefs <- asks $ progDefs . appProg
+    defs <- asks $ allDefs . appProg
     let (tyvars, termvars, globals) = case node of
-          Left zE -> variablesInScopeExpr progDefs zE
+          Left zE -> variablesInScopeExpr defs zE
           Right zT -> (variablesInScopeTy zT, [], [])
     pure ((tyvars, termvars), globals)
   GenerateName defid nodeid typeKind -> do
-    progTypeDefs <- asks $ progTypes . appProg
-    progDefs <- asks $ progDefs . appProg
+    progTypeDefs <- asks $ moduleTypes . progModule . appProg
+    progDefs <- asks $ moduleDefs . progModule . appProg
     names <-
       focusNode' defid nodeid <&> \case
         Left zE -> generateNameExpr typeKind zE
@@ -286,9 +356,17 @@ handleQuestion = \case
       prog <- asks appProg
       focusNode prog defid nodeid
 
+-- This only looks in the editable module, not in any imports
 focusNode :: MonadError ProgError m => Prog -> ID -> ID -> m (Either (Either ExprZ TypeZ) TypeZip)
-focusNode prog defid nodeid =
-  case lookupASTDef defid (progDefs prog) of
+focusNode prog = focusNodeDefs $ moduleDefs $ progModule prog
+
+-- This looks in the editable module and also in any imports
+focusNodeImports :: MonadError ProgError m => Prog -> ID -> ID -> m (Either (Either ExprZ TypeZ) TypeZip)
+focusNodeImports prog = focusNodeDefs $ allDefs prog
+
+focusNodeDefs :: MonadError ProgError m => Map ID Def -> ID -> ID -> m (Either (Either ExprZ TypeZ) TypeZip)
+focusNodeDefs defs defid nodeid =
+  case lookupASTDef defid defs of
     Nothing -> throwError $ DefNotFound defid
     Just def ->
       let mzE = locToEither <$> focusOn nodeid (focus $ astDefExpr def)
@@ -324,14 +402,14 @@ handleEditRequest actions = do
 handleEvalRequest :: MonadEditApp m => EvalReq -> m EvalResp
 handleEvalRequest req = do
   prog <- gets appProg
-  result <- Eval.step (progDefs prog) (evalReqExpr req) (evalReqRedex req)
+  result <- Eval.step (allDefs prog) (evalReqExpr req) (evalReqRedex req)
   case result of
     Left err -> throwError $ EvalError err
     Right (expr, detail) ->
       pure
         EvalResp
           { evalRespExpr = expr
-          , evalRespRedexes = Set.toList $ Eval.redexes (Map.mapMaybe defPrim $ progDefs prog) expr
+          , evalRespRedexes = Set.toList $ Eval.redexes (Map.mapMaybe defPrim $ allDefs prog) expr
           , evalRespDetail = detail
           }
 
@@ -339,102 +417,112 @@ handleEvalRequest req = do
 handleEvalFullRequest :: MonadEditApp m => EvalFullReq -> m EvalFullResp
 handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps}) = do
   prog <- gets appProg
-  result <- evalFull (mkTypeDefMap $ progTypes prog) (progDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
+  result <- evalFull (mkTypeDefMap $ allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
   pure $ case result of
     Left (TimedOut e) -> EvalFullRespTimedOut e
     Right nf -> EvalFullRespNormal nf
 
+-- Prog actions only affect the editable module
 applyProgAction :: MonadEditApp m => Prog -> Maybe ID -> ProgAction -> m (Prog, Maybe ID)
 applyProgAction prog mdefID = \case
-  MoveToDef id_ -> case Map.lookup id_ (progDefs prog) of
+  MoveToDef id_ -> case Map.lookup id_ (moduleDefs $ progModule prog) of
     Nothing -> throwError $ DefNotFound id_
     Just _ -> pure (prog, Just id_)
   DeleteDef id_
-    | Map.member id_ (progDefs prog) -> do
-        let defs = Map.delete id_ (progDefs prog)
-            prog' = prog{progDefs = defs, progSelection = Nothing}
+    | mod <- progModule prog
+    , Map.member id_ (moduleDefs mod) -> do
+        let modDefs' = Map.delete id_ $ moduleDefs mod
+            mod' = mod{moduleDefs = modDefs'}
+            prog' = prog{progModule = mod', progSelection = Nothing}
         -- Run a full TC solely to ensure that no references to the removed id
         -- remain. This is rather inefficient and could be improved in the
         -- future.
-        runExceptT (checkEverything @TypeError NoSmartHoles (progTypes prog) (progDefs prog')) >>= \case
+        runExceptT (checkEverything @TypeError NoSmartHoles CheckEverything{trusted = progImports prog, toCheck = [mod']}) >>= \case
           Left _ -> throwError $ DefInUse id_
           Right _ -> pure ()
         pure (prog', Nothing)
   DeleteDef id_ -> throwError $ DefNotFound id_
-  RenameDef id_ nameStr -> case lookupASTDef id_ (progDefs prog) of
+  RenameDef id_ nameStr -> case lookupASTDef id_ (moduleDefs $ progModule prog) of
     Nothing -> throwError $ DefNotFound id_
     Just def -> do
-      let name = unsafeMkName nameStr
-          existingName = Map.lookupMin $ Map.filter ((== name) . defName) $ progDefs prog
+      let defs = moduleDefs $ progModule prog
+          name = unsafeMkName nameStr
+          existingName = Map.lookupMin $ Map.filter ((== name) . defName) defs
       case existingName of
         Just (existingID, _) -> throwError $ DefAlreadyExists name existingID
         Nothing -> do
+          -- Since references are by ID, which we do not change, there is no problem
+          -- if this definition is referenced anywhere
           let def' = def{astDefName = name}
-          let defs = Map.insert (astDefID def') (DefAST def') (progDefs prog)
-          pure (prog{progDefs = defs, progSelection = Just $ Selection def' Nothing}, mdefID)
+          pure (addDef def' prog{progSelection = Just $ Selection def' Nothing}, mdefID)
   CreateDef n -> do
+    let defs = moduleDefs $ progModule prog
     name <- case n of
       Just nameStr ->
         let name = unsafeMkName nameStr
-            existingName = Map.lookupMin $ Map.filter ((== name) . defName) $ progDefs prog
+            existingName = Map.lookupMin $ Map.filter ((== name) . defName) defs
          in case existingName of
               Just (existingID, _) -> throwError $ DefAlreadyExists name existingID
               Nothing -> pure name
-      Nothing -> freshName $ Set.fromList $ map defName $ Map.elems $ progDefs prog
+      Nothing -> freshName $ Set.fromList $ map defName $ Map.elems defs
     id_ <- fresh
     expr <- newExpr
     ty <- newType
     let def = ASTDef id_ name expr ty
-        defs = Map.insert id_ (DefAST def) (progDefs prog)
-    pure (prog{progDefs = defs, progSelection = Just $ Selection def Nothing}, Just id_)
+    pure (addDef def prog{progSelection = Just $ Selection def Nothing}, Just id_)
   AddTypeDef td -> do
-    runExceptT @TypeError (checkTypeDefs $ progTypes prog <> [TypeDefAST td]) >>= \case
-      -- The frontend should never let this error case happen,
-      -- so we just dump out a raw string for debugging/logging purposes
-      -- (This is not currently true! We should synchronise the frontend with
-      -- the typechecker rules. For instance, the form allows to create
-      --   data T (T : *) = T
-      -- but the TC rejects it.
-      -- see https://github.com/hackworthltd/primer/issues/3)
-      Left err -> throwError $ TypeDefError $ show err
-      Right _ -> pure (prog{progTypes = progTypes prog <> [TypeDefAST td]}, mdefID)
+    runExceptT @TypeError
+      ( runReaderT
+          (checkTypeDefs [TypeDefAST td])
+          (buildTypingContext (allTypes prog) mempty NoSmartHoles)
+      )
+      >>= \case
+        -- The frontend should never let this error case happen,
+        -- so we just dump out a raw string for debugging/logging purposes
+        -- (This is not currently true! We should synchronise the frontend with
+        -- the typechecker rules. For instance, the form allows to create
+        --   data T (T : *) = T
+        -- but the TC rejects it.
+        -- see https://github.com/hackworthltd/primer/issues/3)
+        Left err -> throwError $ TypeDefError $ show err
+        Right _ -> pure (addTypeDef td prog, mdefID)
   BodyAction actions -> do
     withDef mdefID prog $ \def -> do
       smartHoles <- gets $ progSmartHoles . appProg
-      res <- applyActionsToBody smartHoles (progTypes prog) (progDefs prog) def actions
+      res <- applyActionsToBody smartHoles (allTypes prog) (allDefs prog) def actions
       case res of
         Left err -> throwError $ ActionError err
         Right (def', z) -> do
-          let defs = Map.insert (astDefID def) (DefAST def') (progDefs prog)
-              meta = bimap (view (position @1) . target) (view _typeMetaLens . target) $ locToEither z
+          let meta = bimap (view (position @1) . target) (view _typeMetaLens . target) $ locToEither z
               nodeId = either getID getID meta
           let prog' =
-                prog
-                  { progDefs = defs
-                  , progSelection =
-                      Just $
-                        Selection def' $
-                          Just
-                            NodeSelection
-                              { nodeType = BodyNode
-                              , nodeId
-                              , meta
-                              }
-                  }
+                addDef
+                  def'
+                  prog
+                    { progSelection =
+                        Just $
+                          Selection def' $
+                            Just
+                              NodeSelection
+                                { nodeType = BodyNode
+                                , nodeId
+                                , meta
+                                }
+                    }
           pure (prog', mdefID)
   SigAction actions -> do
     withDef mdefID prog $ \def -> do
       smartHoles <- gets $ progSmartHoles . appProg
-      res <- applyActionsToTypeSig smartHoles (progTypes prog) (progDefs prog) def actions
+      res <- applyActionsToTypeSig smartHoles (progImports prog) (progModule prog) def actions
       case res of
         Left err -> throwError $ ActionError err
-        Right (def', defs, zt) -> do
+        Right (def', mod', zt) -> do
           let node = target zt
               meta = view _typeMetaLens node
               nodeId = getID meta
               prog' =
                 prog
-                  { progDefs = defs
+                  { progModule = mod'
                   , progSelection =
                       Just $
                         Selection def' $
@@ -459,12 +547,13 @@ applyProgAction prog mdefID = \case
     Just i -> (,mdefID) <$> copyPasteBody prog fromIds i setup
 
 -- Look up the definition by its given ID, then run the given action with it
+-- only looks in the editable module
 withDef :: MonadEditApp m => Maybe ID -> Prog -> (ASTDef -> m a) -> m a
 withDef mdefID prog f =
   case mdefID of
     Nothing -> throwError NoDefSelected
     Just defid -> do
-      case lookupASTDef defid (progDefs prog) of
+      case lookupASTDef defid (moduleDefs $ progModule prog) of
         Nothing -> throwError $ DefNotFound defid
         Just def -> f def
 
@@ -581,8 +670,12 @@ newEmptyProg =
       ty = TEmptyHole (Meta 2 Nothing Nothing)
       def = DefAST $ ASTDef 0 "main" expr ty
    in Prog
-        { progTypes = []
-        , progDefs = Map.singleton 0 def
+        { progImports = mempty
+        , progModule =
+            Module
+              { moduleTypes = []
+              , moduleDefs = Map.singleton 0 def
+              }
         , progSelection = Nothing
         , progSmartHoles = SmartHoles
         , progLog = Log []
@@ -602,8 +695,11 @@ newEmptyApp =
 newProg :: Prog
 newProg =
   newEmptyProg
-    { progTypes = defaultTypeDefs
-    , progDefs = defaultDefs
+    { progModule =
+        Module
+          { moduleTypes = defaultTypeDefs
+          , moduleDefs = defaultDefs
+          }
     }
 
 defaultDefsNextId :: ID
@@ -670,7 +766,7 @@ instance MonadFresh NameCounter EditAppM where
 
 copyPasteSig :: MonadEditApp m => Prog -> (ID, ID) -> ID -> [Action] -> m Prog
 copyPasteSig p (fromDefId, fromTyId) toDefId setup = do
-  c' <- focusNode p fromDefId fromTyId
+  c' <- focusNodeImports p fromDefId fromTyId
   c <- case c' of
     Left (Left _) -> throwError $ CopyPasteError "tried to copy-paste an expression into a signature"
     Left (Right zt) -> pure $ Left zt
@@ -682,7 +778,7 @@ copyPasteSig p (fromDefId, fromTyId) toDefId setup = do
   -- which will pick up any problems. It is better to do it in one batch,
   -- in case the intermediate state after 'setup' causes more problems
   -- than the final state does.
-  doneSetup <- withDef (Just toDefId) p $ \def -> applyActionsToTypeSig smartHoles (progTypes p) (progDefs p) def setup
+  doneSetup <- withDef (Just toDefId) p $ \def -> applyActionsToTypeSig smartHoles (progImports p) (progModule p) def setup
   tgt <- case doneSetup of
     Left err -> throwError $ ActionError err
     Right (_, _, tgt) -> pure $ focusOnlyType tgt
@@ -698,11 +794,10 @@ copyPasteSig p (fromDefId, fromTyId) toDefId setup = do
   pasted <- case target tgt of
     TEmptyHole _ -> pure $ replace freshCopy tgt
     _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
-  oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (progDefs p)
+  oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (moduleDefs $ progModule p)
   let newDef = oldDef{astDefType = fromZipper pasted}
-  let newDefs = Map.insert toDefId (DefAST newDef) $ progDefs p
   let newSel = NodeSelection SigNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right)
-  let finalProg = p{progDefs = newDefs, progSelection = Just (Selection newDef $ Just newSel)}
+  let finalProg = addDef newDef p{progSelection = Just (Selection newDef $ Just newSel)}
   tcWholeProg finalProg
 
 -- We cannot use bindersAbove as that works on names only, and different scopes
@@ -760,12 +855,15 @@ loopM f a =
     Left a' -> loopM f a'
     Right b -> pure b
 
+-- | Checks every term definition in the editable module.
+-- Does not check typedefs or imported modules.
 tcWholeProg :: forall m. MonadEditApp m => Prog -> m Prog
 tcWholeProg p =
   let tc :: ReaderT Cxt (ExceptT ActionError m) Prog
       tc = do
-        defs' <- mapM (\d -> maybe (pure d) (fmap DefAST . checkDef) $ defAST d) (progDefs p)
-        let p' = p{progDefs = defs'}
+        defs' <- mapM (\d -> maybe (pure d) (fmap DefAST . checkDef) $ defAST d) (moduleDefs $ progModule p)
+        let mod' = (progModule p){moduleDefs = defs'}
+        let p' = p{progModule = mod'}
         -- We need to update the metadata cached in the selection
         let oldSel = progSelection p
         newSel <- case oldSel of
@@ -789,14 +887,14 @@ tcWholeProg p =
                   }
         pure $ p'{progSelection = newSel}
    in do
-        x <- runExceptT $ runReaderT tc $ buildTypingContext (progTypes p) (progDefs p) (progSmartHoles p)
+        x <- runExceptT $ runReaderT tc $ buildTypingContext (allTypes p) (allDefs p) (progSmartHoles p)
         case x of
           Left e -> throwError $ ActionError e
           Right prog -> pure prog
 
 copyPasteBody :: MonadEditApp m => Prog -> (ID, ID) -> ID -> [Action] -> m Prog
 copyPasteBody p (fromDefId, fromId) toDefId setup = do
-  src' <- focusNode p fromDefId fromId
+  src' <- focusNodeImports p fromDefId fromId
   -- reassociate so get Expr+(Type+Type), rather than (Expr+Type)+Type
   let src = case src' of
         Left (Left e) -> Left e
@@ -805,7 +903,7 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do
   smartHoles <- gets $ progSmartHoles . appProg
   -- The Loc zipper captures all the changes, they are only reflected in the
   -- returned Def, which we thus ignore
-  doneSetup <- withDef (Just toDefId) p $ \def -> applyActionsToBody smartHoles (progTypes p) (progDefs p) def setup
+  doneSetup <- withDef (Just toDefId) p $ \def -> applyActionsToBody smartHoles (allTypes p) (allDefs p) def setup
   tgt <- case doneSetup of
     Left err -> throwError $ ActionError err
     Right (_, tgt) -> pure tgt
@@ -826,11 +924,10 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do
       pasted <- case target tgtT of
         TEmptyHole _ -> pure $ replace freshCopy tgtT
         _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
-      oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (progDefs p)
+      oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (moduleDefs $ progModule p)
       let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted}
-      let newDefs = Map.insert toDefId (DefAST newDef) $ progDefs p
       let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right)
-      let finalProg = p{progDefs = newDefs, progSelection = Just (Selection newDef $ Just newSel)}
+      let finalProg = addDef newDef p{progSelection = Just (Selection newDef $ Just newSel)}
       tcWholeProg finalProg
     (Left srcE, InExpr tgtE) -> do
       let sharedScope =
@@ -880,11 +977,10 @@ copyPasteBody p (fromDefId, fromId) toDefId setup = do
       pasted <- case target tgtE of
         EmptyHole _ -> pure $ replace freshCopy tgtE
         _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
-      oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (progDefs p)
+      oldDef <- maybe (throwError $ DefNotFound toDefId) pure $ lookupASTDef toDefId (moduleDefs $ progModule p)
       let newDef = oldDef{astDefExpr = unfocusExpr pasted}
-      let newDefs = Map.insert toDefId (DefAST newDef) $ progDefs p
       let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _exprMetaLens % re _Left)
-      let finalProg = p{progDefs = newDefs, progSelection = Just (Selection newDef $ Just newSel)}
+      let finalProg = addDef newDef p{progSelection = Just (Selection newDef $ Just newSel)}
       tcWholeProg finalProg
 
 lookupASTDef :: ID -> Map ID Def -> Maybe ASTDef
diff --git a/primer/src/Primer/Module.hs b/primer/src/Primer/Module.hs
new file mode 100644
index 000000000..7c3e69e87
--- /dev/null
+++ b/primer/src/Primer/Module.hs
@@ -0,0 +1,12 @@
+module Primer.Module (Module (..)) where
+
+import Foreword
+import Primer.Core (Def, ID, TypeDef)
+import Primer.JSON
+
+data Module = Module
+  { moduleTypes :: [TypeDef]
+  , moduleDefs :: Map ID Def -- The current program: a set of definitions indexed by ID
+  }
+  deriving (Eq, Show, Generic)
+  deriving (FromJSON, ToJSON) via VJSON Module
diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index db4a3d394..02ef32f34 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE TypeApplications #-}
 
 -- | Typechecking for Core expressions.
@@ -17,6 +19,7 @@ module Primer.Typecheck (
   checkKind,
   checkTypeDefs,
   checkValidContext,
+  CheckEverythingRequest (..),
   checkEverything,
   Cxt (..),
   KindOrType (..),
@@ -64,7 +67,8 @@ import qualified Data.Map as M
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as S
 import Data.String (String)
-import Optics (Lens', over, set, view, (%))
+import Optics (Lens', over, set, traverseOf, view, (%))
+import Optics.Traversal (traversed)
 import Primer.Core (
   ASTDef (..),
   ASTTypeDef (..),
@@ -85,7 +89,6 @@ import Primer.Core (
   TypeMeta,
   ValCon (valConArgs, valConName),
   bindName,
-  defAST,
   defID,
   defName,
   defType,
@@ -102,6 +105,7 @@ import Primer.Core (
 import Primer.Core.DSL (branch, emptyHole, meta, meta')
 import Primer.Core.Utils (alphaEqTy, forgetTypeIDs, generateTypeIDs)
 import Primer.JSON (CustomJSON (CustomJSON), FromJSON, ToJSON, VJSON)
+import Primer.Module (Module (moduleDefs, moduleTypes))
 import Primer.Name (Name, NameCounter, freshName)
 import Primer.Subst (substTy)
 
@@ -201,6 +205,9 @@ localTmVars = M.mapMaybe (\case T t -> Just t; K _ -> Nothing) . localCxt
 localTyVars :: Cxt -> Map Name Kind
 localTyVars = M.mapMaybe (\case K k -> Just k; T _ -> Nothing) . localCxt
 
+noSmartHoles :: Cxt -> Cxt
+noSmartHoles cxt = cxt{smartHoles = NoSmartHoles}
+
 -- An empty typing context
 initialCxt :: SmartHoles -> Cxt
 initialCxt sh =
@@ -255,12 +262,12 @@ annotate t (Meta i _ v) = Meta i t v
 
 -- | Check a context is valid
 checkValidContext ::
-  (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e (ReaderT Cxt m), MonadNestedError TypeError e m) =>
+  (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e (ReaderT Cxt m)) =>
   Cxt ->
   m ()
 checkValidContext cxt = do
   let tds = typeDefs cxt
-  checkTypeDefsMap tds
+  runReaderT (checkTypeDefsMap tds) $ initialCxt NoSmartHoles
   runReaderT (checkGlobalCxt $ globalCxt cxt) $ (initialCxt NoSmartHoles){typeDefs = tds}
   checkLocalCxtTys $ localTyVars cxt
   runReaderT (checkLocalCxtTms $ localTmVars cxt) $ extendLocalCxtTys (M.toList $ localTyVars cxt) (initialCxt NoSmartHoles){typeDefs = tds}
@@ -278,7 +285,7 @@ checkValidContext cxt = do
 -- This is the same as 'checkTypeDefs', except it also checks the keys of the
 -- map are consistent with the names in the 'TypeDef's
 checkTypeDefsMap ::
-  (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e m, MonadNestedError TypeError e (ReaderT Cxt m)) =>
+  TypeM e m =>
   Map Name TypeDef ->
   m ()
 checkTypeDefsMap tds =
@@ -286,27 +293,29 @@ checkTypeDefsMap tds =
     then checkTypeDefs $ M.elems tds
     else throwError' $ InternalError "Inconsistent names in a Map Name TypeDef"
 
--- | Check all type definitions, as one recursive group
+-- | Check all type definitions, as one recursive group, in some monadic environment
 checkTypeDefs ::
-  (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e m, MonadNestedError TypeError e (ReaderT Cxt m)) =>
+  TypeM e m =>
   [TypeDef] ->
   m ()
 checkTypeDefs tds = do
+  existingTypes <- asks $ Map.elems . typeDefs
   -- NB: we expect the frontend to only submit acceptable typedefs, so all
   -- errors here are "internal errors" and should never be seen.
   -- (This is not quite true, see
   -- https://github.com/hackworthltd/primer/issues/3)
-  assert (distinct $ map typeDefName tds) "Duplicate-ly-named TypeDefs"
+  assert (distinct $ map typeDefName $ existingTypes <> tds) "Duplicate-ly-named TypeDefs"
   -- Note that constructors are synthesisable, so their names must be globally
   -- unique. We need to be able to work out the type of @TCon "C"@ without any
   -- extra information.
   let atds = mapMaybe typeDefAST tds
+  let allAtds = mapMaybe typeDefAST existingTypes <> atds
   assert
-    (distinct $ concatMap (map valConName . astTypeDefConstructors) atds)
+    (distinct $ concatMap (map valConName . astTypeDefConstructors) allAtds)
     "Duplicate-ly-named constructor (perhaps in different typedefs)"
   -- Note that these checks only apply to non-primitives:
   -- duplicate type names are checked elsewhere, kinds are correct by construction, and there are no constructors.
-  mapM_ checkTypeDef atds
+  local (extendTypeDefCxt tds) $ mapM_ checkTypeDef atds
   where
     -- In the core, we have many different namespaces, so the only name-clash
     -- checking we must do is
@@ -334,10 +343,8 @@ checkTypeDefs tds = do
       assert
         (notElem (astTypeDefName td) $ map fst params)
         "Duplicate names in one tydef: between type-def-name and parameter-names"
-      runReaderT (mapM_ (checkKind KType <=< fakeMeta) $ concatMap valConArgs cons) $
-        extendTypeDefCxt tds $
-          extendLocalCxtTys params $
-            initialCxt NoSmartHoles
+      local (noSmartHoles . extendLocalCxtTys params) $
+        mapM_ (checkKind KType <=< fakeMeta) $ concatMap valConArgs cons
     -- We need metadata to use checkKind, but we don't care about the output,
     -- just a yes/no answer. In this case it is fine to put nonsense in the
     -- metadata as it won't be inspected.
@@ -351,18 +358,38 @@ distinct = go mempty
       | x `S.member` seen = False
       | otherwise = go (S.insert x seen) xs
 
--- | Check all type definitions and top-level definitions, in the empty context
+data CheckEverythingRequest = CheckEverything
+  { trusted :: [Module]
+  , toCheck :: [Module]
+  }
+
+-- | Check a (mutually-recursive set of) module(s), in a given trusted
+-- environment of modules.
+-- Returns just the modules that were requested 'toCheck', with updated cached
+-- type information etc.
 checkEverything ::
   forall e m.
-  (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e m, MonadNestedError TypeError e (ReaderT Cxt m)) =>
+  (MonadFresh ID m, MonadFresh NameCounter m, MonadNestedError TypeError e (ReaderT Cxt m)) =>
   SmartHoles ->
-  [TypeDef] ->
-  Map ID Def ->
-  m (Map ID Def)
-checkEverything sh tydefs defs = do
-  checkTypeDefs tydefs
-  let cxt = buildTypingContext tydefs defs sh
-  flip runReaderT cxt $ mapM (\d -> maybe (pure d) (fmap DefAST . checkDef) $ defAST d) defs
+  CheckEverythingRequest ->
+  m [Module]
+checkEverything sh CheckEverything{trusted, toCheck} =
+  let cxt =
+        buildTypingContext
+          (concatMap moduleTypes trusted)
+          (foldMap moduleDefs trusted)
+          sh
+   in flip runReaderT cxt $ do
+        -- Check that the definition map has the right keys
+        for_ toCheck $ \m -> flip Map.traverseWithKey (moduleDefs m) $ \i d ->
+          unless (i == defID d) $ throwError' $ InternalError "Inconsistant IDs in moduleDefs map"
+        checkTypeDefs $ concatMap moduleTypes toCheck
+        let newTypes = foldMap moduleTypes toCheck
+            newDefs =
+              foldMap (\d -> [(defID d, (defName d, forgetTypeIDs $ defType d))]) $
+                foldMap moduleDefs toCheck
+        local (extendGlobalCxt newDefs . extendTypeDefCxt newTypes) $
+          traverseOf (traversed % #moduleDefs % traversed % #_DefAST) checkDef toCheck
 
 -- | Typecheck a definition.
 -- This checks that the type signature is well-formed, then checks the body
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index f6e2c8134..c488bc629 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -7,9 +7,19 @@ import Foreword
 
 import Control.Monad.Fresh
 import qualified Data.Map.Strict as Map
+import Data.Tuple.Extra (snd3)
 import Optics
 import Primer.Action (
-  Action (ConstructAnn, ConstructArrowL, ConstructGlobalVar, ConstructLet, Delete, EnterType, Move),
+  Action (
+    ConstructAnn,
+    ConstructArrowL,
+    ConstructGlobalVar,
+    ConstructLet,
+    ConstructTCon,
+    Delete,
+    EnterType,
+    Move
+  ),
   Movement (Branch, Child1, Child2),
  )
 import Primer.App (
@@ -20,8 +30,11 @@ import Primer.App (
   Prog (..),
   ProgAction (..),
   ProgError (..),
+  Question (VariablesInScope),
   Selection (..),
   handleEditRequest,
+  handleQuestion,
+  importModules,
   lookupASTDef,
   newApp,
   newEmptyApp,
@@ -34,12 +47,13 @@ import Primer.Core (
   ASTTypeDef (..),
   Def (..),
   Expr' (..),
-  ID,
+  ID (ID),
   Kind (KType),
   Meta (..),
   Type' (..),
   TypeDef (..),
   ValCon (..),
+  defID,
   defName,
   getID,
   _exprMeta,
@@ -67,6 +81,7 @@ import Primer.Core.DSL (
   tvar,
   var,
  )
+import Primer.Module (Module (moduleDefs, moduleTypes))
 import Primer.Name
 import Primer.Primitives (allPrimTypeDefs)
 import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@=?), (@?=))
@@ -91,18 +106,18 @@ unit_move_to_def_and_construct_let :: Assertion
 unit_move_to_def_and_construct_let =
   progActionTest defaultEmptyProg [MoveToDef 2, BodyAction [ConstructLet (Just "x")]] $
     expectSuccess $ \prog prog' ->
-      case astDefExpr <$> lookupASTDef 2 (progDefs prog') of
+      case astDefExpr <$> lookupASTDef 2 (moduleDefs $ progModule prog') of
         Just Let{} ->
           -- Check that main is unchanged
-          Map.lookup 0 (progDefs prog') @?= Map.lookup 0 (progDefs prog)
+          Map.lookup 0 (moduleDefs $ progModule prog') @?= Map.lookup 0 (moduleDefs $ progModule prog)
         _ -> assertFailure "definition not found"
 
 unit_rename_def :: Assertion
 unit_rename_def =
   progActionTest defaultEmptyProg [RenameDef 2 "foo"] $
     expectSuccess $ \_ prog' -> do
-      fmap defName (Map.lookup 2 (progDefs prog')) @?= Just "foo"
-      fmap defName (Map.lookup 0 (progDefs prog')) @?= Just "main"
+      fmap defName (Map.lookup 2 (moduleDefs $ progModule prog')) @?= Just "foo"
+      fmap defName (Map.lookup 0 (moduleDefs $ progModule prog')) @?= Just "main"
 
 unit_rename_def_to_same_name_as_existing_def :: Assertion
 unit_rename_def_to_same_name_as_existing_def =
@@ -118,8 +133,8 @@ unit_delete_def :: Assertion
 unit_delete_def =
   progActionTest defaultEmptyProg [DeleteDef 2] $
     expectSuccess $ \_ prog' -> do
-      fmap defName (Map.lookup 2 (progDefs prog')) @?= Nothing
-      fmap defName (Map.lookup 0 (progDefs prog')) @?= Just "main"
+      fmap defName (Map.lookup 2 (moduleDefs $ progModule prog')) @?= Nothing
+      fmap defName (Map.lookup 0 (moduleDefs $ progModule prog')) @?= Just "main"
 
 unit_delete_def_unknown_id :: Assertion
 unit_delete_def_unknown_id =
@@ -135,7 +150,7 @@ unit_delete_def_used_id =
 unit_delete_def_recursive :: Assertion
 unit_delete_def_recursive =
   progActionTest defaultEmptyProg [MoveToDef 0, BodyAction [ConstructGlobalVar 0], DeleteDef 0] $
-    expectSuccess $ \prog prog' -> Map.delete 0 (progDefs prog) @?= progDefs prog'
+    expectSuccess $ \prog prog' -> Map.delete 0 (moduleDefs $ progModule prog) @?= moduleDefs (progModule prog')
 
 unit_move_to_unknown_def :: Assertion
 unit_move_to_unknown_def =
@@ -152,8 +167,8 @@ unit_construct_let_without_moving_to_def_first =
 unit_create_def :: Assertion
 unit_create_def = progActionTest defaultEmptyProg [CreateDef $ Just "newDef"] $
   expectSuccess $ \_ prog' -> do
-    case lookupASTDef 4 (progDefs prog') of
-      Nothing -> assertFailure $ show $ progDefs prog'
+    case lookupASTDef 4 (moduleDefs $ progModule prog') of
+      Nothing -> assertFailure $ show $ moduleDefs $ progModule prog'
       Just def -> do
         astDefID def @?= 4
         astDefName def @?= "newDef"
@@ -186,11 +201,11 @@ unit_create_typedef =
    in progActionTest defaultEmptyProg [AddTypeDef lst, AddTypeDef tree] $
         expectSuccess $
           \_ prog' -> do
-            case progTypes prog' of
+            case moduleTypes $ progModule prog' of
               [lst', tree'] -> do
                 TypeDefAST lst @=? lst'
                 TypeDefAST tree @=? tree'
-              _ -> assertFailure $ show $ progTypes prog'
+              _ -> assertFailure $ show $ moduleTypes $ progModule prog'
 
 -- "List" is unknown here
 unit_create_typedef_bad_1 :: Assertion
@@ -324,7 +339,7 @@ unit_create_typedef_8 =
           , astTypeDefNameHints = []
           }
    in progActionTest defaultEmptyProg [AddTypeDef td] $
-        expectSuccess $ \_ prog' -> progTypes prog' @?= [TypeDefAST td]
+        expectSuccess $ \_ prog' -> moduleTypes (progModule prog') @?= [TypeDefAST td]
 
 -- Allow clash between type name and constructor name across types
 unit_create_typedef_9 :: Assertion
@@ -344,13 +359,13 @@ unit_create_typedef_9 =
           , astTypeDefNameHints = []
           }
    in progActionTest defaultEmptyProg [AddTypeDef td1, AddTypeDef td2] $
-        expectSuccess $ \_ prog' -> progTypes prog' @?= [TypeDefAST td1, TypeDefAST td2]
+        expectSuccess $ \_ prog' -> moduleTypes (progModule prog') @?= [TypeDefAST td1, TypeDefAST td2]
 
 unit_construct_arrow_in_sig :: Assertion
 unit_construct_arrow_in_sig =
   progActionTest defaultEmptyProg [MoveToDef 2, SigAction [ConstructArrowL, Move Child1]] $
     expectSuccess $ \_ prog' ->
-      case lookupASTDef 2 (progDefs prog') of
+      case lookupASTDef 2 (moduleDefs $ progModule prog') of
         Just def ->
           -- Check that the signature is an arrow type
           case astDefType def of
@@ -364,6 +379,31 @@ unit_construct_arrow_in_sig =
             _ -> assertFailure "not a function"
         _ -> assertFailure "definition not found"
 
+unit_sigaction_creates_holes :: Assertion
+unit_sigaction_creates_holes =
+  let acts =
+        [ -- main :: Char
+          MoveToDef 0
+        , SigAction [ConstructTCon "Char"]
+        , -- other :: Char; other = main
+          MoveToDef 2
+        , SigAction [ConstructTCon "Char"]
+        , BodyAction [ConstructGlobalVar 0]
+        , -- main :: Int
+          -- We expect this to change 'other' to contain a hole
+          MoveToDef 0
+        , SigAction [Delete, ConstructTCon "Int"]
+        ]
+   in progActionTest defaultPrimsProg acts $
+        expectSuccess $ \_ prog' ->
+          case lookupASTDef 2 (moduleDefs $ progModule prog') of
+            Just def ->
+              -- Check that the definition is a non-empty hole
+              case astDefExpr def of
+                Hole _ (GlobalVar _ 0) -> pure ()
+                _ -> assertFailure "expected {? main ?}"
+            _ -> assertFailure "definition not found"
+
 unit_copy_paste_duplicate :: Assertion
 unit_copy_paste_duplicate = do
   let ((p, fromDef, fromType, fromExpr, toDef, _toType, _toExpr), maxID) = create $ do
@@ -374,7 +414,8 @@ unit_copy_paste_duplicate = do
         blankID <- fresh
         blankDef <- ASTDef blankID "blank" <$> emptyHole <*> tEmptyHole
         pure
-          ( newProg{progDefs = Map.fromList [(mainID, DefAST mainDef), (blankID, DefAST blankDef)], progSelection = Nothing}
+          ( newProg{progSelection = Nothing}
+            & #progModule % #moduleDefs .~ Map.fromList [(mainID, DefAST mainDef), (blankID, DefAST blankDef)]
           , mainID
           , getID mainType
           , getID mainExpr
@@ -390,12 +431,12 @@ unit_copy_paste_duplicate = do
     Right (tcp, r) ->
       -- use the typechecked input p, as the result will have had a typecheck run, so
       -- we need the cached kinds to match up
-      let src = lookupASTDef fromDef (progDefs tcp)
+      let src = lookupASTDef fromDef (moduleDefs $ progModule tcp)
           clearIDs = set (_Just % _defIDs) 0
        in do
-            src @?= lookupASTDef fromDef (progDefs r)
-            assertBool "equal to toDef" $ src /= lookupASTDef toDef (progDefs r)
-            clearIDs (set (_Just % #astDefName) "blank" src) @?= clearIDs (lookupASTDef toDef (progDefs r))
+            src @?= lookupASTDef fromDef (moduleDefs $ progModule r)
+            assertBool "equal to toDef" $ src /= lookupASTDef toDef (moduleDefs $ progModule r)
+            clearIDs (set (_Just % #astDefName) "blank" src) @?= clearIDs (lookupASTDef toDef (moduleDefs $ progModule r))
 
 -- ∀a . (∀b,c . a -> b -> ∀d. c -> d)  -> ∀c. ?
 -- copy         ^------------------^
@@ -411,20 +452,20 @@ unit_copy_paste_duplicate = do
 -- - The d is bound within the copied subtree, so it is in-scope
 unit_copy_paste_type_scoping :: Assertion
 unit_copy_paste_type_scoping = do
-  let ((pInitial, defID, srcID, pExpected), maxID) = create $ do
+  let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do
         toCopy <- tvar "a" `tfun` tvar "b" `tfun` tforall "d" KType (tvar "c" `tfun` tvar "d")
         let skel r = tforall "a" KType $ tfun (tforall "b" KType $ tforall "c" KType $ pure toCopy) $ tforall "c" KType r
-        defID' <- fresh
-        defInitial <- ASTDef defID' "main" <$> emptyHole <*> skel tEmptyHole
-        expected <- ASTDef defID' "main" <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "d" KType (tEmptyHole `tfun` tvar "d"))
+        definitionID' <- fresh
+        defInitial <- ASTDef definitionID' "main" <$> emptyHole <*> skel tEmptyHole
+        expected <- ASTDef definitionID' "main" <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "d" KType (tEmptyHole `tfun` tvar "d"))
         pure
-          ( newEmptyProg{progDefs = Map.fromList [(defID', DefAST defInitial)]}
-          , defID'
+          ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)]
+          , definitionID'
           , getID toCopy
-          , newEmptyProg{progDefs = Map.fromList [(defID', DefAST expected)]}
+          , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)]
           )
   let a = newEmptyApp{appProg = pInitial}
-      actions = [MoveToDef defID, CopyPasteSig (defID, srcID) [Move Child1, Move Child2, Move Child1]]
+      actions = [MoveToDef definitionID, CopyPasteSig (definitionID, srcID) [Move Child1, Move Child2, Move Child1]]
       (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions
   case result of
     Left e -> assertFailure $ show e
@@ -433,24 +474,24 @@ unit_copy_paste_type_scoping = do
       -- we need the cached kinds to match up
       let clearIDs = set (traversed % #_DefAST % _defIDs) 0
        in -- clearIDs (set (_Just % #defName) "blank" src ) @?= clearIDs (Map.lookup toDef (progDefs r))
-          clearIDs (progDefs r) @?= clearIDs (progDefs tcpExpected)
+          clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
 
 -- ∀a b.a ~> ∀a.a
 unit_raise :: Assertion
 unit_raise = do
-  let ((pInitial, defID, srcID, pExpected), maxID) = create $ do
-        defID' <- fresh
+  let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do
+        definitionID' <- fresh
         toCopy <- tvar "a"
-        defInitial <- ASTDef defID' "main" <$> emptyHole <*> tforall "a" KType (tforall "b" KType $ pure toCopy)
-        expected <- ASTDef defID' "main" <$> emptyHole <*> tforall "a" KType (tvar "a")
+        defInitial <- ASTDef definitionID' "main" <$> emptyHole <*> tforall "a" KType (tforall "b" KType $ pure toCopy)
+        expected <- ASTDef definitionID' "main" <$> emptyHole <*> tforall "a" KType (tvar "a")
         pure
-          ( newEmptyProg{progDefs = Map.fromList [(defID', DefAST defInitial)]}
-          , defID'
+          ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)]
+          , definitionID'
           , getID toCopy
-          , newEmptyProg{progDefs = Map.fromList [(defID', DefAST expected)]}
+          , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)]
           )
   let a = newEmptyApp{appProg = pInitial}
-      actions = [MoveToDef defID, CopyPasteSig (defID, srcID) [Move Child1, Delete]]
+      actions = [MoveToDef definitionID, CopyPasteSig (definitionID, srcID) [Move Child1, Delete]]
       (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions
   case result of
     Left e -> assertFailure $ show e
@@ -458,7 +499,7 @@ unit_raise = do
       -- use the typechecked input p, as the result will have had a typecheck run, so
       -- we need the cached kinds to match up
       let clearIDs = set (traversed % #_DefAST % _defIDs) 0
-       in clearIDs (progDefs r) @?= clearIDs (progDefs tcpExpected)
+       in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
 
 -- ∀a. List a -> ∀b. b -> Pair a b
 -- /\a . λ x . case x of Nil -> ? ; Cons y ys -> /\@b z -> Pair @a @b y z
@@ -466,8 +507,8 @@ unit_raise = do
 -- /\a . λ x . case x of Nil -> lettype b = ? in let y = ? : a in Pair @a @b y z ; Cons y ys -> /\@b z -> Pair @a @b y z
 unit_copy_paste_expr_1 :: Assertion
 unit_copy_paste_expr_1 = do
-  let ((pInitial, defID, srcID, pExpected), maxID) = create $ do
-        defID' <- fresh
+  let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do
+        definitionID' <- fresh
         ty <- tforall "a" KType $ (tcon "List" `tapp` tvar "a") `tfun` tforall "b" KType (tvar "b" `tfun` (tcon "Pair" `tapp` tvar "a" `tapp` tvar "b"))
         let toCopy' = con "MakePair" `aPP` tvar "a" `aPP` tvar "b" `app` var "y" `app` var "z" -- want different IDs for the two occurences in expected
         toCopy <- toCopy'
@@ -483,16 +524,16 @@ unit_copy_paste_expr_1 = do
         -- TODO: in the future we may want to insert let bindings for variables
         -- which are out of scope in the target, and produce something like
         -- expectPasted <- letType "b" tEmptyHole $ let_ "y" (emptyHole `ann` tvar "a") $ let_ "z" (emptyHole `ann` tvar "b") toCopy'
-        defInitial <- ASTDef defID' "main" <$> skel emptyHole <*> pure ty
-        expected <- ASTDef defID' "main" <$> skel (pure expectPasted) <*> pure ty
+        defInitial <- ASTDef definitionID' "main" <$> skel emptyHole <*> pure ty
+        expected <- ASTDef definitionID' "main" <$> skel (pure expectPasted) <*> pure ty
         pure
-          ( newProg{progDefs = Map.fromList [(defID', DefAST defInitial)]}
-          , defID'
+          ( newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)]
+          , definitionID'
           , getID toCopy
-          , newProg{progDefs = Map.fromList [(defID', DefAST expected)]}
+          , newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)]
           )
   let a = newApp{appProg = pInitial}
-      actions = [MoveToDef defID, CopyPasteBody (defID, srcID) [Move Child1, Move Child1, Move (Branch "Nil")]]
+      actions = [MoveToDef definitionID, CopyPasteBody (definitionID, srcID) [Move Child1, Move Child1, Move (Branch "Nil")]]
       (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions
   case result of
     Left e -> assertFailure $ show e
@@ -500,7 +541,7 @@ unit_copy_paste_expr_1 = do
       -- use the typechecked input p, as the result will have had a typecheck run, so
       -- we need the cached kinds to match up
       let clearIDs = set (traversed % #_DefAST % _defIDs) 0
-       in clearIDs (progDefs r) @?= clearIDs (progDefs tcpExpected)
+       in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
 
 unit_copy_paste_ann :: Assertion
 unit_copy_paste_ann = do
@@ -511,7 +552,7 @@ unit_copy_paste_ann = do
         blankID <- fresh
         blankDef <- ASTDef blankID "blank" <$> emptyHole `ann` tEmptyHole <*> tEmptyHole
         pure
-          ( newProg{progDefs = Map.fromList [(mainID, DefAST mainDef), (blankID, DefAST blankDef)], progSelection = Nothing}
+          ( newProg{progSelection = Nothing} & #progModule % #moduleDefs .~ Map.fromList [(mainID, DefAST mainDef), (blankID, DefAST blankDef)]
           , mainID
           , getID toCopy
           , blankID
@@ -524,28 +565,28 @@ unit_copy_paste_ann = do
     Right (tcp, r) ->
       -- use the typechecked input p, as the result will have had a typecheck run, so
       -- we need the cached kinds to match up
-      let src = lookupASTDef fromDef (progDefs tcp)
+      let src = lookupASTDef fromDef (moduleDefs $ progModule tcp)
           clearIDs = set (_Just % _defIDs) 0
        in do
-            src @?= lookupASTDef fromDef (progDefs r)
-            assertBool "equal to toDef" $ src /= lookupASTDef toDef (progDefs r)
-            clearIDs (set (_Just % #astDefName) "blank" src) @?= clearIDs (lookupASTDef toDef (progDefs r))
+            src @?= lookupASTDef fromDef (moduleDefs $ progModule r)
+            assertBool "equal to toDef" $ src /= lookupASTDef toDef (moduleDefs $ progModule r)
+            clearIDs (set (_Just % #astDefName) "blank" src) @?= clearIDs (lookupASTDef toDef (moduleDefs $ progModule r))
 
 unit_copy_paste_ann2sig :: Assertion
 unit_copy_paste_ann2sig = do
-  let ((pInitial, defID, srcID, pExpected), maxID) = create $ do
-        defID' <- fresh
+  let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do
+        definitionID' <- fresh
         toCopy <- tcon "Bool"
-        defInitial <- ASTDef defID' "main" <$> emptyHole `ann` pure toCopy <*> tEmptyHole
-        expected <- ASTDef defID' "main" <$> emptyHole `ann` pure toCopy <*> tcon "Bool"
+        defInitial <- ASTDef definitionID' "main" <$> emptyHole `ann` pure toCopy <*> tEmptyHole
+        expected <- ASTDef definitionID' "main" <$> emptyHole `ann` pure toCopy <*> tcon "Bool"
         pure
-          ( newProg{progDefs = Map.fromList [(defID', DefAST defInitial)]}
-          , defID'
+          ( newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)]
+          , definitionID'
           , getID toCopy
-          , newProg{progDefs = Map.fromList [(defID', DefAST expected)]}
+          , newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)]
           )
   let a = newApp{appProg = pInitial}
-      actions = [MoveToDef defID, CopyPasteSig (defID, srcID) []]
+      actions = [MoveToDef definitionID, CopyPasteSig (definitionID, srcID) []]
       (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions
   case result of
     Left e -> assertFailure $ show e
@@ -553,23 +594,23 @@ unit_copy_paste_ann2sig = do
       -- use the typechecked input p, as the result will have had a typecheck run, so
       -- we need the cached kinds to match up
       let clearIDs = set (traversed % #_DefAST % _defIDs) 0
-       in clearIDs (progDefs r) @?= clearIDs (progDefs tcpExpected)
+       in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
 
 unit_copy_paste_sig2ann :: Assertion
 unit_copy_paste_sig2ann = do
-  let ((pInitial, defID, srcID, pExpected), maxID) = create $ do
-        defID' <- fresh
+  let ((pInitial, definitionID, srcID, pExpected), maxID) = create $ do
+        definitionID' <- fresh
         toCopy <- tcon "Bool"
-        defInitial <- ASTDef defID' "main" <$> emptyHole <*> pure toCopy
-        expected <- ASTDef defID' "main" <$> emptyHole `ann` tcon "Bool" <*> pure toCopy
+        defInitial <- ASTDef definitionID' "main" <$> emptyHole <*> pure toCopy
+        expected <- ASTDef definitionID' "main" <$> emptyHole `ann` tcon "Bool" <*> pure toCopy
         pure
-          ( newProg{progDefs = Map.fromList [(defID', DefAST defInitial)]}
-          , defID'
+          ( newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST defInitial)]
+          , definitionID'
           , getID toCopy
-          , newProg{progDefs = Map.fromList [(defID', DefAST expected)]}
+          , newProg & #progModule % #moduleDefs .~ Map.fromList [(definitionID', DefAST expected)]
           )
   let a = newApp{appProg = pInitial}
-      actions = [MoveToDef defID, CopyPasteBody (defID, srcID) [ConstructAnn, EnterType]]
+      actions = [MoveToDef definitionID, CopyPasteBody (definitionID, srcID) [ConstructAnn, EnterType]]
       (result, _) = runAppTestM maxID a $ (,) <$> tcWholeProg pExpected <*> handleEditRequest actions
   case result of
     Left e -> assertFailure $ show e
@@ -577,10 +618,81 @@ unit_copy_paste_sig2ann = do
       -- use the typechecked input p, as the result will have had a typecheck run, so
       -- we need the cached kinds to match up
       let clearIDs = set (traversed % #_DefAST % _defIDs) 0
-       in clearIDs (progDefs r) @?= clearIDs (progDefs tcpExpected)
+       in clearIDs (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
+
+-- VariablesInScope sees imported terms
+unit_import_vars :: Assertion
+unit_import_vars =
+  let test = do
+        p <- defaultPrimsProg
+        importModules [progModule p]
+        gets (Map.assocs . moduleDefs . progModule . appProg) >>= \case
+          [(i, DefAST d)] -> do
+            a' <- get
+            (_, vs) <- runReaderT (handleQuestion (VariablesInScope i $ getID $ astDefExpr d)) a'
+            pure $
+              assertBool "VariablesInScope did not report the imported Int.+" $
+                any ((== "Int.+") . snd3) vs
+          _ -> pure $ assertFailure "Expected one def 'main' from newEmptyApp"
+      a = newEmptyApp
+   in case fst $ runAppTestM (ID $ appIdCounter a) a test of
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
+-- Can reference something in an imported module (both types and terms)
+unit_import_reference :: Assertion
+unit_import_reference =
+  let test = do
+        p <- defaultPrimsProg
+        importModules [progModule p]
+        prog <- gets appProg
+        case (findGlobalByName prog "toUpper", Map.assocs $ moduleDefs $ progModule prog) of
+          (Just toUpperDef, [(i, _)]) -> do
+            _ <-
+              handleEditRequest
+                [ MoveToDef i
+                , SigAction [ConstructTCon "Char"]
+                , BodyAction [ConstructGlobalVar $ defID toUpperDef]
+                ]
+            pure $ pure ()
+          (Nothing, _) -> pure $ assertFailure "Could not find the imported toUpper"
+          (Just _, _) -> pure $ assertFailure "Expected one def 'main' from newEmptyApp"
+      a = newEmptyApp
+   in case fst $ runAppTestM (ID $ appIdCounter a) a test of
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
+-- Can copy and paste from an imported module
+unit_copy_paste_import :: Assertion
+unit_copy_paste_import =
+  let test = do
+        p <- defaultPrimsProg
+        importModules [progModule p]
+        prog <- gets appProg
+        case (findGlobalByName prog "other", Map.assocs $ moduleDefs $ progModule prog) of
+          (Just (DefAST other), [(i, _)]) -> do
+            let fromDef = astDefID other
+                fromType = getID $ astDefType other
+                fromExpr = getID $ astDefExpr other
+            _ <-
+              handleEditRequest
+                [ MoveToDef i
+                , CopyPasteSig (fromDef, fromType) []
+                , CopyPasteBody (fromDef, fromExpr) []
+                ]
+            pure $ pure ()
+          (Nothing, _) -> pure $ assertFailure "Could not find the imported 'other'"
+          (Just _, _) -> pure $ assertFailure "Expected one def 'main' from newEmptyApp"
+      a = newEmptyApp
+   in case fst $ runAppTestM (ID $ appIdCounter a) a test of
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
 
 -- * Utilities
 
+findGlobalByName :: Prog -> Name -> Maybe Def
+findGlobalByName p n = find ((== n) . defName) $ concatMap (Map.elems . moduleDefs) $ progModule p : progImports p
+
 -- We use a program with two defs: "main" and "other"
 defaultEmptyProg :: MonadFresh ID m => m Prog
 defaultEmptyProg = do
@@ -592,8 +704,7 @@ defaultEmptyProg = do
       otherDef = ASTDef 2 "other" otherExpr otherType
    in pure $
         newEmptyProg
-          { progDefs = Map.fromList [(0, DefAST mainDef), (2, DefAST otherDef)]
-          , progSelection =
+          { progSelection =
               Just $
                 Selection mainDef $
                   Just
@@ -603,6 +714,9 @@ defaultEmptyProg = do
                       , meta = Left (Meta 1 Nothing Nothing)
                       }
           }
+          & #progModule
+          % #moduleDefs
+          .~ Map.fromList [(0, DefAST mainDef), (2, DefAST otherDef)]
 
 -- `defaultEmptyProg`, plus all primitive definitions (types and terms)
 defaultPrimsProg :: MonadFresh ID m => m Prog
@@ -610,8 +724,8 @@ defaultPrimsProg = do
   p <- defaultEmptyProg
   withPrimDefs $ \_ m ->
     pure $
-      over #progTypes ((TypeDefPrim <$> toList allPrimTypeDefs) <>)
-        . over #progDefs ((DefPrim <$> m) <>)
+      over (#progModule % #moduleTypes) ((TypeDefPrim <$> toList allPrimTypeDefs) <>)
+        . over (#progModule % #moduleDefs) ((DefPrim <$> m) <>)
         $ p
 
 _defIDs :: Traversal' ASTDef ID
diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs
index 5f6560978..0fe70841f 100644
--- a/primer/test/Tests/Eval.hs
+++ b/primer/test/Tests/Eval.hs
@@ -8,14 +8,25 @@ import Data.Map ((!))
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
 import Optics (over, (^.))
+import Primer.App (
+  App (appIdCounter, appProg),
+  EvalReq (EvalReq, evalReqExpr, evalReqRedex),
+  EvalResp (EvalResp, evalRespExpr),
+  Prog (progModule),
+  handleEvalRequest,
+  importModules,
+  newEmptyApp,
+ )
 import Primer.Core (
   ASTDef (..),
   Def (..),
   Expr,
   Expr',
-  ID,
+  ID (ID),
   Type,
   Type',
+  defID,
+  getID,
   _exprMeta,
   _exprTypeMeta,
   _id,
@@ -41,9 +52,11 @@ import Primer.Eval (
  )
 import Primer.Name (Name)
 import Primer.Zipper (target)
+import Protolude.Partial (fromJust)
 import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=))
 import TestM (evalTestM)
 import TestUtils (withPrimDefs)
+import Tests.Action.Prog (defaultPrimsProg, findGlobalByName, runAppTestM)
 
 -- * 'tryReduce' tests
 
@@ -801,6 +814,25 @@ unit_redexes_prim_ann =
         `ann` (tcon "Char" `tfun` tcon "Char")
           `app` (char 'a' `ann` tcon "Char")
 
+-- Test that handleEvalRequest will reduce imported terms
+unit_eval_modules :: Assertion
+unit_eval_modules =
+  let test = do
+        p <- defaultPrimsProg
+        importModules [progModule p]
+        prog <- gets appProg
+        let toUpperId = defID $ fromJust $ findGlobalByName prog "toUpper"
+        foo <- global toUpperId `app` char 'a'
+        EvalResp{evalRespExpr = e} <-
+          handleEvalRequest
+            EvalReq{evalReqExpr = foo, evalReqRedex = getID foo}
+        expect <- char 'A'
+        pure $ e ~= expect
+      a = newEmptyApp
+   in case fst $ runAppTestM (ID $ appIdCounter a) a test of
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
 -- * Misc helpers
 
 -- | Like '@?=' but specifically for expressions.
diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs
index 1758999c6..86250b300 100644
--- a/primer/test/Tests/EvalFull.hs
+++ b/primer/test/Tests/EvalFull.hs
@@ -14,7 +14,16 @@ import Hedgehog hiding (Var, test)
 import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
 import Optics
-import Primer.App (defaultTypeDefs)
+import Primer.App (
+  App (appIdCounter, appProg),
+  EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullReqExpr),
+  EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut),
+  Prog (progModule),
+  defaultTypeDefs,
+  handleEvalFullRequest,
+  importModules,
+  newEmptyApp,
+ )
 import Primer.Core
 import Primer.Core.DSL
 import Primer.Core.Utils (forgetIDs, generateIDs, generateTypeIDs)
@@ -27,9 +36,12 @@ import Primer.Typecheck (
   mkTypeDefMap,
   typeDefs,
  )
+import Protolude.Partial (fromJust)
 import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=))
 import TestM
 import TestUtils (withPrimDefs)
+import Tests.Action.Prog (defaultPrimsProg, findGlobalByName, runAppTestM)
+import Tests.Eval ((~=))
 import Tests.Gen.Core.Typed (checkTest)
 
 unit_1 :: Assertion
@@ -894,6 +906,31 @@ unit_prim_partial_map =
       map_ <- lAM "a" $ lAM "b" $ lam "f" $ letrec "go" worker ((tcon "List" `tapp` tvar "a") `tfun` (tcon "List" `tapp` tvar "b")) $ var "go"
       pure $ DefAST $ ASTDef mapID "map" map_ mapTy
 
+-- Test that handleEvalFullRequest will reduce imported terms
+unit_eval_full_modules :: Assertion
+unit_eval_full_modules =
+  let test = do
+        p <- defaultPrimsProg
+        importModules [progModule p]
+        prog <- gets appProg
+        let toUpperId = defID $ fromJust $ findGlobalByName prog "toUpper"
+        foo <- global toUpperId `app` char 'a'
+        resp <-
+          handleEvalFullRequest
+            EvalFullReq
+              { evalFullReqExpr = foo
+              , evalFullCxtDir = Chk
+              , evalFullMaxSteps = 2
+              }
+        expect <- char 'A'
+        pure $ case resp of
+          EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out"
+          EvalFullRespNormal e -> e ~= expect
+      a = newEmptyApp
+   in case fst $ runAppTestM (ID $ appIdCounter a) a test of
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
 -- * Utilities
 
 evalFullTest :: ID -> M.Map Name TypeDef -> M.Map ID Def -> TerminationBound -> Dir -> Expr -> Either EvalFullError Expr
diff --git a/primer/test/Tests/Primitives.hs b/primer/test/Tests/Primitives.hs
index 8700d9404..a706adc27 100644
--- a/primer/test/Tests/Primitives.hs
+++ b/primer/test/Tests/Primitives.hs
@@ -28,7 +28,7 @@ import Primer.Typecheck (
   TypeError (PrimitiveTypeNotInScope, UnknownTypeConstructor),
   buildTypingContext,
   checkKind,
-  checkTypeDefs,
+  checkValidContext,
   synth,
  )
 
@@ -56,7 +56,7 @@ unit_prim_con_scope = do
 unit_prim_con_scope_ast :: Assertion
 unit_prim_con_scope_ast = do
   -- Our type def is accepted
-  test (checkTypeDefs [charASTDef]) @?= Right ()
+  test (checkValidContext =<< ask) @?= Right ()
   -- Char is in scope (though the wrong kind to accept 'PrimChar's!)
   assertBool "Char is not in scope?" $
     isRight $
diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs
index 6e5d2703d..5248cf43c 100644
--- a/primer/test/Tests/Serialization.hs
+++ b/primer/test/Tests/Serialization.hs
@@ -42,6 +42,7 @@ import Primer.Core (
   TypeMeta,
   ValCon (..),
  )
+import Primer.Module (Module (Module, moduleDefs, moduleTypes))
 import Primer.Name (unsafeMkName)
 import Primer.Typecheck (SmartHoles (SmartHoles))
 import System.FilePath (takeBaseName)
@@ -108,8 +109,12 @@ fixtures =
       progaction = MoveToDef 0
       prog =
         Prog
-          { progTypes = [typeDef]
-          , progDefs = Map.singleton 1 (DefAST def)
+          { progImports = mempty
+          , progModule =
+              Module
+                { moduleTypes = [typeDef]
+                , moduleDefs = Map.singleton 1 (DefAST def)
+                }
           , progSelection = Just selection
           , progSmartHoles = SmartHoles
           , progLog = log
diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json
index d1e2c2178..5d733bf3a 100644
--- a/primer/test/outputs/serialization/edit_response_2.json
+++ b/primer/test/outputs/serialization/edit_response_2.json
@@ -1,38 +1,6 @@
 {
     "Right": {
-        "progDefs": {
-            "1": {
-                "contents": {
-                    "astDefExpr": {
-                        "contents": [
-                            0,
-                            {
-                                "contents": {
-                                    "contents": [],
-                                    "tag": "TEmptyHole"
-                                },
-                                "tag": "TCSynthed"
-                            },
-                            null
-                        ],
-                        "tag": "EmptyHole"
-                    },
-                    "astDefID": 1,
-                    "astDefName": "main",
-                    "astDefType": {
-                        "contents": [
-                            0,
-                            {
-                                "tag": "KType"
-                            },
-                            null
-                        ],
-                        "tag": "TEmptyHole"
-                    }
-                },
-                "tag": "DefAST"
-            }
-        },
+        "progImports": [],
         "progLog": {
             "unlog": [
                 [
@@ -50,6 +18,106 @@
                 ]
             ]
         },
+        "progModule": {
+            "moduleDefs": {
+                "1": {
+                    "contents": {
+                        "astDefExpr": {
+                            "contents": [
+                                0,
+                                {
+                                    "contents": {
+                                        "contents": [],
+                                        "tag": "TEmptyHole"
+                                    },
+                                    "tag": "TCSynthed"
+                                },
+                                null
+                            ],
+                            "tag": "EmptyHole"
+                        },
+                        "astDefID": 1,
+                        "astDefName": "main",
+                        "astDefType": {
+                            "contents": [
+                                0,
+                                {
+                                    "tag": "KType"
+                                },
+                                null
+                            ],
+                            "tag": "TEmptyHole"
+                        }
+                    },
+                    "tag": "DefAST"
+                }
+            },
+            "moduleTypes": [
+                {
+                    "contents": {
+                        "astTypeDefConstructors": [
+                            {
+                                "valConArgs": [
+                                    {
+                                        "contents": [
+                                            [],
+                                            {
+                                                "contents": [
+                                                    [],
+                                                    "b"
+                                                ],
+                                                "tag": "TCon"
+                                            },
+                                            {
+                                                "contents": [
+                                                    [],
+                                                    "a"
+                                                ],
+                                                "tag": "TCon"
+                                            }
+                                        ],
+                                        "tag": "TApp"
+                                    },
+                                    {
+                                        "contents": [
+                                            [],
+                                            "Nat"
+                                        ],
+                                        "tag": "TCon"
+                                    }
+                                ],
+                                "valConName": "C"
+                            }
+                        ],
+                        "astTypeDefName": "T",
+                        "astTypeDefNameHints": [],
+                        "astTypeDefParameters": [
+                            [
+                                "a",
+                                {
+                                    "tag": "KType"
+                                }
+                            ],
+                            [
+                                "b",
+                                {
+                                    "contents": [
+                                        {
+                                            "tag": "KType"
+                                        },
+                                        {
+                                            "tag": "KType"
+                                        }
+                                    ],
+                                    "tag": "KFun"
+                                }
+                            ]
+                        ]
+                    },
+                    "tag": "TypeDefAST"
+                }
+            ]
+        },
         "progSelection": {
             "selectedDef": {
                 "astDefExpr": {
@@ -101,71 +169,6 @@
         },
         "progSmartHoles": {
             "tag": "SmartHoles"
-        },
-        "progTypes": [
-            {
-                "contents": {
-                    "astTypeDefConstructors": [
-                        {
-                            "valConArgs": [
-                                {
-                                    "contents": [
-                                        [],
-                                        {
-                                            "contents": [
-                                                [],
-                                                "b"
-                                            ],
-                                            "tag": "TCon"
-                                        },
-                                        {
-                                            "contents": [
-                                                [],
-                                                "a"
-                                            ],
-                                            "tag": "TCon"
-                                        }
-                                    ],
-                                    "tag": "TApp"
-                                },
-                                {
-                                    "contents": [
-                                        [],
-                                        "Nat"
-                                    ],
-                                    "tag": "TCon"
-                                }
-                            ],
-                            "valConName": "C"
-                        }
-                    ],
-                    "astTypeDefName": "T",
-                    "astTypeDefNameHints": [],
-                    "astTypeDefParameters": [
-                        [
-                            "a",
-                            {
-                                "tag": "KType"
-                            }
-                        ],
-                        [
-                            "b",
-                            {
-                                "contents": [
-                                    {
-                                        "tag": "KType"
-                                    },
-                                    {
-                                        "tag": "KType"
-                                    }
-                                ],
-                                "tag": "KFun"
-                            }
-                        ]
-                    ]
-                },
-                "tag": "TypeDefAST"
-            }
-        ]
+        }
     }
 }
\ No newline at end of file
diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json
index 470e2fce1..69a2ea088 100644
--- a/primer/test/outputs/serialization/prog.json
+++ b/primer/test/outputs/serialization/prog.json
@@ -1,37 +1,5 @@
 {
-    "progDefs": {
-        "1": {
-            "contents": {
-                "astDefExpr": {
-                    "contents": [
-                        0,
-                        {
-                            "contents": {
-                                "contents": [],
-                                "tag": "TEmptyHole"
-                            },
-                            "tag": "TCSynthed"
-                        },
-                        null
-                    ],
-                    "tag": "EmptyHole"
-                },
-                "astDefID": 1,
-                "astDefName": "main",
-                "astDefType": {
-                    "contents": [
-                        0,
-                        {
-                            "tag": "KType"
-                        },
-                        null
-                    ],
-                    "tag": "TEmptyHole"
-                }
-            },
-            "tag": "DefAST"
-        }
-    },
+    "progImports": [],
     "progLog": {
         "unlog": [
             [
@@ -49,6 +17,106 @@
             ]
         ]
     },
+    "progModule": {
+        "moduleDefs": {
+            "1": {
+                "contents": {
+                    "astDefExpr": {
+                        "contents": [
+                            0,
+                            {
+                                "contents": {
+                                    "contents": [],
+                                    "tag": "TEmptyHole"
+                                },
+                                "tag": "TCSynthed"
+                            },
+                            null
+                        ],
+                        "tag": "EmptyHole"
+                    },
+                    "astDefID": 1,
+                    "astDefName": "main",
+                    "astDefType": {
+                        "contents": [
+                            0,
+                            {
+                                "tag": "KType"
+                            },
+                            null
+                        ],
+                        "tag": "TEmptyHole"
+                    }
+                },
+                "tag": "DefAST"
+            }
+        },
+        "moduleTypes": [
+            {
+                "contents": {
+                    "astTypeDefConstructors": [
+                        {
+                            "valConArgs": [
+                                {
+                                    "contents": [
+                                        [],
+                                        {
+                                            "contents": [
+                                                [],
+                                                "b"
+                                            ],
+                                            "tag": "TCon"
+                                        },
+                                        {
+                                            "contents": [
+                                                [],
+                                                "a"
+                                            ],
+                                            "tag": "TCon"
+                                        }
+                                    ],
+                                    "tag": "TApp"
+                                },
+                                {
+                                    "contents": [
+                                        [],
+                                        "Nat"
+                                    ],
+                                    "tag": "TCon"
+                                }
+                            ],
+                            "valConName": "C"
+                        }
+                    ],
+                    "astTypeDefName": "T",
+                    "astTypeDefNameHints": [],
+                    "astTypeDefParameters": [
+                        [
+                            "a",
+                            {
+                                "tag": "KType"
+                            }
+                        ],
+                        [
+                            "b",
+                            {
+                                "contents": [
+                                    {
+                                        "tag": "KType"
+                                    },
+                                    {
+                                        "tag": "KType"
+                                    }
+                                ],
+                                "tag": "KFun"
+                            }
+                        ]
+                    ]
+                },
+                "tag": "TypeDefAST"
+            }
+        ]
+    },
     "progSelection": {
         "selectedDef": {
             "astDefExpr": {
@@ -100,70 +168,5 @@
     },
     "progSmartHoles": {
         "tag": "SmartHoles"
-    },
-    "progTypes": [
-        {
-            "contents": {
-                "astTypeDefConstructors": [
-                    {
-                        "valConArgs": [
-                            {
-                                "contents": [
-                                    [],
-                                    {
-                                        "contents": [
-                                            [],
-                                            "b"
-                                        ],
-                                        "tag": "TCon"
-                                    },
-                                    {
-                                        "contents": [
-                                            [],
-                                            "a"
-                                        ],
-                                        "tag": "TCon"
-                                    }
-                                ],
-                                "tag": "TApp"
-                            },
-                            {
-                                "contents": [
-                                    [],
-                                    "Nat"
-                                ],
-                                "tag": "TCon"
-                            }
-                        ],
-                        "valConName": "C"
-                    }
-                ],
-                "astTypeDefName": "T",
-                "astTypeDefNameHints": [],
-                "astTypeDefParameters": [
-                    [
-                        "a",
-                        {
-                            "tag": "KType"
-                        }
-                    ],
-                    [
-                        "b",
-                        {
-                            "contents": [
-                                {
-                                    "tag": "KType"
-                                },
-                                {
-                                    "tag": "KType"
-                                }
-                            ],
-                            "tag": "KFun"
-                        }
-                    ]
-                ]
-            },
-            "tag": "TypeDefAST"
-        }
-    ]
+    }
 }
\ No newline at end of file