Allow typedef deletions regardless of whether type is in use (#1153)

primer/src/Foreword.hs

@@ -122,9 +122,9 @@ insertAt n y xs =
 
 -- | Delete an element at some index, returning 'Nothing' if it is out
 -- of bounds.
-deleteAt :: Int -> [a] -> Maybe [a]
+deleteAt :: Int -> [b] -> Maybe ([b], b)
 deleteAt n xs = case splitAt n xs of
-  (a, _ : b) -> Just $ a ++ b
+  (a, b : bs) -> Just (a ++ bs, b)
   _ -> Nothing
 
 -- | Apply a function to the element at some index, returning

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,41 @@ 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) ->
+                  let bs' =
+                        bs
+                          & filter \case
+                            CaseBranch (PatCon vcName') _ _ | vcName' == vcName -> False
+                            _ -> True
+                   in pure
+                        ( bs'
+                        , if map (PatCon . valConName) (astTypeDefConstructors def') == map caseBranchName bs'
+                            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 +949,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 . 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' <-
@@ -1043,13 +1108,7 @@ applyProgAction prog = \case
       Right (def', kz) -> do
         let mod' = mod & over #moduleTypes (Map.insert defName $ TypeDefAST def')
             imports = progImports prog
-        mods' <-
-          runExceptT
-            ( runReaderT
-                (checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mod' : mods}))
-                (buildTypingContextFromModules (mod : mods <> imports) smartHoles)
-            )
-            >>= either (throwError . ActionError) pure
+        mods' <- runFullTCPass smartHoles imports (mod' : mods)
         pure
           ( mods'
           , Just
@@ -1981,3 +2040,12 @@ allTyConNames = fmap fst . allConNames
 -- change in the future.
 nextProgID :: Prog -> ID
 nextProgID p = foldl' (\id_ m -> max (nextModuleID m) id_) minBound (progModules p)
+
+runFullTCPass :: MonadEdit m ProgError => SmartHoles -> [Module] -> [Module] -> m [Module]
+runFullTCPass smartHoles imports mods =
+  runExceptT
+    ( runReaderT
+        (checkEverything smartHoles (CheckEverything{trusted = imports, toCheck = mods}))
+        (buildTypingContextFromModules (mods <> imports) smartHoles)
+    )
+    >>= either (throwError . ActionError) pure

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.