From 7644730d0d4db9386dff918e79ec5af2cc18384c Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Mon, 15 May 2023 12:41:53 +0100
Subject: [PATCH 01/21] refactor: Abstract over labelling in available actions
 property test

This will be necessary when we extend to typedefs, since we need to branch here, but can't use `label` in `GenT`.

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/test/Tests/Action/Available.hs | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 8e7895475..6bf6ee744 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -270,11 +270,15 @@ tasty_available_actions_accepted = withTests 500 $
       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)])
+      (defName, (defMut, def)) <-
+        maybe discard (\(t, x) -> label t >> pure x)
+          =<< forAllT
+            ( case partition (isMutable . fst . snd) $ Map.toList allDefs 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)]
+            )
       collect defMut
       case def of
         DefAST{} -> label "AST"

From 2b72a6144c2ca588ad9e3c8c48af17478d50cfd0 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Mon, 15 May 2023 13:27:58 +0100
Subject: [PATCH 02/21] refactor: Match actual function names in hedgehog
 output

This should have been done back when `forDef` etc. acquired their current names.

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/test/Tests/Action/Available.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 6bf6ee744..94ac4c3f9 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -287,18 +287,18 @@ tasty_available_actions_accepted = withTests 500 $
         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))
               ]
       case acts of

From b0aa0d8b430955927ba6d1a5402ae17c82ccfe50 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Wed, 17 May 2023 00:21:21 +0100
Subject: [PATCH 03/21] fix: `AddConField` action sets correct `TypeCache`s

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index f0145aff5..a5787315a 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -138,6 +138,8 @@ import Primer.Core (
   TyConName,
   Type,
   Type' (..),
+  TypeCache (..),
+  TypeCacheBoth (..),
   TypeMeta,
   ValConName,
   caseBranchName,
@@ -819,14 +821,14 @@ applyProgAction prog = \case
       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 $
         \(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

From d5796421c12015a27dae32c85b4489d775a04b60 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Wed, 17 May 2023 01:27:49 +0100
Subject: [PATCH 04/21] feat: allow "renaming" a type to its old name

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index a5787315a..d6307f111 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -650,7 +650,7 @@ 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
+    when (new /= old && new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new
     m' <- traverseOf #moduleTypes updateType m
     let renamedInTypes = over (traversed % #moduleTypes) updateRefsInTypes $ m' : ms
     pure

From 38955eb4f856764219879c96e1ff94c4bce2f741 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Wed, 17 May 2023 02:11:19 +0100
Subject: [PATCH 05/21] feat: make `AddInput` work in typedef con fields

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/Action.hs        | 27 ++++++++++++++++++---------
 primer/src/Primer/Action/Errors.hs |  5 +++--
 2 files changed, 21 insertions(+), 11 deletions(-)

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/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

From 679f23a6ea120f5c3c5f5f70cbbcb0bb63e693a4 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Tue, 20 Jun 2023 13:26:10 +0100
Subject: [PATCH 06/21] refactor: rename updateType{,Def} in applyProgAction

We rename these local definitions to clarify that they work on type
definitions, rather than types in the signature of term definitions or
elsewhere. We also wish to free up the name `updateType` for a future
helper that operates on types both in signatures and embedded inside
expressions.

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index d6307f111..e450edad9 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -651,7 +651,7 @@ applyProgAction prog = \case
         pure (m' : ms, 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
+    m' <- traverseOf #moduleTypes updateTypeDef m
     let renamedInTypes = over (traversed % #moduleTypes) updateRefsInTypes $ m' : ms
     pure
       ( over (traversed % #moduleDefs % traversed % #_DefAST) (updateDefBody . updateDefType) renamedInTypes
@@ -659,7 +659,7 @@ 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.
@@ -688,13 +688,13 @@ applyProgAction prog = \case
   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
@@ -711,13 +711,13 @@ 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)
           type_
@@ -745,7 +745,7 @@ applyProgAction prog = \case
   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' <-
@@ -761,7 +761,7 @@ applyProgAction prog = \case
       updateDefs allCons = transformNamedCaseBranches prog type_ $ \bs -> do
         m' <- DSL.meta
         pure $ insertSubseqBy caseBranchName (CaseBranch (PatCon con) [] (EmptyHole m')) (PatCon . valConName <$> allCons) bs
-      updateType =
+      updateTypeDef =
         alterTypeDef
           ( traverseOf
               #astTypeDefConstructors
@@ -788,7 +788,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'
@@ -801,7 +801,7 @@ applyProgAction prog = \case
             $ Nothing
         )
     where
-      updateType =
+      updateTypeDef =
         alterTypeDef
           ( traverseOf #astTypeDefConstructors $
               maybe (throwError $ ConNotFound con) pure

From eccb0cb6ad9c6297004faedde63a217bab2957da Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 23 May 2023 13:31:26 +0100
Subject: [PATCH 07/21] refactor: extract updateType helper in RenameType
 action

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index e450edad9..f7241653f 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,
@@ -670,21 +671,16 @@ applyProgAction prog = \case
       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
       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

From 6bbb4c14c678049b1e86d214e6e003f238e0e03c Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 23 May 2023 13:38:16 +0100
Subject: [PATCH 08/21] fix: update names in metadata when renaming type

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index f7241653f..236489240 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -151,7 +151,9 @@ import Primer.Core (
   unModuleName,
   unsafeMkGlobalName,
   unsafeMkLocalName,
+  _exprMeta,
   _exprMetaLens,
+  _type,
   _typeMetaLens,
  )
 import Primer.Core.DSL (S, create, emptyHole, tEmptyHole, tvar)
@@ -677,7 +679,12 @@ applyProgAction prog = \case
         over
           #astDefExpr
           $ transform
-          $ over typesInExpr updateType
+            ( 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

From 750fd9b59c9ee9794bd3faf36ec6e755d6e7c038 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 23 May 2023 21:20:13 +0100
Subject: [PATCH 09/21] fix: detect capture when renaming type param

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 236489240..eaef5cf01 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -156,9 +156,9 @@ import Primer.Core (
   _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 (..),
@@ -742,9 +742,7 @@ 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

From 12670ed694c95e16dd415185efabe49deed4c931 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Fri, 2 Jun 2023 15:36:09 +0100
Subject: [PATCH 10/21] fix: use cached type of scrut in transformCaseBranches

Instead of synthesising the type of the scrutinee from scratch, we just
read it from the TypeCache. This relies on the program always being in a
consistent state, which is tested by tasty_available_actions_accepted,
at least for interactions using SmartHoles and the "offered action" api.

This also fixes a bug: previously when we synthesised the type, we
needed to know the context that the scrutinee lives in. However, we only
used the `progCxt`, which is the "top-level"/"global" context -- in
particular this would fail if the scrutinee used a variable introduced
by a lambda (or let, etc).

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index eaef5cf01..5912611de 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -91,6 +91,7 @@ import Optics (
   (.~),
   (?~),
   (^.),
+  (^?),
   _Just,
   _Left,
   _Right,
@@ -153,6 +154,7 @@ import Primer.Core (
   unsafeMkLocalName,
   _exprMeta,
   _exprMetaLens,
+  _synthed,
   _type,
   _typeMetaLens,
  )
@@ -212,7 +214,6 @@ import Primer.Typecheck (
   buildTypingContextFromModules,
   checkEverything,
   checkTypeDefs,
-  synth,
  )
 import Primer.Zipper (
   ExprZ,
@@ -759,7 +760,7 @@ applyProgAction prog = \case
         , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing
         )
     where
-      updateDefs allCons = transformNamedCaseBranches prog type_ $ \bs -> do
+      updateDefs allCons = transformNamedCaseBranches type_ $ \bs -> do
         m' <- DSL.meta
         pure $ insertSubseqBy caseBranchName (CaseBranch (PatCon con) [] (EmptyHole m')) (PatCon . valConName <$> allCons) bs
       updateTypeDef =
@@ -827,7 +828,7 @@ applyProgAction prog = \case
             Just args' -> pure $ Con m con' args'
             Nothing -> throwError $ ConNotSaturated con
         e -> pure e
-      updateDecons = transformNamedCaseBranch prog type_ con $
+      updateDecons = transformNamedCaseBranch type_ con $
         \(CaseBranch vc binds e) -> do
           m' <- DSL.meta' $ Just (TCChkedAt (TEmptyHole ()))
           newName <- LocalName <$> freshName (freeVars e)
@@ -1686,18 +1687,16 @@ alterTypeDef f type_ m = do
 -- | Apply a bottom-up transformation to all branches of case expressions on the given type.
 transformCaseBranches ::
   MonadEdit m ProgError =>
-  Prog ->
   TyConName ->
   (([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)
@@ -1709,25 +1708,23 @@ 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]) ->
   Expr ->
   m Expr
-transformNamedCaseBranches prog type_ f = transformCaseBranches prog type_ (\(bs, fb) -> (,fb) <$> f bs)
+transformNamedCaseBranches type_ f = transformCaseBranches type_ (\(bs, fb) -> (,fb) <$> f 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) ->
   Expr ->
   m Expr
-transformNamedCaseBranch prog type_ con f = transformNamedCaseBranches prog type_ $
+transformNamedCaseBranch type_ con f = transformNamedCaseBranches type_ $
   traverse $
     \cb -> if caseBranchName cb == PatCon con then f cb else pure cb
 

From dbdf8a3a1a1b2b833d4c26eb0a9237e783c41c67 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Tue, 30 May 2023 21:52:07 +0100
Subject: [PATCH 11/21] fix: better metadata in new branch from AddCon

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 5912611de..d5671ab79 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -152,6 +152,7 @@ import Primer.Core (
   unModuleName,
   unsafeMkGlobalName,
   unsafeMkLocalName,
+  _chkedAt,
   _exprMeta,
   _exprMetaLens,
   _synthed,
@@ -760,8 +761,8 @@ applyProgAction prog = \case
         , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing
         )
     where
-      updateDefs allCons = transformNamedCaseBranches 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
       updateTypeDef =
         alterTypeDef
@@ -828,7 +829,7 @@ applyProgAction prog = \case
             Just args' -> pure $ Con m con' args'
             Nothing -> throwError $ ConNotSaturated con
         e -> pure e
-      updateDecons = transformNamedCaseBranch type_ con $
+      updateDecons = transformNamedCaseBranch type_ con . const $
         \(CaseBranch vc binds e) -> do
           m' <- DSL.meta' $ Just (TCChkedAt (TEmptyHole ()))
           newName <- LocalName <$> freshName (freeVars e)
@@ -1685,10 +1686,11 @@ 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 =>
   TyConName ->
-  (([CaseBranch], CaseFallback) -> m ([CaseBranch], CaseFallback)) ->
+  (Maybe (Type' ()) -> ([CaseBranch], CaseFallback) -> m ([CaseBranch], CaseFallback)) ->
   Expr ->
   m Expr
 transformCaseBranches type_ f = transformM $ \case
@@ -1699,7 +1701,7 @@ transformCaseBranches type_ f = transformM $ \case
       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
@@ -1709,10 +1711,10 @@ transformCaseBranches type_ f = transformM $ \case
 transformNamedCaseBranches ::
   MonadEdit m ProgError =>
   TyConName ->
-  ([CaseBranch] -> m [CaseBranch]) ->
+  (Maybe (Type' ()) -> [CaseBranch] -> m [CaseBranch]) ->
   Expr ->
   m Expr
-transformNamedCaseBranches type_ f = transformCaseBranches 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.
@@ -1721,12 +1723,12 @@ transformNamedCaseBranch ::
   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 type_ con f = transformNamedCaseBranches 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)

From 79f7a07663985c1ec1cdc8e4d06fb798796d835f Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Fri, 2 Jun 2023 21:34:52 +0100
Subject: [PATCH 12/21] chore: clarify variable naming in checkEverything

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/Typecheck.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index 9e52f023c..2ca5445de 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -410,13 +410,13 @@ checkEverything sh CheckEverything{trusted, toCheck} =
         let newTypes = foldMap' moduleTypesQualified toCheck
         checkTypeDefs newTypes
         local (extendTypeDefCxt newTypes) $ do
-          -- Kind check and update (for smartholes) all the types.
+          -- 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 +424,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

From 80bc02c7d2eaa0ea5fc4ba902b1eff8ab5c1352c Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Sat, 10 Jun 2023 00:21:23 +0100
Subject: [PATCH 13/21] fix: forgetProgTypecache also acts on typedefs

Since 6197cc180dfaf7c7ba18e0a8352da684516e64d7, type definitions have
contained metadata (since they need IDs so that we can run actions on
them). When forgetting metadata in a Prog, we also need to forget this
metadata.

The reason we have noticed this now is that we are aiming to upgrade the
`tasty_available_actions_accepted` test to cover typedef actions which
will require upgrading `checkEverything` to modify typedefs in a
subsequent commit (it may need to do smartholes, rather than just saying
"no"). As it will then update typecaches, the benchmark tests would
start to fail as (before this current commit) we were not properly
forgetting them.

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App/Utils.hs | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

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

From 61f97b75d320e0f73f8b719305c7a34d26704af5 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Fri, 2 Jun 2023 22:25:36 +0100
Subject: [PATCH 14/21] fix: checkEverything does smartholes inside typedefs

This is needed now that we have actions that affect typedefs.

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs         |  2 +-
 primer/src/Primer/Typecheck.hs   | 64 ++++++++++++++++++--------------
 primer/test/Tests/Action/Prog.hs |  2 +-
 3 files changed, 38 insertions(+), 30 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index d5671ab79..f8def4842 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -639,7 +639,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
diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index 2ca5445de..b2958dc79 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,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
+        (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 +372,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,13 +412,16 @@ 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
+        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.
-          updatedSigs <- 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 defsUpdatedSigs = itoListOf foldDefTypesWithName updatedSigs
           local (extendGlobalCxt defsUpdatedSigs) $
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index 7dc380dfd..bec36b8ed 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -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"]

From 2571fd58501ed75a848306767a3643a2c4980881 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Wed, 21 Jun 2023 20:24:22 +0100
Subject: [PATCH 15/21] refactor: explicit TC error for duplicate parameters

We now explicitly distinguish "two parameters in a typedef are named the
same" and "a parameter is named the same as a constructor, or two
constructors are named the same". (This is a somewhat silly split, as
the second one arguably would be better as two separate checks. The
reason it is broken up this way is that the first makes sense for
primitive typedefs, and the second does not.)

Previously, for ADTs, a repeated parameter name would have been caught
by the check that all parameters+ctors are distinctly named. However, we
now call `checkTypeDef` on primitives as well, which would not be
covered by the ADT check (but primitives are hardcoded and don't repeat
parameter names, so this is a somewhat pointless check).

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/Typecheck.hs   | 3 +++
 primer/test/Tests/Action/Prog.hs | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index b2958dc79..dcac95c1d 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -356,6 +356,9 @@ checkTypeDefs tds = do
     --   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"
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index bec36b8ed..eda3f6304 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

From b8ebb2665a1c0a22b62fe76e099509e3513ad7a8 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Fri, 2 Jun 2023 23:33:06 +0100
Subject: [PATCH 16/21] fix: add correct kind cache in AddConField

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 30 ++++++++++++++++++------------
 1 file changed, 18 insertions(+), 12 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index f8def4842..b98b14c60 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -132,6 +132,7 @@ import Primer.Core (
   GVarName,
   GlobalName (baseName, qualifiedModule),
   ID (..),
+  Kind (KType),
   LocalName (LocalName, unLocalName),
   Meta (..),
   ModuleName (ModuleName),
@@ -216,6 +217,7 @@ import Primer.Typecheck (
   checkEverything,
   checkTypeDefs,
  )
+import Primer.Typecheck qualified as TC
 import Primer.Zipper (
   ExprZ,
   Loc' (InBind, InExpr, InType),
@@ -805,19 +807,23 @@ applyProgAction prog = \case
         )
     where
       updateTypeDef =
-        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.

From e80b8a1f6dcd2e59c5f8bb111c80ade0c21b2c20 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Sat, 10 Jun 2023 01:15:34 +0100
Subject: [PATCH 17/21] fix: don't offer to delete in-use type params

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/API.hs              |  2 +-
 primer/src/Primer/Action/Available.hs | 15 +++++++++++----
 2 files changed, 12 insertions(+), 5 deletions(-)

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/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 ::

From e940ab6aa8275d0cf42f17cedc423588f1d7de36 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Tue, 20 Jun 2023 15:09:05 +0100
Subject: [PATCH 18/21] fix: tcWholeProg not change selection inside ctor field

Previously we would reset the selection to the root of the field's type,
instead of simply updating the metadata of the selection which may point
to some subtype.

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/App.hs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index b98b14c60..c4969cc5a 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -1533,7 +1533,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

From e1b9feec700787c76db50513bb62fc17066258bd Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 16 May 2023 23:16:32 +0100
Subject: [PATCH 19/21] test: Extend available actions property test to cover
 typedefs

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/test/Tests/Action/Available.hs | 111 ++++++++++++++++++++++----
 1 file changed, 96 insertions(+), 15 deletions(-)

diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 94ac4c3f9..f9e1a9eee 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,
@@ -53,6 +57,9 @@ import Primer.App (
   NodeType (..),
   ProgError (ActionError, DefAlreadyExists),
   Selection' (..),
+  TypeDefConsSelection (TypeDefConsSelection),
+  TypeDefNodeSelection (TypeDefConsNodeSelection, TypeDefParamNodeSelection),
+  TypeDefSelection (TypeDefSelection),
   appProg,
   checkAppWellFormed,
   checkProgWellFormed,
@@ -60,12 +67,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 +141,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,26 +276,93 @@ 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)) <-
-        maybe discard (\(t, x) -> label t >> pure x)
-          =<< forAllT
-            ( case partition (isMutable . fst . snd) $ Map.toList allDefs of
+      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 ("forDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName)))
               , defAST def <&> \d' -> (2,) $ do
@@ -301,20 +378,24 @@ tasty_available_actions_accepted = withTests 500 $
                   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
@@ -322,7 +403,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)]
@@ -336,7 +417,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 ::

From a565a5e4376350ba39acbc31ffb5c48ee6fc9564 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Sat, 10 Jun 2023 01:00:58 +0100
Subject: [PATCH 20/21] fix: ignore typedef name clashes for
 available-actions-accepted

This wasn't actually due to test failures, just something I noticed in
passing. The generators which create the initial program are very
unlikely to pick the same names as the test will try to create -- we
leave tweaking the generators to try to exercise this sort of thing more
as future work. (Also note that adding a typedef is not an "offered"
action, so that error wouldn't be hit here, however there is no harm in
explicitly ignoring it.)

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/test/Tests/Action/Available.hs | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index f9e1a9eee..df34773f4 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -55,7 +55,8 @@ import Primer.App (
   Level (Beginner, Expert, Intermediate),
   NodeSelection (..),
   NodeType (..),
-  ProgError (ActionError, DefAlreadyExists),
+  Prog (..),
+  ProgError (ActionError, ConAlreadyExists, DefAlreadyExists, ParamAlreadyExists, TypeDefAlreadyExists),
   Selection' (..),
   TypeDefConsSelection (TypeDefConsSelection),
   TypeDefNodeSelection (TypeDefConsNodeSelection, TypeDefParamNodeSelection),
@@ -450,6 +451,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 (ParamAlreadyExists _), _)) -> do
+          pure ()
         (_, (Left err, _)) -> annotateShow err >> failure
         (_, (Right _, a'')) -> ensureSHNormal a''
     ensureSHNormal a = case checkAppWellFormed a of

From 88728cfc68c03b0c6c2eef78669e1c8d1cfacf99 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Wed, 21 Jun 2023 18:52:28 +0100
Subject: [PATCH 21/21] fix!: typedef actions detects all name clashes

Previously we did not consistently check our input names were fresh,
leading to some actions being accepted, only to later throw a
typechecker error. We now always check the new name is fresh, but for
ease of maintainability we collapse all such errors into one
category (previously we had both `ParamAlreadyExists` and
`TyConParamClash`). Instead of collapsing them, we could split out 5
different sorts of clashes (see comment on `TypeDefModifyNameClash` in
this commit), but this does not seem necessary -- as far as I know,
nobody actually wants to distinguish which of these 5 sorts of clashes
happened.

BREAKING CHANGE: this changes `ProgError`, which is serialised in the
richly-typed API (but not the OpenAPI -- they are converted into http
error codes instead).

Signed-off-by: Ben Price <ben@hackworthltd.com>
---
 primer/src/Primer/Action/ProgError.hs | 10 ++++--
 primer/src/Primer/App.hs              | 44 ++++++++++++++++++---------
 primer/test/Tests/Action/Available.hs | 10 ++++--
 primer/test/Tests/Action/Prog.hs      |  2 +-
 4 files changed, 46 insertions(+), 20 deletions(-)

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 c4969cc5a..12ebc7a96 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -78,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,
@@ -672,7 +677,7 @@ applyProgAction prog = \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
+        assertFreshNameForTypeDef nameRaw (old, d0)
         pure $ Map.insert nameRaw (TypeDefAST d0) $ Map.delete (baseName old) m
       updateRefsInTypes =
         over
@@ -703,11 +708,14 @@ applyProgAction prog = \case
     where
       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 =
@@ -726,12 +734,10 @@ applyProgAction prog = \case
     where
       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
@@ -768,9 +774,12 @@ applyProgAction prog = \case
         pure $ insertSubseqBy caseBranchName (CaseBranch (PatCon con) [] (EmptyHole m')) (PatCon . valConName <$> allCons) bs
       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
@@ -872,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
@@ -1007,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]}
diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index df34773f4..89c95e8e9 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -56,7 +56,13 @@ import Primer.App (
   NodeSelection (..),
   NodeType (..),
   Prog (..),
-  ProgError (ActionError, ConAlreadyExists, DefAlreadyExists, ParamAlreadyExists, TypeDefAlreadyExists),
+  ProgError (
+    ActionError,
+    ConAlreadyExists,
+    DefAlreadyExists,
+    TypeDefAlreadyExists,
+    TypeDefModifyNameClash
+  ),
   Selection' (..),
   TypeDefConsSelection (TypeDefConsSelection),
   TypeDefNodeSelection (TypeDefConsNodeSelection, TypeDefParamNodeSelection),
@@ -455,7 +461,7 @@ tasty_available_actions_accepted = withTests 500 $
           pure ()
         (StudentProvided, (Left (ConAlreadyExists _), _)) -> do
           pure ()
-        (StudentProvided, (Left (ParamAlreadyExists _), _)) -> do
+        (StudentProvided, (Left (TypeDefModifyNameClash _), _)) -> do
           pure ()
         (_, (Left err, _)) -> annotateShow err >> failure
         (_, (Right _, a'')) -> ensureSHNormal a''
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index eda3f6304..88b6f9c25 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -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 =