diff --git a/primer-rel8/test/TestUtils.hs b/primer-rel8/test/TestUtils.hs
index fc9a46a13..02cef5668 100644
--- a/primer-rel8/test/TestUtils.hs
+++ b/primer-rel8/test/TestUtils.hs
@@ -363,10 +363,11 @@ testApp =
     testProg =
       newEmptyProg
         { progImports = [builtinModule, primitiveModule]
-        , progModule =
-            Module
-              { moduleName = ModuleName $ "TestModule" :| []
-              , moduleTypes = mempty
-              , moduleDefs = Map.singleton (baseName $ astDefName testASTDef) (DefAST testASTDef)
-              }
+        , progModules =
+            [ Module
+                { moduleName = ModuleName $ "TestModule" :| []
+                , moduleTypes = mempty
+                , moduleDefs = Map.singleton (baseName $ astDefName testASTDef) (DefAST testASTDef)
+                }
+            ]
         }
diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs
index b448654d7..2f6f5d661 100644
--- a/primer-service/src/Primer/OpenAPI.hs
+++ b/primer-service/src/Primer/OpenAPI.hs
@@ -9,9 +9,9 @@ module Primer.OpenAPI (
 import Data.OpenApi (ToSchema)
 import Data.Text (Text)
 import Data.Typeable (Typeable)
-import Primer.API (Def, Prog, Tree)
+import Primer.API (Def, Module, Prog, Tree)
 import Primer.App (InitialApp)
-import Primer.Core (GlobalName, ID (..), LVarName)
+import Primer.Core (GlobalName, ID (..), LVarName, ModuleName)
 import Primer.Database (Session, SessionName)
 import Primer.Name (Name)
 
@@ -40,4 +40,6 @@ deriving via Name instance Typeable k => ToSchema (GlobalName k)
 deriving via Name instance (ToSchema LVarName)
 instance ToSchema Tree
 instance ToSchema Def
+instance ToSchema ModuleName
+instance ToSchema Module
 instance ToSchema Prog
diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs
index 9a16aac71..6a18608f9 100644
--- a/primer/src/Primer/API.hs
+++ b/primer/src/Primer/API.hs
@@ -21,6 +21,7 @@ module Primer.API (
   getVersion,
   Tree,
   Prog,
+  Module,
   Def,
   getProgram,
   getSessionName,
@@ -70,7 +71,8 @@ import Primer.App (
   handleMutationRequest,
   handleQuestion,
   initialApp,
-  progModule,
+  progImports,
+  progModules,
   runEditAppM,
   runQueryAppM,
  )
@@ -83,6 +85,7 @@ import Primer.Core (
   ID,
   Kind,
   LVarName,
+  ModuleName,
   PrimCon (..),
   TmVarRef (GlobalVarRef, LocalVarRef),
   TyConName,
@@ -123,7 +126,7 @@ import qualified Primer.Database as Database (
     Success
   ),
  )
-import Primer.Module (Module (moduleDefs, moduleTypes))
+import Primer.Module (moduleDefs, moduleName, moduleTypes)
 import Primer.Name (Name, unName)
 import qualified StmContainers.Map as StmMap
 
@@ -301,8 +304,19 @@ instance ToJSON Tree
 
 -- | This type is the API's view of a 'App.Prog'
 -- (this is expected to evolve as we flesh out the API)
-data Prog = Prog
-  { types :: [TyConName]
+newtype Prog = Prog
+  { modules :: [Module]
+  }
+  deriving (Generic)
+
+instance ToJSON Prog
+
+-- | This type is the API's view of a 'Module.Module'
+-- (this is expected to evolve as we flesh out the API)
+data Module = Module
+  { modname :: ModuleName
+  , editable :: Bool
+  , types :: [TyConName]
   , -- We don't use Map Name Def as it is rather redundant since each
     -- Def carries a name field, and it is difficult to enforce that
     -- "the keys of this object match the name field of the
@@ -311,7 +325,7 @@ data Prog = Prog
   }
   deriving (Generic)
 
-instance ToJSON Prog
+instance ToJSON Module
 
 -- | This type is the api's view of a 'Primer.Core.Def'
 -- (this is expected to evolve as we flesh out the API)
@@ -327,18 +341,23 @@ instance ToJSON Def
 
 viewProg :: App.Prog -> Prog
 viewProg p =
-  Prog
-    { types = typeDefName <$> Map.elems (moduleTypes $ progModule p)
-    , defs =
-        ( \d ->
-            Def
-              { name = defName d
-              , type_ = viewTreeType $ defType d
-              , term = viewTreeExpr . astDefExpr <$> defAST d
-              }
-        )
-          <$> Map.elems (moduleDefs $ progModule p)
-    }
+  Prog{modules = map (viewModule True) (progModules p) <> map (viewModule False) (progImports p)}
+  where
+    viewModule e m =
+      Module
+        { modname = moduleName m
+        , editable = e
+        , types = typeDefName <$> Map.elems (moduleTypes m)
+        , defs =
+            ( \d ->
+                Def
+                  { name = defName d
+                  , type_ = viewTreeType $ defType d
+                  , term = viewTreeExpr . astDefExpr <$> defAST d
+                  }
+            )
+              <$> Map.elems (moduleDefs m)
+        }
 
 -- | A simple method to extract 'Tree's from 'Expr's. This is injective.
 -- Currently it is designed to be simple and just enough to enable
diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs
index 1b75720f6..ee952c863 100644
--- a/primer/src/Primer/Action.hs
+++ b/primer/src/Primer/Action.hs
@@ -387,7 +387,7 @@ data ProgAction
   | -- | Rename the definition with the given (base) Name
     RenameDef GVarName Text
   | -- | Create a new definition
-    CreateDef (Maybe Text)
+    CreateDef ModuleName (Maybe Text)
   | -- | Delete a new definition
     DeleteDef GVarName
   | -- | Add a new type definition
@@ -422,8 +422,8 @@ data ProgAction
     --   At the start of the actions, the cursor starts at the root of the definition's type/expression
     CopyPasteSig (GVarName, ID) [Action]
   | CopyPasteBody (GVarName, ID) [Action]
-  | -- | Renames the sole editable module
-    RenameModule (NonEmpty Text)
+  | -- | Renames an editable module (will return an error if asked to rename an imported module)
+    RenameModule ModuleName (NonEmpty Text)
   deriving (Eq, Show, Generic)
   deriving (FromJSON, ToJSON) via VJSON ProgAction
 
@@ -439,24 +439,26 @@ type ActionM m =
 -- | 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.
+-- Note that this may introduce new holes when using SmartHoles, and thus we
+-- return a whole set of modules as well as the one definition we wanted to
+-- change.
 applyActionsToTypeSig ::
   (MonadFresh ID m, MonadFresh NameCounter m) =>
   SmartHoles ->
   [Module] ->
-  Module ->
+  -- | The @Module@ we are focused on, and all the other editable modules
+  (Module, [Module]) ->
   -- | This must be one of the definitions in the @Module@
   ASTDef ->
   [Action] ->
-  m (Either ActionError (ASTDef, Module, TypeZ))
-applyActionsToTypeSig smartHoles imports mod def actions =
+  m (Either ActionError (ASTDef, [Module], TypeZ))
+applyActionsToTypeSig smartHoles imports (mod, mods) def actions =
   runReaderT
     go
-    (buildTypingContextFromModules (mod : imports) smartHoles)
+    (buildTypingContextFromModules (mod : mods <> imports) smartHoles)
     & runExceptT
   where
-    go :: ActionM m => m (ASTDef, Module, 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)
@@ -469,10 +471,8 @@ applyActionsToTypeSig smartHoles imports mod def actions =
       -- We make sure that the updated type is present in the global context.
       -- 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"
+      checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods})
+        >>= \checkedMods -> pure (def', checkedMods, zt)
     -- 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/Action/Available.hs b/primer/src/Primer/Action/Available.hs
index 5d065ae93..22b471460 100644
--- a/primer/src/Primer/Action/Available.hs
+++ b/primer/src/Primer/Action/Available.hs
@@ -100,7 +100,7 @@ actionsForDef l defs def =
               qn = astDefName def
               copyName = uniquifyDefName (qualifiedModule qn) (unName (baseName qn) <> "Copy") defs
            in NoInputRequired
-                [ CreateDef (Just copyName)
+                [ CreateDef (qualifiedModule $ astDefName def) (Just copyName)
                 , CopyPasteSig (astDefName def, sigID) []
                 , CopyPasteBody (astDefName def, bodyID) []
                 ]
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index afaeb537e..aba82842f 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -70,6 +70,7 @@ import Optics (
   Field2 (_2),
   Field3 (_3),
   ReversibleOptic (re),
+  mapped,
   over,
   toListOf,
   traverseOf,
@@ -122,7 +123,6 @@ import Primer.Core (
   defName,
   defPrim,
   getID,
-  moduleNamePretty,
   qualifyName,
   typeDefAST,
   typesInExpr,
@@ -169,7 +169,6 @@ import Primer.Typecheck (
   SmartHoles (NoSmartHoles, SmartHoles),
   TypeError,
   buildTypingContextFromModules,
-  checkDef,
   checkEverything,
   checkTypeDefs,
   mkTypeDefMapQualified,
@@ -207,8 +206,8 @@ import Primer.Zipper (
 data Prog = Prog
   { progImports :: [Module]
   -- ^ Some immutable imported modules
-  , progModule :: Module
-  -- ^ The one editable "current" module
+  , progModules :: [Module]
+  -- ^ The editable "home" modules
   , progSelection :: Maybe Selection
   , progSmartHoles :: SmartHoles
   , progLog :: Log -- The log of all actions
@@ -217,7 +216,7 @@ data Prog = Prog
   deriving (FromJSON, ToJSON) via VJSON Prog
 
 progAllModules :: Prog -> [Module]
-progAllModules p = progModule p : progImports p
+progAllModules p = progModules p <> progImports p
 
 -- Note [Modules]
 -- The invariant is that the @progImports@ modules are never edited, but
@@ -244,7 +243,7 @@ importModules ms = do
       ActionError $
         ImportNameClash $
           (currentNames `intersect` newNames) <> (newNames \\ ordNub newNames)
-  -- Imports must be well-typed (and cannot depend on the editable module)
+  -- Imports must be well-typed (and cannot depend on the editable modules)
   checkedImports <-
     liftError (ActionError . ImportFailed ()) $
       checkEverything NoSmartHoles $
@@ -260,24 +259,6 @@ allTypes p = foldMap moduleTypesQualified $ progAllModules p
 allDefs :: Prog -> DefMap
 allDefs p = foldMap moduleDefsQualified $ progAllModules p
 
--- | Add a definition to the editable module
--- assumes the def has the correct name to go in the editable module
-addDef :: ASTDef -> Prog -> Prog
-addDef d p =
-  let mod = progModule p
-      mod' = insertDef mod $ DefAST d
-   in p{progModule = mod'}
-
--- | Add a type definition to the editable module
--- assumes the def has the correct name to go in the editable module
-addTypeDef :: ASTTypeDef -> Prog -> Prog
-addTypeDef t p =
-  let mod = progModule p
-      tydefs = moduleTypes mod
-      tydefs' = tydefs <> mkTypeDefMap [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.
@@ -353,6 +334,9 @@ data ProgError
   | IndexOutOfRange Int
   | -- | Cannot rename a module to the same name as some other module
     RenameModuleNameClash
+  | ModuleNotFound ModuleName
+  | -- | Cannot edit an imported module
+    ModuleReadonly ModuleName
   deriving (Eq, Show, Generic)
   deriving (FromJSON, ToJSON) via VJSON ProgError
 
@@ -413,11 +397,11 @@ handleQuestion = \case
       prog <- asks appProg
       focusNode prog defname nodeid
 
--- This only looks in the editable module, not in any imports
+-- This only looks in the editable modules, not in any imports
 focusNode :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either (Either ExprZ TypeZ) TypeZip)
-focusNode prog = focusNodeDefs $ moduleDefsQualified $ progModule prog
+focusNode prog = focusNodeDefs $ foldMap moduleDefsQualified $ progModules prog
 
--- This looks in the editable module and also in any imports
+-- This looks in the editable modules and also in any imports
 focusNodeImports :: MonadError ProgError m => Prog -> GVarName -> ID -> m (Either (Either ExprZ TypeZ) TypeZip)
 focusNodeImports prog = focusNodeDefs $ allDefs prog
 
@@ -482,53 +466,45 @@ handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxS
     Right nf -> EvalFullRespNormal nf
 
 -- | Handle a 'ProgAction'
--- These actions only affect the editable module
 -- The 'GVarName' argument is the currently-selected definition, which is
 -- provided for convenience: it is the same as the one in the progSelection.
 applyProgAction :: MonadEdit m => Prog -> Maybe GVarName -> ProgAction -> m Prog
 applyProgAction prog mdefName = \case
-  MoveToDef d -> case Map.lookup d (moduleDefsQualified $ progModule prog) of
-    Nothing -> throwError $ DefNotFound d
-    Just _ -> pure $ prog & #progSelection ?~ Selection d Nothing
-  DeleteDef d ->
-    case deleteDef (progModule prog) d of
+  MoveToDef d -> do
+    m <- lookupEditableModule (qualifiedModule d) prog
+    case Map.lookup d $ moduleDefsQualified m of
+      Nothing -> throwError $ DefNotFound d
+      Just _ -> pure $ prog & #progSelection ?~ Selection d Nothing
+  DeleteDef d -> editModuleCross (qualifiedModule d) prog $ \(m, ms) ->
+    case deleteDef m d of
       Nothing -> throwError $ DefNotFound d
       Just mod' -> do
-        let 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.
         void . liftError (const $ DefInUse d) $
           checkEverything @TypeError
             NoSmartHoles
-            CheckEverything{trusted = progImports prog, toCheck = [mod']}
-        pure prog'
-  RenameDef d nameStr -> case lookupASTDef d (moduleDefsQualified $ progModule prog) of
-    Nothing -> throwError $ DefNotFound d
-    Just def -> do
-      let defs = moduleDefs $ progModule prog
-          oldNameBase = baseName d
-          newNameBase = unsafeMkName nameStr
-          newName = qualifyName (moduleName $ progModule prog) newNameBase
-      if Map.member newNameBase defs
-        then throwError $ DefAlreadyExists newName
-        else do
-          let def' = DefAST def{astDefName = newName}
-          defs' <-
-            maybe (throwError $ ActionError NameCapture) pure $
-              traverse
-                ( traverseOf (#_DefAST % #astDefExpr) $
-                    renameVar (GlobalVarRef d) (GlobalVarRef newName)
-                )
-                (Map.insert newNameBase def' $ Map.delete oldNameBase defs)
-          let prog' =
-                prog
-                  & #progSelection ?~ Selection (defName def') Nothing
-                  & #progModule % #moduleDefs .~ defs'
-          pure prog'
-  CreateDef n -> do
-    let mod = progModule prog
-    let modName = moduleName mod
+            CheckEverything{trusted = progImports prog, toCheck = mod' : ms}
+        pure (mod' : ms, Nothing)
+  RenameDef d nameStr -> editModuleOfCross (Just d) prog $ \(m, ms) def -> do
+    let defs = moduleDefs m
+        oldNameBase = baseName d
+        newNameBase = unsafeMkName nameStr
+        newName = qualifyName (moduleName m) newNameBase
+    if Map.member newNameBase defs
+      then throwError $ DefAlreadyExists newName
+      else do
+        let def' = DefAST def{astDefName = newName}
+        let m' = m{moduleDefs = Map.insert newNameBase def' $ Map.delete oldNameBase defs}
+        renamedModules <-
+          maybe (throwError $ ActionError NameCapture) pure $
+            traverseOf
+              (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
+              (renameVar (GlobalVarRef d) (GlobalVarRef newName))
+              (m' : ms)
+        pure (renamedModules, Just $ Selection (defName def') Nothing)
+  CreateDef modName n -> editModule modName prog $ \mod -> do
     let defs = moduleDefs mod
     name <- case n of
       Just nameStr ->
@@ -541,14 +517,10 @@ applyProgAction prog mdefName = \case
     expr <- newExpr
     ty <- newType
     let def = ASTDef name expr ty
-    pure $ addDef def prog{progSelection = Just $ Selection name Nothing}
-  AddTypeDef td -> do
-    -- The frontend should never let this error happen,
-    -- so we just dump out a raw string for debugging/logging purposes
-    let m = moduleName $ progModule prog
-    unless (m == qualifiedModule (astTypeDefName td)) $
-      throwError $ TypeDefError $ "Cannot create a type definition with incorrect module name: expected " <> moduleNamePretty m
-    addTypeDef td prog
+    pure (insertDef mod $ DefAST def, Just $ Selection name Nothing)
+  AddTypeDef td -> editModuleSameSelection (qualifiedModule $ astTypeDefName td) prog $ \m -> do
+    let tydefs' = moduleTypes m <> mkTypeDefMap [TypeDefAST td]
+    m{moduleTypes = tydefs'}
       <$ liftError
         -- The frontend should never let this error case happen,
         -- so we just dump out a raw string for debugging/logging purposes
@@ -562,13 +534,10 @@ applyProgAction prog mdefName = \case
             (checkTypeDefs $ mkTypeDefMapQualified [TypeDefAST td])
             (buildTypingContextFromModules (progAllModules prog) NoSmartHoles)
         )
-  RenameType old (unsafeMkName -> nameRaw) -> do
-    traverseOf
-      #progModule
-      ( traverseOf #moduleTypes (updateType <=< pure . updateRefsInTypes)
-          <=< pure . over (#moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType)
-      )
-      prog
+  RenameType old (unsafeMkName -> nameRaw) -> editModuleSameSelectionCross (qualifiedModule old) prog $ \(m, ms) -> do
+    m' <- traverseOf #moduleTypes updateType m
+    let renamedInTypes = over (traversed % #moduleTypes) updateRefsInTypes $ m' : ms
+    pure $ over (traversed % #moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) renamedInTypes
     where
       new = qualifyName (qualifiedModule old) nameRaw
       updateType m = do
@@ -593,14 +562,11 @@ applyProgAction prog mdefName = \case
           #astDefExpr
           $ transform $ over typesInExpr $ transform $ over (#_TCon % _2) updateName
       updateName n = if n == old then new else n
-  RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) -> do
-    when (new `elem` allConNames prog) $ throwError $ ConAlreadyExists new
-    traverseOf
-      #progModule
-      ( updateType
-          <=< traverseOf #moduleDefs (pure . updateDefs)
-      )
-      prog
+  RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) ->
+    editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do
+      when (new `elem` allConNames prog) $ throwError $ ConAlreadyExists new
+      m' <- updateType m
+      pure $ over (mapped % #moduleDefs) updateDefs (m' : ms)
     where
       updateType =
         alterTypeDef
@@ -617,11 +583,8 @@ applyProgAction prog mdefName = \case
             over (#_Con % _2) updateName
               . over (#_Case % _3 % traversed % #_CaseBranch % _1) updateName
       updateName n = if n == old then new else n
-  RenameTypeParam type_ old (unsafeMkLocalName -> new) -> do
-    traverseOf
-      #progModule
-      updateType
-      prog
+  RenameTypeParam type_ old (unsafeMkLocalName -> new) ->
+    editModuleSameSelection (qualifiedModule type_) prog updateType
     where
       updateType =
         alterTypeDef
@@ -647,16 +610,14 @@ applyProgAction prog mdefName = \case
           )
           $ over _freeVarsTy $ \(_, v) -> TVar () $ updateName v
       updateName n = if n == old then new else n
-  AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) -> do
-    when (con `elem` allConNames prog) $ throwError $ ConAlreadyExists con
-    traverseOf
-      #progModule
-      ( traverseOf
-          (#moduleDefs % traversed % #_DefAST % #astDefExpr)
-          updateDefs
-          <=< updateType
-      )
-      prog
+  AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) ->
+    editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do
+      when (con `elem` allConNames prog) $ throwError $ ConAlreadyExists con
+      m' <- updateType m
+      traverseOf
+        (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
+        updateDefs
+        $ m' : ms
     where
       updateDefs = transformCaseBranches prog type_ $ \bs -> do
         m' <- DSL.meta
@@ -668,13 +629,10 @@ applyProgAction prog mdefName = \case
               (maybe (throwError $ IndexOutOfRange index) pure . insertAt index (ValCon con []))
           )
           type_
-  SetConFieldType type_ con index new -> do
-    traverseOf
-      #progModule
-      ( traverseOf #moduleDefs updateDefs
-          <=< updateType
-      )
-      prog
+  SetConFieldType type_ con index new ->
+    editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do
+      m' <- updateType m
+      traverseOf (traversed % #moduleDefs) updateDefs (m' : ms)
     where
       updateType =
         alterTypeDef
@@ -721,13 +679,10 @@ applyProgAction prog mdefName = \case
                   )
                   e
             else pure cb
-  AddConField type_ con index new -> do
-    traverseOf
-      #progModule
-      ( traverseOf #moduleDefs updateDefs
-          <=< updateType
-      )
-      prog
+  AddConField type_ con index new ->
+    editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do
+      m' <- updateType m
+      traverseOf (traversed % #moduleDefs) updateDefs (m' : ms)
     where
       updateType =
         alterTypeDef
@@ -768,54 +723,45 @@ applyProgAction prog mdefName = \case
               binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds
               pure $ CaseBranch vc binds' e
             else pure cb
-  BodyAction actions -> do
-    withDef mdefName prog $ \def -> do
-      let smartHoles = progSmartHoles prog
-      res <- applyActionsToBody smartHoles (progAllModules prog) def actions
-      case res of
-        Left err -> throwError $ ActionError err
-        Right (def', z) -> do
-          let meta = bimap (view (position @1) . target) (view _typeMetaLens . target) $ locToEither z
-              nodeId = either getID getID meta
-          let prog' =
-                addDef
-                  def'
-                  prog
-                    { progSelection =
-                        Just $
-                          Selection (astDefName def') $
-                            Just
-                              NodeSelection
-                                { nodeType = BodyNode
-                                , nodeId
-                                , meta
-                                }
+  BodyAction actions -> editModuleOf mdefName prog $ \m def -> do
+    let smartHoles = progSmartHoles prog
+    res <- applyActionsToBody smartHoles (progAllModules prog) def actions
+    case res of
+      Left err -> throwError $ ActionError err
+      Right (def', z) -> do
+        let meta = bimap (view (position @1) . target) (view _typeMetaLens . target) $ locToEither z
+            nodeId = either getID getID meta
+        pure
+          ( insertDef m (DefAST def')
+          , Just $
+              Selection (astDefName def') $
+                Just
+                  NodeSelection
+                    { nodeType = BodyNode
+                    , nodeId
+                    , meta
                     }
-          pure prog'
-  SigAction actions -> do
-    withDef mdefName prog $ \def -> do
-      let smartHoles = progSmartHoles prog
-      res <- applyActionsToTypeSig smartHoles (progImports prog) (progModule prog) def actions
-      case res of
-        Left err -> throwError $ ActionError err
-        Right (def', mod', zt) -> do
-          let node = target zt
-              meta = view _typeMetaLens node
-              nodeId = getID meta
-              prog' =
-                prog
-                  { progModule = mod'
-                  , progSelection =
-                      Just $
-                        Selection (astDefName def') $
-                          Just
-                            NodeSelection
-                              { nodeType = SigNode
-                              , nodeId
-                              , meta = Right meta
-                              }
-                  }
-           in pure prog'
+          )
+  SigAction actions -> editModuleOfCross mdefName prog $ \m def -> do
+    let smartHoles = progSmartHoles prog
+    res <- applyActionsToTypeSig smartHoles (progImports prog) m def actions
+    case res of
+      Left err -> throwError $ ActionError err
+      Right (def', mod', zt) -> do
+        let node = target zt
+            meta = view _typeMetaLens node
+            nodeId = getID meta
+         in pure
+              ( mod'
+              , Just $
+                  Selection (astDefName def') $
+                    Just
+                      NodeSelection
+                        { nodeType = SigNode
+                        , nodeId
+                        , meta = Right meta
+                        }
+              )
   SetSmartHoles smartHoles ->
     pure $ prog & #progSmartHoles .~ smartHoles
   CopyPasteSig fromIds setup -> case mdefName of
@@ -824,10 +770,12 @@ applyProgAction prog mdefName = \case
   CopyPasteBody fromIds setup -> case mdefName of
     Nothing -> throwError NoDefSelected
     Just i -> copyPasteBody prog fromIds i setup
-  RenameModule newName ->
+  RenameModule oldName newName -> do
+    -- Call editModuleSameSelection solely for checking that 'oldName'
+    -- is an editable module
+    _ <- editModuleSameSelection oldName prog pure
     let n = ModuleName $ unsafeMkName <$> newName
-        oldName = moduleName $ progModule prog
-        curMods = RM{imported = progImports prog, editable = progModule prog}
+        curMods = RM{imported = progImports prog, editable = progModules prog}
      in if n == oldName
           then pure prog
           else case renameModule oldName n curMods of
@@ -836,7 +784,7 @@ applyProgAction prog mdefName = \case
               if imported curMods == imported renamedMods
                 then
                   pure $
-                    prog & #progModule .~ editable renamedMods
+                    prog & #progModules .~ editable renamedMods
                       & #progSelection % _Just %~ renameModule' oldName n
                 else
                   throwError $
@@ -847,19 +795,100 @@ applyProgAction prog mdefName = \case
                       InternalFailure "RenameModule: imported modules were edited by renaming"
 
 -- Helper for RenameModule action
-data RenameMods a = RM {imported :: [a], editable :: a}
+data RenameMods a = RM {imported :: [a], editable :: [a]}
   deriving (Functor, Foldable, Traversable)
 
--- Look up the definition by its given Name, then run the given action with it
--- only looks in the editable module
-withDef :: MonadError ProgError m => Maybe GVarName -> Prog -> (ASTDef -> m a) -> m a
-withDef mdefName prog f =
-  case mdefName of
-    Nothing -> throwError NoDefSelected
-    Just defname -> do
-      case lookupASTDef defname (moduleDefsQualified $ progModule prog) of
-        Nothing -> throwError $ DefNotFound defname
-        Just def -> f def
+lookupEditableModule :: MonadError ProgError m => ModuleName -> Prog -> m Module
+lookupEditableModule n p =
+  lookupModule' n p >>= \case
+    Editable m -> pure m
+    Imported _ -> throwError $ ModuleReadonly n
+
+-- | Describes return type of successfully looking a module up in the program.
+-- We get the module and also whether it is imported or not.
+data ModuleLookup = Editable Module | Imported Module
+
+lookupModule' :: MonadError ProgError m => ModuleName -> Prog -> m ModuleLookup
+lookupModule' n p = case (find ((n ==) . moduleName) (progModules p), find ((n ==) . moduleName) (progImports p)) of
+  (Just m, _) -> pure $ Editable m
+  (Nothing, Just m) -> pure $ Imported m
+  (Nothing, Nothing) -> throwError $ ModuleNotFound n
+
+editModule ::
+  MonadError ProgError m =>
+  ModuleName ->
+  Prog ->
+  (Module -> m (Module, Maybe Selection)) ->
+  m Prog
+editModule n p f = do
+  m <- lookupEditableModule n p
+  (m', s) <- f m
+  pure $
+    p
+      { progModules = m' : filter ((/= n) . moduleName) (progModules p)
+      , progSelection = s
+      }
+
+-- A variant of 'editModule' for actions which can affect multiple modules
+editModuleCross ::
+  MonadError ProgError m =>
+  ModuleName ->
+  Prog ->
+  ((Module, [Module]) -> m ([Module], Maybe Selection)) ->
+  m Prog
+editModuleCross n p f = do
+  m <- lookupEditableModule n p
+  let otherModules = filter ((/= n) . moduleName) (progModules p)
+  (m', s) <- f (m, otherModules)
+  pure $
+    p
+      { progModules = m'
+      , progSelection = s
+      }
+
+editModuleSameSelection ::
+  MonadError ProgError m =>
+  ModuleName ->
+  Prog ->
+  (Module -> m Module) ->
+  m Prog
+editModuleSameSelection n p f = editModule n p (fmap (,progSelection p) . f)
+
+-- A variant of 'editModuleSameSelection' for actions which can affect multiple modules
+editModuleSameSelectionCross ::
+  MonadError ProgError m =>
+  ModuleName ->
+  Prog ->
+  ((Module, [Module]) -> m [Module]) ->
+  m Prog
+editModuleSameSelectionCross n p f = editModuleCross n p (fmap (,progSelection p) . f)
+
+editModuleOf ::
+  MonadError ProgError m =>
+  Maybe GVarName ->
+  Prog ->
+  (Module -> ASTDef -> m (Module, Maybe Selection)) ->
+  m Prog
+editModuleOf mdefName prog f = case mdefName of
+  Nothing -> throwError NoDefSelected
+  Just defname -> editModule (qualifiedModule defname) prog $ \m ->
+    case Map.lookup (baseName defname) (moduleDefs m) of
+      Just (DefAST def) -> f m def
+      _ -> throwError $ DefNotFound defname
+
+-- A variant of 'editModuleOf' for actions which can affect multiple modules
+editModuleOfCross ::
+  MonadError ProgError m =>
+  Maybe GVarName ->
+  Prog ->
+  ((Module, [Module]) -> ASTDef -> m ([Module], Maybe Selection)) ->
+  m Prog
+editModuleOfCross mdefName prog f = case mdefName of
+  Nothing -> throwError NoDefSelected
+  Just defname -> editModuleCross (qualifiedModule defname) prog $ \ms@(m, _) ->
+    case Map.lookup (baseName defname) (moduleDefs m) of
+      Just (DefAST def) -> f ms def
+      _ -> throwError $ DefNotFound defname
 
 -- | Undo the last block of actions.
 -- If there are no actions in the log we return the program unchanged.
@@ -981,12 +1010,13 @@ newEmptyProg =
       def = DefAST $ ASTDef (qualifyName (ModuleName $ "Main" :| []) "main") expr ty
    in Prog
         { progImports = mempty
-        , progModule =
-            Module
-              { moduleName = ModuleName $ "Main" :| []
-              , moduleTypes = mempty
-              , moduleDefs = Map.singleton (baseName $ defName def) def
-              }
+        , progModules =
+            [ Module
+                { moduleName = ModuleName $ "Main" :| []
+                , moduleTypes = mempty
+                , moduleDefs = Map.singleton (baseName $ defName def) def
+                }
+            ]
         , progSelection = Nothing
         , progSmartHoles = SmartHoles
         , progLog = Log []
@@ -1007,12 +1037,13 @@ newProg :: Prog
 newProg =
   newEmptyProg
     { progImports = [builtinModule, primitiveModule]
-    , progModule =
-        Module
-          { moduleName = ModuleName $ "Main" :| []
-          , moduleTypes = mempty
-          , moduleDefs = defaultDefs $ ModuleName $ "Main" :| []
-          }
+    , progModules =
+        [ Module
+            { moduleName = ModuleName $ "Main" :| []
+            , moduleTypes = mempty
+            , moduleDefs = defaultDefs $ ModuleName $ "Main" :| []
+            }
+        ]
     }
 
 -- Since IDs should be unique in a module, we record 'defaultDefsNextID'
@@ -1077,31 +1108,36 @@ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do
     Left (Right zt) -> pure $ Left zt
     Right zt -> pure $ Right zt
   let smartHoles = progSmartHoles p
-  -- We intentionally throw away any changes in doneSetup other than via 'tgt'
-  -- as these could be in other definitions referencing this one, due to
-  -- types changing. However, we are going to do a full tc pass anyway,
-  -- 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.
-  (oldDef, doneSetup) <- withDef (Just toDefName) p $ \def -> (def,) <$> applyActionsToTypeSig smartHoles (progImports p) (progModule p) def setup
-  tgt <- case doneSetup of
-    Left err -> throwError $ ActionError err
-    Right (_, _, tgt) -> pure $ focusOnlyType tgt
-  let sharedScope =
-        if fromDefName == toDefName -- optimization only
-          then getSharedScopeTy c $ Right tgt
-          else mempty
-  -- Delete unbound vars
-  let cTgt = either target target c
-      f (m, n) = if Set.member (unLocalName n) sharedScope then pure $ TVar m n else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing)
-  cScoped <- traverseOf _freeVarsTy f cTgt
-  freshCopy <- traverseOf (_typeMeta % _id) (const fresh) cScoped
-  pasted <- case target tgt of
-    TEmptyHole _ -> pure $ replace freshCopy tgt
-    _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
-  let newDef = oldDef{astDefType = fromZipper pasted}
-  let newSel = NodeSelection SigNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right)
-  let finalProg = addDef newDef p{progSelection = Just (Selection (astDefName newDef) $ Just newSel)}
+  finalProg <- editModuleOf (Just toDefName) p $ \mod oldDef -> do
+    let otherModules = filter ((/= moduleName mod) . moduleName) (progModules p)
+    -- We intentionally throw away any changes in doneSetup other than via 'tgt'
+    -- as these could be in other definitions referencing this one, due to
+    -- types changing. However, we are going to do a full tc pass anyway,
+    -- 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 <- applyActionsToTypeSig smartHoles (progImports p) (mod, otherModules) oldDef setup
+    tgt <- case doneSetup of
+      Left err -> throwError $ ActionError err
+      Right (_, _, tgt) -> pure $ focusOnlyType tgt
+    let sharedScope =
+          if fromDefName == toDefName -- optimization only
+            then getSharedScopeTy c $ Right tgt
+            else mempty
+    -- Delete unbound vars
+    let cTgt = either target target c
+        f (m, n) =
+          if Set.member (unLocalName n) sharedScope
+            then pure $ TVar m n
+            else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing)
+    cScoped <- traverseOf _freeVarsTy f cTgt
+    freshCopy <- traverseOf (_typeMeta % _id) (const fresh) cScoped
+    pasted <- case target tgt of
+      TEmptyHole _ -> pure $ replace freshCopy tgt
+      _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
+    let newDef = oldDef{astDefType = fromZipper pasted}
+    let newSel = NodeSelection SigNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right)
+    pure (insertDef mod (DefAST newDef), Just (Selection (astDefName newDef) $ Just newSel))
   tcWholeProg finalProg
 
 -- We cannot use bindersAbove as that works on names only, and different scopes
@@ -1159,15 +1195,20 @@ 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.
+-- | Checks every term and type definition in the editable modules.
+-- Does not check imported modules.
 tcWholeProg :: forall m. MonadEdit m => Prog -> m Prog
 tcWholeProg p =
   let tc :: ReaderT Cxt (ExceptT ActionError m) Prog
       tc = do
-        defs' <- mapM checkDef (moduleDefs $ progModule p)
-        let mod' = (progModule p){moduleDefs = defs'}
-        let p' = p{progModule = mod'}
+        mods' <-
+          checkEverything
+            (progSmartHoles p)
+            CheckEverything
+              { trusted = progImports p
+              , toCheck = progModules p
+              }
+        let p' = p{progModules = mods'}
         -- We need to update the metadata cached in the selection
         let oldSel = progSelection p
         newSel <- case oldSel of
@@ -1200,85 +1241,96 @@ copyPasteBody p (fromDefName, fromId) toDefName setup = do
         Left (Right t) -> Right (Left t)
         Right t -> Right (Right t)
   let smartHoles = progSmartHoles p
-  -- The Loc zipper captures all the changes, they are only reflected in the
-  -- returned Def, which we thus ignore
-  (oldDef, doneSetup) <- withDef (Just toDefName) p $ \def -> (def,) <$> applyActionsToBody smartHoles (progAllModules p) def setup
-  tgt <- case doneSetup of
-    Left err -> throwError $ ActionError err
-    Right (_, tgt) -> pure tgt
-  case (src, tgt) of
-    (_, InBind _) -> throwError $ CopyPasteError "tried to paste an expression into a binder"
-    (Left _, InType _) -> throwError $ CopyPasteError "tried to paste an expression into a type"
-    (Right _, InExpr _) -> throwError $ CopyPasteError "tried to paste a type into an expression"
-    (Right srcT, InType tgtT) -> do
-      let sharedScope =
-            if fromDefName == toDefName -- optimization only
-              then getSharedScopeTy srcT $ Left tgtT
-              else mempty
-      -- Delete unbound vars. TODO: we may want to let-bind them?
-      let srcSubtree = either target target srcT
-          f (m, n) = if Set.member (unLocalName n) sharedScope then pure $ TVar m n else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing)
-      scopedCopy <- traverseOf _freeVarsTy f srcSubtree
-      freshCopy <- traverseOf (_typeMeta % _id) (const fresh) scopedCopy
-      pasted <- case target tgtT of
-        TEmptyHole _ -> pure $ replace freshCopy tgtT
-        _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
-      let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted}
-      let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right)
-      let finalProg = addDef newDef p{progSelection = Just (Selection (astDefName newDef) $ Just newSel)}
-      tcWholeProg finalProg
-    (Left srcE, InExpr tgtE) -> do
-      let sharedScope =
-            if fromDefName == toDefName -- optimization only
-              then getSharedScope srcE tgtE
-              else mempty
-      -- Delete unbound vars. TODO: we may want to let-bind them?
-      let tm (m, n) = if Set.member (unLocalName n) sharedScope then pure $ Var m $ LocalVarRef n else fresh <&> \i -> EmptyHole (Meta i Nothing Nothing)
-          ty (m, n) = if Set.member (unLocalName n) sharedScope then pure $ TVar m n else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing)
-      scopedCopy <- traverseOf _freeTyVars ty =<< traverseOf _freeTmVars tm (target srcE)
-      freshCopy <- traverseOf (_exprTypeMeta % _id) (const fresh) =<< traverseOf (_exprMeta % _id) (const fresh) scopedCopy
-      -- TODO: need to care about types and directions here (and write tests for this caring!)
-      {-
-      - Currently, with smart holes, nothing will go too wrong (i.e. no crashes/rejections happen), but if
-      - smartholes were turned off (which currently needs changing in the source code, then things could go wrong, and the TC throws errors.
-      - The cases we need to consider are (note that the metadata gives us what type each subtree was chk/syn (could be Nothing, due to our
-      - represention, but we can consider that as a hole)
-      - NB: as we always paste into a hole, it will always synth ?, but it may also have been checked against a concrete type
-      - From    To    Want
-      - e ∈ T   ∈ ?   e       if T is ? (or maybe don't special-case this, for consistency?)
-      -               {? e ?} otherwise, to avoid "jumpy holes" (paste a 2∈Nat into '? True', would get '2 {? True ?}', but want '{? 2 ?} True', probably?
-      - T ∋ t   ∈ ?   t : ?       if T is ? (or maybe don't special-case this, for consistency?)
-      -               {? t : T ?} otherwise (avoid jumpy holes, as above)
-      - e ∈ T   R ∋   e       if this would TC (i.e. T and R are consistent)
-      -               {? e ?} otherwise
-      - T ∋ t   R ∋   t           if this would TC (i.e. if T is more specific than R, I expect)
-      -               {? t : T ?} otherwise
-      -
-      - Let's also tabulate what smartholes would give
-      -    From    To    Want                   SH gives               Example ('raise' the term in >e<)
-      -    e ∈ T   ∈ ?   e       if T is ?      e
-      -!!!               {? e ?} otherwise      e, and jumpy holes.    (? : ? -> Bool -> ?) >Succ< True
-      -    T ∋ t   ∈ ?   t : ?       if T is ?  t : ?                  ? >λx.?< ?
-      -!!!               {? t : T ?} otherwise  t : ?                  (? : (Bool -> Bool) -> ?) >λx.?< ?
-      -    e ∈ T   R ∋   e       if  would TC   e                      Bool ∋ not >not True< [using extra not so obv. syn, even if ctors are chk only]
-      -                  {? e ?} otherwise      {? e ?}                Bool ∋ >isEven< ?
-      -    T ∋ t   R ∋   t         if would TC  t                      Bool -> Bool ∋ (? : (Bool -> Bool) -> ?) >(λx.?)<
-      -!!!               {? t : T ?} otherwise  {? t : ? ?}            Bool ∋ (? : (Bool -> Bool) -> ?) >(λx.?)<
-      -
-      - We could also consider what to do with embeddings: R ∋ e ∈ T: what happens for
-      -     Bool ∋ even >(add 0 0)<   [use add so obv. syn, even if ctors are chk only]
-      - ?
-      -
-      - so with SH, we are almost doing well, except we have a case of jumpy holes, and some cases of losing type information,
-      - denoted by !!! above
-      -}
-      pasted <- case target tgtE of
-        EmptyHole _ -> pure $ replace freshCopy tgtE
-        _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
-      let newDef = oldDef{astDefExpr = unfocusExpr pasted}
-      let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _exprMetaLens % re _Left)
-      let finalProg = addDef newDef p{progSelection = Just (Selection (astDefName newDef) $ Just newSel)}
-      tcWholeProg finalProg
+  finalProg <- editModuleOf (Just toDefName) p $ \mod oldDef -> do
+    -- The Loc zipper captures all the changes, they are only reflected in the
+    -- returned Def, which we thus ignore
+    doneSetup <- applyActionsToBody smartHoles (progAllModules p) oldDef setup
+    tgt <- case doneSetup of
+      Left err -> throwError $ ActionError err
+      Right (_, tgt) -> pure tgt
+    case (src, tgt) of
+      (_, InBind _) -> throwError $ CopyPasteError "tried to paste an expression into a binder"
+      (Left _, InType _) -> throwError $ CopyPasteError "tried to paste an expression into a type"
+      (Right _, InExpr _) -> throwError $ CopyPasteError "tried to paste a type into an expression"
+      (Right srcT, InType tgtT) -> do
+        let sharedScope =
+              if fromDefName == toDefName -- optimization only
+                then getSharedScopeTy srcT $ Left tgtT
+                else mempty
+        -- Delete unbound vars. TODO: we may want to let-bind them?
+        let srcSubtree = either target target srcT
+            f (m, n) =
+              if Set.member (unLocalName n) sharedScope
+                then pure $ TVar m n
+                else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing)
+        scopedCopy <- traverseOf _freeVarsTy f srcSubtree
+        freshCopy <- traverseOf (_typeMeta % _id) (const fresh) scopedCopy
+        pasted <- case target tgtT of
+          TEmptyHole _ -> pure $ replace freshCopy tgtT
+          _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
+        let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted}
+        let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _typeMetaLens % re _Right)
+        pure (insertDef mod (DefAST newDef), Just (Selection (astDefName newDef) $ Just newSel))
+      (Left srcE, InExpr tgtE) -> do
+        let sharedScope =
+              if fromDefName == toDefName -- optimization only
+                then getSharedScope srcE tgtE
+                else mempty
+        -- Delete unbound vars. TODO: we may want to let-bind them?
+        let tm (m, n) =
+              if Set.member (unLocalName n) sharedScope
+                then pure $ Var m $ LocalVarRef n
+                else fresh <&> \i -> EmptyHole (Meta i Nothing Nothing)
+            ty (m, n) =
+              if Set.member (unLocalName n) sharedScope
+                then pure $ TVar m n
+                else fresh <&> \i -> TEmptyHole (Meta i Nothing Nothing)
+        scopedCopy <- traverseOf _freeTyVars ty =<< traverseOf _freeTmVars tm (target srcE)
+        freshCopy <-
+          traverseOf (_exprTypeMeta % _id) (const fresh)
+            =<< traverseOf (_exprMeta % _id) (const fresh) scopedCopy
+        -- TODO: need to care about types and directions here (and write tests for this caring!)
+        {-
+        - Currently, with smart holes, nothing will go too wrong (i.e. no crashes/rejections happen), but if
+        - smartholes were turned off (which currently needs changing in the source code, then things could go wrong, and the TC throws errors.
+        - The cases we need to consider are (note that the metadata gives us what type each subtree was chk/syn (could be Nothing, due to our
+        - represention, but we can consider that as a hole)
+        - NB: as we always paste into a hole, it will always synth ?, but it may also have been checked against a concrete type
+        - From    To    Want
+        - e ∈ T   ∈ ?   e       if T is ? (or maybe don't special-case this, for consistency?)
+        -               {? e ?} otherwise, to avoid "jumpy holes" (paste a 2∈Nat into '? True', would get '2 {? True ?}', but want '{? 2 ?} True', probably?
+        - T ∋ t   ∈ ?   t : ?       if T is ? (or maybe don't special-case this, for consistency?)
+        -               {? t : T ?} otherwise (avoid jumpy holes, as above)
+        - e ∈ T   R ∋   e       if this would TC (i.e. T and R are consistent)
+        -               {? e ?} otherwise
+        - T ∋ t   R ∋   t           if this would TC (i.e. if T is more specific than R, I expect)
+        -               {? t : T ?} otherwise
+        -
+        - Let's also tabulate what smartholes would give
+        -    From    To    Want                   SH gives               Example ('raise' the term in >e<)
+        -    e ∈ T   ∈ ?   e       if T is ?      e
+        -!!!               {? e ?} otherwise      e, and jumpy holes.    (? : ? -> Bool -> ?) >Succ< True
+        -    T ∋ t   ∈ ?   t : ?       if T is ?  t : ?                  ? >λx.?< ?
+        -!!!               {? t : T ?} otherwise  t : ?                  (? : (Bool -> Bool) -> ?) >λx.?< ?
+        -    e ∈ T   R ∋   e       if  would TC   e                      Bool ∋ not >not True< [using extra not so obv. syn, even if ctors are chk only]
+        -                  {? e ?} otherwise      {? e ?}                Bool ∋ >isEven< ?
+        -    T ∋ t   R ∋   t         if would TC  t                      Bool -> Bool ∋ (? : (Bool -> Bool) -> ?) >(λx.?)<
+        -!!!               {? t : T ?} otherwise  {? t : ? ?}            Bool ∋ (? : (Bool -> Bool) -> ?) >(λx.?)<
+        -
+        - We could also consider what to do with embeddings: R ∋ e ∈ T: what happens for
+        -     Bool ∋ even >(add 0 0)<   [use add so obv. syn, even if ctors are chk only]
+        - ?
+        -
+        - so with SH, we are almost doing well, except we have a case of jumpy holes, and some cases of losing type information,
+        - denoted by !!! above
+        -}
+        pasted <- case target tgtE of
+          EmptyHole _ -> pure $ replace freshCopy tgtE
+          _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
+        let newDef = oldDef{astDefExpr = unfocusExpr pasted}
+        let newSel = NodeSelection BodyNode (getID $ target pasted) (pasted ^. _target % _exprMetaLens % re _Left)
+        pure (insertDef mod (DefAST newDef), Just (Selection (astDefName newDef) $ Just newSel))
+  tcWholeProg finalProg
 
 lookupASTDef :: GVarName -> DefMap -> Maybe ASTDef
 lookupASTDef name = defAST <=< Map.lookup name
@@ -1337,7 +1389,8 @@ liftError f = runExceptT >=> either (throwError . f) pure
 allConNames :: Prog -> [ValConName]
 allConNames =
   toListOf $
-    #progModule
+    #progModules
+      % traversed
       % #moduleTypes
       % traversed
       % #_TypeDefAST
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index 50cafd414..c293ba200 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -13,7 +13,9 @@ import Optics
 import Primer.Action (
   Action (
     ConstructAnn,
+    ConstructApp,
     ConstructArrowL,
+    ConstructCase,
     ConstructLet,
     ConstructTCon,
     ConstructVar,
@@ -22,7 +24,7 @@ import Primer.Action (
     Move
   ),
   ActionError (ImportNameClash),
-  Movement (Branch, Child1, Child2),
+  Movement (Branch, Child1, Child2, Parent),
  )
 import Primer.App (
   App (..),
@@ -45,7 +47,21 @@ import Primer.App (
   progAllModules,
   tcWholeProg,
  )
-import Primer.Builtins (builtinModule, cCons, cJust, cMakePair, cNil, tBool, tList, tMaybe, tPair)
+import Primer.Builtins (
+  builtinModule,
+  cCons,
+  cJust,
+  cMakePair,
+  cNil,
+  cSucc,
+  cTrue,
+  cZero,
+  tBool,
+  tList,
+  tMaybe,
+  tNat,
+  tPair,
+ )
 import Primer.Core (
   ASTDef (..),
   ASTTypeDef (..),
@@ -67,6 +83,7 @@ import Primer.Core (
   ValConName,
   defAST,
   defName,
+  defType,
   getID,
   qualifyName,
   typeDefAST,
@@ -101,12 +118,13 @@ import Primer.Core.Utils (forgetIDs)
 import Primer.Module (Module (Module, moduleDefs, moduleName, moduleTypes), mkTypeDefMap, moduleDefsQualified, moduleTypesQualified)
 import Primer.Name
 import Primer.Primitives (primitiveGVar, primitiveModule, tChar)
-import Primer.Typecheck (TypeError (UnknownTypeConstructor))
+import Primer.Typecheck (SmartHoles (NoSmartHoles, SmartHoles), TypeError (UnknownTypeConstructor))
 import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@=?), (@?=))
 import TestM (TestM, evalTestM)
-import TestUtils (constructTCon)
+import TestUtils (constructCon, constructTCon)
 import qualified TestUtils
 import Tests.Typecheck (checkProgWellFormed)
+import Prelude (error)
 
 unit_empty_actions_only_change_the_log :: Assertion
 unit_empty_actions_only_change_the_log = progActionTest defaultEmptyProg [] $
@@ -130,19 +148,19 @@ unit_move_to_def_and_construct_let :: Assertion
 unit_move_to_def_and_construct_let =
   progActionTest defaultEmptyProg [moveToDef "other", BodyAction [ConstructLet (Just "x")]] $
     expectSuccess $ \prog prog' ->
-      case astDefExpr <$> lookupASTDef' "other" (moduleDefs $ progModule prog') of
+      case astDefExpr <$> lookupASTDef' "other" prog' of
         Just Let{} ->
           -- Check that main is unchanged
-          Map.lookup "main" (moduleDefs $ progModule prog') @?= Map.lookup "main" (moduleDefs $ progModule prog)
+          lookupDef' "main" prog' @?= lookupDef' "main" prog
         _ -> assertFailure "definition not found"
 
 unit_rename_def :: Assertion
 unit_rename_def =
   progActionTest defaultEmptyProg [renameDef "other" "foo"] $
     expectSuccess $ \_ prog' -> do
-      fmap defName (Map.lookup "other" (moduleDefs $ progModule prog')) @?= Nothing
-      fmap defName (Map.lookup "foo" (moduleDefs $ progModule prog')) @?= Just (gvn "foo")
-      fmap defName (Map.lookup "main" (moduleDefs $ progModule prog')) @?= Just (gvn "main")
+      fmap defName (lookupDef' "other" prog') @?= Nothing
+      fmap defName (lookupDef' "foo" prog') @?= Just (gvn "foo")
+      fmap defName (lookupDef' "main" prog') @?= Just (gvn "main")
 
 unit_rename_def_to_same_name_as_existing_def :: Assertion
 unit_rename_def_to_same_name_as_existing_def =
@@ -163,10 +181,10 @@ unit_rename_def_referenced =
     , renameDef "other" "foo"
     ]
     $ expectSuccess $ \_ prog' -> do
-      fmap defName (Map.lookup "other" (moduleDefs $ progModule prog')) @?= Nothing
-      fmap defName (Map.lookup "foo" (moduleDefs $ progModule prog')) @?= Just (gvn "foo")
-      fmap defName (Map.lookup "main" (moduleDefs $ progModule prog')) @?= Just (gvn "main")
-      fmap (set _exprMeta () . astDefExpr) (defAST =<< Map.lookup "main" (moduleDefs $ progModule prog')) @?= Just (Var () $ globalVarRef "foo")
+      fmap defName (lookupDef' "other" prog') @?= Nothing
+      fmap defName (lookupDef' "foo" prog') @?= Just (gvn "foo")
+      fmap defName (lookupDef' "main" prog') @?= Just (gvn "main")
+      fmap (set _exprMeta () . astDefExpr) (defAST =<< lookupDef' "main" prog') @?= Just (Var () $ globalVarRef "foo")
 
 unit_rename_def_recursive :: Assertion
 unit_rename_def_recursive =
@@ -177,16 +195,16 @@ unit_rename_def_recursive =
     , renameDef "main" "foo"
     ]
     $ expectSuccess $ \_ prog' -> do
-      fmap defName (Map.lookup "main" (moduleDefs $ progModule prog')) @?= Nothing
-      fmap defName (Map.lookup "foo" (moduleDefs $ progModule prog')) @?= Just (gvn "foo")
-      fmap (set _exprMeta () . astDefExpr) (defAST =<< Map.lookup "foo" (moduleDefs $ progModule prog')) @?= Just (Var () $ globalVarRef "foo")
+      fmap defName (lookupDef' "main" prog') @?= Nothing
+      fmap defName (lookupDef' "foo" prog') @?= Just (gvn "foo")
+      fmap (set _exprMeta () . astDefExpr) (defAST =<< lookupDef' "foo" prog') @?= Just (Var () $ globalVarRef "foo")
 
 unit_delete_def :: Assertion
 unit_delete_def =
   progActionTest defaultEmptyProg [deleteDef "other"] $
     expectSuccess $ \_ prog' -> do
-      fmap defName (Map.lookup "other" (moduleDefs $ progModule prog')) @?= Nothing
-      fmap defName (Map.lookup "main" (moduleDefs $ progModule prog')) @?= Just (gvn "main")
+      fmap defName (lookupDef' "other" prog') @?= Nothing
+      fmap defName (lookupDef' "main" prog') @?= Just (gvn "main")
 
 unit_delete_def_unknown_id :: Assertion
 unit_delete_def_unknown_id =
@@ -198,11 +216,35 @@ unit_delete_def_used_id =
   progActionTest defaultEmptyProg [moveToDef "main", BodyAction [ConstructVar $ globalVarRef "other"], deleteDef "other"] $
     expectError (@?= DefInUse (gvn "other"))
 
+unit_delete_def_used_id_cross_module :: Assertion
+unit_delete_def_used_id_cross_module =
+  progActionTest
+    prog
+    [moveToDef "main", BodyAction [ConstructVar $ GlobalVarRef $ qualifyM "foo"], DeleteDef $ qualifyM "foo"]
+    $ expectError (@?= DefInUse (qualifyM "foo"))
+  where
+    n = ModuleName ["Module2"]
+    qualifyM = qualifyName n
+    prog = do
+      p <- defaultEmptyProg
+      e <- emptyHole
+      t <- tEmptyHole
+      let m =
+            Module n mempty $
+              Map.singleton "foo" $
+                DefAST $
+                  ASTDef (qualifyM "foo") e t
+      pure $ p & #progModules %~ (m :)
+
 -- 'foo = foo' shouldn't count as "in use" and block deleting itself
 unit_delete_def_recursive :: Assertion
 unit_delete_def_recursive =
   progActionTest defaultEmptyProg [moveToDef "main", BodyAction [ConstructVar $ globalVarRef "main"], deleteDef "main"] $
-    expectSuccess $ \prog prog' -> Map.delete "main" (moduleDefs $ progModule prog) @?= moduleDefs (progModule prog')
+    expectSuccess $ \prog prog' ->
+      Map.delete
+        (qualifyName mainModuleName "main")
+        (foldMap moduleDefsQualified $ progModules prog)
+        @?= foldMap moduleDefsQualified (progModules prog')
 
 unit_move_to_unknown_def :: Assertion
 unit_move_to_unknown_def =
@@ -217,19 +259,37 @@ unit_construct_let_without_moving_to_def_first =
   progActionTest defaultEmptyProg [BodyAction [ConstructLet (Just "x")]] $ expectError (@?= NoDefSelected)
 
 unit_create_def :: Assertion
-unit_create_def = progActionTest defaultEmptyProg [CreateDef $ Just "newDef"] $
+unit_create_def = progActionTest defaultEmptyProg [CreateDef mainModuleName $ Just "newDef"] $
   expectSuccess $ \_ prog' -> do
-    case lookupASTDef' "newDef" (moduleDefs $ progModule prog') of
-      Nothing -> assertFailure $ show $ moduleDefs $ progModule prog'
+    case lookupASTDef' "newDef" prog' of
+      Nothing -> assertFailure $ show $ moduleDefs <$> progModules prog'
       Just def -> do
         astDefName def @?= gvn "newDef"
         astDefExpr def @?= EmptyHole (Meta 4 Nothing Nothing)
 
 unit_create_def_clash_prim :: Assertion
 unit_create_def_clash_prim =
-  progActionTest defaultFullProg [CreateDef $ Just "toUpper"] $
+  progActionTest defaultFullProg [CreateDef mainModuleName $ Just "toUpper"] $
     expectError (@?= DefAlreadyExists (gvn "toUpper"))
 
+unit_create_def_nonexistant_module :: Assertion
+unit_create_def_nonexistant_module =
+  let nonExistantModule = ModuleName ["NonExistantModule"]
+   in progActionTest defaultEmptyProg [CreateDef nonExistantModule $ Just "newDef"] $
+        expectError (@?= ModuleNotFound nonExistantModule)
+
+unit_create_def_imported_module :: Assertion
+unit_create_def_imported_module =
+  let builtins = ModuleName ["Builtins"]
+      test = do
+        importModules [builtinModule]
+        handleEditRequest [CreateDef builtins $ Just "newDef"]
+      a = newEmptyApp
+   in do
+        case fst $ runAppTestM (ID $ appIdCounter a) a test of
+          Left err -> err @?= ModuleReadonly builtins
+          Right _ -> assertFailure "Expected CreateDef to complain about module being read-only"
+
 unit_create_typedef :: Assertion
 unit_create_typedef =
   let lst =
@@ -252,11 +312,11 @@ unit_create_typedef =
    in progActionTest defaultEmptyProg [AddTypeDef lst, AddTypeDef tree] $
         expectSuccess $
           \_ prog' -> do
-            case Map.elems $ moduleTypes $ progModule prog' of
+            case Map.elems $ foldMap moduleTypes $ progModules prog' of
               [lst', tree'] -> do
                 TypeDefAST lst @=? lst'
                 TypeDefAST tree @=? tree'
-              _ -> assertFailure $ show $ moduleTypes $ progModule prog'
+              _ -> assertFailure $ show $ moduleTypes <$> progModules prog'
 
 -- "List" is unknown here
 unit_create_typedef_bad_1 :: Assertion
@@ -390,7 +450,7 @@ unit_create_typedef_8 =
           , astTypeDefNameHints = []
           }
    in progActionTest defaultEmptyProg [AddTypeDef td] $
-        expectSuccess $ \_ prog' -> Map.elems (moduleTypes (progModule prog')) @?= [TypeDefAST td]
+        expectSuccess $ \_ prog' -> Map.elems (foldMap moduleTypes (progModules prog')) @?= [TypeDefAST td]
 
 -- Allow clash between type name and constructor name across types
 unit_create_typedef_9 :: Assertion
@@ -410,13 +470,13 @@ unit_create_typedef_9 =
           , astTypeDefNameHints = []
           }
    in progActionTest defaultEmptyProg [AddTypeDef td1, AddTypeDef td2] $
-        expectSuccess $ \_ prog' -> Map.elems (moduleTypes (progModule prog')) @?= [TypeDefAST td2, TypeDefAST td1]
+        expectSuccess $ \_ prog' -> Map.elems (foldMap moduleTypes (progModules prog')) @?= [TypeDefAST td2, TypeDefAST td1]
 
 unit_construct_arrow_in_sig :: Assertion
 unit_construct_arrow_in_sig =
   progActionTest defaultEmptyProg [moveToDef "other", SigAction [ConstructArrowL, Move Child1]] $
     expectSuccess $ \_ prog' ->
-      case lookupASTDef' "other" (moduleDefs $ progModule prog') of
+      case lookupASTDef' "other" prog' of
         Just def ->
           -- Check that the signature is an arrow type
           case astDefType def of
@@ -447,7 +507,7 @@ unit_sigaction_creates_holes =
         ]
    in progActionTest defaultFullProg acts $
         expectSuccess $ \_ prog' ->
-          case lookupASTDef' "other" (moduleDefs $ progModule prog') of
+          case lookupASTDef' "other" prog' of
             Just def ->
               -- Check that the definition is a non-empty hole
               case astDefExpr def of
@@ -466,7 +526,7 @@ unit_copy_paste_duplicate = do
         blankDef <- ASTDef toDef <$> emptyHole <*> tEmptyHole
         pure
           ( newProg{progSelection = Nothing}
-              & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST mainDef), ("blank", DefAST blankDef)]
+              & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST mainDef), ("blank", DefAST blankDef)]
           , getID mainType
           , getID mainExpr
           , getID (astDefType blankDef)
@@ -480,12 +540,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 (moduleDefsQualified $ progModule tcp)
+      let src = lookupASTDef fromDef (foldMap moduleDefsQualified $ progModules tcp)
           clearIDs = set (_Just % _defIDs) 0
        in do
-            src @?= lookupASTDef fromDef (moduleDefsQualified $ progModule r)
-            assertBool "equal to toDef" $ src /= lookupASTDef' "blank" (moduleDefs $ progModule r)
-            clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' "blank" (moduleDefs $ progModule r))
+            src @?= lookupASTDef fromDef (foldMap moduleDefsQualified $ progModules r)
+            assertBool "equal to toDef" $ src /= lookupASTDef' "blank" r
+            clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' "blank" r)
 
 -- ∀a . (∀b,c . a -> b -> ∀d. c -> d)  -> ∀c. ?
 -- copy         ^------------------^
@@ -508,9 +568,9 @@ unit_copy_paste_type_scoping = do
         defInitial <- ASTDef mainName <$> emptyHole <*> skel tEmptyHole
         expected <- ASTDef mainName <$> emptyHole <*> skel (tvar "a" `tfun` tEmptyHole `tfun` tforall "d" KType (tEmptyHole `tfun` tvar "d"))
         pure
-          ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)]
+          ( newEmptyProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)]
           , getID toCopy
-          , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST expected)]
+          , newEmptyProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST expected)]
           )
   let a = newEmptyApp{appProg = pInitial}
       actions = [MoveToDef mainName, CopyPasteSig (mainName, srcID) [Move Child1, Move Child2, Move Child1]]
@@ -521,7 +581,7 @@ unit_copy_paste_type_scoping = 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 (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
+       in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected)
 
 -- ∀a b.a ~> ∀a.a
 unit_raise :: Assertion
@@ -533,9 +593,9 @@ unit_raise = do
         defInitial <- ASTDef mainName <$> emptyHole <*> tforall "a" KType (tforall "b" KType $ pure toCopy)
         expected <- ASTDef mainName <$> emptyHole <*> tforall "a" KType (tvar "a")
         pure
-          ( newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)]
+          ( newEmptyProg & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)]
           , getID toCopy
-          , newEmptyProg & #progModule % #moduleDefs .~ Map.fromList [(mainName', DefAST expected)]
+          , newEmptyProg & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST expected)]
           )
   let a = newEmptyApp{appProg = pInitial}
       actions = [MoveToDef mainName, CopyPasteSig (mainName, srcID) [Move Child1, Delete]]
@@ -546,7 +606,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 (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
+       in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules 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
@@ -575,9 +635,9 @@ unit_copy_paste_expr_1 = do
         defInitial <- ASTDef mainName <$> skel emptyHole <*> pure ty
         expected <- ASTDef mainName <$> skel (pure expectPasted) <*> pure ty
         pure
-          ( newProg & #progModule % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)]
+          ( newProg & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST defInitial)]
           , getID toCopy
-          , newProg & #progModule % #moduleDefs .~ Map.fromList [(mainName', DefAST expected)]
+          , newProg & #progModules % _head % #moduleDefs .~ Map.fromList [(mainName', DefAST expected)]
           )
   let a = newApp{appProg = pInitial}
       actions = [MoveToDef mainName, CopyPasteBody (mainName, srcID) [Move Child1, Move Child1, Move (Branch cNil)]]
@@ -588,7 +648,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 (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
+       in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected)
 
 unit_copy_paste_ann :: Assertion
 unit_copy_paste_ann = do
@@ -601,7 +661,7 @@ unit_copy_paste_ann = do
         mainDef <- ASTDef fromDef <$> emptyHole `ann` pure toCopy <*> tEmptyHole
         blankDef <- ASTDef toDef <$> emptyHole `ann` tEmptyHole <*> tEmptyHole
         pure
-          ( newProg{progSelection = Nothing} & #progModule % #moduleDefs .~ Map.fromList [(fromDef', DefAST mainDef), ("blank", DefAST blankDef)]
+          ( newProg{progSelection = Nothing} & #progModules % _head % #moduleDefs .~ Map.fromList [(fromDef', DefAST mainDef), ("blank", DefAST blankDef)]
           , getID toCopy
           )
   let a = newApp{appProg = p}
@@ -612,12 +672,12 @@ 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' (moduleDefs $ progModule tcp)
+      let src = lookupASTDef' fromDef' tcp
           clearIDs = set (_Just % _defIDs) 0
        in do
-            src @?= lookupASTDef' fromDef' (moduleDefs $ progModule r)
-            assertBool "equal to blank" $ src /= lookupASTDef' toDef' (moduleDefs $ progModule r)
-            clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' toDef' (moduleDefs $ progModule r))
+            src @?= lookupASTDef' fromDef' r
+            assertBool "equal to blank" $ src /= lookupASTDef' toDef' r
+            clearIDs (set (_Just % #astDefName) toDef src) @?= clearIDs (lookupASTDef' toDef' r)
 
 unit_copy_paste_ann2sig :: Assertion
 unit_copy_paste_ann2sig = do
@@ -626,9 +686,9 @@ unit_copy_paste_ann2sig = do
         defInitial <- astDef "main" <$> emptyHole `ann` pure toCopy <*> tEmptyHole
         expected <- astDef "main" <$> emptyHole `ann` pure toCopy <*> tcon tBool
         pure
-          ( newProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)]
+          ( newProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)]
           , getID toCopy
-          , newProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST expected)]
+          , newProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST expected)]
           )
   let a = newApp{appProg = pInitial}
       actions = [moveToDef "main", copyPasteSig ("main", srcID) []]
@@ -639,7 +699,7 @@ 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 (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
+       in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected)
 
 unit_copy_paste_sig2ann :: Assertion
 unit_copy_paste_sig2ann = do
@@ -648,9 +708,9 @@ unit_copy_paste_sig2ann = do
         defInitial <- astDef "main" <$> emptyHole <*> pure toCopy
         expected <- astDef "main" <$> emptyHole `ann` tcon tBool <*> pure toCopy
         pure
-          ( newProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)]
+          ( newProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST defInitial)]
           , getID toCopy
-          , newProg & #progModule % #moduleDefs .~ Map.fromList [("main", DefAST expected)]
+          , newProg & #progModules % _head % #moduleDefs .~ Map.fromList [("main", DefAST expected)]
           )
   let a = newApp{appProg = pInitial}
       actions = [moveToDef "main", copyPasteBody ("main", srcID) [ConstructAnn, EnterType]]
@@ -661,15 +721,15 @@ 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 (moduleDefs $ progModule r) @?= clearIDs (moduleDefs $ progModule tcpExpected)
+       in clearIDs (foldMap moduleDefsQualified $ progModules r) @?= clearIDs (foldMap moduleDefsQualified $ progModules tcpExpected)
 
 -- VariablesInScope sees imported terms
 unit_import_vars :: Assertion
 unit_import_vars =
   let test = do
         importModules [builtinModule, primitiveModule]
-        gets (Map.assocs . moduleDefsQualified . progModule . appProg) >>= \case
-          [(i, DefAST d)] -> do
+        gets (fmap (Map.assocs . moduleDefsQualified) . progModules . appProg) >>= \case
+          [[(i, DefAST d)]] -> do
             a' <- get
             (_, vs) <- runReaderT (handleQuestion (VariablesInScope i $ getID $ astDefExpr d)) a'
             pure $
@@ -687,8 +747,8 @@ unit_import_reference =
   let test = do
         importModules [builtinModule, primitiveModule]
         prog <- gets appProg
-        case (findGlobalByName prog $ primitiveGVar "toUpper", Map.assocs $ moduleDefsQualified $ progModule prog) of
-          (Just toUpperDef, [(i, _)]) -> do
+        case (findGlobalByName prog $ primitiveGVar "toUpper", Map.assocs . moduleDefsQualified <$> progModules prog) of
+          (Just toUpperDef, [[(i, _)]]) -> do
             _ <-
               handleEditRequest
                 [ MoveToDef i
@@ -738,8 +798,8 @@ unit_copy_paste_import =
                 }
         importModules [m]
         prog <- gets appProg
-        case (findGlobalByName prog $ TestUtils.gvn ["M"] "foo", Map.assocs $ moduleDefsQualified $ progModule prog) of
-          (Just (DefAST fooDef), [(i, _)]) -> do
+        case (findGlobalByName prog $ TestUtils.gvn ["M"] "foo", Map.assocs . moduleDefsQualified <$> progModules prog) of
+          (Just (DefAST fooDef), [[(i, _)]]) -> do
             let fromDef = astDefName fooDef
                 fromType = getID $ astDefType fooDef
                 fromExpr = getID $ astDefExpr fooDef
@@ -1140,8 +1200,8 @@ unit_generate_names_import :: Assertion
 unit_generate_names_import =
   let test = do
         importModules [builtinModule]
-        gets (Map.assocs . moduleDefsQualified . progModule . appProg) >>= \case
-          [(i, DefAST d)] -> do
+        gets (fmap (Map.assocs . moduleDefsQualified) . progModules . appProg) >>= \case
+          [[(i, DefAST d)]] -> do
             a' <- get
             ns <-
               runReaderT
@@ -1180,7 +1240,8 @@ defaultEmptyProg = do
                       , meta = Left (Meta 1 Nothing Nothing)
                       }
           }
-          & #progModule
+          & #progModules
+          % _head
           % #moduleDefs
           .~ Map.fromList [(astDefBaseName mainDef, DefAST mainDef), (astDefBaseName otherDef, DefAST otherDef)]
 
@@ -1188,7 +1249,7 @@ unit_good_defaultEmptyProg :: Assertion
 unit_good_defaultEmptyProg = checkProgWellFormed defaultEmptyProg
 
 -- `defaultEmptyProg`, plus all primitive definitions (types and terms)
--- and all builtin types, all moved into the editable module
+-- and all builtin types, all moved into an editable module
 -- NB: this means that primitive constructors are unusable, since they
 -- will not typecheck (we now have only a "Main.Char" type, not a
 -- "Primitive.Char" type), but we can now test our error handling for
@@ -1196,7 +1257,7 @@ unit_good_defaultEmptyProg = checkProgWellFormed defaultEmptyProg
 defaultFullProg :: MonadFresh ID m => m Prog
 defaultFullProg = do
   p <- defaultEmptyProg
-  let m = moduleName $ progModule p
+  let m = moduleName $ unsafeHead $ progModules p
       -- We need to move the primitives, which requires renaming
       -- unit_defaultFullModule_no_clash ensures that there will be no clashes
       renamed :: [Module]
@@ -1204,14 +1265,14 @@ defaultFullProg = do
       renamedTypes = renamed ^.. folded % #moduleTypes % folded
       renamedDefs = foldOf (folded % #moduleDefs) renamed
   pure $
-    p & #progModule % #moduleTypes %~ (mkTypeDefMap renamedTypes <>)
-      & #progModule % #moduleDefs %~ (renamedDefs <>)
+    p & #progModules % _head % #moduleTypes %~ (mkTypeDefMap renamedTypes <>)
+      & #progModules % _head % #moduleDefs %~ (renamedDefs <>)
 
 findTypeDef :: TyConName -> Prog -> IO ASTTypeDef
-findTypeDef d p = maybe (assertFailure "couldn't find typedef") pure $ (typeDefAST <=< Map.lookup d) $ p ^. (#progModule % to moduleTypesQualified)
+findTypeDef d p = maybe (assertFailure "couldn't find typedef") pure $ (typeDefAST <=< Map.lookup d) $ foldMap moduleTypesQualified $ progModules p
 
 findDef :: GVarName -> Prog -> IO ASTDef
-findDef d p = maybe (assertFailure "couldn't find def") pure $ (defAST <=< Map.lookup d) $ p ^. (#progModule % to moduleDefsQualified)
+findDef d p = maybe (assertFailure "couldn't find def") pure $ (defAST <=< Map.lookup d) $ foldMap moduleDefsQualified $ progModules p
 
 -- We use the same type definition for all tests related to editing type definitions
 -- (This is added to `defaultFullProg`)
@@ -1231,8 +1292,8 @@ defaultProgEditableTypeDefs ds = do
         ]
   pure $
     p
-      & (#progModule % #moduleTypes) %~ (mkTypeDefMap tds <>)
-      & (#progModule % #moduleDefs) %~ (Map.fromList ((\d -> (baseName $ astDefName d, DefAST d)) <$> ds') <>)
+      & (#progModules % _head % #moduleTypes) %~ (mkTypeDefMap tds <>)
+      & (#progModules % _head % #moduleDefs) %~ (Map.fromList ((\d -> (baseName $ astDefName d, DefAST d)) <$> ds') <>)
 
 tT :: TyConName
 tT = tcn "T"
@@ -1250,7 +1311,7 @@ unit_good_defaultFullProg = checkProgWellFormed defaultFullProg
 unit_defaultFullProg_no_clash :: Assertion
 unit_defaultFullProg_no_clash =
   let (p, _) = create defaultEmptyProg
-      ms = progModule p : [builtinModule, primitiveModule]
+      ms = progModules p <> [builtinModule, primitiveModule]
       typeNames = ms ^.. folded % #moduleTypes % folded % to typeDefName % #baseName
       termNames = ms ^.. folded % #moduleDefs % to Map.keys % folded
    in do
@@ -1265,16 +1326,16 @@ unit_rename_module =
         handleEditRequest
           [ moveToDef "main"
           , BodyAction [ConstructVar $ globalVarRef "main"]
-          , RenameModule ["Module2"]
+          , RenameModule mainModuleName ["Module2"]
           ]
       a = newEmptyApp
    in case fst $ runAppTestM (ID $ appIdCounter a) a test of
         Left err -> assertFailure $ show err
         Right p -> do
-          unModuleName (moduleName $ progModule p) @?= ["Module2"]
+          fmap (unModuleName . moduleName) (progModules p) @?= [["Module2"]]
           selectedDef <$> progSelection p @?= Just (qualifyName (ModuleName ["Module2"]) "main")
-          case Map.elems (moduleDefs $ progModule p) of
-            [DefAST d] -> do
+          case fmap (Map.elems . moduleDefsQualified) (progModules p) of
+            [[DefAST d]] -> do
               let expectedName = qualifyName (ModuleName ["Module2"]) "main"
               astDefName d @?= expectedName
               case astDefExpr d of
@@ -1286,7 +1347,7 @@ unit_rename_module_clash :: Assertion
 unit_rename_module_clash =
   let test = do
         importModules [builtinModule]
-        handleEditRequest [RenameModule ["Builtins"]]
+        handleEditRequest [RenameModule mainModuleName ["Builtins"]]
       a = newEmptyApp
    in do
         unModuleName (moduleName builtinModule) @?= ["Builtins"]
@@ -1294,6 +1355,152 @@ unit_rename_module_clash =
           Left err -> err @?= RenameModuleNameClash
           Right _ -> assertFailure "Expected RenameModule to error, since module names clash with prior import"
 
+unit_rename_module_nonexistant :: Assertion
+unit_rename_module_nonexistant =
+  let nonExistantModule = ModuleName ["NonExistantModule"]
+   in progActionTest defaultEmptyProg [RenameModule nonExistantModule ["Builtins"]] $
+        expectError (@?= ModuleNotFound nonExistantModule)
+
+unit_rename_module_imported :: Assertion
+unit_rename_module_imported =
+  let builtins = ModuleName ["Builtins"]
+      test = do
+        importModules [builtinModule]
+        handleEditRequest [RenameModule builtins ["NewModule"]]
+      a = newEmptyApp
+   in do
+        case fst $ runAppTestM (ID $ appIdCounter a) a test of
+          Left err -> err @?= ModuleReadonly builtins
+          Right _ -> assertFailure "Expected RenameModule to complain about module being read-only"
+
+-- test actions update multiple modules where appropriate
+unit_cross_module_actions :: Assertion
+unit_cross_module_actions =
+  let test = do
+        importModules [builtinModule]
+        -- Setup: define Main.main :: T = case foo (C Zero) of {C p -> C (Succ p)}
+        handleAndTC
+          [ MoveToDef $ gvn "main"
+          , SigAction [constructTCon (qualifyM "T")]
+          , BodyAction
+              [ ConstructApp
+              , Move Child1
+              , ConstructVar (GlobalVarRef $ qualifyM "foo")
+              , Move Parent
+              , Move Child2
+              , ConstructApp
+              , Move Child1
+              , constructCon (qualifyM "C")
+              , Move Parent
+              , Move Child2
+              , constructCon cZero
+              , Move Parent
+              , Move Parent
+              , ConstructCase
+              , Move (Branch (qualifyM "C"))
+              , ConstructApp
+              , Move Child1
+              , constructCon (qualifyM "C")
+              , Move Parent
+              , Move Child2
+              , ConstructApp
+              , Move Child1
+              , constructCon cSucc
+              , Move Parent
+              , Move Child2
+              , ConstructVar (LocalVarRef "a26")
+              ]
+          ]
+        handleAndTC [RenameDef (qualifyM "foo") "bar"]
+        handleAndTC [RenameType (qualifyM "T") "R"]
+        handleAndTC [RenameCon (qualifyM "R") (qualifyM "C") "D"]
+        handleAndTC [AddCon (qualifyM "R") 1 "X"]
+        handleAndTC [SetConFieldType (qualifyM "R") (qualifyM "D") 0 (TCon () tBool)]
+        handleAndTC [AddConField (qualifyM "R") (qualifyM "D") 0 (TCon () tNat)]
+        handleAndTC [RenameModule (moduleName m) ["AnotherModule"]]
+        -- NB: SigAction relies on SmartHoles to fix any introduced inconsistencies
+        oldSH <- gets (progSmartHoles . appProg)
+        handleAndTC
+          [ SetSmartHoles SmartHoles
+          , MoveToDef $ qualifyName (ModuleName ["AnotherModule"]) "bar"
+          , SigAction
+              [ Move Child1
+              , Delete
+              , constructTCon tBool
+              , Move Parent
+              , Move Child2
+              , Delete
+              ]
+          , SetSmartHoles oldSH
+          ]
+        -- A bit of setup to test CopyPasteSig: main :: Nat = bar True (Note bar :: Bool -> ?)
+        handleAndTC
+          [ MoveToDef $ gvn "main"
+          , SigAction [Delete, constructTCon tNat]
+          , BodyAction
+              [ Delete
+              , ConstructApp
+              , Move Child1
+              , ConstructVar $ GlobalVarRef $ qualifyName (ModuleName ["AnotherModule"]) "bar"
+              , Move Parent
+              , Move Child2
+              , constructCon cTrue
+              ]
+          ]
+        -- Copy-paste within the sig of bar to make bar :: Bool -> Bool
+        -- NB: CopyPasteSig relies on SmartHoles to fix any introduced inconsistencies
+        barTy <-
+          gets $
+            fmap defType . flip findGlobalByName (qualifyName (ModuleName ["AnotherModule"]) "bar")
+              . appProg
+        let srcId = case barTy of
+              Just (TFun _ src _) -> getID src
+              _ -> error "Unexpected shape of 'barTy'"
+        handleAndTC
+          [ SetSmartHoles SmartHoles
+          , MoveToDef $ qualifyName (ModuleName ["AnotherModule"]) "bar"
+          , CopyPasteSig
+              (qualifyName (ModuleName ["AnotherModule"]) "bar", srcId)
+              [Move Child2]
+          , SetSmartHoles oldSH
+          ]
+        gets appProg
+      handleAndTC acts = void $ tcWholeProg =<< handleEditRequest acts
+      n = ["Module2"]
+      qualifyM :: Name -> GlobalName k
+      qualifyM = qualifyName $ moduleName m
+      m = fst $
+        create $ do
+          let ty =
+                ASTTypeDef
+                  { astTypeDefName = qualifyM "T"
+                  , astTypeDefParameters = []
+                  , astTypeDefConstructors = [ValCon (qualifyM "C") [TCon () tNat]]
+                  , astTypeDefNameHints = []
+                  }
+          defTy <- tcon (astTypeDefName ty) `tfun` tcon (astTypeDefName ty)
+          defExpr <- emptyHole
+          let def =
+                ASTDef
+                  { astDefName = qualifyM "foo"
+                  , astDefType = defTy
+                  , astDefExpr = defExpr
+                  }
+          pure
+            Module
+              { moduleName = ModuleName n
+              , moduleTypes = Map.singleton "T" (TypeDefAST ty)
+              , moduleDefs = Map.singleton "foo" (DefAST def)
+              }
+      -- We turn off smartholes, as we want to test our actions work without it
+      a =
+        newEmptyApp & #appProg % #progModules %~ (m :)
+          & #appProg % #progSmartHoles .~ NoSmartHoles
+   in do
+        case fst $ runAppTestM (ID $ appIdCounter a) a test of
+          Left err -> assertFailure $ show err
+          Right _ -> pure ()
+
 _defIDs :: Traversal' ASTDef ID
 _defIDs = #astDefExpr % (_exprMeta % _id `adjoin` _exprTypeMeta % _id) `adjoin` #astDefType % _typeMeta % _id
 
@@ -1333,18 +1540,23 @@ runAppTestM startID a m =
     Left err -> (Left err, a)
     Right (res, app') -> (Right res, app')
 
--- Looks up a definition, ignoring any module prefix
+-- Looks up a definition in the main module
 -- Useful in these tests so we don't have to specify
 -- the name of the module all the time
-lookupASTDef' :: Name -> Map Name Def -> Maybe ASTDef
-lookupASTDef' name = defAST <=< Map.lookup name
+lookupDef' :: Name -> Prog -> Maybe Def
+lookupDef' = flip findGlobalByName . qualifyName mainModuleName
+
+lookupASTDef' :: Name -> Prog -> Maybe ASTDef
+lookupASTDef' name = defAST <=< lookupDef' name
 
 astDefBaseName :: ASTDef -> Name
 astDefBaseName = baseName . astDefName
 
--- Some helpers to run actions on the current module
+-- Some helpers to run actions on the "main" module
 mainModuleName :: ModuleName
-mainModuleName = moduleName $ progModule newEmptyProg
+mainModuleName = case progModules newEmptyProg of
+  [m] -> moduleName m
+  _ -> error "expected exactly one module in newEmptyProg"
 
 mainModuleNameText :: NonEmpty Text
 mainModuleNameText = unName <$> unModuleName mainModuleName
diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs
index 1ed56b51b..5720376cf 100644
--- a/primer/test/Tests/Serialization.hs
+++ b/primer/test/Tests/Serialization.hs
@@ -129,12 +129,13 @@ fixtures =
       prog =
         Prog
           { progImports = mempty
-          , progModule =
-              Module
-                { moduleName = ModuleName ["M"]
-                , moduleTypes = mkTypeDefMap [typeDef]
-                , moduleDefs = Map.singleton (baseName $ astDefName def) (DefAST def)
-                }
+          , progModules =
+              [ Module
+                  { moduleName = ModuleName ["M"]
+                  , moduleTypes = mkTypeDefMap [typeDef]
+                  , moduleDefs = Map.singleton (baseName $ astDefName def) (DefAST def)
+                  }
+              ]
           , progSelection = Just selection
           , progSmartHoles = SmartHoles
           , progLog = log
diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs
index b441ad0bf..4a39a6885 100644
--- a/primer/test/Tests/Typecheck.hs
+++ b/primer/test/Tests/Typecheck.hs
@@ -26,7 +26,7 @@ import Primer.App (
   newEmptyProg,
   newProg,
   progAllModules,
-  progModule,
+  progModules,
  )
 import Primer.Builtins (
   boolDef,
@@ -549,7 +549,7 @@ unit_bad_prim_map_base = case runTypecheckTestM NoSmartHoles $ do
   checkEverything
     NoSmartHoles
     CheckEverything
-      { trusted = [progModule newProg]
+      { trusted = progModules newProg
       , toCheck = [Module (ModuleName ["M"]) mempty $ Map.singleton "foo" $ DefPrim foo]
       } of
   Left err -> err @?= InternalError "Inconsistant names in moduleDefs map for module M"
@@ -562,7 +562,7 @@ unit_bad_prim_map_module = case runTypecheckTestM NoSmartHoles $ do
   checkEverything
     NoSmartHoles
     CheckEverything
-      { trusted = [progModule newProg]
+      { trusted = progModules newProg
       , toCheck = [Module (ModuleName ["M"]) mempty $ Map.singleton "foo" $ DefPrim foo]
       } of
   Left err -> err @?= InternalError "Inconsistant names in moduleDefs map for module M"
@@ -575,7 +575,7 @@ unit_bad_prim_type = case runTypecheckTestM NoSmartHoles $ do
   checkEverything
     NoSmartHoles
     CheckEverything
-      { trusted = [progModule newProg]
+      { trusted = progModules newProg
       , toCheck = [Module (ModuleName ["M"]) mempty $ Map.singleton "foo" $ DefPrim foo]
       } of
   Left err -> err @?= UnknownTypeConstructor (tcn ["M"] "NonExistant")
diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json
index bf346e651..bceb1b4a7 100644
--- a/primer/test/outputs/serialization/edit_response_2.json
+++ b/primer/test/outputs/serialization/edit_response_2.json
@@ -18,128 +18,130 @@
                 ]
             ]
         },
-        "progModule": {
-            "moduleDefs": {
-                "main": {
-                    "contents": {
-                        "astDefExpr": {
-                            "contents": [
-                                0,
-                                {
-                                    "contents": {
-                                        "contents": [],
-                                        "tag": "TEmptyHole"
-                                    },
-                                    "tag": "TCSynthed"
-                                },
-                                null
-                            ],
-                            "tag": "EmptyHole"
-                        },
-                        "astDefName": {
-                            "baseName": "main",
-                            "qualifiedModule": [
-                                "M"
-                            ]
-                        },
-                        "astDefType": {
-                            "contents": [
-                                0,
-                                {
-                                    "tag": "KType"
-                                },
-                                null
-                            ],
-                            "tag": "TEmptyHole"
-                        }
-                    },
-                    "tag": "DefAST"
-                }
-            },
-            "moduleName": [
-                "M"
-            ],
-            "moduleTypes": {
-                "T": {
-                    "contents": {
-                        "astTypeDefConstructors": [
-                            {
-                                "valConArgs": [
+        "progModules": [
+            {
+                "moduleDefs": {
+                    "main": {
+                        "contents": {
+                            "astDefExpr": {
+                                "contents": [
+                                    0,
                                     {
-                                        "contents": [
-                                            [],
-                                            {
-                                                "contents": [
-                                                    [],
-                                                    "b"
-                                                ],
-                                                "tag": "TVar"
-                                            },
-                                            {
-                                                "contents": [
-                                                    [],
-                                                    "a"
-                                                ],
-                                                "tag": "TVar"
-                                            }
-                                        ],
-                                        "tag": "TApp"
+                                        "contents": {
+                                            "contents": [],
+                                            "tag": "TEmptyHole"
+                                        },
+                                        "tag": "TCSynthed"
                                     },
+                                    null
+                                ],
+                                "tag": "EmptyHole"
+                            },
+                            "astDefName": {
+                                "baseName": "main",
+                                "qualifiedModule": [
+                                    "M"
+                                ]
+                            },
+                            "astDefType": {
+                                "contents": [
+                                    0,
                                     {
-                                        "contents": [
-                                            [],
-                                            {
-                                                "baseName": "Nat",
-                                                "qualifiedModule": [
-                                                    "Builtins"
-                                                ]
-                                            }
-                                        ],
-                                        "tag": "TCon"
-                                    }
+                                        "tag": "KType"
+                                    },
+                                    null
                                 ],
-                                "valConName": {
-                                    "baseName": "C",
-                                    "qualifiedModule": [
-                                        "M"
-                                    ]
-                                }
+                                "tag": "TEmptyHole"
                             }
-                        ],
-                        "astTypeDefName": {
-                            "baseName": "T",
-                            "qualifiedModule": [
-                                "M"
-                            ]
                         },
-                        "astTypeDefNameHints": [],
-                        "astTypeDefParameters": [
-                            [
-                                "a",
-                                {
-                                    "tag": "KType"
-                                }
-                            ],
-                            [
-                                "b",
+                        "tag": "DefAST"
+                    }
+                },
+                "moduleName": [
+                    "M"
+                ],
+                "moduleTypes": {
+                    "T": {
+                        "contents": {
+                            "astTypeDefConstructors": [
                                 {
-                                    "contents": [
+                                    "valConArgs": [
                                         {
-                                            "tag": "KType"
+                                            "contents": [
+                                                [],
+                                                {
+                                                    "contents": [
+                                                        [],
+                                                        "b"
+                                                    ],
+                                                    "tag": "TVar"
+                                                },
+                                                {
+                                                    "contents": [
+                                                        [],
+                                                        "a"
+                                                    ],
+                                                    "tag": "TVar"
+                                                }
+                                            ],
+                                            "tag": "TApp"
                                         },
                                         {
-                                            "tag": "KType"
+                                            "contents": [
+                                                [],
+                                                {
+                                                    "baseName": "Nat",
+                                                    "qualifiedModule": [
+                                                        "Builtins"
+                                                    ]
+                                                }
+                                            ],
+                                            "tag": "TCon"
                                         }
                                     ],
-                                    "tag": "KFun"
+                                    "valConName": {
+                                        "baseName": "C",
+                                        "qualifiedModule": [
+                                            "M"
+                                        ]
+                                    }
                                 }
+                            ],
+                            "astTypeDefName": {
+                                "baseName": "T",
+                                "qualifiedModule": [
+                                    "M"
+                                ]
+                            },
+                            "astTypeDefNameHints": [],
+                            "astTypeDefParameters": [
+                                [
+                                    "a",
+                                    {
+                                        "tag": "KType"
+                                    }
+                                ],
+                                [
+                                    "b",
+                                    {
+                                        "contents": [
+                                            {
+                                                "tag": "KType"
+                                            },
+                                            {
+                                                "tag": "KType"
+                                            }
+                                        ],
+                                        "tag": "KFun"
+                                    }
+                                ]
                             ]
-                        ]
-                    },
-                    "tag": "TypeDefAST"
+                        },
+                        "tag": "TypeDefAST"
+                    }
                 }
             }
-        },
+        ],
         "progSelection": {
             "selectedDef": {
                 "baseName": "main",
diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json
index c8d0188c9..c6ccbe444 100644
--- a/primer/test/outputs/serialization/prog.json
+++ b/primer/test/outputs/serialization/prog.json
@@ -17,128 +17,130 @@
             ]
         ]
     },
-    "progModule": {
-        "moduleDefs": {
-            "main": {
-                "contents": {
-                    "astDefExpr": {
-                        "contents": [
-                            0,
-                            {
-                                "contents": {
-                                    "contents": [],
-                                    "tag": "TEmptyHole"
-                                },
-                                "tag": "TCSynthed"
-                            },
-                            null
-                        ],
-                        "tag": "EmptyHole"
-                    },
-                    "astDefName": {
-                        "baseName": "main",
-                        "qualifiedModule": [
-                            "M"
-                        ]
-                    },
-                    "astDefType": {
-                        "contents": [
-                            0,
-                            {
-                                "tag": "KType"
-                            },
-                            null
-                        ],
-                        "tag": "TEmptyHole"
-                    }
-                },
-                "tag": "DefAST"
-            }
-        },
-        "moduleName": [
-            "M"
-        ],
-        "moduleTypes": {
-            "T": {
-                "contents": {
-                    "astTypeDefConstructors": [
-                        {
-                            "valConArgs": [
+    "progModules": [
+        {
+            "moduleDefs": {
+                "main": {
+                    "contents": {
+                        "astDefExpr": {
+                            "contents": [
+                                0,
                                 {
-                                    "contents": [
-                                        [],
-                                        {
-                                            "contents": [
-                                                [],
-                                                "b"
-                                            ],
-                                            "tag": "TVar"
-                                        },
-                                        {
-                                            "contents": [
-                                                [],
-                                                "a"
-                                            ],
-                                            "tag": "TVar"
-                                        }
-                                    ],
-                                    "tag": "TApp"
+                                    "contents": {
+                                        "contents": [],
+                                        "tag": "TEmptyHole"
+                                    },
+                                    "tag": "TCSynthed"
                                 },
+                                null
+                            ],
+                            "tag": "EmptyHole"
+                        },
+                        "astDefName": {
+                            "baseName": "main",
+                            "qualifiedModule": [
+                                "M"
+                            ]
+                        },
+                        "astDefType": {
+                            "contents": [
+                                0,
                                 {
-                                    "contents": [
-                                        [],
-                                        {
-                                            "baseName": "Nat",
-                                            "qualifiedModule": [
-                                                "Builtins"
-                                            ]
-                                        }
-                                    ],
-                                    "tag": "TCon"
-                                }
+                                    "tag": "KType"
+                                },
+                                null
                             ],
-                            "valConName": {
-                                "baseName": "C",
-                                "qualifiedModule": [
-                                    "M"
-                                ]
-                            }
+                            "tag": "TEmptyHole"
                         }
-                    ],
-                    "astTypeDefName": {
-                        "baseName": "T",
-                        "qualifiedModule": [
-                            "M"
-                        ]
                     },
-                    "astTypeDefNameHints": [],
-                    "astTypeDefParameters": [
-                        [
-                            "a",
-                            {
-                                "tag": "KType"
-                            }
-                        ],
-                        [
-                            "b",
+                    "tag": "DefAST"
+                }
+            },
+            "moduleName": [
+                "M"
+            ],
+            "moduleTypes": {
+                "T": {
+                    "contents": {
+                        "astTypeDefConstructors": [
                             {
-                                "contents": [
+                                "valConArgs": [
                                     {
-                                        "tag": "KType"
+                                        "contents": [
+                                            [],
+                                            {
+                                                "contents": [
+                                                    [],
+                                                    "b"
+                                                ],
+                                                "tag": "TVar"
+                                            },
+                                            {
+                                                "contents": [
+                                                    [],
+                                                    "a"
+                                                ],
+                                                "tag": "TVar"
+                                            }
+                                        ],
+                                        "tag": "TApp"
                                     },
                                     {
-                                        "tag": "KType"
+                                        "contents": [
+                                            [],
+                                            {
+                                                "baseName": "Nat",
+                                                "qualifiedModule": [
+                                                    "Builtins"
+                                                ]
+                                            }
+                                        ],
+                                        "tag": "TCon"
                                     }
                                 ],
-                                "tag": "KFun"
+                                "valConName": {
+                                    "baseName": "C",
+                                    "qualifiedModule": [
+                                        "M"
+                                    ]
+                                }
                             }
+                        ],
+                        "astTypeDefName": {
+                            "baseName": "T",
+                            "qualifiedModule": [
+                                "M"
+                            ]
+                        },
+                        "astTypeDefNameHints": [],
+                        "astTypeDefParameters": [
+                            [
+                                "a",
+                                {
+                                    "tag": "KType"
+                                }
+                            ],
+                            [
+                                "b",
+                                {
+                                    "contents": [
+                                        {
+                                            "tag": "KType"
+                                        },
+                                        {
+                                            "tag": "KType"
+                                        }
+                                    ],
+                                    "tag": "KFun"
+                                }
+                            ]
                         ]
-                    ]
-                },
-                "tag": "TypeDefAST"
+                    },
+                    "tag": "TypeDefAST"
+                }
             }
         }
-    },
+    ],
     "progSelection": {
         "selectedDef": {
             "baseName": "main",