module Agda.TypeChecking.Pretty.Warning where

import Prelude hiding ( null )

import Control.Monad ( guard )

-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail ( MonadFail )

import Data.Char ( toLower )
import Data.Function
import Data.Maybe

import qualified Data.Set as Set
import Data.Set (Set)

import qualified Data.List as List
import qualified Data.Text as T

import Agda.TypeChecking.Monad.Base
import {-# SOURCE #-} Agda.TypeChecking.Errors
import Agda.TypeChecking.Monad.MetaVars
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.State ( getScope )
import Agda.TypeChecking.Monad ( localTCState )
import Agda.TypeChecking.Positivity () --instance only
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Call
import {-# SOURCE #-} Agda.TypeChecking.Pretty.Constraint (prettyInterestingConstraints, interestingConstraint)
import Agda.TypeChecking.Warnings (MonadWarning, isUnsolvedWarning, onlyShowIfUnsolved, classifyWarning, WhichWarnings(..), warning_)
import Agda.TypeChecking.Monad.Constraints (getAllConstraints)

import Agda.Syntax.Common ( ImportedName'(..), fromImportedName, partitionImportedNames )
import Agda.Syntax.Position
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Scope.Base ( concreteNamesInScope, NameOrModule(..) )
import Agda.Syntax.Internal
import Agda.Syntax.Translation.InternalToAbstract

import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings

import Agda.Utils.Lens
import Agda.Utils.List ( editDistance )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Pretty ( Pretty, prettyShow )
import qualified Agda.Utils.Pretty as P

instance PrettyTCM TCWarning where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM w :: TCWarning
w@(TCWarning CallStack
loc Range
_ Warning
_ Doc
_ Bool
_) = do
    forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"warning" VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ String
"Warning raised at " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow CallStack
loc
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TCWarning -> Doc
tcWarningPrintedWarning TCWarning
w

prettyWarning :: MonadPretty m => Warning -> m Doc
prettyWarning :: forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning = \case

    UnsolvedMetaVariables [Range]
ms  ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unsolved metas at the following locations:" )
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Range]
ms)

    UnsolvedInteractionMetas [Range]
is ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unsolved interaction metas at the following locations:" )
      forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Range]
is)

    UnsolvedConstraints Constraints
cs -> do
      [Doc]
pcs <- forall (m :: * -> *). MonadPretty m => Constraints -> m [Doc]
prettyInterestingConstraints Constraints
cs
      if forall a. Null a => a -> Bool
null [Doc]
pcs
        then forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unsolved constraints"  -- #4065: keep minimal warning text
        else forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Failed to solve the following constraints:"
          , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
List.nub [Doc]
pcs
          ]

    TerminationIssue [TerminationError]
because -> do
      QName -> QName
dropTopLevel <- forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper
      forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Termination checking failed for the following functions:"
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$
             forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> QName
dropTopLevel) forall a b. (a -> b) -> a -> b
$
               forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [QName]
termErrFunctions [TerminationError]
because)
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Problematic calls:"
        forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> *). Foldable t => t Doc -> Doc
P.vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a]
List.nub) forall a b. (a -> b) -> a -> b
$
              forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [a]
List.sortOn forall a. HasRange a => a -> Range
getRange forall a b. (a -> b) -> a -> b
$
              forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [CallInfo]
termErrCalls [TerminationError]
because)

    UnreachableClauses QName
f [Range]
pss -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Unreachable" forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (forall {a}. (Num a, Eq a) => a -> String -> String
plural (forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Range]
pss) String
"clause")
        where
          plural :: a -> String -> String
plural a
1 String
thing = String
thing
          plural a
n String
thing = String
thing forall a. [a] -> [a] -> [a]
++ String
"s"

    CoverageIssue QName
f [(Telescope, [NamedArg DeBruijnPattern])]
pss -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Incomplete pattern matching for" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f forall a. Semigroup a => a -> a -> a
<> m Doc
"."] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Missing cases:") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display [(Telescope, [NamedArg DeBruijnPattern])]
pss)
        where
        display :: (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope
tel, [NamedArg DeBruijnPattern]
ps) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True forall a b. (a -> b) -> a -> b
$
          forall a. Null a => a
empty { clauseTel :: Telescope
clauseTel = Telescope
tel, namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps }

    CoverageNoExactSplit QName
f [Clause]
cs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Exact splitting is enabled, but the following" forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (forall a c. Sized a => a -> c -> c -> c
P.singPlural [Clause]
cs String
"clause" String
"clauses") forall a. [a] -> [a] -> [a]
++
            forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"could not be preserved as definitional equalities in the translation to a case tree:"
           ) forall a. a -> [a] -> [a]
:
      forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True) [Clause]
cs

    NotStrictlyPositive QName
d Seq OccursWhere
ocs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is not strictly positive, because it occurs"
      forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Seq OccursWhere
ocs]

    UnsupportedIndexedMatch Doc
doc -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"This clause uses pattern-matching features that are not yet supported by Cubical Agda,"
           forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"the function to which it belongs will not compute when applied to transports."
             )
      , m Doc
""
      , m Doc
"Reason:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
doc
      , m Doc
""
      ]

    CantGeneralizeOverSorts [MetaId]
ms -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Cannot generalize over unsolved sort metas:"
            , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM MetaId
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text String
"at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
x) | MetaId
x <- [MetaId]
ms ]
            , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any"
            ]

    AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
ps -> forall (m :: * -> *). Applicative m => String -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      String
"The right-hand side must be omitted if there " forall a. [a] -> [a] -> [a]
++
      String
"is an absurd pattern, () or {}, in the left-hand side."

    OldBuiltin String
old String
new -> forall (m :: * -> *). Applicative m => String -> m Doc
fwords forall a b. (a -> b) -> a -> b
$
      String
"Builtin " forall a. [a] -> [a] -> [a]
++ String
old forall a. [a] -> [a] -> [a]
++ String
" no longer exists. " forall a. [a] -> [a] -> [a]
++
      String
"It is now bound by BUILTIN " forall a. [a] -> [a] -> [a]
++ String
new

    Warning
EmptyRewritePragma -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords forall a b. (a -> b) -> a -> b
$ String
"Empty REWRITE pragma"

    Warning
EmptyWhere         -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords forall a b. (a -> b) -> a -> b
$ String
"Empty `where' block (ignored)"

    IllformedAsClause String
s -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords forall a b. (a -> b) -> a -> b
$
      String
"`as' must be followed by an identifier" forall a. [a] -> [a] -> [a]
++ String
s

    ClashesViaRenaming NameOrModule
nm [Name]
xs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
      [ [ case NameOrModule
nm of NameOrModule
NameNotModule -> m Doc
"Name"; NameOrModule
ModuleNotName -> m Doc
"Module" ]
      , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"clashes introduced by `renaming':"
      , forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Name]
xs
      ]

    UselessPatternDeclarationForRecord String
s -> forall (m :: * -> *). Applicative m => String -> m Doc
fwords forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
      [ String
"`pattern' attribute ignored for", String
s, String
"record" ]
      -- the @s@ is a qualifier like "eta" or "coinductive"

    Warning
UselessPublic -> forall (m :: * -> *). Applicative m => String -> m Doc
fwords forall a b. (a -> b) -> a -> b
$ String
"Keyword `public' is ignored here"

    UselessHiding [ImportedName]
xs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Ignoring names in `hiding' directive:"
      , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
"," forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [ImportedName]
xs
      ]

    UselessInline QName
q -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"It is pointless for INLINE'd function" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q] forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"to have a separate Haskell definition"

    Warning
WrongInstanceDeclaration -> forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"Terms marked as eligible for instance search should end with a name, so `instance' is ignored here."

    InstanceWithExplicitArg QName
q -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Instance declarations with explicit arguments are never considered by instance search," forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"so making" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"into an instance has no effect."

    InstanceNoOutputTypeName Doc
b -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Instance arguments whose type does not end in a named or variable type are never considered by instance search," forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"so having an instance argument" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"has no effect."

    InstanceArgWithExplicitArg Doc
b -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Instance arguments with explicit arguments are never considered by instance search," forall a. [a] -> [a] -> [a]
++
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"so having an instance argument" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. Monad m => a -> m a
return Doc
b] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"has no effect."

    InversionDepthReached QName
f -> do
      VerboseLevel
maxDepth <- forall (m :: * -> *). HasOptions m => m VerboseLevel
maxInversionDepth
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Refusing to invert pattern matching of" forall a. [a] -> [a] -> [a]
++ [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f] forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords (String
"because the maximum depth (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show VerboseLevel
maxDepth forall a. [a] -> [a] -> [a]
++ String
") has been reached.") forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Most likely this means you have an unsatisfiable constraint, but it could" forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"also mean that you need to increase the maximum depth using the flag" forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"--inversion-max-depth=N"

    NoGuardednessFlag QName
q ->
      forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q ] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"is declared coinductive, but option" forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"--guardedness is not enabled. Coinductive functions on" forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"this type will likely be rejected by the termination" forall a. [a] -> [a] -> [a]
++
             forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"checker unless this flag is enabled."

    GenericWarning Doc
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    GenericNonFatalError Doc
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    GenericUseless Range
_r Doc
d -> forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d

    SafeFlagPostulate Name
e -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot postulate" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
e] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"with safe flag"

    SafeFlagPragma [String]
xs ->
      let plural :: String
plural | forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [String]
xs forall a. Eq a => a -> a -> Bool
== VerboseLevel
1 = String
""
                 | Bool
otherwise      = String
"s"
      in forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ [forall (m :: * -> *). Applicative m => String -> m Doc
fwords (String
"Cannot set OPTIONS pragma" forall a. [a] -> [a] -> [a]
++ String
plural)]
                forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
xs forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => String -> m Doc
fwords String
"with safe flag."]

    Warning
SafeFlagNonTerminating -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use NON_TERMINATING pragma with safe flag."

    Warning
SafeFlagTerminating -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use TERMINATING pragma with safe flag."

    Warning
SafeFlagWithoutKFlagPrimEraseEquality -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use primEraseEquality with safe and without-K flags.")

    Warning
WithoutKFlagPrimEraseEquality -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Using primEraseEquality with the without-K flag is inconsistent.")

    Warning
SafeFlagNoPositivityCheck -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use NO_POSITIVITY_CHECK pragma with safe flag."

    Warning
SafeFlagPolarity -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use POLARITY pragma with safe flag."

    Warning
SafeFlagNoUniverseCheck -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use NO_UNIVERSE_CHECK pragma with safe flag."

    Warning
SafeFlagEta -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use ETA pragma with safe flag."

    Warning
SafeFlagInjective -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use INJECTIVE pragma with safe flag."

    Warning
SafeFlagNoCoverageCheck -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Cannot use NON_COVERING pragma with safe flag."

    ParseWarning ParseWarning
pw -> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ParseWarning
pw

    DeprecationWarning String
old String
new String
version -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$
      [forall (m :: * -> *). Applicative m => String -> m Doc
text String
old] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"has been deprecated. Use" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => String -> m Doc
text String
new] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords
      String
"instead. This will be an error in Agda" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *). Applicative m => String -> m Doc
text String
version forall a. Semigroup a => a -> a -> a
<> m Doc
"."]

    NicifierIssue DeclarationWarning
w -> forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere (forall a. HasRange a => a -> Range
getRange DeclarationWarning
w) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeclarationWarning
w

    UserWarning Text
str -> forall (m :: * -> *). Applicative m => String -> m Doc
text (Text -> String
T.unpack Text
str)

    ModuleDoesntExport QName
m [Name]
names [Name]
modules [ImportedName]
xs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The module" forall a. [a] -> [a] -> [a]
++ [forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
m] forall a. [a] -> [a] -> [a]
++ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"doesn't export the following:"
      , forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
False (forall {m :: * -> *} {b}.
(Null (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc),
 Semigroup (m Doc), Pretty b) =>
[Name] -> ImportedName' b b -> m Doc
suggestion [Name]
names)   [ImportedName]
ys
      , forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
False (forall {m :: * -> *} {b}.
(Null (m Doc), MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc),
 Semigroup (m Doc), Pretty b) =>
[Name] -> ImportedName' b b -> m Doc
suggestion [Name]
modules) [ImportedName]
ms
      ]
      where
      ys, ms :: [C.ImportedName]
      ys :: [ImportedName]
ys            = forall a b. (a -> b) -> [a] -> [b]
map forall n m. n -> ImportedName' n m
ImportedName   [Name]
ys0
      ms :: [ImportedName]
ms            = forall a b. (a -> b) -> [a] -> [b]
map forall n m. m -> ImportedName' n m
ImportedModule [Name]
ms0
      ([Name]
ys0, [Name]
ms0)    = forall n m. [ImportedName' n m] -> ([n], [m])
partitionImportedNames [ImportedName]
xs
      suggestion :: [Name] -> ImportedName' b b -> m Doc
suggestion [Name]
zs = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Null a => a
empty forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean (forall a b. (a -> b) -> [a] -> [b]
map Name -> QName
C.QName [Name]
zs) forall a. ImportedName' a a -> a
fromImportedName

    DuplicateUsing List1 ImportedName
xs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Duplicates in `using` directive:" forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall l. IsList l => l -> [Item l]
List1.toList List1 ImportedName
xs)

    FixityInRenamingModule List1 Range
_rs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Modules do not have fixity"

    LibraryWarning LibWarning
lw -> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty LibWarning
lw

    InfectiveImport Doc
msg -> forall (m :: * -> *) a. Monad m => a -> m a
return Doc
msg

    CoInfectiveImport Doc
msg -> forall (m :: * -> *) a. Monad m => a -> m a
return Doc
msg

    RewriteNonConfluent Term
lhs Term
rhs1 Term
rhs2 Doc
err -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
      [ m Doc
"Local confluence check failed:"
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs , m Doc
"reduces to both"
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs1 , m Doc
"and" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs2
      , m Doc
"which are not equal because"
      , forall (m :: * -> *) a. Monad m => a -> m a
return Doc
err
      ]

    RewriteMaybeNonConfluent Term
lhs1 Term
lhs2 [Doc]
cs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Couldn't determine overlap between left-hand sides"
          , [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs1 , forall (m :: * -> *). Applicative m => String -> m Doc
text String
"and" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs2 ]
          , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"because of unsolved constraints:"
          ]
        ]
      , forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return) [Doc]
cs
      ]

    RewriteAmbiguousRules Term
lhs Term
rhs1 Term
rhs2 -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ ( forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Global confluence check failed:" , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs]
          , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"can be rewritten to either" , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs1]
          , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"or" , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhs2 forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
          ])
      , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Possible fix: add a rewrite rule with left-hand side"
        , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lhs] , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"to resolve the ambiguity."
        ]
      ]

    RewriteMissingRule Term
u Term
v Term
rhou -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Global confluence check failed:" , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u]
        , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"unfolds to" , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v] , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"which should further unfold to"
        , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhou] , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"but it does not."
        ]
      , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Possible fix: add a rule to rewrite"
        , [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v , m Doc
"to" , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
rhou ]
        ]
      ]

    PragmaCompileErased String
bn QName
qn -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The backend"
      , [ forall (m :: * -> *). Applicative m => String -> m Doc
text String
bn
        , m Doc
"erases"
        , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
qn
        ]
      , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"so the COMPILE pragma will be ignored."
      ]

    NotInScopeW [QName]
xs -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Not in scope:"
      , do
        [QName]
inscope <- forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Set QName
concreteNamesInScope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
        forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
True (forall {m :: * -> *}.
(Null (m Doc), IsString (m Doc), MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 Semigroup (m Doc)) =>
[QName] -> QName -> m Doc
suggestion [QName]
inscope) [QName]
xs
      ]
      where
      suggestion :: [QName] -> QName -> m Doc
suggestion [QName]
inscope QName
x = forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}.
(Null (m Doc), Applicative m) =>
[m Doc] -> m Doc
par forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ [ m Doc
"did you forget space around the ':'?"  | Char
':' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
s ]
        , [ m Doc
"did you forget space around the '->'?" | String
"->" forall a. Eq a => [a] -> [a] -> Bool
`List.isInfixOf` String
s ]
        , forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean [QName]
inscope QName -> Name
C.unqualify QName
x
        ]
        where
        par :: [m Doc] -> m Doc
par []  = forall a. Null a => a
empty
        par [m Doc
d] = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens m Doc
d
        par [m Doc]
ds  = forall (m :: * -> *). Functor m => m Doc -> m Doc
parens forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [m Doc]
ds
        s :: String
s = forall a. Pretty a => a -> String
P.prettyShow QName
x

    AsPatternShadowsConstructorOrPatternSynonym Bool
patsyn -> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Name bound in @-pattern ignored because it shadows"
      , if Bool
patsyn then forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"pattern synonym" else [ m Doc
"constructor" ]
      ]

    RecordFieldWarning RecordFieldWarning
w -> forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning RecordFieldWarning
w

prettyRecordFieldWarning :: MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning :: forall (m :: * -> *). MonadPretty m => RecordFieldWarning -> m Doc
prettyRecordFieldWarning = \case
  DuplicateFieldsWarning [(Name, Range)]
xrs    -> forall (m :: * -> *). MonadPretty m => [Name] -> m Doc
prettyDuplicateFields forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Range)]
xrs
  TooManyFieldsWarning QName
q [Name]
ys [(Name, Range)]
xrs -> forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> [Name] -> m Doc
prettyTooManyFields QName
q [Name]
ys forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Range)]
xrs

prettyDuplicateFields :: MonadPretty m => [C.Name] -> m Doc
prettyDuplicateFields :: forall (m :: * -> *). MonadPretty m => [Name] -> m Doc
prettyDuplicateFields [Name]
xs = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"Duplicate"
    , forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
fields [Name]
xs
    , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs)
    , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"in record"
    ]
  where
  fields :: a -> [m Doc]
fields a
ys = forall a c. Sized a => a -> c -> c -> c
P.singPlural a
ys [forall (m :: * -> *). Applicative m => String -> m Doc
text String
"field"] [forall (m :: * -> *). Applicative m => String -> m Doc
text String
"fields"]

prettyTooManyFields :: MonadPretty m => QName -> [C.Name] -> [C.Name] -> m Doc
prettyTooManyFields :: forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> [Name] -> m Doc
prettyTooManyFields QName
r [Name]
missing [Name]
xs = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"The record type"
    , [forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r]
    , forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"does not have the"
    , forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
fields [Name]
xs
    , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs)
    , if forall a. Null a => a -> Bool
null [Name]
missing then [] else forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ forall (m :: * -> *). Applicative m => String -> [m Doc]
pwords String
"but it would have the"
      , forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
fields [Name]
missing
      , forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
missing)
      ]
    ]
  where
  fields :: a -> [m Doc]
fields a
ys = forall a c. Sized a => a -> c -> c -> c
P.singPlural a
ys [forall (m :: * -> *). Applicative m => String -> m Doc
text String
"field"] [forall (m :: * -> *). Applicative m => String -> m Doc
text String
"fields"]

-- | Report a number of names that are not in scope.
prettyNotInScopeNames
  :: (MonadPretty m, Pretty a, HasRange a)
  => Bool          -- ^ Print range?
  -> (a -> m Doc)  -- ^ Correction suggestion generator.
  -> [a]           -- ^ Names that are not in scope.
  -> m Doc
prettyNotInScopeNames :: forall (m :: * -> *) a.
(MonadPretty m, Pretty a, HasRange a) =>
Bool -> (a -> m Doc) -> [a] -> m Doc
prettyNotInScopeNames Bool
printRange a -> m Doc
suggestion [a]
xs = forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
name [a]
xs
  where
  name :: a -> m Doc
name a
x = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
x
    , if Bool
printRange then m Doc
"at" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. HasRange a => a -> Range
getRange a
x) else forall a. Null a => a
empty
    , a -> m Doc
suggestion a
x
    ]

-- | Suggest some corrections to a misspelled name.
didYouMean
  :: (MonadPretty m, Pretty a, Pretty b)
  => [C.QName]     -- ^ Names in scope.
  -> (a -> b)      -- ^ Canonization function for similarity search.
  -> a             -- ^ A name which is not in scope.
  -> Maybe (m Doc) -- ^ "did you mean" hint.
didYouMean :: forall (m :: * -> *) a b.
(MonadPretty m, Pretty a, Pretty b) =>
[QName] -> (a -> b) -> a -> Maybe (m Doc)
didYouMean [QName]
inscope a -> b
canon a
x
  | forall a. Null a => a -> Bool
null [String]
ys   = forall a. Maybe a
Nothing
  | Bool
otherwise = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ m Doc
"did you mean"
      , forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
" or" forall a b. (a -> b) -> a -> b
$
                 forall a b. (a -> b) -> [a] -> [b]
map (\ String
y -> forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"'" forall a. [a] -> [a] -> [a]
++ String
y forall a. [a] -> [a] -> [a]
++ String
"'") [String]
ys)
        forall a. Semigroup a => a -> a -> a
<> m Doc
"?"
      ]
  where
  strip :: Pretty b => b -> String
  strip :: forall a. Pretty a => a -> String
strip        = forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Char
'_') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
prettyShow
  -- dropModule x = fromMaybe x $ List.stripPrefix "module " x
  maxDist :: a -> a
maxDist a
n    = forall a. Integral a => a -> a -> a
div a
n a
3
  close :: [a] -> [a] -> Bool
close [a]
a [a]
b    = forall a. Eq a => [a] -> [a] -> VerboseLevel
editDistance [a]
a [a]
b forall a. Ord a => a -> a -> Bool
<= forall {a}. Integral a => a -> a
maxDist (forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [a]
a)
  ys :: [String]
ys           = forall a b. (a -> b) -> [a] -> [b]
map forall a. Pretty a => a -> String
prettyShow forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => [a] -> [a] -> Bool
close (forall a. Pretty a => a -> String
strip forall a b. (a -> b) -> a -> b
$ a -> b
canon a
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
strip forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
C.unqualify) [QName]
inscope


prettyTCWarnings :: [TCWarning] -> TCM String
prettyTCWarnings :: [TCWarning] -> TCM String
prettyTCWarnings = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([String] -> String
unlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
List.intersperse String
"") forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> TCM [String]
prettyTCWarnings'

prettyTCWarnings' :: [TCWarning] -> TCM [String]
prettyTCWarnings' :: [TCWarning] -> TCM [String]
prettyTCWarnings' = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Doc -> String
P.render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> [TCWarning]
filterTCWarnings

-- | If there are several warnings, remove the unsolved-constraints warning
-- in case there are no interesting constraints to list.
filterTCWarnings :: [TCWarning] -> [TCWarning]
filterTCWarnings :: [TCWarning] -> [TCWarning]
filterTCWarnings = \case
  -- #4065: Always keep the only warning
  [TCWarning
w] -> [TCWarning
w]
  -- Andreas, 2019-09-10, issue #4065:
  -- If there are several warnings, remove the unsolved-constraints warning
  -- in case there are no interesting constraints to list.
  [TCWarning]
ws  -> (forall a. (a -> Bool) -> [a] -> [a]
`filter` [TCWarning]
ws) forall a b. (a -> b) -> a -> b
$ \ TCWarning
w -> case TCWarning -> Warning
tcWarning TCWarning
w of
    UnsolvedConstraints Constraints
cs -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ProblemConstraint -> Bool
interestingConstraint Constraints
cs
    Warning
_ -> Bool
True


-- | Turns warnings, if any, into errors.
tcWarningsToError :: [TCWarning] -> TCM ()
tcWarningsToError :: [TCWarning] -> TCM ()
tcWarningsToError [TCWarning]
mws = case ([TCWarning]
unsolvedHoles, [TCWarning]
otherWarnings) of
   ([], [])                   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
   (_unsolvedHoles :: [TCWarning]
_unsolvedHoles@(TCWarning
_:[TCWarning]
_), []) -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
SolvedButOpenHoles
   ([TCWarning]
_, ws :: [TCWarning]
ws@(TCWarning
_:[TCWarning]
_))              -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TypeError
NonFatalErrors [TCWarning]
ws
   where
   -- filter out unsolved interaction points for imported module so
   -- that we get the right error message (see test case Fail/Issue1296)
   ([TCWarning]
unsolvedHoles, [TCWarning]
otherWarnings) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (Warning -> Bool
isUnsolvedIM forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
mws
   isUnsolvedIM :: Warning -> Bool
isUnsolvedIM UnsolvedInteractionMetas{} = Bool
True
   isUnsolvedIM Warning
_                          = Bool
False


-- | Depending which flags are set, one may happily ignore some
-- warnings.

applyFlagsToTCWarningsPreserving :: HasOptions m => Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving :: forall (m :: * -> *).
HasOptions m =>
Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving Set WarningName
additionalKeptWarnings [TCWarning]
ws = do
  -- For some reason some SafeFlagPragma seem to be created multiple times.
  -- This is a way to collect all of them and remove duplicates.
  let pragmas :: TCWarning -> ([TCWarning], [String])
pragmas TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of { SafeFlagPragma [String]
ps -> ([TCWarning
w], [String]
ps); Warning
_ -> ([], []) }
  let sfp :: [TCWarning]
sfp = case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Eq a => [a] -> [a]
List.nub (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> ([TCWarning], [String])
pragmas [TCWarning]
ws) of
              (TCWarning CallStack
loc Range
r Warning
w Doc
p Bool
b:[TCWarning]
_, [String]
sfp) ->
                 [CallStack -> Range -> Warning -> Doc -> Bool -> TCWarning
TCWarning CallStack
loc Range
r ([String] -> Warning
SafeFlagPragma [String]
sfp) Doc
p Bool
b]
              ([TCWarning], [String])
_                        -> []

  Set WarningName
pragmaWarnings <- (forall o i. o -> Lens' i o -> i
^. Lens' (Set WarningName) WarningMode
warningSet) forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WarningMode
optWarningMode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  let warnSet :: Set WarningName
warnSet = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set WarningName
pragmaWarnings Set WarningName
additionalKeptWarnings

  -- filter out the warnings the flags told us to ignore
  let cleanUp :: Warning -> Bool
cleanUp Warning
w = let wName :: WarningName
wName = Warning -> WarningName
warningName Warning
w in
        WarningName
wName forall a. Eq a => a -> a -> Bool
/= WarningName
SafeFlagPragma_
        Bool -> Bool -> Bool
&& WarningName
wName forall a. Ord a => a -> Set a -> Bool
`Set.member` Set WarningName
warnSet
        Bool -> Bool -> Bool
&& case Warning
w of
          UnsolvedMetaVariables [Range]
ums    -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null [Range]
ums
          UnsolvedInteractionMetas [Range]
uis -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null [Range]
uis
          UnsolvedConstraints Constraints
ucs      -> Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null Constraints
ucs
          Warning
_                            -> Bool
True

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [TCWarning]
sfp forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
cleanUp forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
ws

applyFlagsToTCWarnings :: HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings :: forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings = forall (m :: * -> *).
HasOptions m =>
Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving forall a. Set a
Set.empty

getAllUnsolvedWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => m [TCWarning]
getAllUnsolvedWarnings :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
m [TCWarning]
getAllUnsolvedWarnings = do
  [Range]
unsolvedInteractions <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedInteractionMetas
  Constraints
unsolvedConstraints  <- forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
  [Range]
unsolvedMetas        <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedMetas

  let checkNonEmpty :: (a -> a) -> a -> f a
checkNonEmpty a -> a
c a
rs = a -> a
c a
rs forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null a
rs)

  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m TCWarning
warning_ forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes
                [ forall {f :: * -> *} {a} {a}.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
UnsolvedInteractionMetas [Range]
unsolvedInteractions
                , forall {f :: * -> *} {a} {a}.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
UnsolvedMetaVariables    [Range]
unsolvedMetas
                , forall {f :: * -> *} {a} {a}.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty Constraints -> Warning
UnsolvedConstraints      Constraints
unsolvedConstraints ]

-- | Collect all warnings that have accumulated in the state.

getAllWarnings :: (MonadFail m, ReadTCState m, MonadWarning m) => WhichWarnings -> m [TCWarning]
getAllWarnings :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings = forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving forall a. Set a
Set.empty

getAllWarningsPreserving :: (MonadFail m, ReadTCState m, MonadWarning m) => Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
Set WarningName -> WhichWarnings -> m [TCWarning]
getAllWarningsPreserving Set WarningName
keptWarnings WhichWarnings
ww = do
  [TCWarning]
unsolved            <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
m [TCWarning]
getAllUnsolvedWarnings
  [TCWarning]
collectedTCWarnings <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [TCWarning] TCState
stTCWarnings

  let showWarn :: Warning -> Bool
showWarn Warning
w = Warning -> WhichWarnings
classifyWarning Warning
w forall a. Ord a => a -> a -> Bool
<= WhichWarnings
ww Bool -> Bool -> Bool
&&
                    Bool -> Bool
not (forall a. Null a => a -> Bool
null [TCWarning]
unsolved Bool -> Bool -> Bool
&& Warning -> Bool
onlyShowIfUnsolved Warning
w)

  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
showWarn forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning))
    forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasOptions m =>
Set WarningName -> [TCWarning] -> m [TCWarning]
applyFlagsToTCWarningsPreserving Set WarningName
keptWarnings
    forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ [TCWarning]
unsolved forall a. [a] -> [a] -> [a]
++ [TCWarning]
collectedTCWarnings

getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr TCErr
err = case TCErr
err of
  TypeError CallStack
_ TCState
tcst Closure TypeError
cls -> case forall a. Closure a -> a
clValue Closure TypeError
cls of
    NonFatalErrors{} -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    TypeError
_ -> forall a. TCM a -> TCM a
localTCState forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcst
      [TCWarning]
ws <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
      -- We filter out the unsolved(Metas/Constraints) to stay
      -- true to the previous error messages.
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isUnsolvedWarning forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
ws
  TCErr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []