diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index d5684bed6..afaeb537e 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -138,7 +138,7 @@ import Primer.Core (
  )
 import Primer.Core.DSL (create, emptyHole, tEmptyHole)
 import qualified Primer.Core.DSL as DSL
-import Primer.Core.Transform (foldApp, renameVar, unfoldApp, unfoldTApp)
+import Primer.Core.Transform (foldApp, renameVar, unfoldAPP, unfoldApp, unfoldTApp)
 import Primer.Core.Utils (freeVars, _freeTmVars, _freeTyVars, _freeVarsTy)
 import Primer.Eval (EvalDetail, EvalError)
 import qualified Primer.Eval as Eval
@@ -690,18 +690,19 @@ applyProgAction prog mdefName = \case
           type_
       updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateDecons <=< updateCons)
       updateCons e = case unfoldApp e of
-        (e'@(Con _ con'), args) | con' == con -> do
-          m' <- DSL.meta
-          case adjustAt index (Hole m') args of
-            Just args' -> foldApp e' =<< traverse (descendM updateCons) args'
-            Nothing -> do
-              -- The constructor is not applied as far as the changed field,
-              -- so the full application still typechecks, but its type has changed.
-              -- Thus, we put the whole thing in to a hole.
-              Hole <$> DSL.meta <*> (foldApp e' =<< traverse (descendM updateCons) args)
-        _ ->
-          -- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
-          descendM updateCons e
+        (h, args) -> case unfoldAPP h of
+          (Con _ con', _tyArgs) | con' == con -> do
+            m' <- DSL.meta
+            case adjustAt index (Hole m') args of
+              Just args' -> foldApp h =<< traverse (descendM updateCons) args'
+              Nothing -> do
+                -- The constructor is not applied as far as the changed field,
+                -- so the full application still typechecks, but its type has changed.
+                -- Thus, we put the whole thing in to a hole.
+                Hole <$> DSL.meta <*> (foldApp h =<< traverse (descendM updateCons) args)
+          _ ->
+            -- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
+            descendM updateCons e
       updateDecons = transformCaseBranches prog type_ $
         traverse $ \cb@(CaseBranch vc binds e) ->
           if vc == con
@@ -740,20 +741,24 @@ applyProgAction prog mdefName = \case
                   )
           )
           type_
-      updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateDecons <=< updateCons)
+      -- NB: we must updateDecons first, as transformCaseBranches may do
+      -- synthesis of the scrutinee's type, using the old typedef. Thus we must
+      -- not update the scrutinee before this happens.
+      updateDefs = traverseOf (traversed % #_DefAST % #astDefExpr) (updateCons <=< updateDecons)
       updateCons e = case unfoldApp e of
-        (e'@(Con _ con'), args) | con' == con -> do
-          m' <- DSL.meta
-          case insertAt index (EmptyHole m') args of
-            Just args' -> foldApp e' =<< traverse (descendM updateCons) args'
-            Nothing ->
-              -- The constructor is not applied as far as the field immediately prior to the new one,
-              -- so the full application still typechecks, but its type has changed.
-              -- Thus, we put the whole thing in to a hole.
-              Hole <$> DSL.meta <*> (foldApp e' =<< traverse (descendM updateCons) args)
-        _ ->
-          -- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
-          descendM updateCons e
+        (h, args) -> case unfoldAPP h of
+          (Con _ con', _tyArgs) | con' == con -> do
+            m' <- DSL.meta
+            case insertAt index (EmptyHole m') args of
+              Just args' -> foldApp h =<< traverse (descendM updateCons) args'
+              Nothing ->
+                -- The constructor is not applied as far as the field immediately prior to the new one,
+                -- so the full application still typechecks, but its type has changed.
+                -- Thus, we put the whole thing in to a hole.
+                Hole <$> DSL.meta <*> (foldApp h =<< traverse (descendM updateCons) args)
+          _ ->
+            -- NB we can't use `transformM` here because we'd end up seeing incomplete applications before full ones
+            descendM updateCons e
       updateDecons = transformCaseBranches prog type_ $
         traverse $ \cb@(CaseBranch vc binds e) ->
           if vc == con
diff --git a/primer/test/Tests/Action/Prog.hs b/primer/test/Tests/Action/Prog.hs
index cdb31334d..50cafd414 100644
--- a/primer/test/Tests/Action/Prog.hs
+++ b/primer/test/Tests/Action/Prog.hs
@@ -86,7 +86,6 @@ import Primer.Core.DSL (
   con,
   create,
   emptyHole,
-  gvar,
   hole,
   lAM,
   lam,
@@ -909,7 +908,11 @@ unit_SetConFieldType :: Assertion
 unit_SetConFieldType =
   progActionTest
     ( defaultProgEditableTypeDefs . sequence . pure $ do
-        x <- con cA `app` lvar "x" `app` (gvar (gvn "y") `ann` tcon (tcn "Bool"))
+        x <-
+          con cA `aPP` tEmptyHole `aPP` tEmptyHole
+            `app` con (vcn "True")
+            `app` con (vcn "True")
+            `app` con (vcn "True")
         astDef "def" x <$> tEmptyHole
     )
     [SetConFieldType tT cA 1 $ TCon () (tcn "Int")]
@@ -923,7 +926,10 @@ unit_SetConFieldType =
       forgetIDs (astDefExpr def)
         @?= forgetIDs
           ( fst . create $
-              con cA `app` lvar "x" `app` hole (gvar (gvn "y") `ann` tcon (tcn "Bool"))
+              con cA `aPP` tEmptyHole `aPP` tEmptyHole
+                `app` con (vcn "True")
+                `app` hole (con (vcn "True"))
+                `app` con (vcn "True")
           )
 
 unit_SetConFieldType_partial_app :: Assertion
@@ -1016,7 +1022,16 @@ unit_AddConField :: Assertion
 unit_AddConField =
   progActionTest
     ( defaultProgEditableTypeDefs $ do
-        x <- con cA `app` con (vcn "True")
+        x <-
+          case_
+            ( con cA `aPP` tEmptyHole `aPP` tEmptyHole
+                `app` con (vcn "True")
+                `app` con (vcn "True")
+                `app` con (vcn "True")
+            )
+            [ branch cA [("p", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole
+            , branch cB [("x", Nothing)] emptyHole
+            ]
         sequence
           [ astDef "def" x <$> tEmptyHole
           ]
@@ -1032,7 +1047,16 @@ unit_AddConField =
       forgetIDs (astDefExpr def)
         @?= forgetIDs
           ( fst . create $
-              con cA `app` con (vcn "True") `app` emptyHole
+              case_
+                ( con cA `aPP` tEmptyHole `aPP` tEmptyHole
+                    `app` con (vcn "True")
+                    `app` emptyHole
+                    `app` con (vcn "True")
+                    `app` con (vcn "True")
+                )
+                [ branch cA [("p", Nothing), ("a24", Nothing), ("q", Nothing), ("p1", Nothing)] emptyHole
+                , branch cB [("x", Nothing)] emptyHole
+                ]
           )
 
 unit_AddConField_partial_app :: Assertion
@@ -1053,8 +1077,31 @@ unit_AddConField_partial_app =
               hole $ con cA `app` con (vcn "True")
           )
 
-unit_AddConField_case :: Assertion
-unit_AddConField_case =
+unit_AddConField_partial_app_end :: Assertion
+unit_AddConField_partial_app_end =
+  progActionTest
+    ( defaultProgEditableTypeDefs $ do
+        x <- con cA `app` con (vcn "True")
+        sequence
+          [ astDef "def" x <$> tEmptyHole
+          ]
+    )
+    [AddConField tT cA 1 $ TCon () (tcn "Int")]
+    $ expectSuccess $ \_ prog' -> do
+      td <- findTypeDef tT prog'
+      astTypeDefConstructors td
+        @?= [ ValCon cA [TCon () (tcn "Bool"), TCon () (tcn "Int"), TCon () (tcn "Bool"), TCon () (tcn "Bool")]
+            , ValCon cB [TVar () "b"]
+            ]
+      def <- findDef (gvn "def") prog'
+      forgetIDs (astDefExpr def)
+        @?= forgetIDs
+          ( fst . create $
+              con cA `app` con (vcn "True") `app` emptyHole
+          )
+
+unit_AddConField_case_ann :: Assertion
+unit_AddConField_case_ann =
   progActionTest
     ( defaultProgEditableTypeDefs $ do
         x <-