diff --git a/primer/src/Primer/API.hs b/primer/src/Primer/API.hs
index 3c542b791..9ebdbacb9 100644
--- a/primer/src/Primer/API.hs
+++ b/primer/src/Primer/API.hs
@@ -1183,7 +1183,7 @@ availableActions = curry3 $ logAPI (noError AvailableActions) $ \(sid, level, se
       (editable, def) <- findASTTypeDef allTypeDefs sel.def
       let getActions = case sel.node of
             Nothing -> Available.forTypeDef
-            Just (TypeDefParamNodeSelection _) -> Available.forTypeDefParamNode
+            Just (TypeDefParamNodeSelection p) -> Available.forTypeDefParamNode p
             Just (TypeDefConsNodeSelection s) -> case s.field of
               Nothing -> Available.forTypeDefConsNode
               Just field -> Available.forTypeDefConsFieldNode s.con field.index field.meta
diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs
index 286cfdbd6..d892f915c 100644
--- a/primer/src/Primer/Action.hs
+++ b/primer/src/Primer/Action.hs
@@ -1052,7 +1052,7 @@ renameForall b zt = case target zt of
 -- | Convert a high-level 'Available.NoInputAction' to a concrete sequence of 'ProgAction's.
 toProgActionNoInput ::
   DefMap ->
-  Either (ASTTypeDef a) ASTDef ->
+  Either (ASTTypeDef TypeMeta) ASTDef ->
   Selection' ID ->
   Available.NoInputAction ->
   Either ActionError [ProgAction]
@@ -1088,14 +1088,23 @@ toProgActionNoInput defs def0 sel0 = \case
     -- 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
-    def <- termDef
-    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
+        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
diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs
index bfa6e0de9..ed615e741 100644
--- a/primer/src/Primer/Action/Available.hs
+++ b/primer/src/Primer/Action/Available.hs
@@ -69,6 +69,7 @@ import Primer.Core (
   Pattern (PatCon, PatPrim),
   PrimCon (PrimChar, PrimInt),
   TyConName,
+  TyVarName,
   Type,
   Type' (..),
   TypeMeta,
@@ -84,7 +85,7 @@ import Primer.Core (
   _typeMetaLens,
  )
 import Primer.Core.Transform (decomposeTAppCon)
-import Primer.Core.Utils (forgetTypeMetadata, freeVars)
+import Primer.Core.Utils (forgetTypeMetadata, freeVars, freeVarsTy)
 import Primer.Def (
   ASTDef (..),
   DefMap,
@@ -367,6 +368,7 @@ forTypeDef l Editable tydefs defs tdName td =
         )
 
 forTypeDefParamNode ::
+  TyVarName ->
   Level ->
   Editable ->
   TypeDefMap ->
@@ -374,13 +376,18 @@ forTypeDefParamNode ::
   TyConName ->
   ASTTypeDef TypeMeta ->
   [Action]
-forTypeDefParamNode _ NonEditable _ _ _ _ = mempty
-forTypeDefParamNode l Editable tydefs defs tdName td =
+forTypeDefParamNode _ _ NonEditable _ _ _ _ = mempty
+forTypeDefParamNode paramName l Editable tydefs defs tdName td =
   sortByPriority l $
     [ Input RenameTypeParam
     ]
       <> mwhen
-        (l == Expert && not (typeInUse tdName td tydefs defs))
+        ( l == Expert
+            && not
+              ( typeInUse tdName td tydefs defs
+                  || any (elem paramName . freeVarsTy) (concatMap valConArgs $ astTypeDefConstructors td)
+              )
+        )
         [NoInput DeleteTypeParam]
 
 forTypeDefConsNode ::
diff --git a/primer/src/Primer/Action/Errors.hs b/primer/src/Primer/Action/Errors.hs
index c98bb02e0..86d454613 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, Pattern, TyConName, Type, Type', ValConName)
+import Primer.Core (Expr, GVarName, ID, LVarName, ModuleName, Pattern, TyConName, Type', ValConName)
 import Primer.JSON (CustomJSON (..), PrimerJSON)
 import Primer.Typecheck.TypeError (TypeError)
 import Primer.Zipper (SomeNode)
@@ -62,7 +62,7 @@ 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
@@ -78,5 +78,6 @@ data ActionError
   | 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/ProgError.hs b/primer/src/Primer/Action/ProgError.hs
index e1ec25550..d960849c6 100644
--- a/primer/src/Primer/Action/ProgError.hs
+++ b/primer/src/Primer/Action/ProgError.hs
@@ -19,6 +19,14 @@ data ProgError
   | TypeDefNotFound TyConName
   | TypeDefAlreadyExists TyConName
   | TypeDefInUse TyConName
+  | -- | Cannot use a name twice in a type definition.
+    -- This includes
+    -- - clash between the type itself and a constructor
+    -- - clash between the type itself and a parameter
+    -- - clash between two constructors
+    -- - clash between two parameters
+    -- - clash between parameter and constructor
+    TypeDefModifyNameClash Name
   | TypeParamInUse TyConName TyVarName
   | ConNotFound ValConName
   | ConAlreadyExists ValConName
@@ -26,9 +34,7 @@ data ProgError
     -- (this should never happen in a well-typed program)
     ConNotSaturated ValConName
   | ParamNotFound TyVarName
-  | ParamAlreadyExists TyVarName
   | NodeIDNotFound ID
-  | TyConParamClash Name
   | ValConParamClash Name
   | ActionError ActionError
   | EvalError EvalError
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index f0145aff5..12ebc7a96 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -65,6 +65,7 @@ import Foreword hiding (mod)
 import Control.Monad.Fresh (MonadFresh (..))
 import Control.Monad.Log (MonadLog, WithSeverity)
 import Control.Monad.NestedError (MonadNestedError, throwError')
+import Data.Data (Data)
 import Data.Generics.Uniplate.Operations (transform, transformM)
 import Data.Generics.Uniplate.Zipper (
   fromZipper,
@@ -77,11 +78,16 @@ import Optics (
   Field1 (_1),
   Field2 (_2),
   Field3 (_3),
+  Fold,
   ReversibleOptic (re),
+  elemOf,
+  folded,
   ifoldMap,
   mapped,
   over,
   set,
+  summing,
+  to,
   traverseOf,
   traversed,
   view,
@@ -90,6 +96,7 @@ import Optics (
   (.~),
   (?~),
   (^.),
+  (^?),
   _Just,
   _Left,
   _Right,
@@ -130,6 +137,7 @@ import Primer.Core (
   GVarName,
   GlobalName (baseName, qualifiedModule),
   ID (..),
+  Kind (KType),
   LocalName (LocalName, unLocalName),
   Meta (..),
   ModuleName (ModuleName),
@@ -138,6 +146,8 @@ import Primer.Core (
   TyConName,
   Type,
   Type' (..),
+  TypeCache (..),
+  TypeCacheBoth (..),
   TypeMeta,
   ValConName,
   caseBranchName,
@@ -148,12 +158,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, freeVarsTy, generateTypeIDs, regenerateExprIDs, regenerateTypeIDs, _freeTmVars, _freeTyVars, _freeVarsTy)
 import Primer.Def (
   ASTDef (..),
@@ -207,8 +221,8 @@ import Primer.Typecheck (
   buildTypingContextFromModules,
   checkEverything,
   checkTypeDefs,
-  synth,
  )
+import Primer.Typecheck qualified as TC
 import Primer.Zipper (
   ExprZ,
   Loc' (InBind, InExpr, InType),
@@ -632,7 +646,7 @@ applyProgAction prog = \case
       -- see https://github.com/hackworthltd/primer/issues/3)
       (TypeDefError . show @TypeError)
       ( runReaderT
-          (checkTypeDefs $ Map.singleton tc (TypeDefAST td))
+          (void $ checkTypeDefs $ Map.singleton tc td')
           (buildTypingContextFromModules (progAllModules prog) NoSmartHoles)
       )
     pure
@@ -648,8 +662,8 @@ applyProgAction prog = \case
         let m' = m{moduleTypes = Map.delete (baseName d) (moduleTypes m)}
         pure (m' : ms, Nothing)
   RenameType old (unsafeMkName -> nameRaw) -> editModuleCross (qualifiedModule old) prog $ \(m, ms) -> do
-    when (new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new
-    m' <- traverseOf #moduleTypes updateType m
+    when (new /= old && new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new
+    m' <- traverseOf #moduleTypes updateTypeDef m
     let renamedInTypes = over (traversed % #moduleTypes) updateRefsInTypes $ m' : ms
     pure
       ( over (traversed % #moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) renamedInTypes
@@ -657,48 +671,51 @@ applyProgAction prog = \case
       )
     where
       new = qualifyName (qualifiedModule old) nameRaw
-      updateType m = do
+      updateTypeDef m = do
         d0 <-
           -- NB We do not allow primitive types to be renamed.
           -- 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
+        assertFreshNameForTypeDef nameRaw (old, d0)
         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) ->
     editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do
       when (new `elem` allValConNames prog) $ throwError $ ConAlreadyExists new
-      m' <- updateType m
+      m' <- updateTypeDef m
       pure
         ( over (mapped % #moduleDefs) updateDefs (m' : ms)
         , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection new Nothing
         )
     where
-      updateType =
+      updateTypeDef =
         alterTypeDef
-          ( traverseOf
-              #astTypeDefConstructors
-              ( maybe (throwError $ ConNotFound old) pure
-                  . findAndAdjust ((== old) . valConName) (#valConName .~ new)
-              )
+          ( \td -> do
+              when (old /= new) $ assertFreshNameForTypeDef (baseName new) (type_, td)
+              traverseOf
+                #astTypeDefConstructors
+                ( maybe (throwError $ ConNotFound old) pure
+                    . findAndAdjust ((== old) . valConName) (#valConName .~ new)
+                )
+                td
           )
           type_
       updateDefs =
@@ -709,20 +726,18 @@ applyProgAction prog = \case
       updateName n = if n == old then new else n
   RenameTypeParam type_ old (unsafeMkLocalName -> new) ->
     editModule (qualifiedModule type_) prog $ \m -> do
-      m' <- updateType m
+      m' <- updateTypeDef m
       pure
         ( m'
         , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefParamNodeSelection new
         )
     where
-      updateType =
+      updateTypeDef =
         alterTypeDef
-          (updateConstructors <=< updateParam)
+          (updateConstructors <=< updateParam <=< \td -> td <$ when (old /= new) (assertFreshNameForTypeDef (unLocalName new) (type_, td)))
           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
@@ -737,13 +752,11 @@ applyProgAction prog = \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) ->
     editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do
       when (con `elem` allValConNames prog) $ throwError $ ConAlreadyExists con
-      m' <- updateType m
+      m' <- updateTypeDef m
       newTy <- maybe (throwError $ TypeDefNotFound type_) pure $ moduleTypesQualified m' Map.!? type_
       allCons <- maybe (throwError $ TypeDefIsPrim type_) (pure . astTypeDefConstructors) $ typeDefAST newTy
       ms' <-
@@ -756,14 +769,17 @@ applyProgAction prog = \case
         , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing
         )
     where
-      updateDefs allCons = transformNamedCaseBranches prog type_ $ \bs -> do
-        m' <- DSL.meta
+      updateDefs allCons = transformNamedCaseBranches type_ $ \t' bs -> do
+        m' <- DSL.meta' $ (\t'' -> TCEmb $ TCBoth{tcChkedAt = t'', tcSynthed = TEmptyHole ()}) <$> t'
         pure $ insertSubseqBy caseBranchName (CaseBranch (PatCon con) [] (EmptyHole m')) (PatCon . valConName <$> allCons) bs
-      updateType =
+      updateTypeDef =
         alterTypeDef
-          ( traverseOf
-              #astTypeDefConstructors
-              (maybe (throwError $ IndexOutOfRange index) pure . insertAt index (ValCon con []))
+          ( \td -> do
+              assertFreshNameForTypeDef (baseName con) (type_, td)
+              traverseOf
+                #astTypeDefConstructors
+                (maybe (throwError $ IndexOutOfRange index) pure . insertAt index (ValCon con []))
+                td
           )
           type_
   DeleteCon tdName vcName -> editModuleCross (qualifiedModule tdName) prog $ \(m, ms) -> do
@@ -786,7 +802,7 @@ applyProgAction prog = \case
     pure (m' : ms, Just $ SelectionTypeDef $ TypeDefSelection tdName Nothing)
   AddConField type_ con index new ->
     editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do
-      m' <- updateType m
+      m' <- updateTypeDef m
       ms' <- traverseOf (traversed % #moduleDefs) updateDefs (m' : ms)
       pure
         ( ms'
@@ -799,34 +815,38 @@ applyProgAction prog = \case
             $ 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
+      updateTypeDef =
+        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
+          m' <- DSL.meta' $ Just (TCEmb $ TCBoth (TEmptyHole ()) (TEmptyHole ()))
           case insertAt index (EmptyHole m') tms of
             Just args' -> pure $ Con m con' args'
             Nothing -> throwError $ ConNotSaturated con
         e -> pure e
-      updateDecons = transformNamedCaseBranch prog type_ con $
+      updateDecons = transformNamedCaseBranch type_ con . const $
         \(CaseBranch vc binds e) -> do
-          m' <- DSL.meta
+          m' <- DSL.meta' $ Just (TCChkedAt (TEmptyHole ()))
           newName <- LocalName <$> freshName (freeVars e)
           binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds
           pure $ CaseBranch vc binds' e
@@ -861,12 +881,10 @@ applyProgAction prog = \case
       alterTypeDef
         ( \td -> do
             checkTypeNotInUse tdName td $ m : ms
+            assertFreshNameForTypeDef (unLocalName paramName) (tdName, td)
             traverseOf
               #astTypeDefParameters
               ( \ps -> do
-                  when
-                    (paramName `elem` map fst ps)
-                    (throwError $ ParamAlreadyExists paramName)
                   maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (paramName, k) ps
               )
               td
@@ -996,6 +1014,13 @@ applyProgAction prog = \case
     mdefName = case progSelection prog of
       Just (SelectionDef s) -> Just s.def
       _ -> Nothing
+    typeDefNames :: Fold (TyConName, ASTTypeDef a) Name
+    typeDefNames =
+      (_1 % to baseName)
+        `summing` (_2 % #astTypeDefParameters % folded % _1 % to unLocalName)
+        `summing` (_2 % #astTypeDefConstructors % folded % #valConName % to baseName)
+    assertFreshNameForTypeDef n tydef =
+      when (elemOf typeDefNames n tydef) $ throwError $ TypeDefModifyNameClash n
 
 -- Helper for RenameModule action
 data RenameMods a = RM {imported :: [a], editable :: [a]}
@@ -1522,7 +1547,11 @@ tcWholeProg p = do
                 -- 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
+                ty <- getTypeDefConFieldType tda conSel.con fieldSel.index
+                id <- case fieldSel.meta of
+                  Left _ -> Nothing -- Any selection in a typedef should have TypeMeta, not ExprMeta
+                  Right m -> pure $ getID m
+                target <$> focusOnTy id ty
   pure $ p'{progSelection = newSel}
 
 -- | Do a full check of a 'Prog', both the imports and the local modules
@@ -1681,23 +1710,22 @@ 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], CaseFallback) -> m ([CaseBranch], CaseFallback)) ->
+  (Maybe (Type' ()) -> ([CaseBranch], CaseFallback) -> m ([CaseBranch], CaseFallback)) ->
   Expr ->
   m Expr
-transformCaseBranches prog type_ f = transformM $ \case
+transformCaseBranches type_ f = transformM $ \case
   Case m scrut bs fb -> 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
     (bs', fb') <-
       if fst (unfoldTApp scrutType) == TCon () type_
-        then f (bs, fb)
+        then f (m ^? _type % _Just % _chkedAt) (bs, fb)
         else pure (bs, fb)
     pure $ Case m scrut bs' fb'
   e -> pure e
@@ -1706,27 +1734,25 @@ transformCaseBranches prog type_ f = transformM $ \case
 -- expressions on the given type, leaving any fallback branch untouched.
 transformNamedCaseBranches ::
   MonadEdit m ProgError =>
-  Prog ->
   TyConName ->
-  ([CaseBranch] -> m [CaseBranch]) ->
+  (Maybe (Type' ()) -> [CaseBranch] -> m [CaseBranch]) ->
   Expr ->
   m Expr
-transformNamedCaseBranches prog type_ f = transformCaseBranches prog type_ (\(bs, fb) -> (,fb) <$> f bs)
+transformNamedCaseBranches type_ f = transformCaseBranches type_ (\m (bs, fb) -> (,fb) <$> f m bs)
 
 -- | Apply a bottom-up transformation to non-fallback case branches matching the
 -- given (type and) constructor.
 transformNamedCaseBranch ::
   MonadEdit m ProgError =>
-  Prog ->
   TyConName ->
   ValConName ->
   -- This only supports ADT case branches, since we cannot edit primitives
-  (CaseBranch -> m CaseBranch) ->
+  (Maybe (Type' ()) -> CaseBranch -> m CaseBranch) ->
   Expr ->
   m Expr
-transformNamedCaseBranch prog type_ con f = transformNamedCaseBranches prog type_ $
+transformNamedCaseBranch type_ con f = transformNamedCaseBranches type_ $ \m ->
   traverse $
-    \cb -> if caseBranchName cb == PatCon con then f cb else pure cb
+    \cb -> if caseBranchName cb == PatCon con then f m cb else pure cb
 
 progCxt :: Prog -> Cxt
 progCxt p = buildTypingContextFromModules (progAllModules p) (progSmartHoles p)
diff --git a/primer/src/Primer/App/Utils.hs b/primer/src/Primer/App/Utils.hs
index b56ee3dee..9be798646 100644
--- a/primer/src/Primer/App/Utils.hs
+++ b/primer/src/Primer/App/Utils.hs
@@ -7,9 +7,10 @@ import Foreword
 
 import Optics (mapped, (%), (%~), (.~))
 import Primer.App (Prog (..))
-import Primer.Core (_exprMeta, _exprTypeMeta, _type, _typeMeta)
+import Primer.Core (TypeMeta, _exprMeta, _exprTypeMeta, _type, _typeMeta)
 import Primer.Def (ASTDef (..))
 import Primer.Module (Module (..))
+import Primer.TypeDef (ASTTypeDef (..), ValCon (..))
 
 forgetProgTypecache :: Prog -> Prog
 forgetProgTypecache =
@@ -17,9 +18,13 @@ forgetProgTypecache =
     . (#progModules % mapped %~ forgetMod)
   where
     forgetMod :: Module -> Module
-    forgetMod = #moduleDefs % mapped % #_DefAST %~ forgetASTDef
+    forgetMod =
+      (#moduleDefs % mapped % #_DefAST %~ forgetASTDef)
+        . (#moduleTypes % mapped % #_TypeDefAST %~ forgetASTTypeDef)
     forgetASTDef :: ASTDef -> ASTDef
     forgetASTDef =
       (#astDefExpr % _exprMeta % _type .~ Nothing)
         . (#astDefExpr % _exprTypeMeta % _type .~ Nothing)
         . (#astDefType % _typeMeta % _type .~ Nothing)
+    forgetASTTypeDef :: ASTTypeDef TypeMeta -> ASTTypeDef TypeMeta
+    forgetASTTypeDef = #astTypeDefConstructors % mapped % #valConArgs % mapped % _typeMeta % _type .~ Nothing
diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index 9e52f023c..dcac95c1d 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -80,6 +80,7 @@ import Optics (
   JoinKinds,
   NoIx,
   Optic',
+  Traversal,
   WithIx,
   castOptic,
   equality,
@@ -92,10 +93,12 @@ import Optics (
   selfIndex,
   to,
   traverseOf,
+  traversed,
   (%),
+  (%~),
+  (.~),
   (^?),
  )
-import Optics.Traversal (traversed)
 import Primer.Core (
   Bind' (..),
   CaseBranch' (..),
@@ -120,6 +123,7 @@ import Primer.Core (
   TypeCacheBoth (..),
   TypeMeta,
   ValConName,
+  baseName,
   bindName,
   caseBranchName,
   qualifyName,
@@ -149,10 +153,12 @@ import Primer.Def (
 import Primer.Module (
   Module (
     moduleDefs,
-    moduleName
+    moduleName,
+    moduleTypes
   ),
   moduleDefsQualified,
   moduleTypesQualified,
+  moduleTypesQualifiedMeta,
  )
 import Primer.Name (Name, NameCounter)
 import Primer.Primitives (primConName, tChar, tInt)
@@ -162,7 +168,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 (
@@ -245,9 +254,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 =
@@ -292,7 +298,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}
@@ -309,8 +315,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
@@ -322,17 +328,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)
@@ -349,8 +354,16 @@ 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"
+      assert
+        (notElem (baseName tc) $ map (unLocalName . fst) params)
+        "Duplicate names in one tydef: between type-def-name and parameter-names"
+      traverseOf #_TypeDefAST (checkADTTypeDef tc) td
+    checkADTTypeDef tc td = do
       let params = astTypeDefParameters td
       let cons = astTypeDefConstructors td
       assert
@@ -362,16 +375,11 @@ checkTypeDefs tds = do
       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
@@ -407,16 +415,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)
@@ -424,7 +435,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/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 8e7895475..89c95e8e9 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,7 @@ module Tests.Action.Available where
 import Foreword
 
 import Control.Monad.Log (WithSeverity)
+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,6 +16,8 @@ import Data.Text qualified as T
 import Data.Text.Lazy qualified as TL
 import GHC.Err (error)
 import Hedgehog (
+  GenT,
+  LabelName,
   PropertyT,
   annotate,
   annotateShow,
@@ -51,8 +55,18 @@ import Primer.App (
   Level (Beginner, Expert, Intermediate),
   NodeSelection (..),
   NodeType (..),
-  ProgError (ActionError, DefAlreadyExists),
+  Prog (..),
+  ProgError (
+    ActionError,
+    ConAlreadyExists,
+    DefAlreadyExists,
+    TypeDefAlreadyExists,
+    TypeDefModifyNameClash
+  ),
   Selection' (..),
+  TypeDefConsSelection (TypeDefConsSelection),
+  TypeDefNodeSelection (TypeDefConsNodeSelection, TypeDefParamNodeSelection),
+  TypeDefSelection (TypeDefSelection),
   appProg,
   checkAppWellFormed,
   checkProgWellFormed,
@@ -60,12 +74,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,
@@ -132,6 +148,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, forgetTypeDefMetadata, typeDefAST)
 import Primer.Typecheck (
   CheckEverythingRequest (CheckEverything, toCheck, trusted),
   SmartHoles (NoSmartHoles, SmartHoles),
@@ -266,51 +283,126 @@ tasty_available_actions_accepted = withTests 500 $
       -- We only test SmartHoles mode (which is the only supported student-facing
       -- mode - NoSmartHoles is only used for internal sanity testing etc)
       a <- forAllT $ genApp SmartHoles cxt
+      let allTypes = progAllTypeDefsMeta $ appProg a
+          allTypes' = forgetTypeDefMetadata . snd <$> allTypes
       let allDefs = progAllDefs $ appProg a
+          allDefs' = snd <$> allDefs
       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 (first (SelectionDef . DefSelection defName) . 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 allTypes' allDefs' defName def'))
+               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 p l defMut allTypes' allDefs' defName def'
+                                )
+                              )
+                      )
+                    ,
+                      ( 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 allTypes' allDefs' defName def'))
+                            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 valConName n i l defMut allTypes' allDefs' defName def'
+                                            )
+                                          )
+                                    )
+                                  ]
+                      )
+                    ]
+        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
+                  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
+                  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
+          def <-
+            bitraverse
+              (maybe (annotate "primitive type def" >> failure) pure . typeDefAST . snd)
+              (maybe (annotate "primitive def" >> failure) pure . defAST . snd)
+              typeOrTermDef
           action <- forAllT $ Gen.element acts'
           collect action
           case action of
             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) (Right def') 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
@@ -318,7 +410,7 @@ tasty_available_actions_accepted = withTests 500 $
                     (map snd $ progAllDefs $ appProg a)
                     (progCxt $ appProg a)
                     l
-                    (Right def')
+                    def
                     loc
                     act'
               let opts' = [Gen.element $ (Offered,) <$> opts | not (null opts)]
@@ -332,7 +424,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 (Right def') 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 ::
@@ -365,6 +457,12 @@ tasty_available_actions_accepted = withTests 500 $
         (StudentProvided, (Left (ActionError (CaseBranchAlreadyExists (PatPrim _))), _)) -> do
           label "add duplicate primitive case branch"
           annotate "ignoring CaseBranchAlreadyExistsPrim error as was generated constructor"
+        (StudentProvided, (Left (TypeDefAlreadyExists _), _)) -> do
+          pure ()
+        (StudentProvided, (Left (ConAlreadyExists _), _)) -> do
+          pure ()
+        (StudentProvided, (Left (TypeDefModifyNameClash _), _)) -> do
+          pure ()
         (_, (Left err, _)) -> annotateShow err >> failure
         (_, (Right _, a'')) -> ensureSHNormal a''
     ensureSHNormal a = case checkAppWellFormed a of
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index 7dc380dfd..88b6f9c25 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -425,7 +425,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\"")
+        expectError (@?= TypeDefError "InternalError \"Duplicate parameter names in one tydef\"")
 
 -- Forbid clash between type name and parameter name
 unit_create_typedef_bad_6 :: Assertion
@@ -985,7 +985,7 @@ unit_RenameTypeParam_clash =
   progActionTest
     (defaultProgEditableTypeDefs $ pure [])
     [RenameTypeParam tT "a" "b"]
-    $ expectError (@?= ParamAlreadyExists "b")
+    $ expectError (@?= TypeDefModifyNameClash "b")
 
 unit_AddCon :: Assertion
 unit_AddCon =
@@ -1285,7 +1285,7 @@ unit_cross_module_actions =
               , Move $ ConChild 0
               , constructSaturatedCon cSucc
               , Move $ ConChild 0
-              , ConstructVar (LocalVarRef "a37")
+              , ConstructVar (LocalVarRef "a26")
               ]
           ]
         handleAndTC [RenameDef (qualifyM "foo") "bar"]