diff --git a/primer-service/exe-server/Main.hs b/primer-service/exe-server/Main.hs
index d5410f85a..81c26f213 100644
--- a/primer-service/exe-server/Main.hs
+++ b/primer-service/exe-server/Main.hs
@@ -344,7 +344,9 @@ instance ConvertLogMessage SomeException LogMsg where
 instance ConvertLogMessage PrimerErr LogMsg where
   convert (DatabaseErr e) = LogMsg e
   convert (UnknownDef e) = LogMsg $ show e
+  convert (UnknownTypeDef e) = LogMsg $ show e
   convert (UnexpectedPrimDef e) = LogMsg $ show e
+  convert (UnexpectedPrimTypeDef e) = LogMsg $ show e
   convert (AddDefError m n e) = LogMsg $ show (m, n, e)
   convert (AddTypeDefError tc vcs e) = LogMsg $ show (tc, vcs, e)
   convert (ActionOptionsNoID e) = LogMsg $ show e
diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs
index 91db986b5..39f9bc2ff 100644
--- a/primer-service/src/Primer/OpenAPI.hs
+++ b/primer-service/src/Primer/OpenAPI.hs
@@ -10,6 +10,12 @@ module Primer.OpenAPI (
 import Foreword
 
 import Data.Aeson (
+  FromJSON,
+  GFromJSON,
+  GToEncoding,
+  GToJSON,
+  ToJSON,
+  Zero,
   toJSON,
  )
 import Data.OpenApi (
@@ -27,6 +33,7 @@ import Data.OpenApi.Internal.Schema (
   rename,
   timeSchema,
  )
+import Data.Text qualified as T
 import Data.Time (
   UTCTime (..),
   fromGregorian,
@@ -42,10 +49,11 @@ import Primer.API (
   Module,
   NewSessionReq,
   NodeBody,
-  NodeSelection (..),
   Prog,
-  Selection (..),
+  Selection,
   Tree,
+  TypeDef,
+  ValCon,
  )
 import Primer.API qualified as API
 import Primer.API.NodeFlavor (
@@ -56,8 +64,8 @@ import Primer.API.NodeFlavor (
  )
 import Primer.API.RecordPair (RecordPair)
 import Primer.Action.Available qualified as Available
-import Primer.App (NodeType)
-import Primer.App.Base (Level)
+import Primer.App (DefSelection, NodeSelection, NodeType, TypeDefSelection)
+import Primer.App.Base (Level, TypeDefConsFieldSelection (..), TypeDefConsSelection (..), TypeDefNodeSelection)
 import Primer.Core (
   GlobalName,
   GlobalNameKind (ADefName, ATyCon, AValCon),
@@ -65,16 +73,21 @@ import Primer.Core (
   LVarName,
   ModuleName,
   PrimCon,
+  TyVarName,
  )
 import Primer.Database (
   LastModified,
   Session,
   SessionName,
  )
-import Primer.JSON (CustomJSON, PrimerJSON)
+import Primer.JSON (CustomJSON (CustomJSON), PrimerJSON)
 import Primer.Name (Name)
 import Servant.API (FromHttpApiData (parseQueryParam), ToHttpApiData (toQueryParam))
 
+newtype PrimerJSONNamed (s :: Symbol) a = PrimerJSONNamed a
+deriving via PrimerJSON a instance (Generic a, GFromJSON Zero (Rep a)) => FromJSON (PrimerJSONNamed s a)
+deriving via PrimerJSON a instance (Generic a, GToJSON Zero (Rep a), GToEncoding Zero (Rep a)) => ToJSON (PrimerJSONNamed s a)
+
 -- $orphanInstances
 --
 -- We define some OpenApi orphan instances in primer-service, to avoid
@@ -89,6 +102,12 @@ instance
   where
   declareNamedSchema _ = genericDeclareNamedSchema (fromAesonOptions (aesonOptions @os)) (Proxy @a)
 
+instance
+  (Typeable a, Generic a, GToSchema (Rep a), KnownSymbol s) =>
+  ToSchema (PrimerJSONNamed s a)
+  where
+  declareNamedSchema _ = rename (Just $ T.pack $ symbolVal $ Proxy @s) <$> declareNamedSchema (Proxy @(PrimerJSON a))
+
 instance ToSchema SessionName
 deriving via PrimerJSON Session instance ToSchema Session
 
@@ -120,12 +139,12 @@ deriving via Text instance (ToSchema Name)
 -- at the openapi level, so api consumers do not have to deal with
 -- three identical types. Note that our openapi interface is a
 -- simplified view, so this collapse is in the correct spirit.
-instance ToSchema (GlobalName 'ADefName) where
-  declareNamedSchema _ = rename (Just "GlobalName") <$> declareNamedSchema (Proxy @(PrimerJSON (GlobalName 'ADefName)))
+deriving via PrimerJSONNamed "GlobalName" (GlobalName 'ADefName) instance ToSchema (GlobalName 'ADefName)
 deriving via GlobalName 'ADefName instance ToSchema (GlobalName 'ATyCon)
 deriving via GlobalName 'ADefName instance ToSchema (GlobalName 'AValCon)
 
 deriving via Name instance (ToSchema LVarName)
+deriving via Name instance (ToSchema TyVarName)
 deriving via PrimerJSON (RecordPair a b) instance (ToSchema a, ToSchema b) => ToSchema (RecordPair a b)
 deriving via PrimerJSON Tree instance ToSchema Tree
 deriving via PrimerJSON API.Name instance ToSchema API.Name
@@ -135,6 +154,8 @@ deriving via PrimerJSON NodeFlavorTextBody instance ToSchema NodeFlavorTextBody
 deriving via PrimerJSON NodeFlavorPrimBody instance ToSchema NodeFlavorPrimBody
 deriving via PrimerJSON NodeFlavorBoxBody instance ToSchema NodeFlavorBoxBody
 deriving via PrimerJSON NodeFlavorNoBody instance ToSchema NodeFlavorNoBody
+deriving via PrimerJSON TypeDef instance ToSchema TypeDef
+deriving via PrimerJSON ValCon instance ToSchema ValCon
 deriving via PrimerJSON Def instance ToSchema Def
 deriving via NonEmpty Name instance ToSchema ModuleName
 deriving via PrimerJSON Module instance ToSchema Module
@@ -146,8 +167,13 @@ deriving via PrimerJSON Available.FreeInput instance ToSchema Available.FreeInpu
 deriving via PrimerJSON Available.Options instance ToSchema Available.Options
 deriving via PrimerJSON Available.Action instance ToSchema Available.Action
 deriving via PrimerJSON ApplyActionBody instance ToSchema ApplyActionBody
-deriving via PrimerJSON Selection instance ToSchema Selection
-deriving via PrimerJSON NodeSelection instance ToSchema NodeSelection
+deriving via PrimerJSONNamed "Selection" Selection instance ToSchema Selection
+deriving via PrimerJSONNamed "TypeDefSelection" (TypeDefSelection ID) instance ToSchema (TypeDefSelection ID)
+deriving via PrimerJSONNamed "TypeDefNodeSelection" (TypeDefNodeSelection ID) instance ToSchema (TypeDefNodeSelection ID)
+deriving via PrimerJSONNamed "TypeDefConsSelection" (TypeDefConsSelection ID) instance ToSchema (TypeDefConsSelection ID)
+deriving via PrimerJSONNamed "TypeDefConsFieldSelection" (TypeDefConsFieldSelection ID) instance ToSchema (TypeDefConsFieldSelection ID)
+deriving via PrimerJSONNamed "DefSelection" (DefSelection ID) instance ToSchema (DefSelection ID)
+deriving via PrimerJSONNamed "NodeSelection" (NodeSelection ID) instance ToSchema (NodeSelection ID)
 deriving via PrimerJSON NodeType instance ToSchema NodeType
 deriving via PrimerJSON Level instance ToSchema Level
 deriving via PrimerJSON NewSessionReq instance ToSchema NewSessionReq
diff --git a/primer-service/src/Primer/Server.hs b/primer-service/src/Primer/Server.hs
index 88096a9e4..7372457cb 100644
--- a/primer-service/src/Primer/Server.hs
+++ b/primer-service/src/Primer/Server.hs
@@ -343,6 +343,8 @@ serve ss q v port logger = do
         DatabaseErr msg -> err500{errBody = encode msg}
         UnknownDef d -> err404{errBody = "Unknown definition: " <> encode (globalNamePretty d)}
         UnexpectedPrimDef d -> err400{errBody = "Unexpected primitive definition: " <> encode (globalNamePretty d)}
+        UnknownTypeDef d -> err404{errBody = "Unknown type definition: " <> encode (globalNamePretty d)}
+        UnexpectedPrimTypeDef d -> err400{errBody = "Unexpected primitive type definition: " <> encode (globalNamePretty d)}
         AddDefError m md pe -> err400{errBody = "Error while adding definition (" <> s <> "): " <> show pe}
           where
             s = encode $ case md of
diff --git a/primer-service/test/Tests/OpenAPI.hs b/primer-service/test/Tests/OpenAPI.hs
index a00773e92..80a639f25 100644
--- a/primer-service/test/Tests/OpenAPI.hs
+++ b/primer-service/test/Tests/OpenAPI.hs
@@ -30,10 +30,11 @@ import Primer.API (
   Module (Module),
   NewSessionReq (..),
   NodeBody (BoxBody, NoBody, PrimBody, TextBody),
-  NodeSelection (..),
   Prog (Prog),
-  Selection (..),
+  Selection,
   Tree,
+  TypeDef (..),
+  ValCon (..),
   viewTreeExpr,
   viewTreeType,
  )
@@ -45,7 +46,17 @@ import Primer.API.NodeFlavor (
  )
 import Primer.API.RecordPair (RecordPair (RecordPair))
 import Primer.Action.Available qualified as Available
-import Primer.App (Level, NodeType)
+import Primer.App (
+  DefSelection (..),
+  Level,
+  NodeSelection (..),
+  NodeType,
+  Selection' (..),
+  TypeDefConsFieldSelection (TypeDefConsFieldSelection),
+  TypeDefConsSelection (..),
+  TypeDefSelection (..),
+ )
+import Primer.App.Base (TypeDefNodeSelection (..))
 import Primer.Core (GVarName, ID (ID), ModuleName, PrimCon (PrimChar, PrimInt))
 import Primer.Database (
   LastModified (..),
@@ -64,6 +75,7 @@ import Primer.Gen.Core.Raw (
   genModuleName,
   genName,
   genTyConName,
+  genTyVarName,
   genType,
   genValConName,
  )
@@ -207,6 +219,18 @@ tasty_NodeFlavorNoBody = testToJSON $ G.enumBounded @_ @NodeFlavorNoBody
 genDef :: ExprGen Def
 genDef = Def <$> genGVarName <*> genExprTree <*> G.maybe genTypeTree
 
+genTypeDef :: ExprGen TypeDef
+genTypeDef =
+  TypeDef
+    <$> genTyConName
+    <*> G.list (R.linear 0 3) genTyVarName
+    <*> G.list (R.linear 0 3) genName
+    <*> G.maybe
+      ( G.list
+          (R.linear 0 3)
+          (ValCon <$> genValConName <*> G.list (R.linear 0 3) genTypeTree)
+      )
+
 tasty_Def :: Property
 tasty_Def = testToJSON $ evalExprGen 0 genDef
 
@@ -215,7 +239,7 @@ genModule =
   Module
     <$> genModuleName
     <*> G.bool
-    <*> G.list (R.linear 0 3) genTyConName
+    <*> G.list (R.linear 0 3) genTypeDef
     <*> G.list (R.linear 0 3) genDef
 
 tasty_Module :: Property
@@ -224,11 +248,33 @@ tasty_Module = testToJSON $ evalExprGen 0 genModule
 genNodeType :: ExprGen NodeType
 genNodeType = G.enumBounded
 
-genNodeSelection :: ExprGen NodeSelection
+genNodeSelection :: ExprGen (NodeSelection ID)
 genNodeSelection = NodeSelection <$> genNodeType <*> genID
 
+genDefSelection :: ExprGen (DefSelection ID)
+genDefSelection = DefSelection <$> genGVarName <*> G.maybe genNodeSelection
+
+genTypeDefSelection :: ExprGen (TypeDefSelection ID)
+genTypeDefSelection =
+  TypeDefSelection
+    <$> genTyConName
+    <*> G.maybe
+      ( G.choice
+          [ TypeDefParamNodeSelection <$> genTyVarName
+          , TypeDefConsNodeSelection
+              <$> ( TypeDefConsSelection
+                      <$> genValConName
+                      <*> G.maybe (TypeDefConsFieldSelection <$> G.integral (R.linear 0 3) <*> genID)
+                  )
+          ]
+      )
+
 genSelection :: ExprGen Selection
-genSelection = Selection <$> genGVarName <*> G.maybe genNodeSelection
+genSelection =
+  G.choice
+    [ SelectionDef <$> genDefSelection
+    , SelectionTypeDef <$> genTypeDefSelection
+    ]
 
 genProg :: Gen Prog
 genProg = evalExprGen 0 $ Prog <$> G.list (R.linear 0 3) genModule <*> G.maybe genSelection <*> G.bool <*> G.bool
@@ -307,7 +353,7 @@ instance Arbitrary ApplyActionBody where
   arbitrary = ApplyActionBody <$> arbitrary <*> arbitrary
 instance Arbitrary Selection where
   arbitrary = hedgehog $ evalExprGen 0 genSelection
-instance Arbitrary NodeSelection where
+instance Arbitrary (NodeSelection ID) where
   arbitrary = hedgehog $ evalExprGen 0 genNodeSelection
 instance Arbitrary a => Arbitrary (NonEmpty a) where
   arbitrary = (:|) <$> arbitrary <*> arbitrary
diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json
index a67c94034..0f495fba2 100644
--- a/primer-service/test/outputs/OpenAPI/openapi.json
+++ b/primer-service/test/outputs/OpenAPI/openapi.json
@@ -100,6 +100,20 @@
                 ],
                 "type": "object"
             },
+            "DefSelection": {
+                "properties": {
+                    "def": {
+                        "$ref": "#/components/schemas/GlobalName"
+                    },
+                    "node": {
+                        "$ref": "#/components/schemas/NodeSelection"
+                    }
+                },
+                "required": [
+                    "def"
+                ],
+                "type": "object"
+            },
             "EvalFullResp": {
                 "oneOf": [
                     {
@@ -187,7 +201,11 @@
                     "MakeTVar",
                     "MakeForall",
                     "RenameForall",
-                    "RenameDef"
+                    "RenameDef",
+                    "RenameType",
+                    "RenameCon",
+                    "RenameTypeParam",
+                    "AddCon"
                 ],
                 "type": "string"
             },
@@ -224,7 +242,7 @@
                     },
                     "types": {
                         "items": {
-                            "$ref": "#/components/schemas/GlobalName"
+                            "$ref": "#/components/schemas/TypeDef"
                         },
                         "type": "array"
                     }
@@ -284,7 +302,8 @@
                     "RaiseType",
                     "DeleteType",
                     "DuplicateDef",
-                    "DeleteDef"
+                    "DeleteDef",
+                    "AddConField"
                 ],
                 "type": "string"
             },
@@ -413,7 +432,7 @@
             },
             "NodeSelection": {
                 "properties": {
-                    "id": {
+                    "meta": {
                         "maximum": 9223372036854775807,
                         "minimum": -9223372036854775808,
                         "type": "integer"
@@ -424,7 +443,7 @@
                 },
                 "required": [
                     "nodeType",
-                    "id"
+                    "meta"
                 ],
                 "type": "object"
             },
@@ -656,18 +675,44 @@
                 "type": "object"
             },
             "Selection": {
-                "properties": {
-                    "def": {
-                        "$ref": "#/components/schemas/GlobalName"
+                "oneOf": [
+                    {
+                        "properties": {
+                            "contents": {
+                                "$ref": "#/components/schemas/DefSelection"
+                            },
+                            "tag": {
+                                "enum": [
+                                    "SelectionDef"
+                                ],
+                                "type": "string"
+                            }
+                        },
+                        "required": [
+                            "tag",
+                            "contents"
+                        ],
+                        "type": "object"
                     },
-                    "node": {
-                        "$ref": "#/components/schemas/NodeSelection"
+                    {
+                        "properties": {
+                            "contents": {
+                                "$ref": "#/components/schemas/TypeDefSelection"
+                            },
+                            "tag": {
+                                "enum": [
+                                    "SelectionTypeDef"
+                                ],
+                                "type": "string"
+                            }
+                        },
+                        "required": [
+                            "tag",
+                            "contents"
+                        ],
+                        "type": "object"
                     }
-                },
-                "required": [
-                    "def"
-                ],
-                "type": "object"
+                ]
             },
             "Session": {
                 "properties": {
@@ -716,10 +761,146 @@
                 ],
                 "type": "object"
             },
+            "TypeDef": {
+                "properties": {
+                    "constructors": {
+                        "items": {
+                            "$ref": "#/components/schemas/ValCon"
+                        },
+                        "type": "array"
+                    },
+                    "name": {
+                        "$ref": "#/components/schemas/GlobalName"
+                    },
+                    "nameHints": {
+                        "items": {
+                            "type": "string"
+                        },
+                        "type": "array"
+                    },
+                    "params": {
+                        "items": {
+                            "type": "string"
+                        },
+                        "type": "array"
+                    }
+                },
+                "required": [
+                    "name",
+                    "params",
+                    "nameHints"
+                ],
+                "type": "object"
+            },
+            "TypeDefConsFieldSelection": {
+                "properties": {
+                    "index": {
+                        "maximum": 9223372036854775807,
+                        "minimum": -9223372036854775808,
+                        "type": "integer"
+                    },
+                    "meta": {
+                        "maximum": 9223372036854775807,
+                        "minimum": -9223372036854775808,
+                        "type": "integer"
+                    }
+                },
+                "required": [
+                    "index",
+                    "meta"
+                ],
+                "type": "object"
+            },
+            "TypeDefConsSelection": {
+                "properties": {
+                    "con": {
+                        "$ref": "#/components/schemas/GlobalName"
+                    },
+                    "field": {
+                        "$ref": "#/components/schemas/TypeDefConsFieldSelection"
+                    }
+                },
+                "required": [
+                    "con"
+                ],
+                "type": "object"
+            },
+            "TypeDefNodeSelection": {
+                "oneOf": [
+                    {
+                        "properties": {
+                            "contents": {
+                                "type": "string"
+                            },
+                            "tag": {
+                                "enum": [
+                                    "TypeDefParamNodeSelection"
+                                ],
+                                "type": "string"
+                            }
+                        },
+                        "required": [
+                            "tag",
+                            "contents"
+                        ],
+                        "type": "object"
+                    },
+                    {
+                        "properties": {
+                            "contents": {
+                                "$ref": "#/components/schemas/TypeDefConsSelection"
+                            },
+                            "tag": {
+                                "enum": [
+                                    "TypeDefConsNodeSelection"
+                                ],
+                                "type": "string"
+                            }
+                        },
+                        "required": [
+                            "tag",
+                            "contents"
+                        ],
+                        "type": "object"
+                    }
+                ]
+            },
+            "TypeDefSelection": {
+                "properties": {
+                    "def": {
+                        "$ref": "#/components/schemas/GlobalName"
+                    },
+                    "node": {
+                        "$ref": "#/components/schemas/TypeDefNodeSelection"
+                    }
+                },
+                "required": [
+                    "def"
+                ],
+                "type": "object"
+            },
             "UUID": {
                 "example": "00000000-0000-0000-0000-000000000000",
                 "format": "uuid",
                 "type": "string"
+            },
+            "ValCon": {
+                "properties": {
+                    "fields": {
+                        "items": {
+                            "$ref": "#/components/schemas/Tree"
+                        },
+                        "type": "array"
+                    },
+                    "name": {
+                        "$ref": "#/components/schemas/GlobalName"
+                    }
+                },
+                "required": [
+                    "name",
+                    "fields"
+                ],
+                "type": "object"
             }
         }
     },
@@ -1079,7 +1260,11 @@
                                 "MakeTVar",
                                 "MakeForall",
                                 "RenameForall",
-                                "RenameDef"
+                                "RenameDef",
+                                "RenameType",
+                                "RenameCon",
+                                "RenameTypeParam",
+                                "AddCon"
                             ],
                             "type": "string"
                         }
diff --git a/primer/src/Foreword.hs b/primer/src/Foreword.hs
index 1ed8aebf3..ab980f6fd 100644
--- a/primer/src/Foreword.hs
+++ b/primer/src/Foreword.hs
@@ -32,6 +32,8 @@ module Foreword (
   curry4,
   unsafeMaximum,
   spanMaybe,
+  adjustAtA',
+  findAndAdjustA',
 ) where
 
 -- In general, we should defer to "Protolude"'s exports and avoid name
@@ -130,6 +132,11 @@ adjustAtA n f xs = case splitAt n xs of
   (a, b : bs) -> f b <&> \b' -> Just $ a ++ [b'] ++ bs
   _ -> pure Nothing
 
+adjustAtA' :: Applicative f => Int -> (a -> f (a, z)) -> [a] -> f (Maybe ([a], z))
+adjustAtA' n f xs = case splitAt n xs of
+  (a, b : bs) -> f b <&> \(b', z) -> Just (a ++ [b'] ++ bs, z)
+  _ -> pure Nothing
+
 -- | Adjust the first element of the list which satisfies the
 -- predicate. Returns 'Nothing' if there is no such element.
 findAndAdjust :: (a -> Bool) -> (a -> a) -> [a] -> Maybe [a]
@@ -143,6 +150,11 @@ findAndAdjustA p f = \case
   [] -> pure Nothing
   x : xs -> if p x then Just . (: xs) <$> f x else (x :) <<$>> findAndAdjustA p f xs
 
+findAndAdjustA' :: Applicative m => (a -> Bool) -> (a -> m (a, z)) -> [a] -> m (Maybe ([a], z))
+findAndAdjustA' p f = \case
+  [] -> pure Nothing
+  x : xs -> if p x then (\(x', z) -> Just . (,z) . (: xs) $ x') <$> f x else first (x :) <<$>> findAndAdjustA' p f xs
+
 -- | Change the type of an error.
 modifyError :: MonadError e' m => (e -> e') -> ExceptT e m a -> m a
 modifyError f = runExceptT >=> either (throwError . f) pure
diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs
index 75342e7df..4cafedc6b 100644
--- a/primer/src/Primer/API.hs
+++ b/primer/src/Primer/API.hs
@@ -36,6 +36,8 @@ module Primer.API (
   viewProg,
   Prog (Prog),
   Module (Module),
+  TypeDef (TypeDef),
+  ValCon (ValCon),
   Def (Def),
   getProgram,
   getProgram',
@@ -62,10 +64,7 @@ module Primer.API (
   viewTreeType,
   viewTreeExpr,
   getApp,
-  Selection (..),
-  viewSelection,
-  NodeSelection (..),
-  viewNodeSelection,
+  Selection,
   undoAvailable,
   redoAvailable,
   Name (..),
@@ -103,6 +102,7 @@ import Primer.Action (ActionError, ProgAction, toProgActionInput, toProgActionNo
 import Primer.Action.Available qualified as Available
 import Primer.App (
   App,
+  DefSelection (..),
   EditAppM,
   Editable,
   EvalFullReq (..),
@@ -110,10 +110,14 @@ import Primer.App (
   EvalResp (..),
   Level,
   MutationRequest,
+  NodeSelection (..),
   NodeType (..),
   ProgError,
   QueryAppM,
   Question (GenerateName),
+  Selection' (..),
+  TypeDefConsSelection (..),
+  TypeDefSelection (..),
   appProg,
   handleEvalFullRequest,
   handleEvalRequest,
@@ -123,6 +127,7 @@ import Primer.App (
   newApp,
   progAllDefs,
   progAllTypeDefs,
+  progAllTypeDefsMeta,
   progCxt,
   progImports,
   progLog,
@@ -134,6 +139,7 @@ import Primer.App (
   unlog,
  )
 import Primer.App qualified as App
+import Primer.App.Base (TypeDefNodeSelection (..))
 import Primer.Core (
   Bind' (..),
   CaseBranch' (..),
@@ -152,6 +158,7 @@ import Primer.Core (
   TyVarName,
   Type,
   Type' (..),
+  TypeMeta,
   ValConName,
   getID,
   unLocalName,
@@ -210,10 +217,11 @@ import Primer.Log (
   PureLog,
   runPureLog,
  )
-import Primer.Module (moduleDefsQualified, moduleName, moduleTypesQualified)
+import Primer.Module (moduleDefsQualified, moduleName, moduleTypesQualifiedMeta)
 import Primer.Name qualified as Name
 import Primer.Primitives (primDefType)
-import Primer.TypeDef (ASTTypeDef (ASTTypeDef), ValCon (ValCon))
+import Primer.TypeDef (ASTTypeDef (..), forgetTypeDefMetadata, typeDefNameHints, typeDefParameters)
+import Primer.TypeDef qualified as TypeDef
 import StmContainers.Map qualified as StmMap
 
 -- | The API environment.
@@ -255,10 +263,12 @@ runPrimerM = runReaderT . unPrimerM
 data PrimerErr
   = DatabaseErr Text
   | UnknownDef GVarName
+  | UnknownTypeDef TyConName
   | UnexpectedPrimDef GVarName
+  | UnexpectedPrimTypeDef TyConName
   | AddDefError ModuleName (Maybe Text) ProgError
   | AddTypeDefError TyConName [ValConName] ProgError
-  | ActionOptionsNoID (Maybe (NodeType, ID))
+  | ActionOptionsNoID Selection
   | ToProgActionError Available.Action ActionError
   | ApplyActionError [ProgAction] ProgError
   | UndoError ProgError
@@ -625,7 +635,7 @@ data Prog = Prog
 data Module = Module
   { modname :: ModuleName
   , editable :: Bool
-  , types :: [TyConName]
+  , types :: [TypeDef]
   , -- 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
@@ -636,6 +646,25 @@ data Module = Module
   deriving (ToJSON, FromJSON) via PrimerJSON Module
   deriving anyclass (NFData)
 
+data TypeDef = TypeDef
+  { name :: TyConName
+  , params :: [TyVarName]
+  , nameHints :: [Name.Name]
+  , constructors :: Maybe [ValCon]
+  -- ^ a `Nothing` here indicates a primitive type (whereas `Just []` is `Void`)
+  }
+  deriving stock (Generic, Show, Read)
+  deriving (ToJSON, FromJSON) via PrimerJSON TypeDef
+  deriving anyclass (NFData)
+
+data ValCon = ValCon
+  { name :: ValConName
+  , fields :: [Tree]
+  }
+  deriving stock (Generic, Show, Read)
+  deriving (ToJSON, FromJSON) via PrimerJSON ValCon
+  deriving anyclass (NFData)
+
 -- | This type is the api's view of a 'Primer.Core.Def'
 -- (this is expected to evolve as we flesh out the API)
 data Def = Def
@@ -652,7 +681,7 @@ viewProg :: App.Prog -> Prog
 viewProg p =
   Prog
     { modules = map (viewModule True) (progModules p) <> map (viewModule False) (progImports p)
-    , selection = viewSelection <$> progSelection p
+    , selection = getID <<$>> progSelection p
     , undoAvailable = not $ null $ unlog $ progLog p
     , redoAvailable = not $ null $ unlog $ redoLog p
     }
@@ -661,7 +690,24 @@ viewProg p =
       Module
         { modname = moduleName m
         , editable = e
-        , types = fst <$> Map.assocs (moduleTypesQualified m)
+        , types =
+            ( \(name, d) ->
+                TypeDef
+                  { name
+                  , params = fst <$> typeDefParameters d
+                  , nameHints = typeDefNameHints d
+                  , constructors = case d of
+                      TypeDef.TypeDefPrim _ -> Nothing
+                      TypeDef.TypeDefAST t ->
+                        Just $
+                          astTypeDefConstructors t <&> \(TypeDef.ValCon nameCon argsCon) ->
+                            ValCon
+                              { name = nameCon
+                              , fields = viewTreeType' . over _typeMeta (show . view _id) <$> argsCon
+                              }
+                  }
+            )
+              <$> Map.assocs (moduleTypesQualifiedMeta m)
         , defs =
             ( \(name, d) ->
                 Def
@@ -676,7 +722,7 @@ viewProg p =
                               flip evalState (0 :: Int) . traverseOf _typeMeta \() -> do
                                 n <- get
                                 put $ n + 1
-                                pure $ "primtype_" <> show d' <> "_" <> show n
+                                pure $ "primtype_" <> Name.unName (Core.baseName name) <> "_" <> show n
                   }
             )
               <$> Map.assocs (moduleDefsQualified m)
@@ -1021,7 +1067,7 @@ createTypeDef ::
 createTypeDef =
   curry3 $
     logAPI (noError CreateTypeDef) \(sid, tyconName, valcons) ->
-      edit sid (App.Edit [App.AddTypeDef tyconName $ ASTTypeDef [] (map (`ValCon` []) valcons) []])
+      edit sid (App.Edit [App.AddTypeDef tyconName $ ASTTypeDef [] (map (`TypeDef.ValCon` []) valcons) []])
         >>= either (throwM . AddTypeDefError tyconName valcons) (pure . viewProg)
 
 availableActions ::
@@ -1033,15 +1079,23 @@ availableActions ::
 availableActions = curry3 $ logAPI (noError AvailableActions) $ \(sid, level, selection) -> do
   prog <- getProgram sid
   let allDefs = progAllDefs prog
-      allTypeDefs = progAllTypeDefs prog
-  (editable, ASTDef{astDefType = type_, astDefExpr = expr}) <- findASTDef allDefs selection.def
-  case selection.node of
-    Nothing ->
-      pure $ Available.forDef (snd <$> allDefs) level editable selection.def
-    Just NodeSelection{..} -> do
-      pure $ case nodeType of
-        SigNode -> Available.forSig level editable type_ id
-        BodyNode -> Available.forBody (snd <$> allTypeDefs) level editable expr id
+      allTypeDefs = progAllTypeDefsMeta prog
+  case selection of
+    SelectionDef sel -> do
+      (editable, ASTDef{astDefType = type_, astDefExpr = expr}) <- findASTDef allDefs sel.def
+      pure $ case sel.node of
+        Nothing -> Available.forDef (snd <$> allDefs) level editable sel.def
+        Just NodeSelection{..} -> case nodeType of
+          SigNode -> Available.forSig level editable type_ meta
+          BodyNode -> Available.forBody (forgetTypeDefMetadata . snd <$> allTypeDefs) level editable expr meta
+    SelectionTypeDef sel -> do
+      (editable, def) <- findASTTypeDef allTypeDefs sel.def
+      pure $ case sel.node of
+        Nothing -> Available.forTypeDef level editable
+        Just (TypeDefParamNodeSelection _) -> Available.forTypeDefParamNode level editable
+        Just (TypeDefConsNodeSelection s) -> case s.field of
+          Nothing -> Available.forTypeDefConsNode level editable
+          Just field -> Available.forTypeDefConsFieldNode level editable def s.con field.index field.meta
 
 actionOptions ::
   (MonadIO m, MonadThrow m, MonadAPILog l m) =>
@@ -1055,17 +1109,9 @@ actionOptions = curry4 $ logAPI (noError ActionOptions) $ \(sid, level, selectio
   let prog = appProg app
       allDefs = progAllDefs prog
       allTypeDefs = progAllTypeDefs prog
-      nodeSel = selection.node <&> \s -> (s.nodeType, s.id)
-  def' <- snd <$> findASTDef allDefs selection.def
-  maybe (throwM $ ActionOptionsNoID nodeSel) pure $
-    Available.options
-      (snd <$> allTypeDefs)
-      (snd <$> allDefs)
-      (progCxt prog)
-      level
-      def'
-      nodeSel
-      action
+  def <- snd <$> findASTTypeOrTermDef prog selection
+  maybe (throwM $ ActionOptionsNoID selection) pure $
+    Available.options (snd <$> allTypeDefs) (snd <$> allDefs) (progCxt prog) level def selection action
 
 findASTDef :: MonadThrow m => Map GVarName (Editable, Def.Def) -> GVarName -> m (Editable, ASTDef)
 findASTDef allDefs def = case allDefs Map.!? def of
@@ -1073,6 +1119,19 @@ findASTDef allDefs def = case allDefs Map.!? def of
   Just (_, Def.DefPrim _) -> throwM $ UnexpectedPrimDef def
   Just (editable, Def.DefAST d) -> pure (editable, d)
 
+findASTTypeDef :: MonadThrow m => Map TyConName (Editable, TypeDef.TypeDef a) -> TyConName -> m (Editable, ASTTypeDef a)
+findASTTypeDef allTypeDefs def = case allTypeDefs Map.!? def of
+  Nothing -> throwM $ UnknownTypeDef def
+  Just (_, TypeDef.TypeDefPrim _) -> throwM $ UnexpectedPrimTypeDef def
+  Just (editable, TypeDef.TypeDefAST d) -> pure (editable, d)
+
+findASTTypeOrTermDef :: MonadThrow f => App.Prog -> Selection -> f (Editable, Either (ASTTypeDef TypeMeta) ASTDef)
+findASTTypeOrTermDef prog = \case
+  App.SelectionTypeDef sel ->
+    Left <<$>> findASTTypeDef (progAllTypeDefsMeta prog) sel.def
+  App.SelectionDef sel ->
+    Right <<$>> findASTDef (progAllDefs prog) sel.def
+
 applyActionNoInput ::
   (MonadIO m, MonadThrow m, MonadAPILog l m) =>
   SessionId ->
@@ -1081,15 +1140,10 @@ applyActionNoInput ::
   PrimerM m Prog
 applyActionNoInput = curry3 $ logAPI (noError ApplyActionNoInput) $ \(sid, selection, action) -> do
   prog <- getProgram sid
-  def <- snd <$> findASTDef (progAllDefs prog) selection.def
+  def <- snd <$> findASTTypeOrTermDef prog selection
   actions <-
     either (throwM . ToProgActionError (Available.NoInput action)) pure $
-      toProgActionNoInput
-        (snd <$> progAllDefs prog)
-        def
-        selection.def
-        (selection.node <&> \s -> (s.nodeType, s.id))
-        action
+      toProgActionNoInput (snd <$> progAllDefs prog) def selection action
   applyActions sid actions
 
 applyActionInput ::
@@ -1100,15 +1154,10 @@ applyActionInput ::
   PrimerM m Prog
 applyActionInput = curry3 $ logAPI (noError ApplyActionInput) $ \(sid, body, action) -> do
   prog <- getProgram sid
-  def <- snd <$> findASTDef (progAllDefs prog) body.selection.def
+  def <- snd <$> findASTTypeOrTermDef prog body.selection
   actions <-
     either (throwM . ToProgActionError (Available.Input action)) pure $
-      toProgActionInput
-        def
-        body.selection.def
-        (body.selection.node <&> \s -> (s.nodeType, s.id))
-        body.option
-        action
+      toProgActionInput def body.selection body.option action
   applyActions sid actions
 
 data ApplyActionBody = ApplyActionBody
@@ -1144,25 +1193,4 @@ redo =
       >>= either (throwM . RedoError) (pure . viewProg)
 
 -- | 'App.Selection' without any node metadata.
-data Selection = Selection
-  { def :: GVarName
-  , node :: Maybe NodeSelection
-  }
-  deriving stock (Eq, Show, Read, Generic)
-  deriving (FromJSON, ToJSON) via PrimerJSON Selection
-  deriving anyclass (NFData)
-
-viewSelection :: App.Selection -> Selection
-viewSelection App.Selection{..} = Selection{def = selectedDef, node = viewNodeSelection <$> selectedNode}
-
--- | 'App.NodeSelection' without any node metadata.
-data NodeSelection = NodeSelection
-  { nodeType :: NodeType
-  , id :: ID
-  }
-  deriving stock (Eq, Show, Read, Generic)
-  deriving (FromJSON, ToJSON) via PrimerJSON NodeSelection
-  deriving anyclass (NFData)
-
-viewNodeSelection :: App.NodeSelection -> NodeSelection
-viewNodeSelection sel@App.NodeSelection{nodeType} = NodeSelection{nodeType, id = getID sel}
+type Selection = App.Selection' ID
diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs
index 1d0e7c6dc..3f791bc08 100644
--- a/primer/src/Primer/Action.hs
+++ b/primer/src/Primer/Action.hs
@@ -1,4 +1,6 @@
+{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 
 module Primer.Action (
@@ -17,6 +19,7 @@ module Primer.Action (
   uniquifyDefName,
   toProgActionInput,
   toProgActionNoInput,
+  applyActionsToField,
 ) where
 
 import Foreword hiding (mod)
@@ -24,18 +27,29 @@ import Foreword hiding (mod)
 import Control.Monad.Fresh (MonadFresh)
 import Data.Aeson (Value)
 import Data.Bifunctor.Swap qualified as Swap
+import Data.Data (Data)
 import Data.Generics.Product (typed)
 import Data.List (findIndex)
 import Data.List.NonEmpty qualified as NE
+import Data.Map (insert)
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Data.Text qualified as T
-import Optics (set, (%), (?~), (^.), (^?), _Just)
+import Optics (over, set, (%), (?~), (^.), (^?), _Just)
 import Primer.Action.Actions (Action (..), Movement (..), QualifiedText)
 import Primer.Action.Available qualified as Available
 import Primer.Action.Errors (ActionError (..))
 import Primer.Action.ProgAction (ProgAction (..))
-import Primer.App.Base (NodeType (..))
+import Primer.App.Base (
+  DefSelection (..),
+  NodeSelection (..),
+  NodeType (..),
+  Selection' (..),
+  TypeDefConsFieldSelection (..),
+  TypeDefConsSelection (..),
+  TypeDefNodeSelection (..),
+  TypeDefSelection (..),
+ )
 import Primer.Core (
   Expr,
   Expr' (..),
@@ -52,6 +66,7 @@ import Primer.Core (
   Type' (..),
   TypeCache (..),
   TypeCacheBoth (..),
+  TypeMeta,
   ValConName,
   baseName,
   bindName,
@@ -94,7 +109,7 @@ import Primer.Def (
   Def (..),
   DefMap,
  )
-import Primer.Module (Module, insertDef)
+import Primer.Module (Module (moduleTypes), insertDef)
 import Primer.Name (Name, NameCounter, unName, unsafeMkName)
 import Primer.Name.Fresh (
   isFresh,
@@ -230,6 +245,49 @@ applyActionsToTypeSig smartHoles imports (mod, mods) (defName, def) actions =
             -- In this case we just refocus on the top of the type.
             z -> maybe unwrapError pure (focusType (unfocusLoc z))
 
+applyActionsToField ::
+  (MonadFresh ID m, MonadFresh NameCounter m) =>
+  SmartHoles ->
+  [Module] ->
+  (Module, [Module]) ->
+  (Name, ValConName, Int, ASTTypeDef TypeMeta) ->
+  [Action] ->
+  m (Either ActionError ([Module], TypeZ))
+applyActionsToField smartHoles imports (mod, mods) (tyName, conName', index, tyDef) actions =
+  runReaderT
+    go
+    (buildTypingContextFromModules (mod : mods <> imports) smartHoles)
+    & runExceptT
+  where
+    go :: ActionM m => m ([Module], TypeZ)
+    go = do
+      (valCons, zt) <-
+        (maybe (throwError $ InternalFailure "applyActionsToField: con name not found") pure =<<) $
+          flip (findAndAdjustA' ((== conName') . valConName)) (astTypeDefConstructors tyDef) \(ValCon _ ts) -> do
+            (t, zt) <-
+              maybe (throwError $ InternalFailure "applyActionsToField: con field index out of bounds") pure
+                =<< flip (adjustAtA' index) ts \fieldType -> do
+                  zt <- withWrappedType fieldType \zt ->
+                    foldlM (\l -> local addParamsToCxt . flip applyActionAndSynth l) (InType zt) actions
+                  pure (target (top zt), zt)
+            pure (ValCon conName' t, zt)
+      let mod' = mod{moduleTypes = insert tyName (TypeDefAST tyDef{astTypeDefConstructors = valCons}) $ moduleTypes mod}
+      (,zt) <$> checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods})
+    addParamsToCxt :: TC.Cxt -> TC.Cxt
+    addParamsToCxt = over #localCxt (<> Map.fromList (map (bimap unLocalName TC.K) $ astTypeDefParameters tyDef))
+    withWrappedType :: ActionM m => Type -> (TypeZ -> m Loc) -> m TypeZ
+    withWrappedType ty f = do
+      wrappedType <- ann emptyHole (pure ty)
+      let unwrapError = throwError $ InternalFailure "applyActionsToField: failed to unwrap type"
+          wrapError = throwError $ InternalFailure "applyActionsToField: failed to wrap type"
+          focusedType = focusType $ focus wrappedType
+      case focusedType of
+        Nothing -> wrapError
+        Just wrappedTy ->
+          f wrappedTy >>= \case
+            InType zt -> pure zt
+            z -> maybe unwrapError pure (focusType (unfocusLoc z))
+
 data Refocus = Refocus
   { pre :: Loc
   , post :: Expr
@@ -857,13 +915,13 @@ renameForall b zt = case target zt of
 
 -- | Convert a high-level 'Available.NoInputAction' to a concrete sequence of 'ProgAction's.
 toProgActionNoInput ::
+  (HasID a, Data a) =>
   DefMap ->
-  ASTDef ->
-  GVarName ->
-  Maybe (NodeType, ID) ->
+  Either (ASTTypeDef a) ASTDef ->
+  Selection' ID ->
   Available.NoInputAction ->
   Either ActionError [ProgAction]
-toProgActionNoInput defs def defName mNodeSel = \case
+toProgActionNoInput defs def0 sel0 = \case
   Available.MakeCase ->
     toProgAction [ConstructCase]
   Available.MakeApp ->
@@ -877,8 +935,9 @@ toProgActionNoInput defs def defName mNodeSel = \case
   Available.LetToRec ->
     toProgAction [ConvertLetToLetrec]
   Available.Raise -> do
-    id <- mid
-    pure [MoveToDef defName, CopyPasteBody (defName, id) [SetCursor id, Move Parent, Delete]]
+    id <- nodeID
+    sel <- termSel
+    pure [MoveToDef sel.def, CopyPasteBody (sel.def, id) [SetCursor id, Move Parent, Delete]]
   Available.EnterHole ->
     toProgAction [EnterHole]
   Available.RemoveHole ->
@@ -890,17 +949,27 @@ toProgActionNoInput defs def defName mNodeSel = \case
     -- on the domain (left) side of the arrow.
     toProgAction [ConstructArrowL, Move Child1]
   Available.AddInput -> do
-    -- This action traverses the function type and adds a function arrow to the end of it,
-    -- resulting in a new argument type. The result type is unchanged.
-    -- The cursor location is also unchanged.
-    -- e.g. A -> B -> C ==> A -> B -> ? -> C
-    id <- mid
-    type_ <- case findType id $ astDefType def of
-      Just t -> pure t
-      Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of
-        Just (TypeNode t) -> pure t
-        Just sm -> Left $ NeedType sm
-        Nothing -> Left $ IDNotFound id
+    type_ <- case def0 of
+      Left def -> do
+        (tName, vcName, field) <- conFieldSel
+        let id = field.meta
+        vc <- maybeToEither (ValConNotFound tName vcName) $ find ((== vcName) . valConName) $ astTypeDefConstructors def
+        t <- maybeToEither (FieldIndexOutOfBounds vcName field.index) $ flip atMay field.index $ valConArgs vc
+        case findType id t of
+          Just t' -> pure $ forgetTypeMetadata t'
+          Nothing -> Left $ IDNotFound id
+      Right def -> do
+        -- This action traverses the function type and adds a function arrow to the end of it,
+        -- resulting in a new argument type. The result type is unchanged.
+        -- The cursor location is also unchanged.
+        -- e.g. A -> B -> C ==> A -> B -> ? -> C
+        id <- nodeID
+        forgetTypeMetadata <$> case findType id $ astDefType def of
+          Just t -> pure t
+          Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of
+            Just (TypeNode t) -> pure t
+            Just sm -> Left $ NeedType sm
+            Nothing -> Left $ IDNotFound id
     l <- case type_ of
       TFun _ a b -> pure $ NE.length $ fst $ unfoldFun a b
       t -> Left $ NeedTFun t
@@ -910,35 +979,72 @@ toProgActionNoInput defs def defName mNodeSel = \case
   Available.MakeTApp ->
     toProgAction [ConstructTApp, Move Child1]
   Available.RaiseType -> do
-    id <- mid
-    pure [MoveToDef defName, CopyPasteSig (defName, id) [SetCursor id, Move Parent, Delete]]
+    id <- nodeID
+    sel <- termSel
+    pure [MoveToDef sel.def, CopyPasteSig (sel.def, id) [SetCursor id, Move Parent, Delete]]
   Available.DeleteType ->
     toProgAction [Delete]
-  Available.DuplicateDef ->
+  Available.DuplicateDef -> do
+    sel <- termSel
+    def <- termDef
     let sigID = getID $ astDefType def
         bodyID = getID $ astDefExpr def
-        copyName = uniquifyDefName (qualifiedModule defName) (unName (baseName defName) <> "Copy") defs
+        copyName = uniquifyDefName (qualifiedModule sel.def) (unName (baseName sel.def) <> "Copy") defs
      in pure
-          [ CreateDef (qualifiedModule defName) (Just copyName)
-          , CopyPasteSig (defName, sigID) []
-          , CopyPasteBody (defName, bodyID) []
+          [ CreateDef (qualifiedModule sel.def) (Just copyName)
+          , CopyPasteSig (sel.def, sigID) []
+          , CopyPasteBody (sel.def, bodyID) []
           ]
-  Available.DeleteDef ->
-    pure [DeleteDef defName]
+  Available.DeleteDef -> do
+    sel <- termSel
+    pure [DeleteDef sel.def]
+  Available.AddConField -> do
+    (defName, sel) <- conSel
+    d <- typeDef
+    vc <-
+      maybe (Left $ ValConNotFound defName sel.con) pure
+        . find ((== sel.con) . valConName)
+        $ astTypeDefConstructors d
+    let index = length $ valConArgs vc -- for now, we always add on to the end
+    pure [AddConField defName sel.con index $ TEmptyHole ()]
   where
-    toProgAction actions = toProg' actions defName <$> maybeToEither NoNodeSelection mNodeSel
-    mid = maybeToEither NoNodeSelection $ snd <$> mNodeSel
+    termSel = case sel0 of
+      SelectionDef s -> pure s
+      SelectionTypeDef _ -> Left NeedTermDefSelection
+    nodeID = do
+      sel <- termSel
+      maybeToEither NoNodeSelection $ (.meta) <$> sel.node
+    typeSel = case sel0 of
+      SelectionDef _ -> Left NeedTypeDefSelection
+      SelectionTypeDef s -> pure s
+    typeNodeSel = do
+      sel <- typeSel
+      maybe (Left NeedTypeDefNodeSelection) (pure . (sel.def,)) sel.node
+    conSel =
+      typeNodeSel >>= \case
+        (s0, TypeDefConsNodeSelection s) -> pure (s0, s)
+        _ -> Left NeedTypeDefConsSelection
+    conFieldSel = do
+      (ty, s) <- conSel
+      maybe (Left NeedTypeDefConsFieldSelection) (pure . (ty,s.con,)) s.field
+    toProgAction actions = do
+      case sel0 of
+        SelectionDef sel -> toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node
+        SelectionTypeDef _ -> do
+          (t, c, f) <- conFieldSel
+          pure [ConFieldAction t c f.index $ SetCursor f.meta : actions]
+    termDef = first (const NeedTermDef) def0
+    typeDef = either Right (Left . const NeedTypeDef) def0
 
 -- | Convert a high-level 'Available.InputAction', and associated 'Available.Option',
 -- to a concrete sequence of 'ProgAction's.
 toProgActionInput ::
-  ASTDef ->
-  GVarName ->
-  Maybe (NodeType, ID) ->
+  Either (ASTTypeDef a) ASTDef ->
+  Selection' ID ->
   Available.Option ->
   Available.InputAction ->
   Either ActionError [ProgAction]
-toProgActionInput def defName mNodeSel opt0 = \case
+toProgActionInput def0 sel0 opt0 = \case
   Available.MakeCon -> do
     opt <- optGlobal
     toProg [ConstructSaturatedCon opt]
@@ -994,9 +1100,49 @@ toProgActionInput def defName mNodeSel opt0 = \case
     toProg [RenameForall opt]
   Available.RenameDef -> do
     opt <- optNoCxt
-    pure [RenameDef defName opt]
+    sel <- termSel
+    pure [RenameDef sel.def opt]
+  Available.RenameType -> do
+    opt <- optNoCxt
+    td <- typeSel
+    pure [RenameType td.def opt]
+  Available.RenameCon -> do
+    opt <- optNoCxt
+    (defName, sel) <- conSel
+    pure [RenameCon defName sel.con opt]
+  Available.RenameTypeParam -> do
+    opt <- optNoCxt
+    (defName, sel) <- typeParamSel
+    pure [RenameTypeParam defName sel opt]
+  Available.AddCon -> do
+    opt <- optNoCxt
+    sel <- typeSel
+    d <- typeDef
+    let index = length $ astTypeDefConstructors d -- for now, we always add on the end
+    pure [AddCon sel.def index opt]
   where
-    mid = maybeToEither NoNodeSelection $ snd <$> mNodeSel
+    termSel = case sel0 of
+      SelectionDef s -> pure s
+      SelectionTypeDef _ -> Left NeedTermDefSelection
+    nodeID = do
+      sel <- termSel
+      maybeToEither NoNodeSelection $ (.meta) <$> sel.node
+    typeSel = case sel0 of
+      SelectionDef _ -> Left NeedTypeDefSelection
+      SelectionTypeDef s -> pure s
+    typeNodeSel = do
+      sel <- typeSel
+      maybe (Left NeedTypeDefNodeSelection) (pure . (sel.def,)) sel.node
+    typeParamSel =
+      typeNodeSel >>= \case
+        (s0, TypeDefParamNodeSelection s) -> pure (s0, s)
+        _ -> Left NeedTypeDefParamSelection
+    conSel =
+      typeNodeSel >>= \case
+        (s0, TypeDefConsNodeSelection s) -> pure (s0, s)
+        _ -> Left NeedTypeDefConsSelection
+    termDef = first (const NeedTermDef) def0
+    typeDef = either Right (Left . const NeedTypeDef) def0
     optVar = case opt0.context of
       Just q -> GlobalVarRef $ unsafeMkGlobalName (q, opt0.option)
       Nothing -> LocalVarRef $ unsafeMkLocalName opt0.option
@@ -1009,9 +1155,18 @@ toProgActionInput def defName mNodeSel opt0 = \case
     optGlobal = case opt0.context of
       Nothing -> Left $ NeedLocal opt0
       Just q -> pure (q, opt0.option)
-    toProg actions = toProg' actions defName <$> maybeToEither NoNodeSelection mNodeSel
+    conFieldSel = do
+      (ty, s) <- conSel
+      maybe (Left NeedTypeDefConsFieldSelection) (pure . (ty,s.con,)) s.field
+    toProg actions = do
+      case sel0 of
+        SelectionDef sel -> toProg' actions sel.def <$> maybeToEither NoNodeSelection sel.node
+        SelectionTypeDef _ -> do
+          (t, c, f) <- conFieldSel
+          pure [ConFieldAction t c f.index $ SetCursor f.meta : actions]
     offerRefined = do
-      id <- mid
+      id <- nodeID
+      def <- termDef
       -- If we have a useful type, offer the refine action, otherwise offer the saturate action.
       case findNodeWithParent id $ astDefExpr def of
         Just (ExprNode e, _) -> pure $ case e ^. _exprMetaLens ^? _type % _Just % _chkedAt of
@@ -1022,10 +1177,10 @@ toProgActionInput def defName mNodeSel opt0 = \case
         Just (sm, _) -> Left $ NeedType sm
         Nothing -> Left $ IDNotFound id
 
-toProg' :: [Action] -> GVarName -> (NodeType, ID) -> [ProgAction]
-toProg' actions defName (nt, id) =
+toProg' :: [Action] -> GVarName -> NodeSelection ID -> [ProgAction]
+toProg' actions defName sel =
   [ MoveToDef defName
-  , (SetCursor id : actions) & case nt of
+  , (SetCursor sel.meta : actions) & case sel.nodeType of
       SigNode -> SigAction
       BodyNode -> BodyAction
   ]
diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs
index 278aada79..245b0fd59 100644
--- a/primer/src/Primer/Action/Available.hs
+++ b/primer/src/Primer/Action/Available.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE NoFieldSelectors #-}
 
 -- | Compute all the possible actions which can be performed on a definition.
@@ -14,10 +15,15 @@ module Primer.Action.Available (
   FreeInput (..),
   Options (..),
   options,
+  forTypeDef,
+  forTypeDefParamNode,
+  forTypeDefConsNode,
+  forTypeDefConsFieldNode,
 ) where
 
 import Foreword
 
+import Data.Either.Extra (eitherToMaybe)
 import Data.Map qualified as Map
 import Data.Set qualified as Set
 import Data.Tuple.Extra (fst3)
@@ -31,9 +37,17 @@ import Optics (
  )
 import Primer.Action.Priorities qualified as P
 import Primer.App.Base (
+  DefSelection (..),
   Editable (..),
   Level (..),
+  NodeSelection (..),
   NodeType (..),
+  Selection' (..),
+  TypeDefConsFieldSelection (..),
+  TypeDefConsSelection (..),
+  TypeDefNodeSelection (..),
+  TypeDefSelection (..),
+  getTypeDefConFieldType,
  )
 import Primer.Core (
   Expr,
@@ -44,6 +58,8 @@ import Primer.Core (
   ModuleName (unModuleName),
   Type,
   Type' (..),
+  TypeMeta,
+  ValConName,
   getID,
   unLocalName,
   _bindMeta,
@@ -89,6 +105,7 @@ import Primer.Zipper (
   focusOn,
   focusOnTy,
   locToEither,
+  target,
  )
 
 -- | An offered action.
@@ -117,6 +134,7 @@ data NoInputAction
   | DeleteType
   | DuplicateDef
   | DeleteDef
+  | AddConField
   deriving stock (Eq, Ord, Show, Read, Enum, Bounded, Generic)
   deriving (ToJSON, FromJSON) via PrimerJSON NoInputAction
 
@@ -140,6 +158,10 @@ data InputAction
   | MakeForall
   | RenameForall
   | RenameDef
+  | RenameType
+  | RenameCon
+  | RenameTypeParam
+  | AddCon
   deriving stock (Eq, Ord, Show, Read, Enum, Bounded, Generic)
   deriving (ToJSON, FromJSON) via PrimerJSON InputAction
 
@@ -285,6 +307,54 @@ forType l type_ =
           ]
     delete = [NoInput DeleteType]
 
+forTypeDef ::
+  Level ->
+  Editable ->
+  [Action]
+forTypeDef _ NonEditable = mempty
+forTypeDef l Editable =
+  sortByPriority
+    l
+    [ Input RenameType
+    , Input AddCon
+    ]
+
+forTypeDefParamNode ::
+  Level ->
+  Editable ->
+  [Action]
+forTypeDefParamNode _ NonEditable = mempty
+forTypeDefParamNode l Editable =
+  sortByPriority
+    l
+    [ Input RenameTypeParam
+    ]
+
+forTypeDefConsNode ::
+  Level ->
+  Editable ->
+  [Action]
+forTypeDefConsNode _ NonEditable = mempty
+forTypeDefConsNode l Editable =
+  sortByPriority
+    l
+    [ NoInput AddConField
+    , Input RenameCon
+    ]
+
+forTypeDefConsFieldNode ::
+  Level ->
+  Editable ->
+  ASTTypeDef TypeMeta ->
+  ValConName ->
+  Int ->
+  ID ->
+  [Action]
+forTypeDefConsFieldNode _ NonEditable _ _ _ _ = mempty
+forTypeDefConsFieldNode l Editable def con index id =
+  maybe mempty (sortByPriority l . forType l) $
+    findType id =<< getTypeDefConFieldType def con index
+
 -- | An input for an 'InputAction'.
 data Option = Option
   { option :: Text
@@ -319,13 +389,13 @@ options ::
   DefMap ->
   Cxt ->
   Level ->
-  ASTDef ->
-  Maybe (NodeType, ID) ->
+  Either (ASTTypeDef TypeMeta) ASTDef ->
+  Selection' ID ->
   InputAction ->
   -- | Returns 'Nothing' if an ID was required but not passed, passed but not found in the tree,
   -- or found but didn't correspond to the expected sort of entity (type/expr/pattern).
   Maybe Options
-options typeDefs defs cxt level def mNodeSel = \case
+options typeDefs defs cxt level def0 sel0 = \case
   MakeCon ->
     pure
       . noFree
@@ -380,6 +450,14 @@ options typeDefs defs cxt level def mNodeSel = \case
     freeVar <$> genNames (Right $ Just k)
   RenameDef ->
     pure $ freeVar []
+  RenameType ->
+    pure $ freeVar []
+  RenameCon ->
+    pure $ freeVar []
+  RenameTypeParam ->
+    pure $ freeVar []
+  AddCon ->
+    pure $ freeVar []
   where
     freeVar opts = Options{opts, free = FreeVarName}
     noFree opts = Options{opts, free = FreeNone}
@@ -394,24 +472,47 @@ options typeDefs defs cxt level def mNodeSel = \case
       pure $
         (first (localOpt . unLocalName) <$> locals)
           <> (first globalOpt <$> globals)
-    findNode = do
-      (nt, id) <- mNodeSel
-      case nt of
-        BodyNode -> fst <$> findNodeWithParent id (astDefExpr def)
-        SigNode -> TypeNode <$> findType id (astDefType def)
-    genNames typeOrKind = do
-      z <- focusNode =<< mNodeSel
-      pure $ map localOpt $ flip runReader cxt $ case z of
-        Left zE -> generateNameExpr typeOrKind zE
-        Right zT -> generateNameTy typeOrKind zT
-    varsInScope = do
-      nodeSel <- mNodeSel
-      focusNode nodeSel <&> \case
-        Left zE -> variablesInScopeExpr defs zE
-        Right zT -> (variablesInScopeTy zT, [], [])
-    focusNode (nt, id) = case nt of
-      BodyNode -> Left . locToEither <$> focusOn id (astDefExpr def)
-      SigNode -> fmap Right $ focusOnTy id $ astDefType def
+    findNode = case sel0 of
+      SelectionDef sel -> do
+        nodeSel <- sel.node
+        def <- eitherToMaybe def0
+        case nodeSel.nodeType of
+          BodyNode -> fst <$> findNodeWithParent nodeSel.meta (astDefExpr def)
+          SigNode -> TypeNode <$> findType nodeSel.meta (astDefType def)
+      SelectionTypeDef sel -> do
+        (_, zT) <- conField sel
+        pure $ TypeNode $ target zT
+    genNames typeOrKind =
+      map localOpt . flip runReader cxt <$> case sel0 of
+        SelectionDef sel -> do
+          z <- focusNode =<< sel.node
+          pure $ case z of
+            Left zE -> generateNameExpr typeOrKind zE
+            Right zT -> generateNameTy typeOrKind zT
+        SelectionTypeDef sel -> do
+          (_, zT) <- conField sel
+          pure $ generateNameTy typeOrKind zT
+    varsInScope = case sel0 of
+      SelectionDef sel -> do
+        nodeSel <- sel.node
+        focusNode nodeSel <&> \case
+          Left zE -> variablesInScopeExpr defs zE
+          Right zT -> (variablesInScopeTy zT, [], [])
+      SelectionTypeDef sel -> do
+        (def, zT) <- conField sel
+        pure (astTypeDefParameters def <> variablesInScopeTy zT, [], [])
+    focusNode nodeSel = do
+      def <- eitherToMaybe def0
+      case nodeSel.nodeType of
+        BodyNode -> Left . locToEither <$> focusOn nodeSel.meta (astDefExpr def)
+        SigNode -> fmap Right $ focusOnTy nodeSel.meta $ astDefType def
+    conField sel = do
+      (con, field) <- case sel of
+        TypeDefSelection _ (Just (TypeDefConsNodeSelection (TypeDefConsSelection con (Just field)))) ->
+          Just (con, field)
+        _ -> Nothing
+      def <- either Just (const Nothing) def0
+      map (def,) $ focusOnTy field.meta =<< getTypeDefConFieldType def con field.index
     -- Extract the source of the function type we were checked at
     -- i.e. the type that a lambda-bound variable would have here
     lamVarTy = \case
@@ -455,6 +556,7 @@ sortByPriority l =
         DeleteType -> P.delete
         DuplicateDef -> P.duplicate
         DeleteDef -> P.delete
+        AddConField -> P.addConField
       Input a -> case a of
         MakeCon -> P.useSaturatedValueCon
         MakeInt -> P.makeInt
@@ -474,3 +576,7 @@ sortByPriority l =
         MakeForall -> P.constructForall
         RenameForall -> P.rename
         RenameDef -> P.rename
+        RenameType -> P.rename
+        AddCon -> P.addCon
+        RenameCon -> P.rename
+        RenameTypeParam -> P.rename
diff --git a/primer/src/Primer/Action/Errors.hs b/primer/src/Primer/Action/Errors.hs
index 9e6d705c4..64f4fdb40 100644
--- a/primer/src/Primer/Action/Errors.hs
+++ b/primer/src/Primer/Action/Errors.hs
@@ -13,7 +13,7 @@ import Data.Aeson (FromJSON (..), ToJSON (..))
 import Primer.Action.Actions (Action)
 import Primer.Action.Available qualified as Available
 import Primer.Action.Movement (Movement)
-import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, Type)
+import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, TyConName, Type', ValConName)
 import Primer.JSON (CustomJSON (..), PrimerJSON)
 import Primer.Typecheck.TypeError (TypeError)
 import Primer.Zipper (SomeNode)
@@ -57,12 +57,22 @@ data ActionError
     -- The extra unit is to avoid having two constructors with a single
     -- TypeError field, breaking our MonadNestedError machinery...
     ImportFailed () TypeError
-  | NeedTFun Type
+  | NeedTFun (Type' ())
   | NeedType SomeNode
   | NeedGlobal Available.Option
   | NeedLocal Available.Option
   | NeedInt Available.Option
   | NeedChar Available.Option
+  | NeedTermDef
+  | NeedTypeDef
+  | NeedTermDefSelection
+  | NeedTypeDefSelection
+  | NeedTypeDefNodeSelection
+  | NeedTypeDefConsSelection
+  | NeedTypeDefConsFieldSelection
+  | NeedTypeDefParamSelection
   | NoNodeSelection
+  | ValConNotFound TyConName ValConName
+  | FieldIndexOutOfBounds ValConName Int
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON ActionError
diff --git a/primer/src/Primer/Action/Priorities.hs b/primer/src/Primer/Action/Priorities.hs
index 12d09c847..bbc84293c 100644
--- a/primer/src/Primer/Action/Priorities.hs
+++ b/primer/src/Primer/Action/Priorities.hs
@@ -55,6 +55,10 @@ module Primer.Action.Priorities (
   constructTypeApp,
   constructForall,
 
+  -- * Type def actions.
+  addCon,
+  addConField,
+
   -- * Generic actions.
   rename,
   duplicate,
@@ -146,3 +150,9 @@ raise _ = 300
 
 delete :: Level -> Int
 delete _ = maxBound
+
+addCon :: Level -> Int
+addCon _ = 10
+
+addConField :: Level -> Int
+addConField _ = 10
diff --git a/primer/src/Primer/Action/ProgAction.hs b/primer/src/Primer/Action/ProgAction.hs
index 47653b24e..e278ec36b 100644
--- a/primer/src/Primer/Action/ProgAction.hs
+++ b/primer/src/Primer/Action/ProgAction.hs
@@ -47,6 +47,8 @@ data ProgAction
     BodyAction [Action]
   | -- | Execute a sequence of actions on the type annotation of the definition
     SigAction [Action]
+  | -- | Execute a sequence of actions on the type of a field of a constructor in a typedef
+    ConFieldAction TyConName ValConName Int [Action]
   | SetSmartHoles SmartHoles
   | -- | CopyPaste (d,i) as
     --   remembers the tree in def d, node i
diff --git a/primer/src/Primer/Action/ProgError.hs b/primer/src/Primer/Action/ProgError.hs
index a2fa35c27..fe90e21cf 100644
--- a/primer/src/Primer/Action/ProgError.hs
+++ b/primer/src/Primer/Action/ProgError.hs
@@ -7,10 +7,10 @@ import Primer.Action.Errors (ActionError)
 import Primer.Core.Meta (GVarName, ModuleName, TyConName, TyVarName, ValConName)
 import Primer.Eval.EvalError (EvalError)
 import Primer.JSON (CustomJSON (..), PrimerJSON)
-import Primer.Name (Name)
 
 data ProgError
   = NoDefSelected
+  | NoTypeDefSelected
   | DefNotFound GVarName
   | DefAlreadyExists GVarName
   | DefInUse GVarName
@@ -24,8 +24,6 @@ data ProgError
     ConNotSaturated ValConName
   | ParamNotFound TyVarName
   | ParamAlreadyExists TyVarName
-  | TyConParamClash Name
-  | ValConParamClash Name
   | ActionError ActionError
   | EvalError EvalError
   | -- | Currently copy/paste is only exposed in the frontend via select
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 2a879b779..6339bb5be 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -1,5 +1,8 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE ViewPatterns #-}
 
 -- This module defines the high level application functions.
@@ -31,6 +34,7 @@ module Primer.App (
   progAllModules,
   progAllDefs,
   progAllTypeDefs,
+  progAllTypeDefsMeta,
   allValConNames,
   allTyConNames,
   progCxt,
@@ -48,8 +52,6 @@ module Primer.App (
   handleEvalFullRequest,
   importModules,
   MutationRequest (..),
-  Selection (..),
-  NodeSelection (..),
   EvalReq (..),
   EvalResp (..),
   EvalFullReq (..),
@@ -78,7 +80,6 @@ import Optics (
   Field3 (_3),
   ReversibleOptic (re),
   ifoldMap,
-  lens,
   mapped,
   over,
   set,
@@ -90,6 +91,7 @@ import Optics (
   (.~),
   (?~),
   (^.),
+  (^?),
   _Just,
   _Left,
   _Right,
@@ -101,13 +103,23 @@ import Primer.Action (
   ProgAction (..),
   applyAction',
   applyActionsToBody,
+  applyActionsToField,
   applyActionsToTypeSig,
  )
 import Primer.Action.ProgError (ProgError (..))
 import Primer.App.Base (
+  DefSelection (..),
   Editable (..),
   Level (..),
+  NodeSelection (..),
   NodeType (..),
+  Selection,
+  Selection' (..),
+  TypeDefConsFieldSelection (..),
+  TypeDefConsSelection (..),
+  TypeDefNodeSelection (..),
+  TypeDefSelection (..),
+  getTypeDefConFieldType,
  )
 import Primer.Core (
   Bind' (Bind),
@@ -115,11 +127,10 @@ import Primer.Core (
   CaseBranch' (CaseBranch),
   Expr,
   Expr' (Case, Con, EmptyHole, Hole, Var),
-  ExprMeta,
   GVarName,
   GlobalName (baseName, qualifiedModule),
-  HasID (_id),
   ID (..),
+  Kind (KType),
   LocalName (LocalName, unLocalName),
   Meta (..),
   ModuleName (ModuleName),
@@ -127,6 +138,8 @@ import Primer.Core (
   TyConName,
   Type,
   Type' (..),
+  TypeCache (..),
+  TypeCacheBoth (..),
   TypeMeta,
   ValConName,
   getID,
@@ -136,12 +149,16 @@ import Primer.Core (
   unModuleName,
   unsafeMkGlobalName,
   unsafeMkLocalName,
+  _chkedAt,
+  _exprMeta,
   _exprMetaLens,
+  _synthed,
+  _type,
   _typeMetaLens,
  )
-import Primer.Core.DSL (S, create, emptyHole, tEmptyHole, tvar)
+import Primer.Core.DSL (S, create, emptyHole, tEmptyHole)
 import Primer.Core.DSL qualified as DSL
-import Primer.Core.Transform (renameVar, unfoldTApp)
+import Primer.Core.Transform (renameTyVar, renameVar, unfoldTApp)
 import Primer.Core.Utils (freeVars, generateTypeIDs, regenerateExprIDs, regenerateTypeIDs, _freeTmVars, _freeTyVars, _freeVarsTy)
 import Primer.Def (
   ASTDef (..),
@@ -163,6 +180,7 @@ import Primer.Module (
   insertDef,
   moduleDefsQualified,
   moduleTypesQualified,
+  moduleTypesQualifiedMeta,
   nextModuleID,
   primitiveModule,
   qualifyDefName,
@@ -194,7 +212,6 @@ import Primer.Typecheck (
   buildTypingContextFromModules,
   checkEverything,
   checkTypeDefs,
-  synth,
  )
 import Primer.Typecheck qualified as TC
 import Primer.Zipper (
@@ -273,6 +290,11 @@ progAllTypeDefs p =
   foldMap' (fmap (Editable,) . moduleTypesQualified) (progModules p)
     <> foldMap' (fmap (NonEditable,) . moduleTypesQualified) (progImports p)
 
+progAllTypeDefsMeta :: Prog -> Map TyConName (Editable, TypeDef TypeMeta)
+progAllTypeDefsMeta p =
+  foldMap' (fmap (Editable,) . moduleTypesQualifiedMeta) (progModules p)
+    <> foldMap' (fmap (NonEditable,) . moduleTypesQualifiedMeta) (progImports p)
+
 progAllDefs :: Prog -> Map GVarName (Editable, Def)
 progAllDefs p =
   foldMap' (fmap (Editable,) . moduleDefsQualified) (progModules p)
@@ -325,11 +347,12 @@ newEmptyProgImporting imported =
               ]
           , progImports = imported'
           , progSelection =
-              Just
-                Selection
-                  { selectedDef = qualifyName moduleName defName
-                  , selectedNode = Nothing
-                  }
+              Just $
+                SelectionDef
+                  DefSelection
+                    { def = qualifyName moduleName defName
+                    , node = Nothing
+                    }
           }
       , nextID
       , toEnum 0
@@ -396,6 +419,9 @@ importModules ms = do
 allTypes :: Prog -> TypeDefMap
 allTypes = fmap snd . progAllTypeDefs
 
+allTypesMeta :: Prog -> Map TyConName (TypeDef TypeMeta)
+allTypesMeta = fmap snd . progAllTypeDefsMeta
+
 -- | Get all definitions from all modules (including imports)
 allDefs :: Prog -> DefMap
 allDefs = fmap snd . progAllDefs
@@ -415,33 +441,6 @@ newtype Log = Log {unlog :: [[ProgAction]]}
 defaultLog :: Log
 defaultLog = Log mempty
 
--- | Describes what interface element the user has selected.
--- A definition in the left hand nav bar, and possibly a node in that definition.
-data Selection = Selection
-  { selectedDef :: GVarName
-  -- ^ the ID of some ASTDef
-  , selectedNode :: Maybe NodeSelection
-  }
-  deriving stock (Eq, Show, Read, Generic, Data)
-  deriving (FromJSON, ToJSON) via PrimerJSON Selection
-  deriving anyclass (NFData)
-
--- | A selected node, in the body or type signature of some definition.
--- We have the following invariant: @nodeType = SigNode ==> isRight meta@
-data NodeSelection = NodeSelection
-  { nodeType :: NodeType
-  , meta :: Either ExprMeta TypeMeta
-  }
-  deriving stock (Eq, Show, Read, Generic, Data)
-  deriving (FromJSON, ToJSON) via PrimerJSON NodeSelection
-  deriving anyclass (NFData)
-
-instance HasID NodeSelection where
-  _id =
-    lens
-      (either getID getID . meta)
-      (flip $ \id -> over #meta $ bimap (set _id id) (set _id id))
-
 -- | The type of requests which can mutate the application state.
 data MutationRequest
   = Undo
@@ -552,7 +551,8 @@ handleEditRequest actions = do
     go :: (Prog, Maybe GVarName) -> ProgAction -> m (Prog, Maybe GVarName)
     go (prog, mdef) a =
       applyProgAction prog mdef a <&> \prog' ->
-        (prog', selectedDef <$> progSelection prog')
+        -- TODO this ignores any selection from a type def selection
+        (prog', (.def) <$> ((\case SelectionDef s -> Just s; _ -> Nothing) =<< progSelection prog'))
 
 -- | Handle an eval request (we assume that all such requests are implicitly in a synthesisable context)
 handleEvalRequest ::
@@ -594,7 +594,7 @@ applyProgAction prog mdefName = \case
     m <- lookupEditableModule (qualifiedModule d) prog
     case Map.lookup d $ moduleDefsQualified m of
       Nothing -> throwError $ DefNotFound d
-      Just _ -> pure $ prog & #progSelection ?~ Selection d Nothing
+      Just _ -> pure $ prog & #progSelection ?~ SelectionDef (DefSelection d Nothing)
   DeleteDef d -> editModuleCross (qualifiedModule d) prog $ \(m, ms) ->
     case deleteDef m d of
       Nothing -> throwError $ DefNotFound d
@@ -617,7 +617,7 @@ applyProgAction prog mdefName = \case
               (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
               (renameVar (GlobalVarRef d) (GlobalVarRef newName))
               (m' : ms)
-        pure (renamedModules, Just $ Selection newName Nothing)
+        pure (renamedModules, Just $ SelectionDef $ DefSelection newName Nothing)
   CreateDef modName n -> editModule modName prog $ \mod -> do
     let defs = moduleDefs mod
     name <- case n of
@@ -631,12 +631,12 @@ applyProgAction prog mdefName = \case
     expr <- newExpr
     ty <- newType
     let def = ASTDef expr ty
-    pure (insertDef mod name $ DefAST def, Just $ Selection (qualifyName modName name) Nothing)
-  AddTypeDef tc td -> editModuleSameSelection (qualifiedModule tc) prog $ \m -> do
+    pure (insertDef mod name $ DefAST def, Just $ SelectionDef $ DefSelection (qualifyName modName name) Nothing)
+  AddTypeDef tc td -> editModule (qualifiedModule tc) prog $ \m -> do
     td' <- generateTypeDefIDs $ TypeDefAST td
     let tydefs' = moduleTypes m <> Map.singleton (baseName tc) td'
-    m{moduleTypes = tydefs'}
-      <$ liftError
+    void $
+      liftError
         -- The frontend should never let this error case happen,
         -- so we just dump out a raw string for debugging/logging purposes
         -- (This is not currently true! We should synchronise the frontend with
@@ -646,14 +646,21 @@ applyProgAction prog mdefName = \case
         -- see https://github.com/hackworthltd/primer/issues/3)
         (TypeDefError . show @TypeError)
         ( runReaderT
-            (checkTypeDefs $ Map.singleton tc (TypeDefAST td))
+            (checkTypeDefs $ Map.singleton tc td')
             (buildTypingContextFromModules (progAllModules prog) NoSmartHoles)
         )
-  RenameType old (unsafeMkName -> nameRaw) -> editModuleSameSelectionCross (qualifiedModule old) prog $ \(m, ms) -> do
-    when (new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new
+    pure
+      ( m{moduleTypes = tydefs'}
+      , Just $ SelectionTypeDef $ TypeDefSelection tc Nothing
+      )
+  RenameType old (unsafeMkName -> nameRaw) -> editModuleCross (qualifiedModule old) prog $ \(m, ms) -> do
+    when (new /= old && new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new
     m' <- traverseOf #moduleTypes updateType m
     let renamedInTypes = over (traversed % #moduleTypes) updateRefsInTypes $ m' : ms
-    pure $ over (traversed % #moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) renamedInTypes
+    pure
+      ( over (traversed % #moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) renamedInTypes
+      , Just $ SelectionTypeDef $ TypeDefSelection new Nothing
+      )
     where
       new = qualifyName (qualifiedModule old) nameRaw
       updateType m = do
@@ -662,31 +669,33 @@ applyProgAction prog mdefName = \case
           -- To relax this, we'd have to be careful about how it interacts with type-checking of primitive literals.
           maybe (throwError $ TypeDefIsPrim old) pure . typeDefAST
             =<< maybe (throwError $ TypeDefNotFound old) pure (Map.lookup (baseName old) m)
-        when (nameRaw `elem` map (unLocalName . fst) (astTypeDefParameters d0)) $ throwError $ TyConParamClash nameRaw
         pure $ Map.insert nameRaw (TypeDefAST d0) $ Map.delete (baseName old) m
       updateRefsInTypes =
         over
           (traversed % #_TypeDefAST % #astTypeDefConstructors % traversed % #valConArgs % traversed)
-          $ transform
-          $ over (#_TCon % _2) updateName
-      updateDefType =
-        over
-          #astDefType
-          $ transform
-          $ over (#_TCon % _2) updateName
+          updateType'
+      updateDefType = over #astDefType updateType'
       updateDefBody =
         over
           #astDefExpr
           $ transform
-          $ over typesInExpr
-          $ transform
-          $ over (#_TCon % _2) updateName
+            ( over typesInExpr updateType'
+                . over (_exprMeta % _type % _Just) \case
+                  TCSynthed t -> TCSynthed $ updateType' t
+                  TCChkedAt t -> TCChkedAt $ updateType' t
+                  TCEmb (TCBoth t1 t2) -> TCEmb (TCBoth (updateType' t1) (updateType' t2))
+            )
       updateName n = if n == old then new else n
+      updateType' :: Data a => Type' a -> Type' a
+      updateType' = transform $ over (#_TCon % _2) updateName
   RenameCon type_ old (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> new) ->
-    editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do
+    editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do
       when (new `elem` allValConNames prog) $ throwError $ ConAlreadyExists new
       m' <- updateType m
-      pure $ over (mapped % #moduleDefs) updateDefs (m' : ms)
+      pure
+        ( over (mapped % #moduleDefs) updateDefs (m' : ms)
+        , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection new Nothing
+        )
     where
       updateType =
         alterTypeDef
@@ -704,7 +713,12 @@ applyProgAction prog mdefName = \case
               . over (#_Case % _3 % traversed % #_CaseBranch % _1) updateName
       updateName n = if n == old then new else n
   RenameTypeParam type_ old (unsafeMkLocalName -> new) ->
-    editModuleSameSelection (qualifiedModule type_) prog updateType
+    editModule (qualifiedModule type_) prog $ \m -> do
+      m' <- updateType m
+      pure
+        ( m'
+        , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefParamNodeSelection new
+        )
     where
       updateType =
         alterTypeDef
@@ -712,9 +726,6 @@ applyProgAction prog mdefName = \case
           type_
       updateParam def = do
         when (new `elem` map fst (astTypeDefParameters def)) $ throwError $ ParamAlreadyExists new
-        let nameRaw = unLocalName new
-        when (nameRaw == baseName type_) $ throwError $ TyConParamClash nameRaw
-        when (nameRaw `elem` map (baseName . valConName) (astTypeDefConstructors def)) $ throwError $ ValConParamClash nameRaw
         def
           & traverseOf
             #astTypeDefParameters
@@ -728,20 +739,23 @@ applyProgAction prog mdefName = \case
               % #valConArgs
               % traversed
           )
-          $ traverseOf _freeVarsTy
-          $ \(_, v) -> tvar $ updateName v
-      updateName n = if n == old then new else n
+          $ maybe (throwError $ ActionError NameCapture) pure . renameTyVar old new
   AddCon type_ index (unsafeMkGlobalName . (fmap unName (unModuleName (qualifiedModule type_)),) -> con) ->
-    editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do
+    editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do
       when (con `elem` allValConNames prog) $ throwError $ ConAlreadyExists con
       m' <- updateType m
-      traverseOf
-        (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
-        updateDefs
-        $ m' : ms
+      ms' <-
+        traverseOf
+          (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
+          updateDefs
+          $ m' : ms
+      pure
+        ( ms'
+        , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing
+        )
     where
-      updateDefs = transformCaseBranches prog type_ $ \bs -> do
-        m' <- DSL.meta
+      updateDefs = transformCaseBranches prog type_ $ \t' bs -> do
+        m' <- DSL.meta' $ (\t'' -> TCEmb $ TCBoth{tcChkedAt = t'', tcSynthed = TEmptyHole ()}) <$> t'
         maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (CaseBranch con [] (EmptyHole m')) bs
       updateType =
         alterTypeDef
@@ -795,62 +809,80 @@ applyProgAction prog mdefName = \case
                   Nothing -> throwError $ ConNotSaturated con
               e -> pure e
       updateDecons = transformCaseBranches prog type_ $
-        traverse $ \cb@(CaseBranch vc binds e) ->
-          if vc == con
-            then do
-              Bind _ v <- maybe (throwError $ IndexOutOfRange index) pure $ binds !? index
-              CaseBranch vc binds
-                <$>
-                -- TODO a custom traversal could be more efficient - reusing `_freeTmVars` means that we continue in
-                -- to parts of the tree where `v` is shadowed, and thus where the traversal will never have any effect
-                traverseOf
-                  _freeTmVars
-                  ( \(m, v') ->
-                      if v' == v
-                        then Hole <$> DSL.meta <*> pure (Var m $ LocalVarRef v')
-                        else pure (Var m $ LocalVarRef v')
-                  )
-                  e
-            else pure cb
+        const $
+          traverse $ \cb@(CaseBranch vc binds e) ->
+            if vc == con
+              then do
+                Bind _ v <- maybe (throwError $ IndexOutOfRange index) pure $ binds !? index
+                CaseBranch vc binds
+                  <$>
+                  -- TODO a custom traversal could be more efficient - reusing `_freeTmVars` means that we continue in
+                  -- to parts of the tree where `v` is shadowed, and thus where the traversal will never have any effect
+                  traverseOf
+                    _freeTmVars
+                    ( \(m, v') ->
+                        if v' == v
+                          then Hole <$> DSL.meta <*> pure (Var m $ LocalVarRef v')
+                          else pure (Var m $ LocalVarRef v')
+                    )
+                    e
+              else pure cb
   AddConField type_ con index new ->
-    editModuleSameSelectionCross (qualifiedModule type_) prog $ \(m, ms) -> do
+    editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do
       m' <- updateType m
-      traverseOf (traversed % #moduleDefs) updateDefs (m' : ms)
+      ms' <- traverseOf (traversed % #moduleDefs) updateDefs (m' : ms)
+      pure
+        ( ms'
+        , Just
+            . SelectionTypeDef
+            . TypeDefSelection type_
+            . Just
+            . TypeDefConsNodeSelection
+            . TypeDefConsSelection con
+            $ Nothing
+        )
     where
       updateType =
-        alterTypeDef
-          ( traverseOf #astTypeDefConstructors $
-              maybe (throwError $ ConNotFound con) pure
-                <=< findAndAdjustA
-                  ((== con) . valConName)
-                  ( traverseOf
-                      #valConArgs
-                      ( maybe (throwError $ IndexOutOfRange index) pure
-                          <=< liftA2 (insertAt index) (generateTypeIDs new) . pure
+        let new' =
+              runReaderT
+                (liftError (ActionError . TypeError) $ fmap TC.typeTtoType $ TC.checkKind KType =<< generateTypeIDs new)
+                (progCxt prog)
+         in alterTypeDef
+              ( traverseOf #astTypeDefConstructors $
+                  maybe (throwError $ ConNotFound con) pure
+                    <=< findAndAdjustA
+                      ((== con) . valConName)
+                      ( traverseOf
+                          #valConArgs
+                          ( maybe (throwError $ IndexOutOfRange index) pure
+                              <=< liftA2 (insertAt index) new' . pure
+                          )
                       )
-                  )
-          )
-          type_
+              )
+              type_
       -- NB: we must updateDecons first, as transformCaseBranches may do
       -- synthesis of the scrutinee's type, using the old typedef. Thus we must
       -- not update the scrutinee before this happens.
       updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons)
       updateCons = transformM $ \case
         Con m con' tms | con' == con -> do
-          m' <- DSL.meta
+          id <- fresh
+          let m' = Meta id (Just (TCEmb $ TCBoth (TEmptyHole ()) (TEmptyHole ()))) Nothing
           case insertAt index (EmptyHole m') tms of
             Just args' -> pure $ Con m con' args'
             Nothing -> throwError $ ConNotSaturated con
         e -> pure e
       updateDecons = transformCaseBranches prog type_ $
-        traverse $ \cb@(CaseBranch vc binds e) ->
-          if vc == con
-            then do
-              m' <- DSL.meta
-              newName <- LocalName <$> freshName (freeVars e)
-              binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds
-              pure $ CaseBranch vc binds' e
-            else pure cb
+        const $
+          traverse $ \cb@(CaseBranch vc binds e) ->
+            if vc == con
+              then do
+                id <- fresh
+                let m' = Meta id (Just (TCChkedAt (TEmptyHole ()))) Nothing
+                newName <- LocalName <$> freshName (freeVars e)
+                binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds
+                pure $ CaseBranch vc binds' e
+              else pure cb
   BodyAction actions -> editModuleOf mdefName prog $ \m defName def -> do
     let smartHoles = progSmartHoles prog
     res <- applyActionsToBody smartHoles (progAllModules prog) def actions
@@ -860,8 +892,8 @@ applyProgAction prog mdefName = \case
         let meta = bimap (view _exprMetaLens . target) (view _typeMetaLens . target) $ locToEither z
         pure
           ( insertDef m defName (DefAST def')
-          , Just $
-              Selection (qualifyDefName m defName) $
+          , Just . SelectionDef $
+              DefSelection (qualifyDefName m defName) $
                 Just
                   NodeSelection
                     { nodeType = BodyNode
@@ -878,14 +910,36 @@ applyProgAction prog mdefName = \case
             meta = view _typeMetaLens node
          in pure
               ( mod'
-              , Just $
-                  Selection (qualifyDefName curMod defName) $
+              , Just . SelectionDef $
+                  DefSelection (qualifyDefName curMod defName) $
                     Just
                       NodeSelection
                         { nodeType = SigNode
                         , meta = Right meta
                         }
               )
+  ConFieldAction tyName con index actions -> editModuleOfCrossType (Just tyName) prog $ \ms defName def -> do
+    let smartHoles = progSmartHoles prog
+    applyActionsToField smartHoles (progImports prog) ms (defName, con, index, def) actions >>= \case
+      Left err -> throwError $ ActionError err
+      Right (mod', _zt) ->
+        pure
+          ( mod'
+          , Just $
+              SelectionTypeDef
+                TypeDefSelection
+                  { def = tyName
+                  , node =
+                      Just $
+                        TypeDefConsNodeSelection
+                          TypeDefConsSelection
+                            { con
+                            , field =
+                                -- TODO if we set selection, we get weird metadata errors
+                                Nothing
+                            }
+                  }
+          )
   SetSmartHoles smartHoles ->
     pure $ prog & #progSmartHoles .~ smartHoles
   CopyPasteSig fromIds setup -> case mdefName of
@@ -1015,6 +1069,19 @@ editModuleOfCross mdefName prog f = case mdefName of
       Just (DefAST def) -> f ms (baseName defname) def
       _ -> throwError $ DefNotFound defname
 
+editModuleOfCrossType ::
+  MonadError ProgError m =>
+  Maybe TyConName ->
+  Prog ->
+  ((Module, [Module]) -> Name -> ASTTypeDef TypeMeta -> m ([Module], Maybe Selection)) ->
+  m Prog
+editModuleOfCrossType mdefName prog f = case mdefName of
+  Nothing -> throwError NoTypeDefSelected
+  Just defname -> editModuleCross (qualifiedModule defname) prog $ \ms@(m, _) ->
+    case Map.lookup (baseName defname) (moduleTypes m) of
+      Just (TypeDefAST def) -> f ms (baseName defname) def
+      _ -> throwError $ TypeDefNotFound defname
+
 -- | Undo the last block of actions.
 --
 -- If there are no actions in the log we return the program unchanged.
@@ -1345,7 +1412,7 @@ copyPasteSig p (fromDefName, fromTyId) toDefName setup = do
       _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
     let newDef = oldDef{astDefType = fromZipper pasted}
     let newSel = NodeSelection SigNode (pasted ^. _target % _typeMetaLens % re _Right)
-    pure (insertDef mod toDefBaseName (DefAST newDef), Just (Selection toDefName $ Just newSel))
+    pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel))
   liftError ActionError $ tcWholeProg finalProg
 
 -- We cannot use bindersAbove as that works on names only, and different scopes
@@ -1413,9 +1480,9 @@ tcWholeProg p = do
   let oldSel = progSelection p
   newSel <- case oldSel of
     Nothing -> pure Nothing
-    Just s -> do
-      let defName_ = s ^. #selectedDef
-      updatedNode <- case s ^. #selectedNode of
+    Just (SelectionDef s) -> do
+      let defName_ = s.def
+      updatedNode <- case s.node of
         Nothing -> pure Nothing
         Just sel@NodeSelection{nodeType} -> do
           n <- runExceptT $ focusNode p' defName_ $ getID sel
@@ -1424,11 +1491,23 @@ tcWholeProg p = do
             (SigNode, Right (Right x)) -> pure $ Just $ NodeSelection SigNode $ x ^. _target % _typeMetaLens % re _Right
             _ -> pure Nothing -- something's gone wrong: expected a SigNode, but found it in the body, or vv, or just not found it
       pure $
-        Just $
-          Selection
-            { selectedDef = defName_
-            , selectedNode = updatedNode
+        Just . SelectionDef $
+          DefSelection
+            { def = defName_
+            , node = updatedNode
             }
+    Just (SelectionTypeDef s) ->
+      pure . Just . SelectionTypeDef $
+        s & over (#node % mapped % #_TypeDefConsNodeSelection) \conSel ->
+          conSel & over #field \case
+            Nothing -> Nothing
+            Just fieldSel ->
+              flip (set #meta) fieldSel . (Right . (^. _typeMetaLens)) <$> do
+                -- If something goes wrong in finding the metadata, we just don't set a field selection.
+                -- This is similar to what we do when selection is in a term, above.
+                td <- Map.lookup s.def $ allTypesMeta p
+                tda <- typeDefAST td
+                getTypeDefConFieldType tda conSel.con fieldSel.index
   pure $ p'{progSelection = newSel}
 
 -- | Do a full check of a 'Prog', both the imports and the local modules
@@ -1500,7 +1579,7 @@ copyPasteBody p (fromDefName, fromId) toDefName setup = do
           _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
         let newDef = oldDef{astDefExpr = unfocusExpr $ unfocusType pasted}
         let newSel = NodeSelection BodyNode (pasted ^. _target % _typeMetaLens % re _Right)
-        pure (insertDef mod toDefBaseName (DefAST newDef), Just (Selection toDefName $ Just newSel))
+        pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel))
       (Left srcE, InExpr tgtE) -> do
         let sharedScope =
               if fromDefName == toDefName
@@ -1557,7 +1636,7 @@ copyPasteBody p (fromDefName, fromId) toDefName setup = do
           _ -> throwError $ CopyPasteError "copy/paste setup didn't select an empty hole"
         let newDef = oldDef{astDefExpr = unfocusExpr pasted}
         let newSel = NodeSelection BodyNode (pasted ^. _target % _exprMetaLens % re _Left)
-        pure (insertDef mod toDefBaseName (DefAST newDef), Just (Selection toDefName $ Just newSel))
+        pure (insertDef mod toDefBaseName (DefAST newDef), Just (SelectionDef $ DefSelection toDefName $ Just newSel))
   liftError ActionError $ tcWholeProg finalProg
 
 lookupASTDef :: GVarName -> DefMap -> Maybe ASTDef
@@ -1587,23 +1666,23 @@ alterTypeDef f type_ m = do
     m
 
 -- | Apply a bottom-up transformation to all branches of case expressions on the given type.
+-- The transformation function gets the type the case was checked at as well as all the branches.
 transformCaseBranches ::
   MonadEdit m ProgError =>
   Prog ->
   TyConName ->
-  ([CaseBranch] -> m [CaseBranch]) ->
+  (Maybe (Type' ()) -> [CaseBranch] -> m [CaseBranch]) ->
   Expr ->
   m Expr
-transformCaseBranches prog type_ f = transformM $ \case
+transformCaseBranches _ type_ f = transformM $ \case
   Case m scrut bs -> do
-    scrutType <-
-      fst
-        <$> runReaderT
-          (liftError (ActionError . TypeError) $ synth scrut)
-          (progCxt prog)
+    let scrutType' = scrut ^? _exprMetaLens % _type % _Just % _synthed
+    scrutType <- case scrutType' of
+      Nothing -> throwError' $ InternalFailure "transformCaseBranches: scrutinees did not have a cached synthesised type"
+      Just t -> pure t
     Case m scrut
       <$> if fst (unfoldTApp scrutType) == TCon () type_
-        then f bs
+        then f (m ^? _type % _Just % _chkedAt) bs
         else pure bs
   e -> pure e
 
diff --git a/primer/src/Primer/App/Base.hs b/primer/src/Primer/App/Base.hs
index 6f4f834f5..0abf4544d 100644
--- a/primer/src/Primer/App/Base.hs
+++ b/primer/src/Primer/App/Base.hs
@@ -1,20 +1,48 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE NoFieldSelectors #-}
+
 -- | Definitions needed to build the app.
 -- These are not part of the core language, but we may want to use them in dependencies of 'Primer.App'.
 module Primer.App.Base (
   Level (..),
   Editable (..),
   NodeType (..),
+  Selection,
+  Selection' (..),
+  TypeDefSelection (..),
+  TypeDefNodeSelection (..),
+  TypeDefConsSelection (..),
+  TypeDefConsFieldSelection (..),
+  DefSelection (..),
+  NodeSelection (..),
+  getTypeDefConFieldType,
 ) where
 
 import Protolude
 
 import Data.Data (Data)
+import Optics
+import Primer.Core (
+  ExprMeta,
+  GVarName,
+  HasID (..),
+  TyConName,
+  TyVarName,
+  Type',
+  TypeMeta,
+  ValConName,
+  getID,
+ )
 import Primer.JSON (
   CustomJSON (CustomJSON),
   FromJSON,
   PrimerJSON,
   ToJSON,
  )
+import Primer.TypeDef (ASTTypeDef, ValCon (..), astTypeDefConstructors)
 
 -- | The current programming "level". This setting determines which
 -- actions are displayed to the student, the labels on UI elements,
@@ -38,3 +66,76 @@ data NodeType = BodyNode | SigNode
   deriving stock (Eq, Show, Read, Bounded, Enum, Generic, Data)
   deriving (FromJSON, ToJSON) via PrimerJSON NodeType
   deriving anyclass (NFData)
+
+-- | Describes which element of a (type or term) definition the student has selected.
+-- We have the following invariant: when this contains a `NodeSelection` with @nodeType = SigNode@,
+-- or any `TypeDefConsFieldSelection`, then they will always have @meta = Right _@.
+type Selection = Selection' (Either ExprMeta TypeMeta)
+
+data Selection' a
+  = SelectionDef (DefSelection a)
+  | SelectionTypeDef (TypeDefSelection a)
+  deriving stock (Eq, Show, Read, Functor, Generic, Data)
+  deriving (FromJSON, ToJSON) via PrimerJSON (Selection' a)
+  deriving anyclass (NFData)
+
+-- | Some element of a type definition.
+data TypeDefSelection a = TypeDefSelection
+  { def :: TyConName
+  , node :: Maybe (TypeDefNodeSelection a)
+  }
+  deriving stock (Eq, Show, Read, Functor, Generic, Data)
+  deriving (FromJSON, ToJSON) via PrimerJSON (TypeDefSelection a)
+  deriving anyclass (NFData)
+
+-- | Some element in a type definition, other than simply the definition itself.
+data TypeDefNodeSelection a
+  = TypeDefParamNodeSelection TyVarName
+  | TypeDefConsNodeSelection (TypeDefConsSelection a)
+  deriving stock (Eq, Show, Read, Functor, Generic, Data)
+  deriving (FromJSON, ToJSON) via PrimerJSON (TypeDefNodeSelection a)
+  deriving anyclass (NFData)
+
+-- | Some element of a definition of a constructor.
+data TypeDefConsSelection a = TypeDefConsSelection
+  { con :: ValConName
+  , field :: Maybe (TypeDefConsFieldSelection a)
+  }
+  deriving stock (Eq, Show, Read, Functor, Generic, Data)
+  deriving (FromJSON, ToJSON) via PrimerJSON (TypeDefConsSelection a)
+  deriving anyclass (NFData)
+
+-- | Some element of a field in the definition of a constructor.
+data TypeDefConsFieldSelection a = TypeDefConsFieldSelection
+  { index :: Int
+  , meta :: a
+  }
+  deriving stock (Eq, Show, Read, Functor, Generic, Data)
+  deriving (FromJSON, ToJSON) via PrimerJSON (TypeDefConsFieldSelection a)
+  deriving anyclass (NFData)
+
+-- | Some element of a term definition.
+data DefSelection a = DefSelection
+  { def :: GVarName
+  , node :: Maybe (NodeSelection a)
+  }
+  deriving stock (Eq, Show, Read, Functor, Generic, Data)
+  deriving (FromJSON, ToJSON) via PrimerJSON (DefSelection a)
+  deriving anyclass (NFData)
+
+-- | Some element of a node, in the body or type signature of a term definition.
+data NodeSelection a = NodeSelection
+  { nodeType :: NodeType
+  , meta :: a
+  }
+  deriving stock (Eq, Show, Read, Functor, Generic, Data)
+  deriving (FromJSON, ToJSON) via PrimerJSON (NodeSelection a)
+  deriving anyclass (NFData)
+
+instance HasID a => HasID (NodeSelection a) where
+  _id = lens (getID . (.meta)) (flip $ over #meta . set _id)
+
+getTypeDefConFieldType :: ASTTypeDef a -> ValConName -> Int -> Maybe (Type' a)
+getTypeDefConFieldType def con index =
+  flip atMay index . valConArgs
+    =<< find ((== con) . valConName) (astTypeDefConstructors def)
diff --git a/primer/src/Primer/Core/Meta.hs b/primer/src/Primer/Core/Meta.hs
index c9101b8ec..161a473be 100644
--- a/primer/src/Primer/Core/Meta.hs
+++ b/primer/src/Primer/Core/Meta.hs
@@ -159,6 +159,12 @@ instance HasID ID where
 instance HasID (Meta a) where
   _id = position @1
 
+instance (HasID a, HasID b) => HasID (Either a b) where
+  _id =
+    lens
+      (either getID getID)
+      (flip $ \id -> bimap (set _id id) (set _id id))
+
 -- This instance is used in 'Primer.Zipper', but it would be an orphan if we defined it there.
 instance HasID a => HasID (Zipper a a) where
   _id = lens getter setter
diff --git a/primer/src/Primer/JSON.hs b/primer/src/Primer/JSON.hs
index d72dec9a6..ef7a17428 100644
--- a/primer/src/Primer/JSON.hs
+++ b/primer/src/Primer/JSON.hs
@@ -13,8 +13,7 @@ import Data.Aeson (
   ToJSON,
   ToJSONKey,
  )
-import Deriving.Aeson (CustomJSON (..))
-import Deriving.Aeson.Stock (Vanilla)
+import Deriving.Aeson (CustomJSON (..), OmitNothingFields)
 
 -- | A type for Primer API JSON encodings.
 --
@@ -43,4 +42,10 @@ import Deriving.Aeson.Stock (Vanilla)
 --
 -- * @SumTwoElemArray@ is unsupported by openapi3 as it is unrepresentable in
 --   a schema.
-type PrimerJSON a = Vanilla a
+type PrimerJSON a =
+  CustomJSON
+    '[ -- This protects some clients (e.g. TypeScript) from spurious equality failures
+       -- due to null-vs-omitted inconsistency.
+       OmitNothingFields
+     ]
+    a
diff --git a/primer/src/Primer/Module.hs b/primer/src/Primer/Module.hs
index 35213bd2f..2f31cc452 100644
--- a/primer/src/Primer/Module.hs
+++ b/primer/src/Primer/Module.hs
@@ -2,6 +2,7 @@ module Primer.Module (
   Module (..),
   qualifyTyConName,
   moduleTypesQualified,
+  moduleTypesQualifiedMeta,
   qualifyDefName,
   moduleDefsQualified,
   insertDef,
@@ -77,7 +78,10 @@ qualifyTyConName :: Module -> Name -> TyConName
 qualifyTyConName m = qualifyName (moduleName m)
 
 moduleTypesQualified :: Module -> TypeDefMap
-moduleTypesQualified m = mapKeys (qualifyTyConName m) $ forgetTypeDefMetadata <$> moduleTypes m
+moduleTypesQualified = map forgetTypeDefMetadata . moduleTypesQualifiedMeta
+
+moduleTypesQualifiedMeta :: Module -> Map TyConName (TypeDef TypeMeta)
+moduleTypesQualifiedMeta m = mapKeys (qualifyTyConName m) $ moduleTypes m
 
 qualifyDefName :: Module -> Name -> GVarName
 qualifyDefName m = qualifyName (moduleName m)
diff --git a/primer/src/Primer/TypeDef.hs b/primer/src/Primer/TypeDef.hs
index 8c8c123eb..d1c04fb8f 100644
--- a/primer/src/Primer/TypeDef.hs
+++ b/primer/src/Primer/TypeDef.hs
@@ -54,7 +54,7 @@ type TypeDefMap = Map TyConName (TypeDef ())
 
 -- | Definition of a primitive data type
 data PrimTypeDef = PrimTypeDef
-  { primTypeDefParameters :: [Kind]
+  { primTypeDefParameters :: [(TyVarName, Kind)]
   , primTypeDefNameHints :: [Name]
   }
   deriving stock (Eq, Show, Read, Data, Generic)
@@ -94,16 +94,16 @@ typeDefNameHints :: TypeDef b -> [Name]
 typeDefNameHints = \case
   TypeDefPrim t -> primTypeDefNameHints t
   TypeDefAST t -> astTypeDefNameHints t
-typeDefParameters :: TypeDef b -> [Kind]
+typeDefParameters :: TypeDef b -> [(TyVarName, Kind)]
 typeDefParameters = \case
   TypeDefPrim t -> primTypeDefParameters t
-  TypeDefAST t -> snd <$> astTypeDefParameters t
+  TypeDefAST t -> astTypeDefParameters t
 typeDefAST :: TypeDef b -> Maybe (ASTTypeDef b)
 typeDefAST = \case
   TypeDefPrim _ -> Nothing
   TypeDefAST t -> Just t
 typeDefKind :: TypeDef b -> Kind
-typeDefKind = foldr KFun KType . typeDefParameters
+typeDefKind = foldr (KFun . snd) KType . typeDefParameters
 
 -- | A traversal over the contstructor fields in an typedef.
 _typedefFields :: Traversal (TypeDef b) (TypeDef c) (Type' b) (Type' c)
diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index 87e3b9cd2..71dc8a17f 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -79,6 +79,7 @@ import Optics (
   JoinKinds,
   NoIx,
   Optic',
+  Traversal,
   WithIx,
   castOptic,
   equality,
@@ -91,11 +92,13 @@ import Optics (
   selfIndex,
   to,
   traverseOf,
+  traversed,
   (%),
+  (%~),
+  (.~),
   (^?),
   _Just,
  )
-import Optics.Traversal (traversed)
 import Primer.Core (
   Bind' (..),
   CaseBranch' (..),
@@ -103,7 +106,7 @@ import Primer.Core (
   Expr' (..),
   ExprMeta,
   GVarName,
-  GlobalName (baseName, qualifiedModule),
+  GlobalName (qualifiedModule),
   ID,
   Kind (..),
   LVarName,
@@ -118,6 +121,7 @@ import Primer.Core (
   TypeCacheBoth (..),
   TypeMeta,
   ValConName,
+  baseName,
   bindName,
   qualifyName,
   unLocalName,
@@ -146,10 +150,12 @@ import Primer.Def (
 import Primer.Module (
   Module (
     moduleDefs,
-    moduleName
+    moduleName,
+    moduleTypes
   ),
   moduleDefsQualified,
   moduleTypesQualified,
+  moduleTypesQualifiedMeta,
  )
 import Primer.Name (Name, NameCounter)
 import Primer.Primitives (primConName)
@@ -159,7 +165,10 @@ import Primer.TypeDef (
   TypeDef (..),
   TypeDefMap,
   ValCon (valConArgs, valConName),
+  forgetTypeDefMetadata,
+  generateTypeDefIDs,
   typeDefAST,
+  typeDefParameters,
  )
 import Primer.Typecheck.Cxt (Cxt (Cxt, globalCxt, localCxt, smartHoles, typeDefs))
 import Primer.Typecheck.Kindcheck (
@@ -241,9 +250,6 @@ extendTypeDefCxt typedefs cxt = cxt{typeDefs = typedefs <> typeDefs cxt}
 localTmVars :: Cxt -> Map LVarName Type
 localTmVars = M.mapKeys LocalName . M.mapMaybe (\case T t -> Just t; K _ -> Nothing) . localCxt
 
-noSmartHoles :: Cxt -> Cxt
-noSmartHoles cxt = cxt{smartHoles = NoSmartHoles}
-
 -- An empty typing context
 initialCxt :: SmartHoles -> Cxt
 initialCxt sh =
@@ -288,7 +294,7 @@ checkValidContext ::
   m ()
 checkValidContext cxt = do
   let tds = typeDefs cxt
-  runReaderT (checkTypeDefs tds) $ initialCxt NoSmartHoles
+  void $ runReaderT (checkTypeDefs =<< traverse generateTypeDefIDs tds) $ initialCxt NoSmartHoles
   runReaderT (checkGlobalCxt $ globalCxt cxt) $ (initialCxt NoSmartHoles){typeDefs = tds}
   checkLocalCxtTys $ localTyVars cxt
   runReaderT (checkLocalCxtTms $ localTmVars cxt) $ extendLocalCxtTys (M.toList $ localTyVars cxt) (initialCxt NoSmartHoles){typeDefs = tds}
@@ -305,8 +311,8 @@ checkValidContext cxt = do
 -- | Check all type definitions, as one recursive group, in some monadic environment
 checkTypeDefs ::
   TypeM e m =>
-  TypeDefMap ->
-  m ()
+  Map TyConName (TypeDef TypeMeta) ->
+  m (Map TyConName (TypeDef (Meta Kind)))
 checkTypeDefs tds = do
   existingTypes <- asks typeDefs
   -- NB: we expect the frontend to only submit acceptable typedefs, so all
@@ -318,17 +324,16 @@ checkTypeDefs tds = do
   -- required when checking @? ∋ Con ...@, as we need to be able to
   -- work out what typedef the constructor belongs to without any
   -- extra information.
-  let atds = Map.mapMaybe typeDefAST tds
-  let allAtds = Map.mapMaybe typeDefAST existingTypes <> atds
+  let tds' = forgetTypeDefMetadata <$> tds
+  let atds' = Map.mapMaybe typeDefAST tds'
+  let allAtds = Map.mapMaybe typeDefAST existingTypes <> atds'
   assert
     (distinct $ concatMap (map valConName . astTypeDefConstructors) allAtds)
     "Duplicate-ly-named constructor (perhaps in different typedefs)"
   -- Note that these checks only apply to non-primitives:
   -- duplicate type names are checked elsewhere, kinds are correct by construction, and there are no constructors.
-  local (extendTypeDefCxt tds) $ traverseWithKey_ checkTypeDef atds
+  local (extendTypeDefCxt tds') $ Map.traverseWithKey checkTypeDef tds
   where
-    traverseWithKey_ :: Applicative f => (k -> v -> f ()) -> Map k v -> f ()
-    traverseWithKey_ f = void . Map.traverseWithKey f
     -- In the core, we have many different namespaces, so the only name-clash
     -- checking we must do is
     -- - between two constructors (possibly of different types)
@@ -345,8 +350,13 @@ checkTypeDefs tds = do
     -- But note that we allow
     -- - type names clashing with constructor names (possibly in different
     --   types)
-
     checkTypeDef tc td = do
+      let params = typeDefParameters td
+      assert
+        (distinct $ map (unLocalName . fst) params)
+        "Duplicate parameter names in one tydef"
+      traverseOf #_TypeDefAST (checkADTTypeDef tc) td
+    checkADTTypeDef tc td = do
       let params = astTypeDefParameters td
       let cons = astTypeDefConstructors td
       assert
@@ -355,19 +365,11 @@ checkTypeDefs tds = do
               qualifiedModule tc : fmap (qualifiedModule . valConName) cons
         )
         "Module name of type and all constructors must be the same"
-      assert
-        (distinct $ map (unLocalName . fst) params <> map (baseName . valConName) cons)
-        "Duplicate names in one tydef: between parameter-names and constructor-names"
-      assert
-        (notElem (baseName tc) $ map (unLocalName . fst) params)
-        "Duplicate names in one tydef: between type-def-name and parameter-names"
-      local (noSmartHoles . extendLocalCxtTys params) $
-        mapM_ (checkKind' KType <=< fakeMeta) $
-          concatMap valConArgs cons
-    -- We need metadata to use checkKind, but we don't care about the output,
-    -- just a yes/no answer. In this case it is fine to put nonsense in the
-    -- metadata as it won't be inspected.
-    fakeMeta = generateTypeIDs
+      local (extendLocalCxtTys params) $
+        traverseOf astTypeDefConArgs (checkKind' KType) td
+
+astTypeDefConArgs :: Traversal (ASTTypeDef a) (ASTTypeDef b) (Type' a) (Type' b)
+astTypeDefConArgs = #astTypeDefConstructors % traversed % #valConArgs % traversed
 
 distinct :: Ord a => [a] -> Bool
 distinct = go mempty
@@ -403,16 +405,19 @@ checkEverything ::
 checkEverything sh CheckEverything{trusted, toCheck} =
   let cxt = buildTypingContextFromModules trusted sh
    in flip runReaderT cxt $ do
-        let newTypes = foldMap' moduleTypesQualified toCheck
-        checkTypeDefs newTypes
-        local (extendTypeDefCxt newTypes) $ do
-          -- Kind check and update (for smartholes) all the types.
+        let newTypes = foldMap' moduleTypesQualifiedMeta toCheck
+        -- Kind check all the type definitions, and update (with smartholes)
+        updatedTypes <- checkTypeDefs newTypes
+        let typeDefTtoTypeDef = (#_TypeDefAST % astTypeDefConArgs) %~ typeTtoType
+        let toCheck' = toCheck <&> \m -> m & #moduleTypes .~ M.fromList [(baseName n, typeDefTtoTypeDef d) | (n, d) <- M.toList updatedTypes, qualifiedModule n == moduleName m]
+        local (extendTypeDefCxt $ forgetTypeDefMetadata <$> updatedTypes) $ do
+          -- Kind check and update (for smartholes) all the type signatures.
           -- Note that this may give ill-typed definitions if the type changes
           -- since we have not checked the expressions against the new types.
-          updatedTypes <- traverseOf (traverseDefs % #_DefAST % #astDefType) (fmap typeTtoType . checkKind' KType) toCheck
+          updatedSigs <- traverseOf (traverseDefs % #_DefAST % #astDefType) (fmap typeTtoType . checkKind' KType) toCheck'
           -- Now extend the context with the new types
-          let defsUpdatedTypes = itoListOf foldDefTypesWithName updatedTypes
-          local (extendGlobalCxt defsUpdatedTypes) $
+          let defsUpdatedSigs = itoListOf foldDefTypesWithName updatedSigs
+          local (extendGlobalCxt defsUpdatedSigs) $
             -- Check the body (of AST definitions) against the new type
             traverseOf
               (traverseDefs % #_DefAST)
@@ -420,7 +425,7 @@ checkEverything sh CheckEverything{trusted, toCheck} =
                   e <- check (forgetTypeMetadata $ astDefType def) (astDefExpr def)
                   pure $ def{astDefExpr = exprTtoExpr e}
               )
-              updatedTypes
+              updatedSigs
   where
     -- The first argument of traverseDefs' is intended to either
     -- - be equality, giving a traveral
diff --git a/primer/src/Primer/Typecheck/Cxt.hs b/primer/src/Primer/Typecheck/Cxt.hs
index 6ffd63c4d..ada1aad01 100644
--- a/primer/src/Primer/Typecheck/Cxt.hs
+++ b/primer/src/Primer/Typecheck/Cxt.hs
@@ -28,4 +28,4 @@ data Cxt = Cxt
   , globalCxt :: Map GVarName Type
   -- ^ global variables (i.e. IDs of top-level definitions)
   }
-  deriving stock (Show)
+  deriving stock (Show, Generic)
diff --git a/primer/src/Primer/Zipper.hs b/primer/src/Primer/Zipper.hs
index 5dad673eb..55d98d0e7 100644
--- a/primer/src/Primer/Zipper.hs
+++ b/primer/src/Primer/Zipper.hs
@@ -448,7 +448,7 @@ findNodeWithParent id x = do
     InBind (BindCase bz) -> (CaseBindNode $ caseBindZFocus bz, Just . ExprNode . target . unfocusCaseBind $ bz)
 
 -- | Find a sub-type in a larger type by its ID.
-findType :: ID -> Type -> Maybe Type
+findType :: (Data a, HasID a) => ID -> Type' a -> Maybe (Type' a)
 findType id ty = target <$> focusOnTy id ty
 
 -- | An AST node tagged with its "sort" - i.e. if it's a type or expression or binding etc.
diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 5c16f2862..4e185e2aa 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE OverloadedRecordDot #-}
 
@@ -6,6 +7,8 @@ module Tests.Action.Available where
 import Foreword
 
 import Control.Monad.Log (WithSeverity)
+import Data.Aeson.Text (encodeToLazyText)
+import Data.Bitraversable (bitraverse)
 import Data.ByteString.Lazy.Char8 qualified as BS
 import Data.List.Extra (enumerate, partition)
 import Data.Map qualified as M
@@ -14,12 +17,15 @@ import Data.Text qualified as T
 import Data.Text.Lazy qualified as TL
 import GHC.Err (error)
 import Hedgehog (
+  GenT,
+  LabelName,
   PropertyT,
   annotate,
   annotateShow,
   collect,
   discard,
   failure,
+  footnoteShow,
   label,
   success,
   (===),
@@ -28,6 +34,7 @@ import Hedgehog.Gen qualified as Gen
 import Hedgehog.Internal.Property (forAllWithT)
 import Hedgehog.Range qualified as Range
 import Optics (ix, toListOf, (%), (.~), (^..), _head)
+import Primer.API (viewProg)
 import Primer.Action (
   ActionError (CaseBindsClash, NameCapture),
   Movement (Child1, Child2),
@@ -46,11 +53,18 @@ import Primer.Action.Available (
 import Primer.Action.Available qualified as Available
 import Primer.App (
   App,
+  DefSelection (..),
   EditAppM,
   Editable (..),
   Level (Beginner, Expert, Intermediate),
+  NodeSelection (..),
   NodeType (..),
+  Prog (..),
   ProgError (ActionError, DefAlreadyExists),
+  Selection' (..),
+  TypeDefConsSelection (TypeDefConsSelection),
+  TypeDefNodeSelection (TypeDefConsNodeSelection, TypeDefParamNodeSelection),
+  TypeDefSelection (TypeDefSelection),
   appProg,
   checkAppWellFormed,
   checkProgWellFormed,
@@ -58,12 +72,14 @@ import Primer.App (
   nextProgID,
   progAllDefs,
   progAllTypeDefs,
+  progAllTypeDefsMeta,
   progCxt,
   progImports,
   progModules,
   progSmartHoles,
   runEditAppM,
  )
+import Primer.App.Base (TypeDefConsFieldSelection (..))
 import Primer.Builtins (builtinModuleName, cCons, cFalse, cTrue, tBool, tList, tNat)
 import Primer.Core (
   Expr,
@@ -74,6 +90,7 @@ import Primer.Core (
   Kind (KFun, KType),
   ModuleName (ModuleName, unModuleName),
   Type,
+  TypeMeta,
   getID,
   mkSimpleModuleName,
   moduleNamePretty,
@@ -127,6 +144,7 @@ import Primer.Module (
 import Primer.Name (Name (unName))
 import Primer.Test.TestM (evalTestM)
 import Primer.Test.Util (clearMeta, clearTypeMeta, testNoSevereLogs)
+import Primer.TypeDef (ASTTypeDef (astTypeDefConstructors), TypeDef (TypeDefAST, TypeDefPrim), ValCon (..), astTypeDefParameters, typeDefAST)
 import Primer.Typecheck (
   CheckEverythingRequest (CheckEverything, toCheck, trusted),
   SmartHoles (NoSmartHoles, SmartHoles),
@@ -187,16 +205,16 @@ mkTests deps (defName, DefAST def') =
         Available.Input a ->
           Input a
             . fromMaybe (error "id not found")
-            $ Available.options typeDefs defs cxt level def id a
+            $ Available.options typeDefs defs cxt level (Right def) id a
    in testGroup testName $
         enumeratePairs
           <&> \(level, mut) ->
-            let defActions = map (offered level Nothing) $ Available.forDef defs level mut d
+            let defActions = map (offered level $ SelectionDef $ DefSelection defName Nothing) $ Available.forDef defs level mut d
                 bodyActions =
                   map
                     ( \id ->
                         ( id
-                        , map (offered level (Just (BodyNode, id))) $
+                        , map (offered level $ SelectionDef $ DefSelection defName $ Just $ NodeSelection BodyNode id) $
                             Available.forBody
                               typeDefs
                               level
@@ -211,7 +229,7 @@ mkTests deps (defName, DefAST def') =
                   map
                     ( \id ->
                         ( id
-                        , map (offered level (Just (SigNode, id))) $ Available.forSig level mut (astDefType def) id
+                        , map (offered level (SelectionDef $ DefSelection defName $ Just $ NodeSelection SigNode id)) $ Available.forSig level mut (astDefType def) id
                         )
                     )
                     . toListOf (_typeMeta % _id)
@@ -261,51 +279,131 @@ tasty_available_actions_accepted = withTests 500 $
       -- We only test SmartHoles mode (which is the only supported user-facing
       -- mode - NoSmartHoles is only used for internal sanity testing etc)
       a <- forAllT $ genApp SmartHoles cxt
+      let allTypes = progAllTypeDefsMeta $ appProg a
       let allDefs = progAllDefs $ appProg a
       let isMutable = \case
             Editable -> True
             NonEditable -> False
-      (defName, (defMut, def)) <- case partition (isMutable . fst . snd) $ Map.toList allDefs of
-        ([], []) -> discard
-        (mut, []) -> label "all mut" >> forAllT (Gen.element mut)
-        ([], immut) -> label "all immut" >> forAllT (Gen.element immut)
-        (mut, immut) -> label "mixed mut/immut" >> forAllT (Gen.frequency [(9, Gen.element mut), (1, Gen.element immut)])
+      let genDef :: Map name (Editable, def) -> GenT WT (Maybe (LabelName, (Editable, (name, def))))
+          genDef m =
+            second (\(n, (e, t)) -> (e, (n, t)))
+              <<$>> case partition (isMutable . fst . snd) $ Map.toList m of
+                ([], []) -> pure Nothing
+                (mut, []) -> Just . ("all mut",) <$> Gen.element mut
+                ([], immut) -> Just . ("all immut",) <$> Gen.element immut
+                (mut, immut) -> Just . ("mixed mut/immut",) <$> Gen.frequency [(9, Gen.element mut), (1, Gen.element immut)]
+      (defMut, typeOrTermDef) <-
+        maybe discard (\(t, x) -> label t >> pure x)
+          =<< forAllT
+            ( Gen.choice
+                [ second (second Left) <<$>> genDef allTypes
+                , second (second Right) <<$>> genDef allDefs
+                ]
+            )
       collect defMut
-      case def of
-        DefAST{} -> label "AST"
-        DefPrim{} -> label "Prim"
-      (loc, acts) <-
-        fmap snd . forAllWithT fst $
-          Gen.frequency $
+      case typeOrTermDef of
+        Left (_, t) ->
+          label "type" >> case t of
+            TypeDefPrim{} -> label "Prim"
+            TypeDefAST{} -> label "AST"
+        Right (_, t) ->
+          label "term" >> case t of
+            DefPrim{} -> label "Prim"
+            DefAST{} -> label "AST"
+      (loc, acts) <- case typeOrTermDef of
+        Left (defName, def) ->
+          (fmap snd . forAllWithT fst) case typeDefAST def of
+            Nothing -> Gen.discard
+            Just def' ->
+              let typeDefSel = SelectionTypeDef . TypeDefSelection defName
+                  forTypeDef = ("forTypeDef", (typeDefSel Nothing, Available.forTypeDef l defMut))
+               in Gen.frequency
+                    [ (1, pure forTypeDef)
+                    ,
+                      ( 2
+                      , case astTypeDefParameters def' of
+                          [] -> pure forTypeDef
+                          ps -> do
+                            (p, _) <- Gen.element ps
+                            pure
+                              ( "forTypeDefParamNode"
+                              ,
+                                ( typeDefSel $ Just $ TypeDefParamNodeSelection p
+                                , Available.forTypeDefParamNode l defMut
+                                )
+                              )
+                      )
+                    ,
+                      ( 5
+                      , case astTypeDefConstructors def' of
+                          [] -> pure forTypeDef
+                          cs -> do
+                            ValCon{valConName, valConArgs} <- Gen.element cs
+                            let typeDefConsNodeSel = typeDefSel . Just . TypeDefConsNodeSelection . TypeDefConsSelection valConName
+                                forTypeDefConsNode = ("forTypeDefConsNode", (typeDefConsNodeSel Nothing, Available.forTypeDefConsNode l defMut))
+                            case valConArgs of
+                              [] -> pure forTypeDefConsNode
+                              as ->
+                                Gen.frequency
+                                  [ (1, pure forTypeDefConsNode)
+                                  ,
+                                    ( 5
+                                    , do
+                                        (n, t) <- Gen.element $ zip [0 ..] as
+                                        i <- Gen.element $ t ^.. typeIDs
+                                        pure
+                                          ( "forTypeDefConsFieldNode"
+                                          ,
+                                            ( typeDefConsNodeSel . Just $ TypeDefConsFieldSelection n i
+                                            , Available.forTypeDefConsFieldNode l defMut def' valConName n i
+                                            )
+                                          )
+                                    )
+                                  ]
+                      )
+                    ]
+        Right (defName, def) ->
+          fmap (first (SelectionDef . DefSelection defName) . snd) . forAllWithT fst . Gen.frequency $
             catMaybes
-              [ Just (1, pure ("actionsForDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName)))
+              [ Just (1, pure ("forDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName)))
               , defAST def <&> \d' -> (2,) $ do
                   let ty = astDefType d'
                       ids = ty ^.. typeIDs
                   i <- Gen.element ids
-                  let hedgehogMsg = "actionsForDefSig id " <> show i
-                  pure (hedgehogMsg, (Just (SigNode, i), Available.forSig l defMut ty i))
+                  let hedgehogMsg = "forSig id " <> show i
+                  pure (hedgehogMsg, (Just $ NodeSelection SigNode i, Available.forSig l defMut ty i))
               , defAST def <&> \d' -> (7,) $ do
                   let expr = astDefExpr d'
                       ids = expr ^.. exprIDs
                   i <- Gen.element ids
-                  let hedgehogMsg = "actionsForDefBody id " <> show i
-                  pure (hedgehogMsg, (Just (BodyNode, i), Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i))
+                  let hedgehogMsg = "forBody id " <> show i
+                  pure (hedgehogMsg, (Just $ NodeSelection BodyNode i, Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i))
               ]
+      annotateShow loc
       case acts of
         [] -> label "no offered actions" >> success
         acts' -> do
-          action <- forAllT $ Gen.element acts'
+          def <-
+            bitraverse
+              (maybe (annotate "primitive type def" >> failure) pure . typeDefAST . snd)
+              (maybe (annotate "primitive def" >> failure) pure . defAST . snd)
+              typeOrTermDef
+          let bias = Nothing
+          -- these seem to be the only two action which still cause errors
+          -- let bias = Just $ Available.Input Available.AddCon
+          -- let bias = Just $ Available.NoInput Available.AddConField
+          action <- maybe (forAllT $ Gen.element acts') pure $ (bias <*) . guard . (`elem` acts') =<< bias
           collect action
+          footnoteShow action
           case action of
+            act@(Available.Input Available.AddCon) | Just act /= bias -> discard
+            act@(Available.NoInput Available.AddConField) | Just act /= bias -> discard
             Available.NoInput act' -> do
-              def' <- maybe (annotate "primitive def" >> failure) pure $ defAST def
               progActs <-
                 either (\e -> annotateShow e >> failure) pure $
-                  toProgActionNoInput (map snd $ progAllDefs $ appProg a) def' defName loc act'
+                  toProgActionNoInput (map snd $ progAllDefs $ appProg a) def loc act'
               actionSucceeds (handleEditRequest progActs) a
             Available.Input act' -> do
-              def' <- maybe (annotate "primitive def" >> failure) pure $ defAST def
               Available.Options{Available.opts, Available.free} <-
                 maybe (annotate "id not found" >> failure) pure $
                   Available.options
@@ -313,7 +411,7 @@ tasty_available_actions_accepted = withTests 500 $
                     (map snd $ progAllDefs $ appProg a)
                     (progCxt $ appProg a)
                     l
-                    def'
+                    def
                     loc
                     act'
               let opts' = [Gen.element $ (Offered,) <$> opts | not (null opts)]
@@ -327,7 +425,7 @@ tasty_available_actions_accepted = withTests 500 $
                 [] -> annotate "no options" >> success
                 options -> do
                   opt <- forAllT $ Gen.choice options
-                  progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput def' defName loc (snd opt) act'
+                  progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput def loc (snd opt) act'
                   actionSucceedsOrCapture (fst opt) (handleEditRequest progActs) a
   where
     runEditAppMLogs ::
@@ -340,7 +438,8 @@ tasty_available_actions_accepted = withTests 500 $
     actionSucceeds :: HasCallStack => EditAppM (PureLog (WithSeverity ())) ProgError a -> App -> PropertyT WT ()
     actionSucceeds m a =
       runEditAppMLogs m a >>= \case
-        (Left err, _) -> annotateShow err >> failure
+        -- copy output to primer-app to view prog - use as `initialProg` arg to `AppProg` in `App.tsx`
+        (Left err, _) -> annotateShow err >> annotate (TL.unpack $ encodeToLazyText $ viewProg $ appProg a) >> failure
         (Right _, a') -> ensureSHNormal a'
     -- If we submit our own name rather than an offered one, then
     -- we should expect that name capture/clashing may happen
@@ -595,12 +694,12 @@ offeredActionTest' sh l inputDef position action = do
   let offered = case position of
         InBody _ -> Available.forBody cxt.typeDefs l Editable expr id
         InSig _ -> Available.forSig l Editable sig id
-  let options = Available.options cxt.typeDefs defs cxt l exprDef (Just (BodyNode, id))
+  let options = Available.options cxt.typeDefs defs cxt l (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id)
   action' <- case action of
     Left a ->
       pure $
         if Available.NoInput a `elem` offered
-          then Right $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) exprDef exprDefName (Just (BodyNode, id)) a
+          then Right $ toProgActionNoInput @TypeMeta (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a
           else Left $ ActionNotOffered (Available.NoInput a) offered
     Right (a, o) -> do
       if Available.Input a `elem` offered
@@ -609,7 +708,7 @@ offeredActionTest' sh l inputDef position action = do
           Just os ->
             pure $
               if o `elem` os.opts
-                then Right $ toProgActionInput exprDef exprDefName (Just (BodyNode, id)) o a
+                then Right $ toProgActionInput (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) o a
                 else Left $ OptionNotOffered o os.opts
         else pure $ Left $ ActionNotOffered (Available.Input a) offered
   action'' <- for action' $ \case
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index 63f45d80d..3c3a35a3f 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE OverloadedRecordDot #-}
 
 module Tests.Action.Prog where
 
@@ -35,6 +36,7 @@ import Primer.Action (
  )
 import Primer.App (
   App,
+  DefSelection (..),
   Log (..),
   NodeSelection (..),
   NodeType (..),
@@ -42,7 +44,7 @@ import Primer.App (
   ProgAction (..),
   ProgError (..),
   Question (GenerateName, VariablesInScope),
-  Selection (..),
+  Selection' (..),
   appIdCounter,
   appNameCounter,
   appProg,
@@ -160,7 +162,7 @@ unit_move_to_def_main = progActionTest defaultEmptyProg [moveToDef "main"] $
     prog'
       @?= prog
         { progLog = Log [[moveToDef "main"]]
-        , progSelection = Just $ Selection (gvn "main") Nothing
+        , progSelection = Just $ SelectionDef $ DefSelection (gvn "main") Nothing
         }
 
 -- Expression actions are tested in ActionTest - here we just check that we can modify the correct
@@ -418,31 +420,7 @@ unit_create_typedef_bad_5 =
           , astTypeDefNameHints = []
           }
    in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $
-        expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between parameter-names and constructor-names\"")
-
--- Forbid clash between type name and parameter name
-unit_create_typedef_bad_6 :: Assertion
-unit_create_typedef_bad_6 =
-  let td =
-        ASTTypeDef
-          { astTypeDefParameters = [("T", KType)]
-          , astTypeDefConstructors = []
-          , astTypeDefNameHints = []
-          }
-   in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $
-        expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between type-def-name and parameter-names\"")
-
--- Forbid clash between parameter name and constructor name
-unit_create_typedef_bad_7 :: Assertion
-unit_create_typedef_bad_7 =
-  let td =
-        ASTTypeDef
-          { astTypeDefParameters = [("a", KType)]
-          , astTypeDefConstructors = [ValCon (vcn "a") []]
-          , astTypeDefNameHints = []
-          }
-   in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $
-        expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between parameter-names and constructor-names\"")
+        expectError (@?= TypeDefError "InternalError \"Duplicate parameter names in one tydef\"")
 
 -- Forbid clash between type name and name of a primitive type
 unit_create_typedef_bad_prim :: Assertion
@@ -499,7 +477,7 @@ unit_construct_arrow_in_sig =
             TFun _ lhs _ ->
               -- Check that the selection is focused on the lhs, as we instructed
               case progSelection prog' of
-                Just (Selection d (Just sel@NodeSelection{nodeType = SigNode})) -> do
+                Just (SelectionDef (DefSelection d (Just sel@NodeSelection{nodeType = SigNode}))) -> do
                   d @?= qualifyName mainModuleName "other"
                   getID sel @?= getID lhs
                 _ -> assertFailure "no selection"
@@ -1285,6 +1263,40 @@ unit_AddConField_case_ann =
                 ]
           )
 
+unit_ConFieldAction :: Assertion
+unit_ConFieldAction =
+  progActionTest
+    ( defaultProgEditableTypeDefs $ do
+        e <- con cA $ replicate 3 $ con0 $ vcn "True"
+        t <- tEmptyHole
+        pure [astDef "def" e t]
+    )
+    [ConFieldAction tT cA 1 [ConstructArrowL]]
+    $ expectSuccess
+    $ \_ prog' -> do
+      td <- findTypeDef tT prog'
+      def <- findDef (gvn "def") prog'
+      astTypeDefConstructors td
+        @?= [ ValCon
+                cA
+                [ TCon () (tcn "Bool")
+                , TFun () (TCon () (tcn "Bool")) (TEmptyHole ())
+                , TCon () (tcn "Bool")
+                ]
+            , ValCon cB [TApp () (TApp () (TCon () tT) (TVar () "b")) (TVar () "a"), TVar () "b"]
+            ]
+      forgetMetadata (astDefExpr def)
+        @?= forgetMetadata
+          ( create' $
+              do
+                con
+                  cA
+                  [ con0 $ vcn "True"
+                  , hole $ con0 $ vcn "True"
+                  , con0 $ vcn "True"
+                  ]
+          )
+
 -- Check that we see name hints from imported modules
 -- (This differs from the tests in Tests.Question by testing the actual action,
 -- rather than the underlying functionality)
@@ -1323,7 +1335,11 @@ unit_rename_module =
         Left err -> assertFailure $ show err
         Right p -> do
           fmap (unModuleName . moduleName) (progModules p) @?= [["Module2"]]
-          selectedDef <$> progSelection p @?= Just (qualifyName (ModuleName ["Module2"]) "main")
+          sel <- case progSelection p of
+            Just (SelectionDef s) -> pure s
+            Just (SelectionTypeDef _) -> assertFailure "typedef selected"
+            Nothing -> assertFailure "no selection"
+          sel.def @?= qualifyName (ModuleName ["Module2"]) "main"
           case fmap (Map.assocs . moduleDefsQualified) (progModules p) of
             [[(n, DefAST d)]] -> do
               let expectedName = qualifyName (ModuleName ["Module2"]) "main"
@@ -1392,7 +1408,7 @@ unit_cross_module_actions =
               , Move $ ConChild 0
               , constructSaturatedCon cSucc
               , Move $ ConChild 0
-              , ConstructVar (LocalVarRef "a37")
+              -- , ConstructVar (LocalVarRef "a37")
               ]
           ]
         handleAndTC [RenameDef (qualifyM "foo") "bar"]
@@ -1506,7 +1522,7 @@ unit_sh_lost_id =
         Just def ->
           case astDefExpr <$> defAST def of
             Just (Var m (GlobalVarRef f)) | f == foo -> case progSelection prog' of
-              Just Selection{selectedDef, selectedNode = Just sel} ->
+              Just (SelectionDef DefSelection{def = selectedDef, node = Just sel}) ->
                 unless (selectedDef == foo && getID sel == getID m) $
                   assertFailure "expected selection to point at the recursive reference"
               _ -> assertFailure "expected the selection to point at some node"
@@ -1544,8 +1560,8 @@ defaultEmptyProg = do
    in pure $
         newEmptyProg'
           { progSelection =
-              Just $
-                Selection (gvn "main") $
+              Just . SelectionDef $
+                DefSelection (gvn "main") $
                   Just
                     NodeSelection
                       { nodeType = BodyNode
diff --git a/primer/test/Tests/Serialization.hs b/primer/test/Tests/Serialization.hs
index 3594a1f08..24186a519 100644
--- a/primer/test/Tests/Serialization.hs
+++ b/primer/test/Tests/Serialization.hs
@@ -13,6 +13,7 @@ import Data.Map.Strict qualified as Map
 import Data.String (String)
 import Primer.Action (Action (Move, SetCursor), ActionError (IDNotFound), Movement (Child1))
 import Primer.App (
+  DefSelection (..),
   EvalResp (EvalResp, evalRespDetail, evalRespExpr, evalRespRedexes),
   Log (..),
   NodeSelection (..),
@@ -20,7 +21,8 @@ import Primer.App (
   Prog (..),
   ProgAction (BodyAction, MoveToDef),
   ProgError (NoDefSelected),
-  Selection (..),
+  Selection,
+  Selection' (..),
   defaultLog,
  )
 import Primer.Builtins (tNat)
@@ -151,12 +153,13 @@ fixtures =
           }
       selection :: Selection
       selection =
-        Selection (qualifyName modName defName) $
-          Just
-            NodeSelection
-              { nodeType = BodyNode
-              , meta = Left exprMeta
-              }
+        SelectionDef $
+          DefSelection (qualifyName modName defName) $
+            Just
+              NodeSelection
+                { nodeType = BodyNode
+                , meta = Left exprMeta
+                }
       reductionDetail :: EvalDetail
       reductionDetail =
         BetaReduction $
diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs
index 58f4d8ec2..d5cfe39e9 100644
--- a/primer/test/Tests/Typecheck.hs
+++ b/primer/test/Tests/Typecheck.hs
@@ -18,6 +18,9 @@ import Primer.App (
     progSmartHoles,
     redoLog
   ),
+  TypeDefConsFieldSelection (..),
+  TypeDefConsSelection (..),
+  TypeDefSelection (..),
   appIdCounter,
   appInit,
   appNameCounter,
@@ -30,6 +33,7 @@ import Primer.App (
   tcWholeProgWithImports,
  )
 import Primer.App qualified as App
+import Primer.App.Base (TypeDefNodeSelection (..))
 import Primer.Builtins (
   boolDef,
   cCons,
@@ -782,6 +786,10 @@ tcaFunctorial :: (Functor f, Eq (f (TypeCacheAlpha a))) => TypeCacheAlpha (f a)
 tcaFunctorial = (==) `on` (fmap TypeCacheAlpha . unTypeCacheAlpha)
 instance Eq (TypeCacheAlpha a) => Eq (TypeCacheAlpha (Maybe a)) where
   (==) = tcaFunctorial
+instance (Eq (TypeCacheAlpha a), Eq (TypeCacheAlpha b)) => Eq (TypeCacheAlpha (Either a b)) where
+  TypeCacheAlpha (Left a1) == TypeCacheAlpha (Left a2) = TypeCacheAlpha a1 == TypeCacheAlpha a2
+  TypeCacheAlpha (Right b1) == TypeCacheAlpha (Right b2) = TypeCacheAlpha b1 == TypeCacheAlpha b2
+  _ == _ = False
 instance (Eq (TypeCacheAlpha a), Eq b) => Eq (TypeCacheAlpha (Expr' (Meta a) b)) where
   (==) = (==) `on` (((_exprMeta % _type) %~ TypeCacheAlpha) . unTypeCacheAlpha)
 instance Eq (TypeCacheAlpha Def) where
@@ -799,12 +807,22 @@ instance Eq (TypeCacheAlpha [Module]) where
   (==) = tcaFunctorial
 instance Eq (TypeCacheAlpha ExprMeta) where
   (==) = tcaFunctorial
-instance Eq (TypeCacheAlpha App.NodeSelection) where
+instance Eq (TypeCacheAlpha TypeMeta) where
+  (==) = tcaFunctorial
+instance Eq (TypeCacheAlpha Kind) where
+  TypeCacheAlpha k1 == TypeCacheAlpha k2 = k1 == k2
+instance Eq (TypeCacheAlpha (App.NodeSelection (Either ExprMeta TypeMeta))) where
   TypeCacheAlpha (App.NodeSelection t1 m1) == TypeCacheAlpha (App.NodeSelection t2 m2) =
     t1 == t2 && ((==) `on` first TypeCacheAlpha) m1 m2
 instance Eq (TypeCacheAlpha App.Selection) where
-  TypeCacheAlpha (App.Selection d1 n1) == TypeCacheAlpha (App.Selection d2 n2) =
+  TypeCacheAlpha (App.SelectionDef (App.DefSelection d1 n1)) == TypeCacheAlpha (App.SelectionDef (App.DefSelection d2 n2)) =
     d1 == d2 && TypeCacheAlpha n1 == TypeCacheAlpha n2
+  TypeCacheAlpha (App.SelectionTypeDef (TypeDefSelection a1 (Just (TypeDefConsNodeSelection (TypeDefConsSelection n1 (Just (TypeDefConsFieldSelection b1 m1)))))))
+    == TypeCacheAlpha (App.SelectionTypeDef (TypeDefSelection a2 (Just (TypeDefConsNodeSelection (TypeDefConsSelection n2 (Just (TypeDefConsFieldSelection b2 m2))))))) =
+      a1 == a2 && b1 == b2 && n1 == n2 && TypeCacheAlpha m1 == TypeCacheAlpha m2
+  TypeCacheAlpha (App.SelectionTypeDef (TypeDefSelection n1 s1)) == TypeCacheAlpha (App.SelectionTypeDef (TypeDefSelection n2 s2)) =
+    n1 == n2 && s1 == s2
+  _ == _ = False
 instance Eq (TypeCacheAlpha Prog) where
   TypeCacheAlpha (Prog i1 m1 s1 sh1 l1 r1) == TypeCacheAlpha (Prog i2 m2 s2 sh2 l2 r2) =
     TypeCacheAlpha i1 == TypeCacheAlpha i2
diff --git a/primer/test/outputs/serialization/edit_response_2.json b/primer/test/outputs/serialization/edit_response_2.json
index 5fd634d7a..ebdaa70a6 100644
--- a/primer/test/outputs/serialization/edit_response_2.json
+++ b/primer/test/outputs/serialization/edit_response_2.json
@@ -147,28 +147,31 @@
             }
         ],
         "progSelection": {
-            "selectedDef": {
-                "baseName": "main",
-                "qualifiedModule": [
-                    "M"
-                ]
-            },
-            "selectedNode": {
-                "meta": {
-                    "Left": [
-                        0,
-                        {
-                            "contents": {
-                                "contents": [],
-                                "tag": "TEmptyHole"
-                            },
-                            "tag": "TCSynthed"
-                        },
-                        null
+            "contents": {
+                "def": {
+                    "baseName": "main",
+                    "qualifiedModule": [
+                        "M"
                     ]
                 },
-                "nodeType": "BodyNode"
-            }
+                "node": {
+                    "meta": {
+                        "Left": [
+                            0,
+                            {
+                                "contents": {
+                                    "contents": [],
+                                    "tag": "TEmptyHole"
+                                },
+                                "tag": "TCSynthed"
+                            },
+                            null
+                        ]
+                    },
+                    "nodeType": "BodyNode"
+                }
+            },
+            "tag": "SelectionDef"
         },
         "progSmartHoles": "SmartHoles",
         "redoLog": {
diff --git a/primer/test/outputs/serialization/prog.json b/primer/test/outputs/serialization/prog.json
index 02b6dc308..fcfeb7ab3 100644
--- a/primer/test/outputs/serialization/prog.json
+++ b/primer/test/outputs/serialization/prog.json
@@ -146,28 +146,31 @@
         }
     ],
     "progSelection": {
-        "selectedDef": {
-            "baseName": "main",
-            "qualifiedModule": [
-                "M"
-            ]
-        },
-        "selectedNode": {
-            "meta": {
-                "Left": [
-                    0,
-                    {
-                        "contents": {
-                            "contents": [],
-                            "tag": "TEmptyHole"
-                        },
-                        "tag": "TCSynthed"
-                    },
-                    null
+        "contents": {
+            "def": {
+                "baseName": "main",
+                "qualifiedModule": [
+                    "M"
                 ]
             },
-            "nodeType": "BodyNode"
-        }
+            "node": {
+                "meta": {
+                    "Left": [
+                        0,
+                        {
+                            "contents": {
+                                "contents": [],
+                                "tag": "TEmptyHole"
+                            },
+                            "tag": "TCSynthed"
+                        },
+                        null
+                    ]
+                },
+                "nodeType": "BodyNode"
+            }
+        },
+        "tag": "SelectionDef"
     },
     "progSmartHoles": "SmartHoles",
     "redoLog": {
diff --git a/primer/test/outputs/serialization/selection.json b/primer/test/outputs/serialization/selection.json
index 0ac964006..3f33224c0 100644
--- a/primer/test/outputs/serialization/selection.json
+++ b/primer/test/outputs/serialization/selection.json
@@ -1,24 +1,27 @@
 {
-    "selectedDef": {
-        "baseName": "main",
-        "qualifiedModule": [
-            "M"
-        ]
-    },
-    "selectedNode": {
-        "meta": {
-            "Left": [
-                0,
-                {
-                    "contents": {
-                        "contents": [],
-                        "tag": "TEmptyHole"
-                    },
-                    "tag": "TCSynthed"
-                },
-                null
+    "contents": {
+        "def": {
+            "baseName": "main",
+            "qualifiedModule": [
+                "M"
             ]
         },
-        "nodeType": "BodyNode"
-    }
+        "node": {
+            "meta": {
+                "Left": [
+                    0,
+                    {
+                        "contents": {
+                            "contents": [],
+                            "tag": "TEmptyHole"
+                        },
+                        "tag": "TCSynthed"
+                    },
+                    null
+                ]
+            },
+            "nodeType": "BodyNode"
+        }
+    },
+    "tag": "SelectionDef"
 }
\ No newline at end of file