feat: Allow typedef deletions regardless of whether type is in use

This includes fixing up expressions utilising the deleted type/constructor/field so that they still make sense. Mostly this involves replacing subexpressions with holes.

Note that this does not yet include deleting type parameters, which we still cannot modify at all when the type is in use. But we aim to relax this restriction as well shortly.

We add a unit tests for each action. Note that we didn't actually have any for the old behaviour, due to time constraints when that was implemented. Although the `tasty_available_actions_accepted` property test caught a lot of issues for us.

Signed-off-by: George Thomas <[email protected]>

primer/src/Primer/Action/Available.hs

@@ -377,14 +377,11 @@ forTypeDef l Editable tydefs defs tdName td =
   sortByPriority l
     $ [ Input RenameType
       , Input AddCon
+      , NoInput DeleteTypeDef
       ]
     <> mwhen
-      (not $ typeInUse tdName td tydefs defs)
-      ( [NoInput DeleteTypeDef]
-          <> mwhen
-            (l == Expert)
-            [Input AddTypeParam]
-      )
+      (l == Expert && not (typeInUse tdName td tydefs defs))
+      [Input AddTypeParam]
 
 forTypeDefParamNode ::
   TyVarName ->
@@ -443,12 +440,13 @@ forTypeDefConsNode ::
   ASTTypeDef TypeMeta KindMeta ->
   [Action]
 forTypeDefConsNode _ NonEditable _ _ _ _ = mempty
-forTypeDefConsNode l Editable tydefs defs tdName td =
-  sortByPriority l
-    $ [ NoInput AddConField
-      , Input RenameCon
-      ]
-    <> mwhen (not $ typeInUse tdName td tydefs defs) [NoInput DeleteCon]
+forTypeDefConsNode l Editable _ _ _ _ =
+  sortByPriority
+    l
+    [ NoInput AddConField
+    , Input RenameCon
+    , NoInput DeleteCon
+    ]
 
 forTypeDefConsFieldNode ::
   ValConName ->
@@ -462,9 +460,9 @@ forTypeDefConsFieldNode ::
   ASTTypeDef TypeMeta KindMeta ->
   [Action]
 forTypeDefConsFieldNode _ _ _ _ NonEditable _ _ _ _ = mempty
-forTypeDefConsFieldNode con index id l Editable tydefs defs tdName td =
+forTypeDefConsFieldNode con index id l Editable _ _ _ td =
   sortByPriority l
-    $ mwhen ((view _id <$> fieldType) == Just id && not (typeInUse tdName td tydefs defs)) [NoInput DeleteConField]
+    $ mwhen ((view _id <$> fieldType) == Just id) [NoInput DeleteConField]
     <> case findTypeOrKind id =<< fieldType of
       Nothing -> mempty
       Just (Left t) -> forType l t

primer/src/Primer/App.hs

@@ -140,6 +140,7 @@ import Primer.Core (
   CaseBranch,
   CaseBranch' (CaseBranch),
   CaseFallback,
+  CaseFallback' (CaseExhaustive),
   Expr,
   Expr' (Case, Con, EmptyHole, Var),
   GVarName,
@@ -176,7 +177,7 @@ import Primer.Core (
   _type,
   _typeMetaLens,
  )
-import Primer.Core.DSL (S, create)
+import Primer.Core.DSL (S, create, emptyHole, tEmptyHole)
 import Primer.Core.DSL qualified as DSL
 import Primer.Core.Transform (renameTyVar, renameVar, unfoldTApp)
 import Primer.Core.Utils (
@@ -633,7 +634,7 @@ handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxS
     Right nf -> EvalFullRespNormal nf
 
 -- | Handle a 'ProgAction'
-applyProgAction :: MonadEdit m ProgError => Prog -> ProgAction -> m Prog
+applyProgAction :: forall m. MonadEdit m ProgError => Prog -> ProgAction -> m Prog
 applyProgAction prog = \case
   MoveToDef d -> do
     m <- lookupEditableModule (qualifiedModule d) prog
@@ -698,14 +699,45 @@ applyProgAction prog = \case
       ( m{moduleTypes = tydefs'}
       , Just $ SelectionTypeDef $ TypeDefSelection tc Nothing
       )
-  DeleteTypeDef d -> editModuleCross (qualifiedModule d) prog $ \(m, ms) ->
-    case moduleTypesQualified m Map.!? d of
-      Nothing -> throwError $ TypeDefNotFound d
-      Just (TypeDefPrim _) -> throwError $ TypeDefIsPrim d
-      Just (TypeDefAST td) -> do
-        checkTypeNotInUse d td $ m : ms
-        let m' = m{moduleTypes = Map.delete (baseName d) (moduleTypes m)}
-        pure (m' : ms, Nothing)
+  DeleteTypeDef d -> editModuleOfCrossType (Just d) prog $ \(m, ms) defName def -> do
+    let updateExpr = \case
+          Con _ c _ | c `elem` map valConName (astTypeDefConstructors def) -> emptyHole
+          e -> pure e
+    ms' <-
+      ((m & over #moduleTypes (Map.delete defName)) : ms)
+        & ( traverseOf
+              (traversed % #moduleDefs % traversed % #_DefAST)
+              ( traverseOf
+                  #astDefExpr
+                  ( transformM (traverseOf typesInExpr updateType)
+                      <=< transformM updateExpr
+                  )
+                  <=< traverseOf #astDefType updateType
+              )
+              <=< traverseOf
+                ( traversed
+                    % #moduleTypes
+                    % traversed
+                    % #_TypeDefAST
+                    % #astTypeDefConstructors
+                    % traversed
+                    % #valConArgs
+                    % traversed
+                )
+                updateType
+          )
+    -- There would otherwise be some awkward cases to patch up, such as modifying metadata in type annotations
+    -- to reflect the change from `KType` to `KHole`.
+    -- Note that this also automatically cleans up all pattern matches on this type,
+    -- since we will have set the type of the scrutinee to a hole,
+    -- and thus the typechecker removes all branches.
+    -- This is why we don't bother explicitly fixing up patterns in the above traversals.
+    ms'' <- runFullTCPass (progSmartHoles prog) (progImports prog) ms'
+    pure (ms'', Nothing)
+    where
+      updateType = transformM \case
+        TCon _ n | n == d -> tEmptyHole
+        e -> pure e
   RenameType old (unsafeMkName -> nameRaw) -> editModuleCross (qualifiedModule old) prog $ \(m, ms) -> do
     when (new /= old && new `elem` allTyConNames prog) $ throwError $ TypeDefAlreadyExists new
     m' <- traverseOf #moduleTypes updateTypeDef m
@@ -830,24 +862,37 @@ applyProgAction prog = \case
                 td
           )
           type_
-  DeleteCon tdName vcName -> editModuleCross (qualifiedModule tdName) prog $ \(m, ms) -> do
-    m' <-
-      alterTypeDef
-        ( \td -> do
-            checkTypeNotInUse tdName td $ m : ms
-            traverseOf
-              #astTypeDefConstructors
-              ( \cons -> do
-                  unless
-                    (vcName `elem` map valConName cons)
-                    (throwError $ ConNotFound vcName)
-                  pure $ filter ((/= vcName) . valConName) cons
-              )
-              td
+  DeleteCon tdName vcName -> editModuleOfCrossType (Just tdName) prog $ \(m, ms) defName def -> do
+    def' <-
+      traverseOf
+        #astTypeDefConstructors
+        ( \cons -> do
+            unless
+              (vcName `elem` map valConName cons)
+              (throwError $ ConNotFound vcName)
+            pure $ filter ((/= vcName) . valConName) cons
         )
-        tdName
-        m
-    pure (m' : ms, Just $ SelectionTypeDef $ TypeDefSelection tdName Nothing)
+        def
+    ms' <-
+      ((m & over #moduleTypes (Map.insert defName $ TypeDefAST def')) : ms)
+        & traverseOf
+          (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
+          ( transformCaseBranches
+              tdName
+              ( \_ (bs, fb) ->
+                  pure
+                    ( bs
+                        & filter \case
+                          CaseBranch (PatCon vcName') _ _ | vcName' == vcName -> False
+                          _ -> True
+                    , if null $ astTypeDefConstructors def' then CaseExhaustive else fb
+                    )
+              )
+              <=< transformM \case
+                Con _ c _ | c == vcName -> emptyHole
+                e -> pure e
+          )
+    pure (ms', Just $ SelectionTypeDef $ TypeDefSelection tdName Nothing)
   AddConField type_ con index new ->
     editModuleCross (qualifiedModule type_) prog $ \(m, ms) -> do
       m' <- updateTypeDef m
@@ -900,31 +945,47 @@ applyProgAction prog = \case
           newName <- LocalName <$> freshName (freeVars e)
           binds' <- maybe (throwError $ IndexOutOfRange index) pure $ insertAt index (Bind m' newName) binds
           pure $ CaseBranch vc binds' e
-  DeleteConField tdName vcName index -> editModuleCross (qualifiedModule tdName) prog $ \(m, ms) -> do
-    m' <-
-      alterTypeDef
-        ( \td -> do
-            checkTypeNotInUse tdName td $ m : ms
-            traverseOf
-              #astTypeDefConstructors
-              ( maybe (throwError $ ConNotFound vcName) pure
-                  <=< findAndAdjustA
-                    ((== vcName) . valConName)
-                    (traverseOf #valConArgs $ maybe (throwError $ IndexOutOfRange index) pure . map fst . deleteAt index)
-              )
-              td
+  DeleteConField tdName vcName index -> editModuleOfCrossType (Just tdName) prog $ \(m, ms) defName def -> do
+    def' <-
+      traverseOf
+        #astTypeDefConstructors
+        ( maybe (throwError $ ConNotFound vcName) pure
+            <=< findAndAdjustA
+              ((== vcName) . valConName)
+              (traverseOf #valConArgs $ map fst . deleteIndex)
         )
-        tdName
-        m
+        def
+    ms' <-
+      ((m & over #moduleTypes (Map.insert defName $ TypeDefAST def')) : ms)
+        & traverseOf
+          (traversed % #moduleDefs % traversed % #_DefAST % #astDefExpr)
+          ( transformNamedCaseBranch
+              tdName
+              vcName
+              ( \_ (CaseBranch vc binds e) -> do
+                  (binds', Bind _ var) <- deleteIndex binds
+                  CaseBranch vc binds'
+                    <$> ( e & traverseOf _freeTmVars \case
+                            (_, v) | v == var -> emptyHole
+                            (meta, v) -> pure $ Var meta $ LocalVarRef v
+                        )
+              )
+              <=< transformM \case
+                Con meta c es | c == vcName -> map (Con meta c . fst) $ deleteIndex es
+                e -> pure e
+          )
     pure
-      ( m' : ms
+      ( ms'
       , Just
           . SelectionTypeDef
           . TypeDefSelection tdName
           . Just
           . TypeDefConsNodeSelection
           $ TypeDefConsSelection vcName Nothing
       )
+    where
+      deleteIndex :: [a] -> m ([a], a)
+      deleteIndex = maybe (throwError $ IndexOutOfRange index) pure . deleteAt index
   AddTypeParam tdName index paramName0 k -> editModuleCross (qualifiedModule tdName) prog $ \(m, ms) -> do
     let paramName = unsafeMkLocalName paramName0
     m' <-

primer/test/Tests/Action/Available.hs

@@ -97,6 +97,7 @@ import Primer.App (
  )
 import Primer.App qualified as App
 import Primer.App.Base (TypeDefConsFieldSelection (..))
+import Primer.App.Utils (forgetProgTypecache)
 import Primer.Builtins (builtinModuleName, cCons, cFalse, cTrue, tBool, tList, tNat)
 import Primer.Core (
   Expr,
@@ -533,7 +534,9 @@ data SucceedOrCapture a
 ensureSHNormal :: App -> PropertyT WT ()
 ensureSHNormal a = case checkAppWellFormed a of
   Left err -> annotateShow err >> failure
-  Right a' -> TypeCacheAlpha a === TypeCacheAlpha a'
+  Right a' ->
+    TypeCacheAlpha (forgetProgTypecache $ appProg a)
+      === TypeCacheAlpha (forgetProgTypecache $ appProg a')
 
 genLoc ::
   forall m.

primer/test/Tests/Action/Prog.hs

@@ -875,6 +875,27 @@ unit_copy_paste_import =
         Left err -> assertFailure $ show err
         Right assertion -> assertion
 
+unit_DeleteTypeDef :: Assertion
+unit_DeleteTypeDef = progActionTest
+  ( defaultProgEditableTypeDefs
+      $ sequence
+        [ do
+            x <- emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tEmptyHole)
+            astDef "def" x <$> tEmptyHole
+        ]
+  )
+  [DeleteTypeDef tT]
+  $ expectSuccess
+  $ \_ prog' -> do
+    assertBool "type deleted" $ Map.notMember tT $ foldMap' moduleTypesQualified $ progModules prog'
+    def <- findDef (gvn "def") prog'
+    forgetMetadata (astDefExpr def)
+      @?= forgetMetadata
+        ( create'
+            $ emptyHole
+            `ann` (tEmptyHole `tapp` tcon (tcn "Bool") `tapp` tEmptyHole)
+        )
+
 unit_RenameType :: Assertion
 unit_RenameType =
   progActionTest
@@ -1078,6 +1099,37 @@ unit_AddCon_sparse =
                 emptyHole
           )
 
+unit_DeleteCon :: Assertion
+unit_DeleteCon = progActionTest
+  ( defaultProgEditableTypeDefs
+      $ sequence
+        [ do
+            x <-
+              case_
+                (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int")))
+                [ branch cA [("x", Nothing), ("y", Nothing), ("z", Nothing)] emptyHole
+                , branch cB [("s", Nothing), ("t", Nothing)] emptyHole
+                ]
+            astDef "def" x <$> tEmptyHole
+        ]
+  )
+  [DeleteCon tT cA]
+  $ expectSuccess
+  $ \_ prog' -> do
+    td <- findTypeDef tT prog'
+    astTypeDefConstructors td
+      @?= [ ValCon cB [TApp () (TApp () (TCon () tT) (TVar () "b")) (TVar () "a"), TVar () "b"]
+          ]
+    def <- findDef (gvn "def") prog'
+    forgetMetadata (astDefExpr def)
+      @?= forgetMetadata
+        ( create'
+            $ case_
+              (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int")))
+              [ branch cB [("s", Nothing), ("t", Nothing)] emptyHole
+              ]
+        )
+
 unit_AddConField :: Assertion
 unit_AddConField =
   progActionTest
@@ -1160,6 +1212,52 @@ unit_AddConField_case_ann =
                 ]
           )
 
+unit_DeleteConField :: Assertion
+unit_DeleteConField =
+  progActionTest
+    ( defaultProgEditableTypeDefs $ do
+        x <-
+          case_
+            ( con
+                cA
+                [ con0 (vcn "True")
+                , con0 (vcn "False")
+                , con0 (vcn "True")
+                ]
+                `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole)
+            )
+            [ branch cA [("x", Nothing), ("y", Nothing), ("z", Nothing)] emptyHole
+            , branch cB [("s", Nothing), ("t", Nothing)] emptyHole
+            ]
+        sequence
+          [ astDef "def" x <$> tEmptyHole
+          ]
+    )
+    [DeleteConField tT cA 1]
+    $ expectSuccess
+    $ \_ prog' -> do
+      td <- findTypeDef tT prog'
+      astTypeDefConstructors td
+        @?= [ ValCon cA [TCon () (tcn "Bool"), TCon () (tcn "Bool")]
+            , ValCon cB [TApp () (TApp () (TCon () tT) (TVar () "b")) (TVar () "a"), TVar () "b"]
+            ]
+      def <- findDef (gvn "def") prog'
+      forgetMetadata (astDefExpr def)
+        @?= forgetMetadata
+          ( create'
+              $ case_
+                ( con
+                    cA
+                    [ con0 (vcn "True")
+                    , con0 (vcn "True")
+                    ]
+                    `ann` (tcon tT `tapp` tEmptyHole `tapp` tEmptyHole)
+                )
+                [ branch cA [("x", Nothing), ("z", Nothing)] emptyHole
+                , branch cB [("s", Nothing), ("t", Nothing)] emptyHole
+                ]
+          )
+
 unit_ConFieldAction :: Assertion
 unit_ConFieldAction =
   progActionTest