Eradicate GenericWarning

Having `GenericWarning` as a pool of random warnings does not make sense anymore now that we switch warnings individually.
agda · Feb 16, 2024 · 0b8a99a · 0b8a99a
1 parent 9178a23
commit 0b8a99a
Show file tree

Hide file tree

Showing 7 changed files with 1 addition and 20 deletions.
diff --git a/src/full/Agda/Interaction/Highlighting/Generate.hs b/src/full/Agda/Interaction/Highlighting/Generate.hs
@@ -447,7 +447,6 @@ warningHighlighting' b w = case tcWarning w of
   InstanceArgWithExplicitArg{} -> mempty
   InversionDepthReached{}    -> mempty
   NoGuardednessFlag{}        -> mempty
-  GenericWarning{}           -> mempty
   -- Andreas, 2020-03-21, issue #4456:
   -- Error warnings that do not have dedicated highlighting
   -- are highlighted as errors.

diff --git a/src/full/Agda/Interaction/Options/Warnings.hs b/src/full/Agda/Interaction/Options/Warnings.hs
@@ -246,7 +246,6 @@ data WarningName
   | FixityInRenamingModule_
   | InvalidCharacterLiteral_
   | UselessPragma_
-  | GenericWarning_
   | IllformedAsClause_
   | InstanceArgWithExplicitArg_
   | InstanceWithExplicitArg_
@@ -439,7 +438,6 @@ warningNameDescription = \case
   DeprecationWarning_              -> "Deprecated features."
   InvalidCharacterLiteral_         -> "Illegal character literals."
   UselessPragma_                   -> "Pragmas that get ignored."
-  GenericWarning_                  -> ""
   IllformedAsClause_               -> "Illformed `as'-clauses in `import' statements."
   InstanceNoOutputTypeName_        -> "Instance arguments whose type does not end in a named or variable type; those are never considered by instance search."
   InstanceArgWithExplicitArg_      -> "Instance arguments with explicit arguments; those are never considered by instance search."

diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -4194,10 +4194,6 @@ data Warning
   -- ^ A coinductive record was declared but neither --guardedness nor
   --   --sized-types is enabled.
 
-  -- Generic warnings for one-off things
-  | GenericWarning           Doc
-    -- ^ Harmless generic warning (not an error)
-
   -- Safe flag errors
   | SafeFlagPostulate C.Name
   | SafeFlagPragma [String]                -- ^ Unsafe OPTIONS.
@@ -4315,7 +4311,6 @@ warningName = \case
   FixityInRenamingModule{}     -> FixityInRenamingModule_
   InvalidCharacterLiteral{}    -> InvalidCharacterLiteral_
   UselessPragma{}              -> UselessPragma_
-  GenericWarning{}             -> GenericWarning_
   InversionDepthReached{}      -> InversionDepthReached_
   InteractionMetaBoundaries{}  -> InteractionMetaBoundaries_{}
   ModuleDoesntExport{}         -> ModuleDoesntExport_

diff --git a/src/full/Agda/TypeChecking/Pretty/Warning.hs b/src/full/Agda/TypeChecking/Pretty/Warning.hs
@@ -219,8 +219,6 @@ prettyWarning = \case
              pwords "this type will likely be rejected by the termination" ++
              pwords "checker unless this flag is enabled."
 
-    GenericWarning d -> return d
-
     InvalidCharacterLiteral c -> fsep $
       pwords "Invalid character literal" ++ [text $ show c] ++
       pwords "(surrogate code points are not supported)"

diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs
@@ -34,7 +34,7 @@ import Agda.Syntax.Info hiding (defAbstract)
 
 import Agda.TypeChecking.Monad
 import qualified Agda.TypeChecking.Monad.Benchmark as Bench
-import Agda.TypeChecking.Warnings ( warning, genericWarning )
+import Agda.TypeChecking.Warnings ( warning )
 
 import Agda.TypeChecking.Constraints
 import Agda.TypeChecking.Conversion

diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
@@ -40,7 +40,6 @@ instance EmbPrj Warning where
     EmptyRewritePragma                    -> icodeN 2 EmptyRewritePragma
     UselessPublic                         -> icodeN 3 UselessPublic
     UselessInline a                       -> icodeN 4 UselessInline a
-    GenericWarning a                      -> icodeN 5 GenericWarning a
     InvalidCharacterLiteral a             -> __IMPOSSIBLE__
     SafeFlagPostulate a                   -> __IMPOSSIBLE__
     SafeFlagPragma a                      -> __IMPOSSIBLE__
@@ -107,7 +106,6 @@ instance EmbPrj Warning where
     [2]                  -> valuN EmptyRewritePragma
     [3]                  -> valuN UselessPublic
     [4, a]               -> valuN UselessInline a
-    [5, a]               -> valuN GenericWarning a
     [6, a, b, c]         -> valuN DeprecationWarning a b c
     [7, a]               -> valuN NicifierIssue a
     [8, a]               -> valuN InversionDepthReached a
@@ -404,7 +402,6 @@ instance EmbPrj WarningName where
     FixityInRenamingModule_                      -> 48
     InvalidCharacterLiteral_                     -> 49
     UselessPragma_                               -> 50
-    GenericWarning_                              -> 51
     IllformedAsClause_                           -> 52
     InstanceArgWithExplicitArg_                  -> 53
     InstanceWithExplicitArg_                     -> 54
@@ -520,7 +517,6 @@ instance EmbPrj WarningName where
     48  -> return FixityInRenamingModule_
     49  -> return InvalidCharacterLiteral_
     50  -> return UselessPragma_
-    51  -> return GenericWarning_
     52  -> return IllformedAsClause_
     53  -> return InstanceArgWithExplicitArg_
     54  -> return InstanceWithExplicitArg_

diff --git a/src/full/Agda/TypeChecking/Warnings.hs b/src/full/Agda/TypeChecking/Warnings.hs
@@ -1,7 +1,6 @@
 
 module Agda.TypeChecking.Warnings
   ( MonadWarning(..)
-  , genericWarning
   , warning'_, warning_, warning', warning, warnings
   , raiseWarningsOnUsage
   , isUnsolvedWarning
@@ -79,10 +78,6 @@ instance MonadWarning TCM where
 -- * Raising warnings
 ---------------------------------------------------------------------------
 
-{-# SPECIALIZE genericWarning :: P.Doc -> TCM () #-}
-genericWarning :: MonadWarning m => P.Doc -> m ()
-genericWarning = warning . GenericWarning
-
 {-# SPECIALIZE warning'_ :: CallStack -> Warning -> TCM TCWarning #-}
 warning'_ :: (MonadWarning m) => CallStack -> Warning -> m TCWarning
 warning'_ loc w = do