From c0f66a47df0b66b03504b245c96aa5d16485ccc2 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/23] 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>
---
 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 93a32760c37f5e6c267dbb918f1eb52b70aef7a0 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/23] 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>
---
 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 f1a59dad47788a5b8763a1247b04aaa5d8464b60 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 16 May 2023 23:16:32 +0100
Subject: [PATCH 03/23] test: Extend available actions property test to cover
 typedefs

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

diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 94ac4c3f9..16ada421e 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, typeDefAST)
 import Primer.Typecheck (
   CheckEverythingRequest (CheckEverything, toCheck, trusted),
   SmartHoles (NoSmartHoles, SmartHoles),
@@ -266,26 +276,91 @@ 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
       let allDefs = progAllDefs $ appProg a
       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))
+               in Gen.frequency
+                    [ (1, pure forTypeDef)
+                    ,
+                      ( 2
+                      , case astTypeDefParameters def' of
+                          [] -> pure forTypeDef
+                          ps -> do
+                            (p, _) <- Gen.element ps
+                            pure
+                              ( "forTypeDefParamNode"
+                              ,
+                                ( typeDefSel $ Just $ TypeDefParamNodeSelection p
+                                , Available.forTypeDefParamNode l defMut
+                                )
+                              )
+                      )
+                    ,
+                      ( 5
+                      , case astTypeDefConstructors def' of
+                          [] -> pure forTypeDef
+                          cs -> do
+                            ValCon{valConName, valConArgs} <- Gen.element cs
+                            let typeDefConsNodeSel = typeDefSel . Just . TypeDefConsNodeSelection . TypeDefConsSelection valConName
+                                forTypeDefConsNode = ("forTypeDefConsNode", (typeDefConsNodeSel Nothing, Available.forTypeDefConsNode l defMut))
+                            case valConArgs of
+                              [] -> pure forTypeDefConsNode
+                              as ->
+                                Gen.frequency
+                                  [ (1, pure forTypeDefConsNode)
+                                  ,
+                                    ( 5
+                                    , do
+                                        (n, t) <- Gen.element $ zip [0 ..] as
+                                        i <- Gen.element $ t ^.. typeIDs
+                                        pure
+                                          ( "forTypeDefConsFieldNode"
+                                          ,
+                                            ( typeDefConsNodeSel . Just $ TypeDefConsFieldSelection n i
+                                            , Available.forTypeDefConsFieldNode l defMut def' valConName n i
+                                            )
+                                          )
+                                    )
+                                  ]
+                      )
+                    ]
+        Right (defName, def) ->
+          fmap (first (SelectionDef . DefSelection defName) . snd) . forAllWithT fst . Gen.frequency $
             catMaybes
               [ Just (1, pure ("forDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName)))
               , defAST def <&> \d' -> (2,) $ do
@@ -301,20 +376,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 +401,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 +415,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 ead8c8945ac467f16bc9a7e82bb2aed8cd1a1fb0 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Wed, 17 May 2023 00:21:21 +0100
Subject: [PATCH 04/23] `AddConField` - update TC

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

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index f0145aff5..2a0a772e8 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,16 @@ applyProgAction prog = \case
       updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons)
       updateCons = transformM $ \case
         Con m con' tms | con' == con -> do
-          m' <- DSL.meta
+          id <- fresh
+          let m' = Meta id (Just (TCEmb $ TCBoth (TEmptyHole ()) (TEmptyHole ()))) Nothing
           case insertAt index (EmptyHole m') tms of
             Just args' -> pure $ Con m con' args'
             Nothing -> throwError $ ConNotSaturated con
         e -> pure e
       updateDecons = transformNamedCaseBranch prog type_ con $
         \(CaseBranch vc binds e) -> do
-          m' <- DSL.meta
+          id <- fresh
+          let m' = Meta id (Just (TCChkedAt (TEmptyHole ()))) Nothing
           newName <- LocalName <$> freshName (freeVars e)
           binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds
           pure $ CaseBranch vc binds' e

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

Signed-off-by: George Thomas <georgefsthomas@gmail.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 2a0a772e8..ebd75fc6c 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 eec165951000325d5faa717d409176e08660405c Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Wed, 17 May 2023 02:11:19 +0100
Subject: [PATCH 06/23] make `AddInput` work in con fields

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
---
 primer/src/Primer/Action.hs           | 35 ++++++++++++++++++---------
 primer/src/Primer/Action/Errors.hs    |  5 ++--
 primer/test/Tests/Action/Available.hs |  3 ++-
 3 files changed, 28 insertions(+), 15 deletions(-)

diff --git a/primer/src/Primer/Action.hs b/primer/src/Primer/Action.hs
index 286cfdbd6..ed0f3c9bf 100644
--- a/primer/src/Primer/Action.hs
+++ b/primer/src/Primer/Action.hs
@@ -30,6 +30,7 @@ import Control.Monad.Fresh (MonadFresh)
 import Data.Aeson (Value)
 import Data.Bifunctor.Swap qualified as Swap
 import Data.Bitraversable (bisequence)
+import Data.Data (Data)
 import Data.Functor.Compose (Compose (..))
 import Data.Generics.Product (typed)
 import Data.List (delete, findIndex, insertBy)
@@ -1051,6 +1052,7 @@ renameForall b zt = case target zt of
 
 -- | Convert a high-level 'Available.NoInputAction' to a concrete sequence of 'ProgAction's.
 toProgActionNoInput ::
+  (HasID a, Data a) =>
   DefMap ->
   Either (ASTTypeDef a) ASTDef ->
   Selection' ID ->
@@ -1084,18 +1086,27 @@ toProgActionNoInput defs def0 sel0 = \case
     -- on the domain (left) side of the arrow.
     toProgAction [ConstructArrowL, Move Child1]
   Available.AddInput -> do
-    -- This action traverses the function type and adds a function arrow to the end of it,
-    -- resulting in a new argument type. The result type is unchanged.
-    -- The cursor location is also unchanged.
-    -- e.g. A -> B -> C ==> A -> B -> ? -> C
-    id <- 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
+        -- This action traverses the function type and adds a function arrow to the end of it,
+        -- resulting in a new argument type. The result type is unchanged.
+        -- The cursor location is also unchanged.
+        -- e.g. A -> B -> C ==> A -> B -> ? -> C
+        id <- nodeID
+        forgetTypeMetadata <$> case findType id $ astDefType def of
+          Just t -> pure t
+          Nothing -> case map fst $ findNodeWithParent id $ astDefExpr def of
+            Just (TypeNode t) -> pure t
+            Just sm -> Left $ NeedType sm
+            Nothing -> Left $ IDNotFound id
     l <- case type_ of
       TFun _ a b -> pure $ NE.length $ fst $ unfoldFun a b
       t -> Left $ NeedTFun t
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/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 16ada421e..648f894ac 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -86,6 +86,7 @@ import Primer.Core (
   ModuleName (ModuleName, unModuleName),
   Pattern (PatPrim),
   Type,
+  TypeMeta,
   getID,
   mkSimpleModuleName,
   moduleNamePretty,
@@ -701,7 +702,7 @@ offeredActionTest' sh l inputDef position action = do
     Left a ->
       pure $
         if Available.NoInput a `elem` offered
-          then Right $ toProgActionNoInput (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a
+          then Right $ toProgActionNoInput @TypeMeta (foldMap' moduleDefsQualified $ progModules prog) (Right exprDef) (SelectionDef $ DefSelection exprDefName $ Just $ NodeSelection BodyNode id) a
           else Left $ ActionNotOffered (Available.NoInput a) offered
     Right (a, o) -> do
       if Available.Input a `elem` offered

From 1ad0eec111ea67c3478533d7f53baa4710284659 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 23 May 2023 13:14:34 +0100
Subject: [PATCH 07/23] less strict duplicate name checking

we never consistently checked these things in `applyProgAction`, and it would be awkward to do so. besides, why do we care?

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
---
 primer/src/Primer/App.hs         |  4 ----
 primer/src/Primer/Typecheck.hs   |  9 +++------
 primer/test/Tests/Action/Prog.hs | 26 +-------------------------
 3 files changed, 4 insertions(+), 35 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index ebd75fc6c..0d5e69063 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -665,7 +665,6 @@ 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
         pure $ Map.insert nameRaw (TypeDefAST d0) $ Map.delete (baseName old) m
       updateRefsInTypes =
         over
@@ -723,9 +722,6 @@ applyProgAction prog = \case
           type_
       updateParam def = do
         when (new `elem` map fst (astTypeDefParameters def)) $ throwError $ ParamAlreadyExists new
-        let nameRaw = unLocalName new
-        when (nameRaw == baseName type_) $ throwError $ TyConParamClash nameRaw
-        when (nameRaw `elem` map (baseName . valConName) (astTypeDefConstructors def)) $ throwError $ ValConParamClash nameRaw
         def
           & traverseOf
             #astTypeDefParameters
diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index f57ae36d9..3119b309c 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -106,7 +106,7 @@ import Primer.Core (
   Expr' (..),
   ExprMeta,
   GVarName,
-  GlobalName (baseName, qualifiedModule),
+  GlobalName (qualifiedModule),
   ID,
   Kind (..),
   LVarName,
@@ -362,11 +362,8 @@ checkTypeDefs tds = do
         )
         "Module name of type and all constructors must be the same"
       assert
-        (distinct $ map (unLocalName . fst) params <> map (baseName . valConName) cons)
-        "Duplicate names in one tydef: between parameter-names and constructor-names"
-      assert
-        (notElem (baseName tc) $ map (unLocalName . fst) params)
-        "Duplicate names in one tydef: between type-def-name and parameter-names"
+        (distinct $ map (unLocalName . fst) params)
+        "Duplicate parameter names in one tydef"
       local (noSmartHoles . extendLocalCxtTys params) $
         mapM_ (checkKind' KType <=< fakeMeta) $
           concatMap valConArgs cons
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index 7dc380dfd..82d7e381a 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -425,31 +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\"")
-
--- Forbid clash between type name and parameter name
-unit_create_typedef_bad_6 :: Assertion
-unit_create_typedef_bad_6 =
-  let td =
-        ASTTypeDef
-          { astTypeDefParameters = [("T", KType)]
-          , astTypeDefConstructors = []
-          , astTypeDefNameHints = []
-          }
-   in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $
-        expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between type-def-name and parameter-names\"")
-
--- Forbid clash between parameter name and constructor name
-unit_create_typedef_bad_7 :: Assertion
-unit_create_typedef_bad_7 =
-  let td =
-        ASTTypeDef
-          { astTypeDefParameters = [("a", KType)]
-          , astTypeDefConstructors = [ValCon (vcn "a") []]
-          , astTypeDefNameHints = []
-          }
-   in progActionTest defaultEmptyProg [AddTypeDef (tcn "T") td] $
-        expectError (@?= TypeDefError "InternalError \"Duplicate names in one tydef: between parameter-names and constructor-names\"")
+        expectError (@?= TypeDefError "InternalError \"Duplicate parameter names in one tydef\"")
 
 -- Forbid clash between type name and name of a primitive type
 unit_create_typedef_bad_prim :: Assertion

From 3af356fd30318569b4d677fa45cc48ab8366e87b Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 23 May 2023 13:31:26 +0100
Subject: [PATCH 08/23] refactor - updateType'

-- TODO rename `updateType` to `updateTypeDef` and this to `updateType`? in all branches?

Signed-off-by: George Thomas <georgefsthomas@gmail.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 0d5e69063..5c13aee79 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,
@@ -669,21 +670,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 59a75dd79413146a381767d6fd1181b8f3d3f300 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 23 May 2023 13:38:16 +0100
Subject: [PATCH 09/23] update names in metadata when renaming type

Signed-off-by: George Thomas <georgefsthomas@gmail.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 5c13aee79..d574f057b 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)
@@ -676,7 +678,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 dd5b275838ff53d4b1e62f7b75bfa8bc16b3161b Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Tue, 23 May 2023 21:20:13 +0100
Subject: [PATCH 10/23] detect capture when renaming type param

Signed-off-by: George Thomas <georgefsthomas@gmail.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 d574f057b..18a3698de 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 (..),
@@ -738,9 +738,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 19fd24181e791363b1fce0371225bf749953ee25 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Wed, 24 May 2023 11:59:15 +0100
Subject: [PATCH 11/23] WIP - more fixes needed (see TODOs, then re-run test to
 check for more)

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
---
 primer/src/Primer/App.hs              | 13 +++++++------
 primer/test/Tests/Action/Available.hs | 16 ++++++++++++++--
 2 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 18a3698de..d577be573 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -755,6 +755,8 @@ applyProgAction prog = \case
         , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing
         )
     where
+      -- TODO we sometimes don't write the expected metadata
+      -- meaning that type checking modifies the tree further
       updateDefs allCons = transformNamedCaseBranches prog type_ $ \bs -> do
         m' <- DSL.meta
         pure $ insertSubseqBy caseBranchName (CaseBranch (PatCon con) [] (EmptyHole m')) (PatCon . valConName <$> allCons) bs
@@ -936,7 +938,7 @@ applyProgAction prog = \case
     let smartHoles = progSmartHoles prog
     applyActionsToField smartHoles (progImports prog) ms (defName, con, index, def) actions >>= \case
       Left err -> throwError $ ActionError err
-      Right (mod', zt) ->
+      Right (mod', _zt) ->
         pure
           ( mod'
           , Just $
@@ -949,11 +951,8 @@ applyProgAction prog = \case
                           TypeDefConsSelection
                             { con
                             , field =
-                                Just
-                                  TypeDefConsFieldSelection
-                                    { index
-                                    , meta = Right $ zt ^. _target % _typeMetaLens
-                                    }
+                                -- TODO if we set selection, we get weird metadata errors
+                                Nothing
                             }
                   }
           )
@@ -1695,6 +1694,8 @@ transformCaseBranches prog type_ f = transformM $ \case
       fst
         <$> runReaderT
           (liftError (ActionError . TypeError) $ synth scrut)
+          -- TODO we need the local cxt here as well, somehow
+          -- would avoid unknown-variable errors in `AddConField`, at least
           (progCxt prog)
     (bs', fb') <-
       if fst (unfoldTApp scrutType) == TCon () type_
diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 648f894ac..533aa010a 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -7,6 +7,7 @@ module Tests.Action.Available where
 import Foreword
 
 import Control.Monad.Log (WithSeverity)
+import Data.Aeson.Text (encodeToLazyText)
 import Data.Bitraversable (bitraverse)
 import Data.ByteString.Lazy.Char8 qualified as BS
 import Data.List.Extra (enumerate, partition)
@@ -24,6 +25,7 @@ import Hedgehog (
   collect,
   discard,
   failure,
+  footnoteShow,
   label,
   success,
   (===),
@@ -31,6 +33,7 @@ import Hedgehog (
 import Hedgehog.Gen qualified as Gen
 import Hedgehog.Internal.Property (forAllWithT)
 import Optics (ix, toListOf, (%), (.~), (^..), _head)
+import Primer.API (viewProg)
 import Primer.Action (
   ActionError (CaseBindsClash, CaseBranchAlreadyExists, NameCapture),
   Movement (Child1, Child2),
@@ -55,6 +58,7 @@ import Primer.App (
   Level (Beginner, Expert, Intermediate),
   NodeSelection (..),
   NodeType (..),
+  Prog (..),
   ProgError (ActionError, DefAlreadyExists),
   Selection' (..),
   TypeDefConsSelection (TypeDefConsSelection),
@@ -386,9 +390,16 @@ tasty_available_actions_accepted = withTests 500 $
               (maybe (annotate "primitive type def" >> failure) pure . typeDefAST . snd)
               (maybe (annotate "primitive def" >> failure) pure . defAST . snd)
               typeOrTermDef
-          action <- forAllT $ Gen.element acts'
+          let bias = Nothing
+          -- these seem to be the only two action which still cause errors
+          -- let bias = Just $ Available.Input Available.AddCon
+          -- let bias = Just $ Available.NoInput Available.AddConField
+          action <- maybe (forAllT $ Gen.element acts') pure $ (bias <*) . guard . (`elem` acts') =<< bias
           collect action
+          footnoteShow action
           case action of
+            act@(Available.Input Available.AddCon) | Just act /= bias -> discard
+            act@(Available.NoInput Available.AddConField) | Just act /= bias -> discard
             Available.NoInput act' -> do
               progActs <-
                 either (\e -> annotateShow e >> failure) pure $
@@ -429,7 +440,8 @@ tasty_available_actions_accepted = withTests 500 $
     actionSucceeds :: HasCallStack => EditAppM (PureLog (WithSeverity ())) ProgError a -> App -> PropertyT WT ()
     actionSucceeds m a =
       runEditAppMLogs m a >>= \case
-        (Left err, _) -> annotateShow err >> failure
+        -- copy output to primer-app to view prog - use as `initialProg` arg to `AppProg` in `App.tsx`
+        (Left err, _) -> annotateShow err >> annotate (TL.unpack $ encodeToLazyText $ viewProg $ appProg a) >> failure
         (Right _, a') -> ensureSHNormal a'
     -- If we submit our own name rather than an offered one, then
     -- we should expect that name capture/clashing may happen

From 88fad9ffec214eb9f8f3798483b7f1d038136ff0 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Tue, 30 May 2023 21:52:07 +0100
Subject: [PATCH 12/23] fix: better metadata on rhs of new branch when addcon;
 that action now fails for different reason

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
---
 primer/src/Primer/App.hs | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index d577be573..7e34636f8 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -91,6 +91,7 @@ import Optics (
   (.~),
   (?~),
   (^.),
+  (^?),
   _Just,
   _Left,
   _Right,
@@ -151,6 +152,7 @@ import Primer.Core (
   unModuleName,
   unsafeMkGlobalName,
   unsafeMkLocalName,
+  _chkedAt,
   _exprMeta,
   _exprMetaLens,
   _type,
@@ -755,10 +757,8 @@ applyProgAction prog = \case
         , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing
         )
     where
-      -- TODO we sometimes don't write the expected metadata
-      -- meaning that type checking modifies the tree further
-      updateDefs allCons = transformNamedCaseBranches prog type_ $ \bs -> do
-        m' <- DSL.meta
+      updateDefs allCons = transformNamedCaseBranches prog 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 =
         alterTypeDef
@@ -826,7 +826,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 prog type_ con . const $
         \(CaseBranch vc binds e) -> do
           id <- fresh
           let m' = Meta id (Just (TCChkedAt (TEmptyHole ()))) Nothing
@@ -1681,11 +1681,12 @@ 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
@@ -1699,7 +1700,7 @@ transformCaseBranches prog type_ f = transformM $ \case
           (progCxt prog)
     (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
@@ -1710,10 +1711,10 @@ 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 prog type_ f = transformCaseBranches prog type_ (\m (bs, fb) -> (,fb) <$> f m bs)
 
 -- | Apply a bottom-up transformation to non-fallback case branches matching the
 -- given (type and) constructor.
@@ -1723,12 +1724,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 prog type_ con f = transformNamedCaseBranches prog type_ $
+transformNamedCaseBranch prog type_ con f = transformNamedCaseBranches prog 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 a779b5cceff1795abb867646691c1bacfb9ed6d1 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Fri, 2 Jun 2023 15:36:09 +0100
Subject: [PATCH 13/23] fix: use cached type of scrut in
 transformCaseBranches...

I now understand your comment about needing the local cxt! I don't know
why it was implemented in this way in the first place, and it seems
rather silly given that we now (I changed this a few commits ago) extract the cached chkedAt type below!

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

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 7e34636f8..c9229f3ae 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -155,6 +155,7 @@ import Primer.Core (
   _chkedAt,
   _exprMeta,
   _exprMetaLens,
+  _synthed,
   _type,
   _typeMetaLens,
  )
@@ -214,7 +215,6 @@ import Primer.Typecheck (
   buildTypingContextFromModules,
   checkEverything,
   checkTypeDefs,
-  synth,
  )
 import Primer.Zipper (
   ExprZ,
@@ -757,7 +757,7 @@ applyProgAction prog = \case
         , Just $ SelectionTypeDef $ TypeDefSelection type_ $ Just $ TypeDefConsNodeSelection $ TypeDefConsSelection con Nothing
         )
     where
-      updateDefs allCons = transformNamedCaseBranches prog type_ $ \t' bs -> do
+      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 =
@@ -826,7 +826,7 @@ applyProgAction prog = \case
             Just args' -> pure $ Con m con' args'
             Nothing -> throwError $ ConNotSaturated con
         e -> pure e
-      updateDecons = transformNamedCaseBranch prog type_ con . const $
+      updateDecons = transformNamedCaseBranch type_ con . const $
         \(CaseBranch vc binds e) -> do
           id <- fresh
           let m' = Meta id (Just (TCChkedAt (TEmptyHole ()))) Nothing
@@ -1684,20 +1684,16 @@ alterTypeDef f type_ m = do
 -- The transformation function gets the type the case was checked at as well as all the branches.
 transformCaseBranches ::
   MonadEdit m ProgError =>
-  Prog ->
   TyConName ->
   (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)
-          -- TODO we need the local cxt here as well, somehow
-          -- would avoid unknown-variable errors in `AddConField`, at least
-          (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 (m ^? _type % _Just % _chkedAt) (bs, fb)
@@ -1709,25 +1705,23 @@ transformCaseBranches prog type_ f = transformM $ \case
 -- expressions on the given type, leaving any fallback branch untouched.
 transformNamedCaseBranches ::
   MonadEdit m ProgError =>
-  Prog ->
   TyConName ->
   (Maybe (Type' ()) -> [CaseBranch] -> m [CaseBranch]) ->
   Expr ->
   m Expr
-transformNamedCaseBranches prog type_ f = transformCaseBranches prog type_ (\m (bs, fb) -> (,fb) <$> f m 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
   (Maybe (Type' ()) -> CaseBranch -> m CaseBranch) ->
   Expr ->
   m Expr
-transformNamedCaseBranch prog type_ con f = transformNamedCaseBranches prog type_ $ \m ->
+transformNamedCaseBranch type_ con f = transformNamedCaseBranches type_ $ \m ->
   traverse $
     \cb -> if caseBranchName cb == PatCon con then f m cb else pure cb
 

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

Signed-off-by: George Thomas <georgefsthomas@gmail.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 3119b309c..752375909 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -409,13 +409,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)
@@ -423,7 +423,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 b3590e62853203516489ce5aac9be91e139397f9 Mon Sep 17 00:00:00 2001
From: Ben Price <ben@hackworthltd.com>
Date: Fri, 2 Jun 2023 22:25:36 +0100
Subject: [PATCH 15/23] fix: checkEverything does smartholes inside typedefs

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
---
 primer/src/Primer/App.hs       |  2 +-
 primer/src/Primer/Typecheck.hs | 63 ++++++++++++++++++----------------
 2 files changed, 34 insertions(+), 31 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index c9229f3ae..783bc8307 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))
+          (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 752375909..bdb8056e6 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -71,6 +71,8 @@ import Data.Map qualified as M
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as S
 import Optics (
+  (.~),
+  (%~),
   A_Prism,
   A_Setter,
   A_Traversal,
@@ -95,9 +97,8 @@ import Optics (
   traverseOf,
   (%),
   (^?),
-  _Just,
- )
-import Optics.Traversal (traversed)
+  _Just, Traversal,
+ traversed)
 import Primer.Core (
   Bind' (..),
   CaseBranch' (..),
@@ -130,7 +131,7 @@ import Primer.Core (
   _exprMeta,
   _exprTypeMeta,
   _synthed,
-  _typeMeta,
+  _typeMeta, baseName,
  )
 import Primer.Core.DSL (S, branch, create', emptyHole, meta, meta')
 import Primer.Core.Transform (decomposeTAppCon, mkTAppCon, unfoldTApp)
@@ -151,10 +152,10 @@ import Primer.Def (
 import Primer.Module (
   Module (
     moduleDefs,
-    moduleName
+    moduleName, moduleTypes
   ),
   moduleDefsQualified,
-  moduleTypesQualified,
+  moduleTypesQualified, moduleTypesQualifiedMeta,
  )
 import Primer.Name (Name, NameCounter)
 import Primer.Primitives (primConName, tChar, tInt)
@@ -164,7 +165,7 @@ import Primer.TypeDef (
   TypeDef (..),
   TypeDefMap,
   ValCon (valConArgs, valConName),
-  typeDefAST,
+  typeDefAST, forgetTypeDefMetadata, typeDefParameters, generateTypeDefIDs,
  )
 import Primer.Typecheck.Cxt (Cxt (Cxt, globalCxt, localCxt, smartHoles, typeDefs))
 import Primer.Typecheck.Kindcheck (
@@ -294,7 +295,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}
@@ -311,8 +312,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
@@ -324,17 +325,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)
@@ -351,8 +351,13 @@ checkTypeDefs tds = do
     -- But note that we allow
     -- - type names clashing with constructor names (possibly in different
     --   types)
-
     checkTypeDef tc td = do
+      let params = typeDefParameters td
+      assert
+        (distinct $ map (unLocalName . fst) params)
+        "Duplicate parameter names in one tydef"
+      traverseOf #_TypeDefAST (checkADTTypeDef tc) td
+    checkADTTypeDef tc td = do
       let params = astTypeDefParameters td
       let cons = astTypeDefConstructors td
       assert
@@ -361,16 +366,11 @@ checkTypeDefs tds = do
               qualifiedModule tc : fmap (qualifiedModule . valConName) cons
         )
         "Module name of type and all constructors must be the same"
-      assert
-        (distinct $ map (unLocalName . fst) params)
-        "Duplicate parameter names in one tydef"
-      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
@@ -406,13 +406,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) $

From d3a0d6e355a5bfd5fa1d9df51085ea88a66c6d9e 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/23] fix: stable kind cache when AddConField

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

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 783bc8307..7b2cfec42 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -157,7 +157,7 @@ import Primer.Core (
   _exprMetaLens,
   _synthed,
   _type,
-  _typeMetaLens,
+  _typeMetaLens, Kind (KType),
  )
 import Primer.Core.DSL (S, create, emptyHole, tEmptyHole)
 import Primer.Core.DSL qualified as DSL
@@ -800,8 +800,10 @@ applyProgAction prog = \case
             $ Nothing
         )
     where
-      updateType =
-        alterTypeDef
+      updateType  =
+        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
@@ -809,7 +811,7 @@ applyProgAction prog = \case
                   ( traverseOf
                       #valConArgs
                       ( maybe (throwError $ IndexOutOfRange index) pure
-                          <=< liftA2 (insertAt index) (generateTypeIDs new) . pure
+                          <=< liftA2 (insertAt index) new' . pure
                       )
                   )
           )

From ba123ab04cdb8a24416a48b3c361f921d52b9437 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Fri, 9 Jun 2023 21:49:38 +0100
Subject: [PATCH 17/23] post-rebase fixup - format and fix warnings

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
---
 primer/src/Primer/App.hs       | 38 +++++++++++++++++++---------------
 primer/src/Primer/Typecheck.hs | 29 +++++++++++++++-----------
 2 files changed, 38 insertions(+), 29 deletions(-)

diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 7b2cfec42..1cddaaa81 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),
@@ -157,7 +158,7 @@ import Primer.Core (
   _exprMetaLens,
   _synthed,
   _type,
-  _typeMetaLens, Kind (KType),
+  _typeMetaLens,
  )
 import Primer.Core.DSL (S, create, emptyHole, tEmptyHole)
 import Primer.Core.DSL qualified as DSL
@@ -216,6 +217,7 @@ import Primer.Typecheck (
   checkEverything,
   checkTypeDefs,
  )
+import Primer.Typecheck qualified as TC
 import Primer.Zipper (
   ExprZ,
   Loc' (InBind, InExpr, InType),
@@ -639,7 +641,7 @@ applyProgAction prog = \case
       -- see https://github.com/hackworthltd/primer/issues/3)
       (TypeDefError . show @TypeError)
       ( runReaderT
-          (checkTypeDefs $ Map.singleton tc td')
+          (void $ checkTypeDefs $ Map.singleton tc td')
           (buildTypingContextFromModules (progAllModules prog) NoSmartHoles)
       )
     pure
@@ -800,22 +802,24 @@ applyProgAction prog = \case
             $ Nothing
         )
     where
-      updateType  =
-        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
+      updateType =
+        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.
diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index bdb8056e6..4031f329e 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -71,8 +71,6 @@ import Data.Map qualified as M
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as S
 import Optics (
-  (.~),
-  (%~),
   A_Prism,
   A_Setter,
   A_Traversal,
@@ -83,6 +81,7 @@ import Optics (
   JoinKinds,
   NoIx,
   Optic',
+  Traversal,
   WithIx,
   castOptic,
   equality,
@@ -95,10 +94,13 @@ import Optics (
   selfIndex,
   to,
   traverseOf,
+  traversed,
   (%),
+  (%~),
+  (.~),
   (^?),
-  _Just, Traversal,
- traversed)
+  _Just,
+ )
 import Primer.Core (
   Bind' (..),
   CaseBranch' (..),
@@ -123,6 +125,7 @@ import Primer.Core (
   TypeCacheBoth (..),
   TypeMeta,
   ValConName,
+  baseName,
   bindName,
   caseBranchName,
   qualifyName,
@@ -131,7 +134,7 @@ import Primer.Core (
   _exprMeta,
   _exprTypeMeta,
   _synthed,
-  _typeMeta, baseName,
+  _typeMeta,
  )
 import Primer.Core.DSL (S, branch, create', emptyHole, meta, meta')
 import Primer.Core.Transform (decomposeTAppCon, mkTAppCon, unfoldTApp)
@@ -152,10 +155,12 @@ import Primer.Def (
 import Primer.Module (
   Module (
     moduleDefs,
-    moduleName, moduleTypes
+    moduleName,
+    moduleTypes
   ),
   moduleDefsQualified,
-  moduleTypesQualified, moduleTypesQualifiedMeta,
+  moduleTypesQualified,
+  moduleTypesQualifiedMeta,
  )
 import Primer.Name (Name, NameCounter)
 import Primer.Primitives (primConName, tChar, tInt)
@@ -165,7 +170,10 @@ import Primer.TypeDef (
   TypeDef (..),
   TypeDefMap,
   ValCon (valConArgs, valConName),
-  typeDefAST, forgetTypeDefMetadata, typeDefParameters, generateTypeDefIDs,
+  forgetTypeDefMetadata,
+  generateTypeDefIDs,
+  typeDefAST,
+  typeDefParameters,
  )
 import Primer.Typecheck.Cxt (Cxt (Cxt, globalCxt, localCxt, smartHoles, typeDefs))
 import Primer.Typecheck.Kindcheck (
@@ -248,9 +256,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 =
@@ -410,7 +415,7 @@ checkEverything sh CheckEverything{trusted, 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]
+        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

From 6c9d519ec17e6c521d86402fab2ba47e1f250b09 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Fri, 9 Jun 2023 22:25:02 +0100
Subject: [PATCH 18/23] fix test

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
---
 primer/test/Tests/Action/Prog.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index 82d7e381a..d0f366993 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -1261,7 +1261,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 1f6d8c4c4055e9818e65b34f50f470a5991f5fbd Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Fri, 9 Jun 2023 22:48:16 +0100
Subject: [PATCH 19/23] fix available actions test

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

diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 533aa010a..ae628a89d 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -146,7 +146,7 @@ import Primer.Module (
 import Primer.Name (Name (unName))
 import Primer.Test.TestM (evalTestM)
 import Primer.Test.Util (clearMeta, clearTypeMeta, testNoSevereLogs)
-import Primer.TypeDef (ASTTypeDef (astTypeDefConstructors), TypeDef (TypeDefAST, TypeDefPrim), ValCon (..), astTypeDefParameters, typeDefAST)
+import Primer.TypeDef (ASTTypeDef (astTypeDefConstructors), TypeDef (TypeDefAST, TypeDefPrim), ValCon (..), astTypeDefParameters, forgetTypeDefMetadata, typeDefAST)
 import Primer.Typecheck (
   CheckEverythingRequest (CheckEverything, toCheck, trusted),
   SmartHoles (NoSmartHoles, SmartHoles),
@@ -282,7 +282,9 @@ tasty_available_actions_accepted = withTests 500 $
       -- 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
@@ -318,7 +320,7 @@ tasty_available_actions_accepted = withTests 500 $
             Nothing -> Gen.discard
             Just def' ->
               let typeDefSel = SelectionTypeDef . TypeDefSelection defName
-                  forTypeDef = ("forTypeDef", (typeDefSel Nothing, Available.forTypeDef l defMut))
+                  forTypeDef = ("forTypeDef", (typeDefSel Nothing, Available.forTypeDef l defMut allTypes' allDefs' defName def'))
                in Gen.frequency
                     [ (1, pure forTypeDef)
                     ,
@@ -331,7 +333,7 @@ tasty_available_actions_accepted = withTests 500 $
                               ( "forTypeDefParamNode"
                               ,
                                 ( typeDefSel $ Just $ TypeDefParamNodeSelection p
-                                , Available.forTypeDefParamNode l defMut
+                                , Available.forTypeDefParamNode l defMut allTypes' allDefs' defName def'
                                 )
                               )
                       )
@@ -342,7 +344,7 @@ tasty_available_actions_accepted = withTests 500 $
                           cs -> do
                             ValCon{valConName, valConArgs} <- Gen.element cs
                             let typeDefConsNodeSel = typeDefSel . Just . TypeDefConsNodeSelection . TypeDefConsSelection valConName
-                                forTypeDefConsNode = ("forTypeDefConsNode", (typeDefConsNodeSel Nothing, Available.forTypeDefConsNode l defMut))
+                                forTypeDefConsNode = ("forTypeDefConsNode", (typeDefConsNodeSel Nothing, Available.forTypeDefConsNode l defMut allTypes' allDefs' defName def'))
                             case valConArgs of
                               [] -> pure forTypeDefConsNode
                               as ->
@@ -357,7 +359,7 @@ tasty_available_actions_accepted = withTests 500 $
                                           ( "forTypeDefConsFieldNode"
                                           ,
                                             ( typeDefConsNodeSel . Just $ TypeDefConsFieldSelection n i
-                                            , Available.forTypeDefConsFieldNode l defMut def' valConName n i
+                                            , Available.forTypeDefConsFieldNode valConName n i l defMut allTypes' allDefs' defName def'
                                             )
                                           )
                                     )

From 78e2d01d61b95b59bc0cb9ace6265e25ac883917 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Sat, 10 Jun 2023 00:21:23 +0100
Subject: [PATCH 20/23] fix forgetProgTypecache to fix benchmark tests

Signed-off-by: George Thomas <georgefsthomas@gmail.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 791df62b96e25c5a5bd93ae66da7b8e9198e579c Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Sat, 10 Jun 2023 01:00:58 +0100
Subject: [PATCH 21/23] ignore capture-like failures for typedef names

this wasn't actually due to test failures, just something I noticed in passing - perhaps we should tweak generators to try to exercise this sort of thing more?

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

diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index ae628a89d..da5b91c53 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -59,7 +59,7 @@ import Primer.App (
   NodeSelection (..),
   NodeType (..),
   Prog (..),
-  ProgError (ActionError, DefAlreadyExists),
+  ProgError (ActionError, ConAlreadyExists, DefAlreadyExists, ParamAlreadyExists, TypeDefAlreadyExists),
   Selection' (..),
   TypeDefConsSelection (TypeDefConsSelection),
   TypeDefNodeSelection (TypeDefConsNodeSelection, TypeDefParamNodeSelection),
@@ -463,6 +463,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 1bcfd2205c53e98d47f36074536c447d580f5b94 Mon Sep 17 00:00:00 2001
From: George Thomas <georgefsthomas@gmail.com>
Date: Sat, 10 Jun 2023 01:15:34 +0100
Subject: [PATCH 22/23] don't offer to delete in-use type params

Signed-off-by: George Thomas <georgefsthomas@gmail.com>
---
 primer/src/Primer/API.hs              |  2 +-
 primer/src/Primer/Action/Available.hs | 13 ++++++++++---
 primer/test/Tests/Action/Available.hs |  2 +-
 3 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..f76a5ddb2 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,
@@ -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/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index da5b91c53..3b09453f3 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -333,7 +333,7 @@ tasty_available_actions_accepted = withTests 500 $
                               ( "forTypeDefParamNode"
                               ,
                                 ( typeDefSel $ Just $ TypeDefParamNodeSelection p
-                                , Available.forTypeDefParamNode l defMut allTypes' allDefs' defName def'
+                                , Available.forTypeDefParamNode p l defMut allTypes' allDefs' defName def'
                                 )
                               )
                       )

From 8487cfab7b4bce6b9c26d001bd1a098db3d38360 Mon Sep 17 00:00:00 2001
From: Drew Hess <src@drewhess.com>
Date: Sun, 11 Jun 2023 13:51:55 +0100
Subject: [PATCH 23/23] rebase on `main` post-fixup

Signed-off-by: Drew Hess <src@drewhess.com>
---
 primer/src/Primer/Action/Available.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/primer/src/Primer/Action/Available.hs b/primer/src/Primer/Action/Available.hs
index f76a5ddb2..ed615e741 100644
--- a/primer/src/Primer/Action/Available.hs
+++ b/primer/src/Primer/Action/Available.hs
@@ -85,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,